1structure ratReduce :> ratReduce = 2struct 3 4open HolKernel boolLib Abbrev ratSyntax ratTheory 5 6val zero = mk_rat_of_num (numSyntax.mk_numeral Arbnum.zero) 7val one = mk_rat_of_num (numSyntax.mk_numeral Arbnum.one) 8 9val neg1 = mk_rat_ainv one 10val neg1neg1 = mk_rat_div(neg1, neg1) 11 12val ratmul_thms = CONJUNCTS RAT_MUL_NUM_CALCULATE 13val ratmul_convs = map REWR_CONV ratmul_thms 14val rateq_thms = CONJUNCTS RAT_EQ_NUM_CALCULATE 15val rateq_convs = map REWR_CONV rateq_thms 16val ratadd_thms = CONJUNCTS RAT_ADD_NUM_CALCULATE 17val ratadd_convs = map REWR_CONV ratadd_thms 18 19fun expose_num t = 20 if is_rat_ainv t then expose_num (rand t) 21 else if is_rat_of_num t then expose_num (rand t) 22 else t 23fun expose_num_conv c t = 24 if is_rat_ainv t then RAND_CONV (expose_num_conv c) t 25 else if is_rat_of_num t then RAND_CONV (expose_num_conv c) t 26 else c t 27 28val NOT_F = last (CONJUNCTS boolTheory.NOT_CLAUSES) 29val T_AND = hd (CONJUNCTS (SPEC_ALL boolTheory.AND_CLAUSES)) 30val T_IMP = hd (CONJUNCTS (SPEC_ALL boolTheory.IMP_CLAUSES)) 31 32fun ERROR f msg c t = 33 c t handle HOL_ERR _ => raise mk_HOL_ERR "ratReduce" f msg 34 35val prove_two_nonzero_preconds = 36 ERROR "prove_two_nonzero_preconds" "denominators not both non-zero" 37 (LAND_CONV (BINOP_CONV 38 (RAND_CONV 39 (FIRST_CONV rateq_convs THENC 40 EVERY_CONJ_CONV reduceLib.REDUCE_CONV) THENC 41 REWR_CONV NOT_F) THENC 42 REWR_CONV T_AND) THENC 43 REWR_CONV T_IMP) 44 45(* given term of form 46 (n1 / d1) * (n2 / d2) 47 where n's and d's are either &n, or -&n, returns theorem saying 48 |- t = n' / d' 49 with n' and d' similarly literal-shaped. No normalisation is done on result 50*) 51fun coremul_conv t = 52 let 53 val (t1,t2) = dest_rat_mul t 54 val th0 = PART_MATCH (lhand o lhs o rand) RAT_DIVDIV_MUL t1 55 val th1 = PART_MATCH (rand o lhs o rand) th0 t2 56 in 57 CONV_RULE (RAND_CONV 58 (RAND_CONV 59 (BINOP_CONV 60 (FIRST_CONV ratmul_convs THENC 61 expose_num_conv reduceLib.REDUCE_CONV))) THENC 62 prove_two_nonzero_preconds) 63 th1 64 end 65 66val rataddmul_rwc = PURE_REWRITE_CONV (ratadd_thms @ ratmul_thms) 67 68fun coreadd_conv t = 69 let 70 val (t1,t2) = dest_rat_add t 71 val th0 = PART_MATCH (lhand o lhs o rand) RAT_DIVDIV_ADD t1 72 val th1 = PART_MATCH (rand o lhs o rand) th0 t2 73 in 74 CONV_RULE (RAND_CONV 75 (RAND_CONV 76 (BINOP_CONV 77 (rataddmul_rwc THENC 78 expose_num_conv reduceLib.REDUCE_CONV))) THENC 79 prove_two_nonzero_preconds) 80 th1 81 end 82 83val denom1_conv = REWR_CONV (GSYM RAT_DIV_1) 84fun maybe_denom1_conv t = 85 if is_rat_div t then ALL_CONV t 86 else denom1_conv t 87 88val neg1_neq0 = 89 (RAND_CONV (FIRST_CONV rateq_convs THENC 90 EVERY_CONJ_CONV reduceLib.REDUCE_CONV) THENC 91 REWR_CONV NOT_F) (mk_neg(mk_eq(neg1,zero))) |> EQT_ELIM 92val mul_n1n1_id = MATCH_MP (GEN_ALL RAT_DIV_INV) neg1_neq0 93 94(* ensures that a fraction has positive denominator by multiplying with -1/-1 95 if necessary *) 96fun posdenom_conv t = 97 let 98 val (n,d) = ratSyntax.dest_rat_div t 99 in 100 if is_rat_ainv d then 101 REWR_CONV (GSYM RAT_MUL_RID) THENC 102 RAND_CONV (REWR_CONV (GSYM mul_n1n1_id)) THENC 103 coremul_conv 104 else ALL_CONV 105 end t 106 107fun binop_prenorm c = 108 BINOP_CONV (maybe_denom1_conv THENC posdenom_conv) THENC c 109 110val xn = mk_var("x", numSyntax.num) 111val nb1_x = mk_rat_of_num (mk_comb(numSyntax.numeral_tm, numSyntax.mk_bit1 xn)) 112val nb2_x = mk_rat_of_num (mk_comb(numSyntax.numeral_tm, numSyntax.mk_bit2 xn)) 113 114fun mk_div_eq1 t = 115 TAC_PROOF(([], mk_eq(mk_rat_div(t,t), one)), 116 MATCH_MP_TAC RAT_DIV_INV >> 117 REWRITE_TAC [RAT_EQ_NUM_CALCULATE] >> 118 REWRITE_TAC [arithmeticTheory.NUMERAL_DEF, 119 arithmeticTheory.BIT2, 120 arithmeticTheory.BIT1, numTheory.NOT_SUC, 121 arithmeticTheory.ADD_CLAUSES]) 122 123val div_eq_1 = map mk_div_eq1 [nb1_x, nb2_x] 124 125val elim_neg0_conv = LAND_CONV (REWR_CONV RAT_AINV_0) 126 127fun elim_common_factor t = let 128 open Arbint 129 val (n,d) = dest_rat_div t 130 val n_i = int_of_term n 131in 132 if n_i = zero then REWR_CONV RAT_DIV_0 t 133 else let 134 val d_i = int_of_term d 135 val _ = d_i > zero orelse 136 raise mk_HOL_ERR "realSimps" "elim_common_factor" 137 "denominator must be positive" 138 val g = fromNat (Arbnum.gcd (toNat (abs n_i), toNat (abs d_i))) 139 val _ = g <> one orelse 140 raise mk_HOL_ERR "ratReduce" "elim_common_factor" 141 "No common factor" 142 val frac_1 = mk_rat_div(term_of_int g, term_of_int g) 143 val frac_new_t = 144 mk_rat_div(term_of_int (n_i div g), term_of_int (d_i div g)) 145 val mul_t = mk_rat_mul(frac_new_t, frac_1) 146 val eqn1 = coremul_conv mul_t 147 val frac_1_eq_1 = FIRST_CONV (map REWR_CONV div_eq_1) frac_1 148 val eqn2 = 149 TRANS (SYM eqn1) 150 (AP_TERM(mk_comb(rat_mul_tm, frac_new_t)) frac_1_eq_1) 151 in 152 CONV_RULE (RAND_CONV (REWR_CONV RAT_MUL_RID THENC 153 TRY_CONV (REWR_CONV RAT_DIV_1))) 154 eqn2 155 end 156end 157 158val RAT_MUL_CONV = 159 binop_prenorm coremul_conv THENC TRY_CONV elim_neg0_conv THENC 160 TRY_CONV elim_common_factor THENC 161 EVERY_CONV (map (TRY_CONV o REWR_CONV) [RAT_DIV_1, RAT_DIV_0]) 162 163(* given fraction; finds gcd of numerator and denominator (as Arbnum.num) *) 164fun find_gcd t = 165 let 166 val (n,d) = dest_rat_div t 167 val num1 = numSyntax.dest_numeral (expose_num n) 168 val num2 = numSyntax.dest_numeral (expose_num d) 169 in 170 Arbnum.gcd(num1,num2) 171 end 172 173val RAT_ADD_CONV = 174 binop_prenorm coreadd_conv THENC TRY_CONV elim_neg0_conv THENC 175 TRY_CONV elim_common_factor THENC 176 EVERY_CONV (map (TRY_CONV o REWR_CONV) [RAT_DIV_1, RAT_DIV_0]) 177 178end (* struct *) 179