1(* ========================================================================= *) 2(* Tools for reasoning about positive reals (posreals). *) 3(* ========================================================================= *) 4 5structure posrealTools :> posrealTools = 6struct 7 8open HolKernel Parse boolLib simpLib posrealTheory; 9 10val ERR = mk_HOL_ERR "posrealTools"; 11 12(* ------------------------------------------------------------------------- *) 13(* Two useful case-splits on posreals *) 14(* pcases: finite and infinite *) 15(* pcases3: finite non-zero and infinite *) 16(* ------------------------------------------------------------------------- *) 17 18local 19 val posreal = Type `:posreal`; 20 21 fun pcase_split x = 22 STRIP_ASSUME_TAC (SPEC x posreal_cases) 23 THEN POP_ASSUM (fn th => FULL_SIMP_TAC boolSimps.bool_ss [th]); 24 25 fun pcase3_split x = 26 STRIP_ASSUME_TAC (SPEC x posreal_trich) 27 THEN POP_ASSUM (fn th => FULL_SIMP_TAC boolSimps.bool_ss [th]); 28in 29 fun pcases goal = 30 let val v = genvar posreal in X_GEN_TAC v THEN pcase_split v end goal; 31 32 val pcases_on = Q_TAC pcase_split; 33 34 fun pcases3 goal = 35 let val v = genvar posreal in X_GEN_TAC v THEN pcase3_split v end goal; 36 37 val pcases3_on = Q_TAC pcase3_split; 38end; 39 40(* ------------------------------------------------------------------------- *) 41(* Useful rewrites for basic posreal arithmetic. *) 42(* ------------------------------------------------------------------------- *) 43 44val posreal_SS = simpLib.SSFRAG 45 {ac = [], name = SOME "posreal", 46 congs = [], 47 convs = [], 48 dprocs = [], 49 filter = NONE, 50 rewrs = [(* addition *) 51 add_lzero, add_rzero, add_linfty, add_rinfty, 52 (* subtraction *) 53 sub_lzero, sub_rzero, 54 (* less than or equal *) 55 le_refl, le_zero, zero_le, le_infty, infty_le, le_addl, 56 le_addr, addl_le, addr_le, 57 (* less than *) 58 lt_addl, lt_addr, addl_lt, addr_lt, 59 (* multiplication *) 60 mul_lzero, mul_rzero, mul_lone, mul_rone, 61 (* reciprocal *) 62 inv_zero, inv_one, inv_infty, inv_eq_zero, inv_antimono, inv_inj, 63 inv_one_le, inv_le_one, inv_eq_infty, inv_eq_one, inv_inv, 64 (* division *) 65 div_rone, 66 (* cancellations *) 67 (* halves *) 68 half_between, 69 (* thirds *) 70 thirds_between, 71 (* injecting from the naturals *) 72 posreal_of_num_inj, posreal_of_num_not_infty, posreal_of_num_le, 73 posreal_of_num_lt, posreal_of_num_add, posreal_of_num_sub, 74 posreal_of_num_mul, 75 (* injecting from the reals *) 76 preal_not_infty, 77 (* min *) 78 min_le1, min_le2, min_refl, min_linfty, min_rinfty, 79 min_lzero, min_rzero, 80 (* max *) 81 le_max1, le_max2, max_refl, max_linfty, max_rinfty, 82 max_lzero, max_rzero, 83 (* bound1 *) 84 bound1_basic, bound1_infty]}; 85 86val posreal_ss = simpLib.++ (realSimps.real_ss, posreal_SS); 87 88(* ------------------------------------------------------------------------- *) 89(* A calculator for rational posreals. *) 90(* ------------------------------------------------------------------------- *) 91 92val dest_preal_div = dest_binop ``preal_div`` (ERR "dest_preal_div" ""); 93 94val posreal_of_num_tm = ``posreal_of_num``; 95 96fun numeral_factor_conv k tm = 97 let 98 val _ = k <> Arbnum.zero orelse raise ERR "numeral_factor_conv" "k = 0" 99 val n = numSyntax.dest_numeral tm 100 val (nq,nr) = Arbnum.divmod (n,k) 101 val _ = nr = Arbnum.zero orelse raise ERR "numeral_factor_conv" "k | n" 102 val k' = numSyntax.mk_numeral k 103 val nq' = numSyntax.mk_numeral nq 104 val mul_tm = numSyntax.mk_mult (k',nq') 105 in 106 GSYM (reduceLib.MUL_CONV mul_tm) 107 end; 108 109fun rat_cancel_conv k = 110 LAND_CONV (RAND_CONV (numeral_factor_conv k)) THENC 111 RAND_CONV (RAND_CONV (numeral_factor_conv k)) THENC 112 LAND_CONV (REWR_CONV (GSYM posreal_of_num_mul)) THENC 113 RAND_CONV (REWR_CONV (GSYM posreal_of_num_mul)) THENC 114 REWR_CONV rat_cancel; 115 116fun rat_reduce_conv tm = 117 let 118 val (a,b) = dest_preal_div tm 119 val m = numSyntax.dest_numeral (rand a) 120 val _ = m <> Arbnum.zero orelse raise ERR "rat_reduce_conv" "0 numerator" 121 val n = numSyntax.dest_numeral (rand b) 122 val _ = n <> Arbnum.zero orelse raise ERR "rat_reduce_conv" "0 denominator" 123 val g = Arbnum.gcd (m,n) 124 in 125 if g = Arbnum.one then raise ERR "rat_reduce_conv" "reduced" 126 else rat_cancel_conv g tm 127 end; 128 129val rat_reduce_pat = 130 Term `preal_div (posreal_of_num (NUMERAL x)) (posreal_of_num (NUMERAL y))`; 131 132val posreal_reduce_SS = simpLib.SSFRAG 133 {ac = [], 134 congs = [], 135 name = SOME "posreal_reduce", 136 convs = [{name = "rat_reduce_conv (posreals)", conv = K (K rat_reduce_conv), 137 trace = 2, key = SOME ([],rat_reduce_pat)}], 138 dprocs = [], 139 filter = NONE, 140 rewrs = [(* equality *) 141 posreal_of_num_not_infty, posreal_of_num_inj, eq_rat, eq_ratl, 142 rat_eq_infty, 143 (* addition *) 144 posreal_of_num_add, add_rat, add_ratl, add_ratr, add_linfty, 145 add_rinfty, 146 (* subtraction *) 147 posreal_of_num_sub, sub_rat, sub_ratl, sub_ratr, sub_linfty_rat, 148 sub_linfty_num, sub_rinfty_rat, sub_rinfty_num, 149 (* less than or equal *) 150 le_rat, le_ratl, le_ratr, le_infty, infty_le, 151 posreal_of_num_le, 152 (* less than *) 153 posreal_of_num_lt, 154 (* multiplication *) 155 posreal_of_num_mul, mul_rat, mul_ratl, mul_ratr, mul_linfty_rat, 156 mul_linfty_num, mul_rinfty_rat, mul_rinfty_num, mul_infty_infty, 157 (* reciprocal *) 158 (* division *) 159 div_rat, div_ratl, div_ratr, div_rzero_num, div_rzero_rat, 160 div_lzero, div_rinfty, div_linfty_num, div_linfty_rat, div_rone, 161 (* cancellations *) 162 (* min *) 163 min_linfty, min_rinfty, min_num, min_ratl, min_ratr, min_rat, 164 (* max *) 165 max_linfty, max_rinfty, max_num, max_ratl, max_ratr, max_rat, 166 (* bound1 *) 167 bound1_infty, bound1_num, bound1_rat]}; 168 169val posreal_reduce_ss = 170 simpLib.++ 171 (simpLib.++ (boolSimps.bool_ss, numSimps.REDUCE_ss), posreal_reduce_SS); 172 173(* ------------------------------------------------------------------------- *) 174(* AC normalizer for multiplication. *) 175(* ------------------------------------------------------------------------- *) 176 177val dest_mul = dest_binop ``preal_mul`` (ERR "dest_mul" ""); 178val is_mul = can dest_mul; 179 180local 181 fun terminate is_op rid tm = 182 (if is_op tm then RAND_CONV (terminate is_op rid) 183 else REWR_CONV (GSYM rid)) tm; 184 185 fun dest_inv inv tm = 186 if is_comb tm andalso rator tm = inv then (false, rand tm) else (true, tm); 187 188 fun bubble is_op swap inv tm = 189 (if not (is_op tm) orelse not (is_op (rand tm)) then ALL_CONV else 190 let 191 val (a1,b1) = dest_comb tm 192 val (s1,t1) = dest_inv inv (rand a1) 193 val (s2,t2) = dest_inv inv (rand (rator b1)) 194 val finished = 195 case compare (t1,t2) of LESS => true 196 | EQUAL => not (s1 = false andalso s2 = true) 197 | GREATER => false 198 in 199 if finished then ALL_CONV 200 else REWR_CONV swap THENC RAND_CONV (bubble is_op swap inv) 201 end) tm; 202 203 fun sort is_op swap inv tm = 204 (if not (is_op tm) then ALL_CONV 205 else RAND_CONV (sort is_op swap inv) THENC bubble is_op swap inv) tm; 206 207 fun permute is_op assoc rid swap inv = 208 SIMP_CONV boolSimps.bool_ss [assoc] 209 THENC terminate is_op rid 210 THENC sort is_op swap inv; 211in 212 fun permute_conv is_op assoc rid swap inv tm = 213 (if is_op tm then permute is_op assoc rid swap inv else NO_CONV) tm; 214end; 215 216val permute_mul_conv = 217 permute_conv is_mul mul_assoc mul_rone mul_swap ``preal_inv``; 218 219end; 220