1structure realSyntax :> realSyntax = 2struct 3 4 local open realTheory in end; 5 open HolKernel Abbrev 6 7 val ERR = mk_HOL_ERR "realSyntax" 8 9 10 (* Fundamental terms, mainly constants *) 11 12 fun mk_raconst (n, ty) = mk_thy_const {Thy = "realax", Name = n, Ty = ty} 13 fun mk_rconst (n, ty) = mk_thy_const {Thy = "real", Name = n, Ty = ty} 14 15 val real_ty = mk_thy_type {Thy = "realax", Tyop = "real", Args = []} 16 val bop_ty = real_ty --> real_ty --> real_ty 17 val rel_ty = real_ty --> real_ty --> bool 18 19 val real_injection = mk_rconst("real_of_num", numSyntax.num --> real_ty) 20 21 val zero_tm = mk_comb(real_injection, numSyntax.zero_tm) 22 val one_tm = mk_comb(real_injection, numSyntax.mk_numeral (Arbnum.fromInt 1)) 23 val negate_tm = mk_raconst("real_neg", real_ty --> real_ty) 24 val absval_tm = mk_rconst("abs", real_ty --> real_ty) 25 val plus_tm = mk_raconst("real_add", bop_ty) 26 val minus_tm = mk_rconst("real_sub", bop_ty) 27 val mult_tm = mk_raconst("real_mul", bop_ty) 28 val div_tm = mk_rconst("/", bop_ty) 29 val exp_tm = mk_rconst("pow", real_ty --> numSyntax.num --> real_ty) 30 31 val real_eq_tm = mk_thy_const { Thy = "min", Name = "=", Ty = rel_ty} 32 val less_tm = mk_raconst("real_lt", rel_ty) 33 val leq_tm = mk_rconst("real_lte", rel_ty) 34 val greater_tm = mk_rconst("real_gt", rel_ty) 35 val geq_tm = mk_rconst("real_ge", rel_ty) 36 37 val min_tm = mk_rconst("min", bop_ty) 38 val max_tm = mk_rconst("max", bop_ty) 39 40 (* Functions *) 41 42 fun dest1 c fnm nm t = let 43 val (f, x) = dest_comb t 44 val _ = assert (same_const f) c 45 in 46 x 47 end handle HOL_ERR _ => raise ERR fnm ("Term is not a "^nm) 48 49 fun dest2 c fnm nm t = let 50 val (fx, y) = dest_comb t 51 val (f, x) = dest_comb fx 52 val _ = assert (same_const f) c 53in 54 (x, y) 55 end handle HOL_ERR _ => raise ERR fnm ("Term is not a "^nm) 56 57 val dest_negated = dest1 negate_tm "dest_negated" "negation" 58 val is_negated = can dest_negated 59 fun mk_negated t = mk_comb(negate_tm, t) 60 61 val dest_injected = dest1 real_injection "dest_injected" "injection" 62 val is_injected = can dest_injected 63 fun mk_injected t = mk_comb(real_injection, t) 64 65 66 67 fun is_real_literal t = let 68 (* returns true if a term is in the range of the implicit injection from 69 the integers *) 70 fun remove_negs t = remove_negs (dest_negated t) handle HOL_ERR _ => t 71 val number_part = dest_injected (remove_negs t) 72 in 73 numSyntax.is_numeral number_part 74 end handle HOL_ERR _ => false 75 76 fun term_of_int i = let 77 fun posint i = 78 mk_comb(real_injection, numSyntax.mk_numeral(Arbint.toNat i)) 79 in 80 if Arbint.<(i,Arbint.zero) then mk_negated(posint(Arbint.~ i)) 81 else posint i 82 end 83 84 85 fun flip f (x,y) = f (y, x) 86 val dest_plus = dest2 plus_tm "dest_plus" "plus" 87 val is_plus = can dest_plus 88 fun mk_plus(t1, t2) = list_mk_comb(plus_tm, [t1, t2]) 89 fun list_mk_plus tlist = 90 case tlist of 91 [] => raise ERR "list_mk_plus" "Empty list" 92 | [t] => t 93 | t::ts => List.foldl (flip mk_plus) t ts 94 fun strip_plus t = let 95 fun recurse a k = 96 case k of 97 [] => a 98 | (t::ts) => let 99 val (t1, t2) = dest_plus t 100 in 101 recurse a (t2::t1::ts) 102 end handle HOL_ERR _ => recurse (t::a) ts 103 in 104 recurse [] [t] 105 end 106 107 val dest_minus = dest2 minus_tm "dest_minus" "subtraction" 108 val is_minus = can dest_minus 109 fun mk_minus(t1,t2) = list_mk_comb(minus_tm, [t1, t2]) 110 111 val dest_mult = dest2 mult_tm "dest_mult" "multiplication" 112 val is_mult = can dest_mult 113 fun mk_mult(t1, t2) = list_mk_comb(mult_tm, [t1, t2]) 114 fun list_mk_mult tlist = 115 case tlist of 116 [] => raise ERR "list_mk_mult" "Empty list" 117 | [t] => t 118 | t::ts => List.foldl (flip mk_mult) t ts 119 fun strip_mult t = let 120 fun recurse a k = 121 case k of 122 [] => a 123 | t::ts => let 124 val (t1, t2) = dest_mult t 125 in 126 recurse a (t2::t1::ts) 127 end handle HOL_ERR _ => recurse (t::a) ts 128 in 129 recurse [] [t] 130 end 131 132 133 val dest_div = dest2 div_tm "dest_div" "division" 134 val is_div = can dest_div 135 fun mk_div(t1, t2) = list_mk_comb(div_tm, [t1, t2]) 136 137 val dest_absval = dest1 absval_tm "dest_absval" "absolute value" 138 val is_absval = can dest_absval 139 fun mk_absval t = mk_comb(absval_tm, t) 140 141 val dest_less = dest2 less_tm "dest_less" "less-than term" 142 val is_less = can dest_less 143 fun mk_less(t1, t2) = list_mk_comb(less_tm, [t1, t2]) 144 145 val dest_leq = dest2 leq_tm "dest_leq" "less-than-or-equal term" 146 val is_leq = can dest_leq 147 fun mk_leq(t1, t2) = list_mk_comb(leq_tm, [t1, t2]) 148 149 val dest_greater = dest2 greater_tm "dest_greater" "greater-than term" 150 val is_greater = can dest_greater 151 fun mk_greater(t1, t2) = list_mk_comb(greater_tm, [t1, t2]) 152 153 val dest_geq = dest2 geq_tm "dest_geq" "greater-than-or-equal term" 154 val is_geq = can dest_geq 155 fun mk_geq(t1, t2) = list_mk_comb(geq_tm, [t1, t2]) 156 157 val dest_min = dest2 min_tm "dest_min" "min term" 158 val is_min = can dest_min 159 fun mk_min(t1, t2) = list_mk_comb(min_tm, [t1, t2]) 160 161 val dest_max = dest2 max_tm "dest_max" "max term" 162 val is_max = can dest_max 163 fun mk_max(t1, t2) = list_mk_comb(max_tm, [t1, t2]) 164 165 val dest_pow = dest2 exp_tm "dest_pow" "pow term" 166 val is_pow = can dest_pow 167 fun mk_pow(t1,t2) = list_mk_comb(exp_tm, [t1, t2]) 168 169 170 fun int_of_term t = let 171 val (is_pos, n) = 172 case Lib.total dest_negated t of 173 NONE => (true, numSyntax.dest_numeral (dest_injected t)) 174 | SOME neg_i => (false, numSyntax.dest_numeral (dest_injected neg_i)) 175 in 176 if is_pos then Arbint.fromNat n 177 else Arbint.~(Arbint.fromNat n) 178 end 179 180 val (inv_tm,mk_inv,dest_inv,is_inv) = syntax_fns1 "realax" "inv" 181 182end ; 183