26 val reorient_simproc = |
26 val reorient_simproc = |
27 Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc); |
27 Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc); |
28 |
28 |
29 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) |
29 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) |
30 val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; |
30 val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; |
|
31 |
|
32 |
|
33 (** Utilities **) |
|
34 |
|
35 fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; |
|
36 |
|
37 fun find_first_numeral past (t::terms) = |
|
38 ((snd (HOLogic.dest_number t), rev past @ terms) |
|
39 handle TERM _ => find_first_numeral (t::past) terms) |
|
40 | find_first_numeral past [] = raise TERM("find_first_numeral", []); |
|
41 |
|
42 val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; |
|
43 |
|
44 fun mk_minus t = |
|
45 let val T = Term.fastype_of t |
|
46 in Const (@{const_name HOL.uminus}, T --> T) $ t end; |
|
47 |
|
48 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
|
49 fun mk_sum T [] = mk_number T 0 |
|
50 | mk_sum T [t,u] = mk_plus (t, u) |
|
51 | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
|
52 |
|
53 (*this version ALWAYS includes a trailing zero*) |
|
54 fun long_mk_sum T [] = mk_number T 0 |
|
55 | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
|
56 |
|
57 val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT; |
|
58 |
|
59 (*decompose additions AND subtractions as a sum*) |
|
60 fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) = |
|
61 dest_summing (pos, t, dest_summing (pos, u, ts)) |
|
62 | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) = |
|
63 dest_summing (pos, t, dest_summing (not pos, u, ts)) |
|
64 | dest_summing (pos, t, ts) = |
|
65 if pos then t::ts else mk_minus t :: ts; |
|
66 |
|
67 fun dest_sum t = dest_summing (true, t, []); |
|
68 |
|
69 val mk_diff = HOLogic.mk_binop @{const_name HOL.minus}; |
|
70 val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT; |
|
71 |
|
72 val mk_times = HOLogic.mk_binop @{const_name HOL.times}; |
|
73 |
|
74 fun one_of T = Const(@{const_name HOL.one},T); |
|
75 |
|
76 (* build product with trailing 1 rather than Numeral 1 in order to avoid the |
|
77 unnecessary restriction to type class number_ring |
|
78 which is not required for cancellation of common factors in divisions. |
|
79 *) |
|
80 fun mk_prod T = |
|
81 let val one = one_of T |
|
82 fun mk [] = one |
|
83 | mk [t] = t |
|
84 | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) |
|
85 in mk end; |
|
86 |
|
87 (*This version ALWAYS includes a trailing one*) |
|
88 fun long_mk_prod T [] = one_of T |
|
89 | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); |
|
90 |
|
91 val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT; |
|
92 |
|
93 fun dest_prod t = |
|
94 let val (t,u) = dest_times t |
|
95 in dest_prod t @ dest_prod u end |
|
96 handle TERM _ => [t]; |
|
97 |
|
98 (*DON'T do the obvious simplifications; that would create special cases*) |
|
99 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); |
|
100 |
|
101 (*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
102 fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t |
|
103 | dest_coeff sign t = |
|
104 let val ts = sort TermOrd.term_ord (dest_prod t) |
|
105 val (n, ts') = find_first_numeral [] ts |
|
106 handle TERM _ => (1, ts) |
|
107 in (sign*n, mk_prod (Term.fastype_of t) ts') end; |
|
108 |
|
109 (*Find first coefficient-term THAT MATCHES u*) |
|
110 fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
111 | find_first_coeff past u (t::terms) = |
|
112 let val (n,u') = dest_coeff 1 t |
|
113 in if u aconv u' then (n, rev past @ terms) |
|
114 else find_first_coeff (t::past) u terms |
|
115 end |
|
116 handle TERM _ => find_first_coeff (t::past) u terms; |
|
117 |
|
118 (*Fractions as pairs of ints. Can't use Rat.rat because the representation |
|
119 needs to preserve negative values in the denominator.*) |
|
120 fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); |
|
121 |
|
122 (*Don't reduce fractions; sums must be proved by rule add_frac_eq. |
|
123 Fractions are reduced later by the cancel_numeral_factor simproc.*) |
|
124 fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); |
|
125 |
|
126 val mk_divide = HOLogic.mk_binop @{const_name HOL.divide}; |
|
127 |
|
128 (*Build term (p / q) * t*) |
|
129 fun mk_fcoeff ((p, q), t) = |
|
130 let val T = Term.fastype_of t |
|
131 in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; |
|
132 |
|
133 (*Express t as a product of a fraction with other sorted terms*) |
|
134 fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t |
|
135 | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) = |
|
136 let val (p, t') = dest_coeff sign t |
|
137 val (q, u') = dest_coeff 1 u |
|
138 in (mk_frac (p, q), mk_divide (t', u')) end |
|
139 | dest_fcoeff sign t = |
|
140 let val (p, t') = dest_coeff sign t |
|
141 val T = Term.fastype_of t |
|
142 in (mk_frac (p, 1), mk_divide (t', one_of T)) end; |
|
143 |
31 |
144 |
32 (** New term ordering so that AC-rewriting brings numerals to the front **) |
145 (** New term ordering so that AC-rewriting brings numerals to the front **) |
33 |
146 |
34 (*Order integers by absolute value and then by sign. The standard integer |
147 (*Order integers by absolute value and then by sign. The standard integer |
35 ordering is not well-founded.*) |
148 ordering is not well-founded.*) |
59 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) |
172 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) |
60 end; |
173 end; |
61 |
174 |
62 fun numtermless tu = (numterm_ord tu = LESS); |
175 fun numtermless tu = (numterm_ord tu = LESS); |
63 |
176 |
64 (*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*) |
|
65 val num_ss = HOL_ss settermless numtermless; |
177 val num_ss = HOL_ss settermless numtermless; |
66 |
|
67 |
|
68 (** Utilities **) |
|
69 |
|
70 fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; |
|
71 |
|
72 fun find_first_numeral past (t::terms) = |
|
73 ((snd (HOLogic.dest_number t), rev past @ terms) |
|
74 handle TERM _ => find_first_numeral (t::past) terms) |
|
75 | find_first_numeral past [] = raise TERM("find_first_numeral", []); |
|
76 |
|
77 val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; |
|
78 |
|
79 fun mk_minus t = |
|
80 let val T = Term.fastype_of t |
|
81 in Const (@{const_name HOL.uminus}, T --> T) $ t end; |
|
82 |
|
83 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
|
84 fun mk_sum T [] = mk_number T 0 |
|
85 | mk_sum T [t,u] = mk_plus (t, u) |
|
86 | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
|
87 |
|
88 (*this version ALWAYS includes a trailing zero*) |
|
89 fun long_mk_sum T [] = mk_number T 0 |
|
90 | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
|
91 |
|
92 val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT; |
|
93 |
|
94 (*decompose additions AND subtractions as a sum*) |
|
95 fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) = |
|
96 dest_summing (pos, t, dest_summing (pos, u, ts)) |
|
97 | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) = |
|
98 dest_summing (pos, t, dest_summing (not pos, u, ts)) |
|
99 | dest_summing (pos, t, ts) = |
|
100 if pos then t::ts else mk_minus t :: ts; |
|
101 |
|
102 fun dest_sum t = dest_summing (true, t, []); |
|
103 |
|
104 val mk_diff = HOLogic.mk_binop @{const_name HOL.minus}; |
|
105 val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT; |
|
106 |
|
107 val mk_times = HOLogic.mk_binop @{const_name HOL.times}; |
|
108 |
|
109 fun one_of T = Const(@{const_name HOL.one},T); |
|
110 |
|
111 (* build product with trailing 1 rather than Numeral 1 in order to avoid the |
|
112 unnecessary restriction to type class number_ring |
|
113 which is not required for cancellation of common factors in divisions. |
|
114 *) |
|
115 fun mk_prod T = |
|
116 let val one = one_of T |
|
117 fun mk [] = one |
|
118 | mk [t] = t |
|
119 | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) |
|
120 in mk end; |
|
121 |
|
122 (*This version ALWAYS includes a trailing one*) |
|
123 fun long_mk_prod T [] = one_of T |
|
124 | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); |
|
125 |
|
126 val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT; |
|
127 |
|
128 fun dest_prod t = |
|
129 let val (t,u) = dest_times t |
|
130 in dest_prod t @ dest_prod u end |
|
131 handle TERM _ => [t]; |
|
132 |
|
133 (*DON'T do the obvious simplifications; that would create special cases*) |
|
134 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); |
|
135 |
|
136 (*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
137 fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t |
|
138 | dest_coeff sign t = |
|
139 let val ts = sort TermOrd.term_ord (dest_prod t) |
|
140 val (n, ts') = find_first_numeral [] ts |
|
141 handle TERM _ => (1, ts) |
|
142 in (sign*n, mk_prod (Term.fastype_of t) ts') end; |
|
143 |
|
144 (*Find first coefficient-term THAT MATCHES u*) |
|
145 fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
146 | find_first_coeff past u (t::terms) = |
|
147 let val (n,u') = dest_coeff 1 t |
|
148 in if u aconv u' then (n, rev past @ terms) |
|
149 else find_first_coeff (t::past) u terms |
|
150 end |
|
151 handle TERM _ => find_first_coeff (t::past) u terms; |
|
152 |
|
153 (*Fractions as pairs of ints. Can't use Rat.rat because the representation |
|
154 needs to preserve negative values in the denominator.*) |
|
155 fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); |
|
156 |
|
157 (*Don't reduce fractions; sums must be proved by rule add_frac_eq. |
|
158 Fractions are reduced later by the cancel_numeral_factor simproc.*) |
|
159 fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); |
|
160 |
|
161 val mk_divide = HOLogic.mk_binop @{const_name HOL.divide}; |
|
162 |
|
163 (*Build term (p / q) * t*) |
|
164 fun mk_fcoeff ((p, q), t) = |
|
165 let val T = Term.fastype_of t |
|
166 in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; |
|
167 |
|
168 (*Express t as a product of a fraction with other sorted terms*) |
|
169 fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t |
|
170 | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) = |
|
171 let val (p, t') = dest_coeff sign t |
|
172 val (q, u') = dest_coeff 1 u |
|
173 in (mk_frac (p, q), mk_divide (t', u')) end |
|
174 | dest_fcoeff sign t = |
|
175 let val (p, t') = dest_coeff sign t |
|
176 val T = Term.fastype_of t |
|
177 in (mk_frac (p, 1), mk_divide (t', one_of T)) end; |
|
178 |
178 |
179 |
179 |
180 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) |
180 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) |
181 val add_0s = thms "add_0s"; |
181 val add_0s = thms "add_0s"; |
182 val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"]; |
182 val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"]; |
215 [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym]; |
215 [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym]; |
216 |
216 |
217 (*combine unary minus with numeric literals, however nested within a product*) |
217 (*combine unary minus with numeric literals, however nested within a product*) |
218 val mult_minus_simps = |
218 val mult_minus_simps = |
219 [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; |
219 [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; |
220 |
|
221 (*Apply the given rewrite (if present) just once*) |
|
222 fun trans_tac NONE = all_tac |
|
223 | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); |
|
224 |
|
225 fun simplify_meta_eq rules = |
|
226 let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules |
|
227 in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end |
|
228 |
220 |
229 structure CancelNumeralsCommon = |
221 structure CancelNumeralsCommon = |
230 struct |
222 struct |
231 val mk_sum = mk_sum |
223 val mk_sum = mk_sum |
232 val dest_sum = dest_sum |
224 val dest_sum = dest_sum |
233 val mk_coeff = mk_coeff |
225 val mk_coeff = mk_coeff |
234 val dest_coeff = dest_coeff 1 |
226 val dest_coeff = dest_coeff 1 |
235 val find_first_coeff = find_first_coeff [] |
227 val find_first_coeff = find_first_coeff [] |
236 val trans_tac = fn _ => trans_tac |
228 val trans_tac = K Arith_Data.trans_tac |
237 |
229 |
238 val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ |
230 val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ |
239 diff_simps @ minus_simps @ @{thms add_ac} |
231 diff_simps @ minus_simps @ @{thms add_ac} |
240 val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps |
232 val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps |
241 val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} |
233 val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} |