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