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