1structure numSyntax :> numSyntax = 2struct 3 open HolKernel Abbrev; 4 5 local open arithmeticTheory whileTheory numeralTheory in end; 6 7 val ERR = mk_HOL_ERR "numSyntax"; 8 9(*--------------------------------------------------------------------------- 10 Constants 11 ---------------------------------------------------------------------------*) 12 13 val num = mk_thy_type {Thy = "num", Tyop = "num", Args = []} 14 15 val suc_tm = prim_mk_const {Name="SUC", Thy="num"} 16 val zero_tm = prim_mk_const {Name="0", Thy="num"} 17 val less_tm = prim_mk_const {Name="<", Thy="prim_rec"} 18 val measure_tm = prim_mk_const {Name="measure", Thy="prim_rec"} 19 val pre_tm = prim_mk_const {Name="PRE", Thy="prim_rec"} 20 val alt_zero_tm = prim_mk_const {Name="ZERO", Thy="arithmetic"} 21 val bit1_tm = prim_mk_const {Name="BIT1", Thy="arithmetic"} 22 val bit2_tm = prim_mk_const {Name="BIT2", Thy="arithmetic"} 23 val div2_tm = prim_mk_const {Name="DIV2", Thy="arithmetic"} 24 val div_tm = prim_mk_const {Name="DIV", Thy="arithmetic"} 25 val divmod_tm = prim_mk_const {Name="DIVMOD", Thy="arithmetic"}; 26 val even_tm = prim_mk_const {Name="EVEN", Thy="arithmetic"} 27 val exp_tm = prim_mk_const {Name="EXP", Thy="arithmetic"} 28 val fact_tm = prim_mk_const {Name="FACT", Thy="arithmetic"} 29 val funpow_tm = prim_mk_const {Name="FUNPOW", Thy="arithmetic"} 30 val geq_tm = prim_mk_const {Name=">=", Thy="arithmetic"} 31 val greater_tm = prim_mk_const {Name=">", Thy="arithmetic"} 32 val leq_tm = prim_mk_const {Name="<=", Thy="arithmetic"} 33 val max_tm = prim_mk_const {Name="MAX", Thy="arithmetic"} 34 val min_tm = prim_mk_const {Name="MIN", Thy="arithmetic"} 35 val minus_tm = prim_mk_const {Name="-", Thy="arithmetic"} 36 val mod_tm = prim_mk_const {Name="MOD", Thy="arithmetic"} 37 val mult_tm = prim_mk_const {Name="*", Thy="arithmetic"} 38 val num_case_tm = prim_mk_const {Name="num_CASE",Thy="arithmetic"} 39 val numeral_tm = prim_mk_const {Name="NUMERAL", Thy="arithmetic"} 40 val odd_tm = prim_mk_const {Name="ODD", Thy="arithmetic"} 41 val plus_tm = prim_mk_const {Name="+", Thy="arithmetic"} 42 val least_tm = prim_mk_const {Name="LEAST", Thy="while"}; 43 val while_tm = prim_mk_const {Name="WHILE", Thy="while"} 44 45 46(*--------------------------------------------------------------------------- 47 Constructors 48 ---------------------------------------------------------------------------*) 49 50 fun mk_monop c tm = mk_comb(c,tm) 51 fun mk_binop c (tm1,tm2) = mk_comb(mk_comb(c,tm1),tm2); 52 53 val mk_bit1 = mk_monop bit1_tm 54 val mk_bit2 = mk_monop bit2_tm 55 val mk_div = mk_binop div_tm 56 val mk_div2 = mk_monop div2_tm 57 val mk_even = mk_monop even_tm 58 val mk_exp = mk_binop exp_tm 59 val mk_fact = mk_monop fact_tm 60 val mk_geq = mk_binop geq_tm 61 val mk_greater = mk_binop greater_tm 62 val mk_leq = mk_binop leq_tm 63 val mk_less = mk_binop less_tm 64 val mk_max = mk_binop max_tm 65 val mk_min = mk_binop min_tm 66 val mk_minus = mk_binop minus_tm 67 val mk_mod = mk_binop mod_tm 68 val mk_mult = mk_binop mult_tm 69 val mk_odd = mk_monop odd_tm 70 val mk_plus = mk_binop plus_tm 71 val mk_pre = mk_monop pre_tm 72 val mk_suc = mk_monop suc_tm 73 74 fun mk_num_case(b,f,n) = 75 list_mk_comb(inst[alpha |-> type_of b] num_case_tm, [n,b,f]); 76 77 fun mk_funpow(f,n,x) = 78 list_mk_comb(inst [alpha |-> type_of x] funpow_tm, [f,n,x]); 79 80 fun mk_while(P,g,x) = 81 list_mk_comb(inst [alpha |-> type_of x] while_tm, [P,g,x]); 82 83 fun mk_least P = 84 mk_comb(inst [alpha |-> fst(dom_rng(type_of P))] least_tm, P); 85 86 fun mk_divmod(m,n,a) = list_mk_comb(divmod_tm, [m,n,a]); 87 88 fun mk_measure (f,x,y) = 89 list_mk_comb(inst [alpha |-> type_of x] measure_tm, [f,x,y]); 90 91 (* Partial application of measure is often more useful *) 92 fun mk_cmeasure f = 93 mk_comb(inst [alpha |-> fst(dom_rng (type_of f))] measure_tm, f); 94 95 96(*--------------------------------------------------------------------------- 97 Destructors 98 ---------------------------------------------------------------------------*) 99 100 val dest_bit1 = dest_monop bit1_tm (ERR "dest_bit1" "") 101 val dest_bit2 = dest_monop bit2_tm (ERR "dest_bit2" "") 102 val dest_div = dest_binop div_tm (ERR "dest_div" "") 103 val dest_div2 = dest_monop div2_tm (ERR "dest_div2" "") 104 val dest_even = dest_monop even_tm (ERR "dest_even" "") 105 val dest_exp = dest_binop exp_tm (ERR "dest_exp" "") 106 val dest_fact = dest_monop fact_tm (ERR "dest_fact" ""); 107 val dest_geq = dest_binop geq_tm (ERR "dest_geq" "") 108 val dest_greater = dest_binop greater_tm (ERR "dest_greater" "") 109 val dest_least = dest_monop least_tm (ERR "dest_least" ""); 110 val dest_leq = dest_binop leq_tm (ERR "dest_leq" "") 111 val dest_less = dest_binop less_tm (ERR "dest_less" "") 112 val dest_max = dest_binop max_tm (ERR "dest_max" "") 113 val dest_min = dest_binop min_tm (ERR "dest_min" "") 114 val dest_minus = dest_binop minus_tm (ERR "dest_minus" "") 115 val dest_mod = dest_binop mod_tm (ERR "dest_mod" "") 116 val dest_mult = dest_binop mult_tm (ERR "dest_mult" "") 117 val dest_odd = dest_monop odd_tm (ERR "dest_odd" ""); 118 val dest_plus = dest_binop plus_tm (ERR "dest_plus" "") 119 val dest_pre = dest_monop pre_tm (ERR "dest_pre" "") 120 val dest_suc = dest_monop suc_tm (ERR "dest_suc" "") 121 122 fun dest_num_case tm = 123 case strip_comb tm 124 of (ncase,[n,b,f]) => 125 if same_const num_case_tm ncase 126 then (b,f,n) 127 else raise ERR "dest_num_case" "not an application of \"num_CASE\"" 128 | _ => raise ERR "dest_num_case" "not an application of \"num_CASE\"" 129 130 fun dest_funpow tm = 131 case strip_comb tm 132 of (funpow,[f,n,x]) => 133 if same_const funpow_tm funpow 134 then (f,n,x) 135 else raise ERR "dest_funpow" "not an application of \"FUNPOW\"" 136 | _ => raise ERR "dest_funpow" "not an application of \"FUNPOW\""; 137 138 139 fun dest_while tm = 140 case strip_comb tm 141 of (whle,[P,g,x]) => 142 if same_const while_tm whle 143 then (P,g,x) 144 else raise ERR "dest_while" "not an application of \"WHILE\"" 145 | _ => raise ERR "dest_while" "not an application of \"WHILE\""; 146 147 fun dest_divmod tm = 148 case strip_comb tm 149 of (dm,[m,n,a]) => 150 if same_const divmod_tm dm 151 then (m,n,a) 152 else raise ERR "dest_divmod" "not an application of \"divmod\"" 153 | _ => raise ERR "dest_divmod" "not an application of \"divmod\""; 154 155 fun dest_measure tm = 156 case strip_comb tm 157 of (m,[f,x,y]) => 158 if same_const measure_tm m 159 then (f,x,y) 160 else raise ERR "dest_measure" "not an application of \"measure\"" 161 | _ => raise ERR "dest_measure" "not an application of \"measure\""; 162 163 fun dest_cmeasure tm = 164 case total dest_comb tm 165 of NONE => raise ERR "dest_cmeasure" "not an application of \"measure\"" 166 | SOME (m,f) => if same_const measure_tm m then f 167 else raise ERR "dest_cmeasure" 168 "not an application of \"measure\"" 169 170(*--------------------------------------------------------------------------- 171 Query operations 172 ---------------------------------------------------------------------------*) 173 174 val is_bit1 = can dest_bit1 175 val is_bit2 = can dest_bit2 176 val is_div = can dest_div 177 val is_div2 = can dest_div2 178 val is_divmod = can dest_divmod 179 val is_even = can dest_even 180 val is_exp = can dest_exp 181 val is_fact = can dest_fact 182 val is_funpow = can dest_funpow 183 val is_geq = can dest_geq 184 val is_greater = can dest_greater 185 val is_least = can dest_least 186 val is_leq = can dest_leq 187 val is_less = can dest_less 188 val is_max = can dest_max 189 val is_measure = can dest_measure 190 val is_min = can dest_min 191 val is_minus = can dest_minus 192 val is_mod = can dest_mod 193 val is_mult = can dest_mult 194 val is_num_case = can dest_num_case 195 val is_odd = can dest_odd 196 val is_plus = can dest_plus 197 val is_pre = can dest_pre 198 val is_suc = can dest_suc 199 val is_while = can dest_while 200 201 202(*--------------------------------------------------------------------------- 203 Numerals are treated specially 204 ---------------------------------------------------------------------------*) 205 206 val mk_numeral = Literal.gen_mk_numeral { 207 mk_comb = Term.mk_comb, 208 ALT_ZERO = alt_zero_tm, 209 ZERO = zero_tm, 210 NUMERAL = numeral_tm, 211 BIT1 = bit1_tm, 212 BIT2 = bit2_tm 213 }; 214 215 fun dest_numeral t = 216 Literal.dest_numeral t handle HOL_ERR _ => 217 raise ERR "dest_numeral" "term is not a numeral" 218 219 val is_numeral = can dest_numeral 220 221 val int_of_term = Arbnum.toInt o dest_numeral 222 fun term_of_int i = mk_numeral(Arbnum.fromInt i) 223 224(*--------------------------------------------------------------------------- 225 Dealing with lists of things to be added or multiplied. 226 ---------------------------------------------------------------------------*) 227 228 fun list_mk_plus (h::t) = rev_itlist (C (curry mk_plus)) t h 229 | list_mk_plus [] = raise ERR "list_mk_plus" "empty list"; 230 231 fun list_mk_mult (h::t) = rev_itlist (C (curry mk_mult)) t h 232 | list_mk_mult [] = raise ERR "list_mk_mult" "empty list"; 233 234 val strip_plus = strip_binop (total dest_plus) 235 val strip_mult = strip_binop (total dest_mult) 236 237(*--------------------------------------------------------------------------- 238 Lifting ML Arbnums to HOL nums 239 ---------------------------------------------------------------------------*) 240 241fun lift_num ty arbnum = mk_numeral arbnum 242 243end 244