1structure fracUtils :> fracUtils = 2struct 3 4open HolKernel boolLib Parse bossLib; 5 6(* interactive mode 7app load ["pairTheory", "pairLib", 8 "integerTheory", "intLib", 9 "jbUtils"]; 10*) 11 12open 13 pairTheory pairLib 14 integerTheory intLib 15 jbUtils; 16 17(*-------------------------------------------------------------------------- 18 * dest_frac : term -> term * term list 19 *--------------------------------------------------------------------------*) 20 21fun dest_frac (t1:term) = 22 if is_comb t1 then 23 let 24 val (top_rator, top_rand) = dest_comb t1 25 in 26 if top_rator ~~ ``abs_frac`` then 27 let 28 val (this_nmr, this_dnm) = dest_pair (top_rand); 29 in 30 (``abs_frac``,[this_nmr,this_dnm]) 31 end 32 else 33 if top_rator ~~ ``frac_ainv`` orelse top_rator ~~ ``frac_minv`` orelse 34 top_rator ~~ ``rep_rat`` 35 then 36 (top_rator, [top_rand]) 37 else 38 let 39 val (this_op, this_first, this_second) = dest_binop_triple t1 40 in 41 (this_op, [this_first, this_second]) 42 end 43 end 44 else (* t1 must be a variable *) 45 (t1,[]) 46 47(* ---------- test cases ---------- * 48 dest_frac ``f1:frac``; 49 dest_frac ``abs_frac(3i,4i)``; 50 dest_frac ``frac_add f1 f2``; 51 dest_frac ``frac_add (frac_sub f1 f2) f3``; 52 dest_frac ``frac_add (abs_frac(3i,4i)) (abs_frac(4i,5i))``; 53 * ---------- test cases ---------- *) 54 55(*-------------------------------------------------------------------------- 56 * extract_frac : term -> term list 57 *--------------------------------------------------------------------------*) 58 59fun extract_frac (t1:term) = extract_terms_of_type ``:frac`` t1; 60 61(* ---------- test cases ---------- * 62 extract_frac ``4i + (frac_nmr(abs_frac(3i,4i))) = 3``; 63 extract_frac ``frac_add f1 f2 = sub f1 f2``; 64 extract_frac ``!f1 f2. nmr (frac_add f1 f2) = frac_dnm (frac_sub f1 f2)``; 65 extract_frac ``frac_nmr (frac_add f1 f2) = frac_dnm (frac_sub f1 f2)``; 66 * ---------- test cases ---------- *) 67 68(*-------------------------------------------------------------------------- 69 * extract_abs_frac : term -> term list 70 *--------------------------------------------------------------------------*) 71 72fun extract_abs_frac (t1:term) = 73 if is_comb t1 then 74 let 75 val (top_rator, top_rand) = dest_comb t1 76 in 77 if top_rator ~~ ``abs_frac`` then [t1] 78 else 79 op_union aconv (extract_abs_frac top_rator) (extract_abs_frac top_rand) 80 end 81 else 82 []; 83 84(* ---------- test cases ---------- * 85 extract_abs_frac ``abs_rat( abs_frac(1,2) ) + abs_rat (abs_frac(1,3) ) = abs_rat(abs_frac (5,6))``; 86 extract_abs_frac ``4i + (frac_nmr(abs_frac(3i,4i))) = 3``; 87 extract_abs_frac ``frac_nmr (abs_frac(4,frac_nmr(abs_frac(3,4))))``; 88 * ---------- test cases ---------- *) 89 90(*-------------------------------------------------------------------------- 91 * extract_frac_fun : term list -> term -> (term * term * term) list 92 *--------------------------------------------------------------------------*) 93 94fun ttrip_eq (t1,t2,t3) (ta,tb,tc) = 95 pair_eq (pair_eq aconv aconv) aconv ((t1,t2),t3) ((ta,tb),tc) 96 97fun extract_frac_fun (l2:term list) (t1:term) = 98 if is_comb t1 then 99 let 100 val (top_rator, top_rand) = dest_comb t1; 101 in 102 if tmem top_rator l2 andalso is_comb top_rand then 103 let 104 val (second_rator, second_rand) = dest_comb top_rand; 105 in 106 if second_rator ~~ ``abs_frac`` then 107 let 108 val (this_nmr, this_dnm) = dest_pair (second_rand) 109 val sub_fracs = 110 op_union ttrip_eq 111 (extract_frac_fun l2 this_nmr) 112 (extract_frac_fun l2 this_dnm) 113 in 114 [(top_rator,this_nmr,this_dnm)] @ sub_fracs 115 end 116 else (* not second_rator = ``abs_frac`` *) 117 extract_frac_fun l2 top_rand 118 end 119 else (* not (top_rator = l2 andalso is_comb top_rand) *) 120 op_union ttrip_eq (extract_frac_fun l2 top_rator) 121 (extract_frac_fun l2 top_rand) 122 end 123 else (* not is_comb t1 *) 124 []; 125 126(* ---------- test cases ---------- * 127 extract_frac_fun [``frac_nmr``] ``4i + (nmr(abs_frac(3i,4i)))``; 128 extract_frac_fun [``frac_nmr``] ``frac_add (abs_frac(4,frac_nmr(abs_frac(3,4)))) (abs_frac(3,4))``; 129 extract_frac_fun [``frac_nmr``] ``frac_nmr(abs_frac(3,4)) + frac_dnm(abs_frac(4,5))``; 130 extract_frac_fun [``frac_nmr``] ``frac_nmr (abs_frac(4,frac_nmr(abs_frac(3,4))))``; 131 extract_frac_fun [``frac_nmr``] ``frac_nmr (abs_frac(4,frac_nmr(abs_frac(3,4))))``; 132 extract_frac_fun [``frac_nmr``,``frac_dnm``] ``nmr(abs_frac(3,4)) + dnm(abs_frac(4,5))``; 133 * ---------- test cases ---------- *) 134 135(*-------------------------------------------------------------------------- 136 * INT_GT0_CONV : conv 137 * 138 * t1 (with t1 greater than zero) 139 * ----------- 140 * |- 0 < t1 141 *--------------------------------------------------------------------------*) 142 143fun INT_GT0_CONV (t1:term) = 144 EQT_ELIM (intLib.ARITH_CONV ``0 < ^t1``); 145 146(*========================================================================== 147 * end of structure 148 *==========================================================================*) 149end; 150