|
1 (* Title: HOL/int_factor_simprocs.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 2000 University of Cambridge |
|
5 |
|
6 Factor cancellation simprocs for the integers (and for fields). |
|
7 |
|
8 This file can't be combined with int_arith1 because it requires IntDiv.thy. |
|
9 *) |
|
10 |
|
11 |
|
12 (*To quote from Provers/Arith/cancel_numeral_factor.ML: |
|
13 |
|
14 Cancels common coefficients in balanced expressions: |
|
15 |
|
16 u*#m ~~ u'*#m' == #n*u ~~ #n'*u' |
|
17 |
|
18 where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) |
|
19 and d = gcd(m,m') and n=m/d and n'=m'/d. |
|
20 *) |
|
21 |
|
22 val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of_eq_neg}, @{thm le_number_of_eq}]; |
|
23 |
|
24 local |
|
25 open Int_Numeral_Simprocs |
|
26 in |
|
27 |
|
28 structure CancelNumeralFactorCommon = |
|
29 struct |
|
30 val mk_coeff = mk_coeff |
|
31 val dest_coeff = dest_coeff 1 |
|
32 val trans_tac = fn _ => trans_tac |
|
33 |
|
34 val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s |
|
35 val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps |
|
36 val norm_ss3 = HOL_ss addsimps @{thms mult_ac} |
|
37 fun norm_tac ss = |
|
38 ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
39 THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
40 THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
41 |
|
42 val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps |
|
43 fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
44 val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq |
|
45 [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left}, |
|
46 @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}]; |
|
47 end |
|
48 |
|
49 (*Version for integer division*) |
|
50 structure IntDivCancelNumeralFactor = CancelNumeralFactorFun |
|
51 (open CancelNumeralFactorCommon |
|
52 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
53 val mk_bal = HOLogic.mk_binop @{const_name Divides.div} |
|
54 val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT |
|
55 val cancel = @{thm zdiv_zmult_zmult1} RS trans |
|
56 val neg_exchanges = false |
|
57 ) |
|
58 |
|
59 (*Version for fields*) |
|
60 structure DivideCancelNumeralFactor = CancelNumeralFactorFun |
|
61 (open CancelNumeralFactorCommon |
|
62 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
63 val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} |
|
64 val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT |
|
65 val cancel = @{thm mult_divide_mult_cancel_left} RS trans |
|
66 val neg_exchanges = false |
|
67 ) |
|
68 |
|
69 structure EqCancelNumeralFactor = CancelNumeralFactorFun |
|
70 (open CancelNumeralFactorCommon |
|
71 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
72 val mk_bal = HOLogic.mk_eq |
|
73 val dest_bal = HOLogic.dest_bin "op =" Term.dummyT |
|
74 val cancel = @{thm mult_cancel_left} RS trans |
|
75 val neg_exchanges = false |
|
76 ) |
|
77 |
|
78 structure LessCancelNumeralFactor = CancelNumeralFactorFun |
|
79 (open CancelNumeralFactorCommon |
|
80 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
81 val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} |
|
82 val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT |
|
83 val cancel = @{thm mult_less_cancel_left} RS trans |
|
84 val neg_exchanges = true |
|
85 ) |
|
86 |
|
87 structure LeCancelNumeralFactor = CancelNumeralFactorFun |
|
88 (open CancelNumeralFactorCommon |
|
89 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
90 val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} |
|
91 val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT |
|
92 val cancel = @{thm mult_le_cancel_left} RS trans |
|
93 val neg_exchanges = true |
|
94 ) |
|
95 |
|
96 val cancel_numeral_factors = |
|
97 map Int_Numeral_Base_Simprocs.prep_simproc |
|
98 [("ring_eq_cancel_numeral_factor", |
|
99 ["(l::'a::{idom,number_ring}) * m = n", |
|
100 "(l::'a::{idom,number_ring}) = m * n"], |
|
101 K EqCancelNumeralFactor.proc), |
|
102 ("ring_less_cancel_numeral_factor", |
|
103 ["(l::'a::{ordered_idom,number_ring}) * m < n", |
|
104 "(l::'a::{ordered_idom,number_ring}) < m * n"], |
|
105 K LessCancelNumeralFactor.proc), |
|
106 ("ring_le_cancel_numeral_factor", |
|
107 ["(l::'a::{ordered_idom,number_ring}) * m <= n", |
|
108 "(l::'a::{ordered_idom,number_ring}) <= m * n"], |
|
109 K LeCancelNumeralFactor.proc), |
|
110 ("int_div_cancel_numeral_factors", |
|
111 ["((l::int) * m) div n", "(l::int) div (m * n)"], |
|
112 K IntDivCancelNumeralFactor.proc), |
|
113 ("divide_cancel_numeral_factor", |
|
114 ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", |
|
115 "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", |
|
116 "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], |
|
117 K DivideCancelNumeralFactor.proc)]; |
|
118 |
|
119 (* referenced by rat_arith.ML *) |
|
120 val field_cancel_numeral_factors = |
|
121 map Int_Numeral_Base_Simprocs.prep_simproc |
|
122 [("field_eq_cancel_numeral_factor", |
|
123 ["(l::'a::{field,number_ring}) * m = n", |
|
124 "(l::'a::{field,number_ring}) = m * n"], |
|
125 K EqCancelNumeralFactor.proc), |
|
126 ("field_cancel_numeral_factor", |
|
127 ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", |
|
128 "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", |
|
129 "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], |
|
130 K DivideCancelNumeralFactor.proc)] |
|
131 |
|
132 end; |
|
133 |
|
134 Addsimprocs cancel_numeral_factors; |
|
135 |
|
136 (*examples: |
|
137 print_depth 22; |
|
138 set timing; |
|
139 set trace_simp; |
|
140 fun test s = (Goal s; by (Simp_tac 1)); |
|
141 |
|
142 test "9*x = 12 * (y::int)"; |
|
143 test "(9*x) div (12 * (y::int)) = z"; |
|
144 test "9*x < 12 * (y::int)"; |
|
145 test "9*x <= 12 * (y::int)"; |
|
146 |
|
147 test "-99*x = 132 * (y::int)"; |
|
148 test "(-99*x) div (132 * (y::int)) = z"; |
|
149 test "-99*x < 132 * (y::int)"; |
|
150 test "-99*x <= 132 * (y::int)"; |
|
151 |
|
152 test "999*x = -396 * (y::int)"; |
|
153 test "(999*x) div (-396 * (y::int)) = z"; |
|
154 test "999*x < -396 * (y::int)"; |
|
155 test "999*x <= -396 * (y::int)"; |
|
156 |
|
157 test "-99*x = -81 * (y::int)"; |
|
158 test "(-99*x) div (-81 * (y::int)) = z"; |
|
159 test "-99*x <= -81 * (y::int)"; |
|
160 test "-99*x < -81 * (y::int)"; |
|
161 |
|
162 test "-2 * x = -1 * (y::int)"; |
|
163 test "-2 * x = -(y::int)"; |
|
164 test "(-2 * x) div (-1 * (y::int)) = z"; |
|
165 test "-2 * x < -(y::int)"; |
|
166 test "-2 * x <= -1 * (y::int)"; |
|
167 test "-x < -23 * (y::int)"; |
|
168 test "-x <= -23 * (y::int)"; |
|
169 *) |
|
170 |
|
171 (*And the same examples for fields such as rat or real: |
|
172 test "0 <= (y::rat) * -2"; |
|
173 test "9*x = 12 * (y::rat)"; |
|
174 test "(9*x) / (12 * (y::rat)) = z"; |
|
175 test "9*x < 12 * (y::rat)"; |
|
176 test "9*x <= 12 * (y::rat)"; |
|
177 |
|
178 test "-99*x = 132 * (y::rat)"; |
|
179 test "(-99*x) / (132 * (y::rat)) = z"; |
|
180 test "-99*x < 132 * (y::rat)"; |
|
181 test "-99*x <= 132 * (y::rat)"; |
|
182 |
|
183 test "999*x = -396 * (y::rat)"; |
|
184 test "(999*x) / (-396 * (y::rat)) = z"; |
|
185 test "999*x < -396 * (y::rat)"; |
|
186 test "999*x <= -396 * (y::rat)"; |
|
187 |
|
188 test "(- ((2::rat) * x) <= 2 * y)"; |
|
189 test "-99*x = -81 * (y::rat)"; |
|
190 test "(-99*x) / (-81 * (y::rat)) = z"; |
|
191 test "-99*x <= -81 * (y::rat)"; |
|
192 test "-99*x < -81 * (y::rat)"; |
|
193 |
|
194 test "-2 * x = -1 * (y::rat)"; |
|
195 test "-2 * x = -(y::rat)"; |
|
196 test "(-2 * x) / (-1 * (y::rat)) = z"; |
|
197 test "-2 * x < -(y::rat)"; |
|
198 test "-2 * x <= -1 * (y::rat)"; |
|
199 test "-x < -23 * (y::rat)"; |
|
200 test "-x <= -23 * (y::rat)"; |
|
201 *) |
|
202 |
|
203 |
|
204 (** Declarations for ExtractCommonTerm **) |
|
205 |
|
206 local |
|
207 open Int_Numeral_Simprocs |
|
208 in |
|
209 |
|
210 (*Find first term that matches u*) |
|
211 fun find_first_t past u [] = raise TERM ("find_first_t", []) |
|
212 | find_first_t past u (t::terms) = |
|
213 if u aconv t then (rev past @ terms) |
|
214 else find_first_t (t::past) u terms |
|
215 handle TERM _ => find_first_t (t::past) u terms; |
|
216 |
|
217 (** Final simplification for the CancelFactor simprocs **) |
|
218 val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq |
|
219 [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, @{thm numeral_1_eq_1}]; |
|
220 |
|
221 fun cancel_simplify_meta_eq cancel_th ss th = |
|
222 simplify_one ss (([th, cancel_th]) MRS trans); |
|
223 |
|
224 structure CancelFactorCommon = |
|
225 struct |
|
226 val mk_sum = long_mk_prod |
|
227 val dest_sum = dest_prod |
|
228 val mk_coeff = mk_coeff |
|
229 val dest_coeff = dest_coeff |
|
230 val find_first = find_first_t [] |
|
231 val trans_tac = fn _ => trans_tac |
|
232 val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} |
|
233 fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) |
|
234 end; |
|
235 |
|
236 (*mult_cancel_left requires a ring with no zero divisors.*) |
|
237 structure EqCancelFactor = ExtractCommonTermFun |
|
238 (open CancelFactorCommon |
|
239 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
240 val mk_bal = HOLogic.mk_eq |
|
241 val dest_bal = HOLogic.dest_bin "op =" Term.dummyT |
|
242 val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_cancel_left} |
|
243 ); |
|
244 |
|
245 (*zdiv_zmult_zmult1_if is for integer division (div).*) |
|
246 structure IntDivCancelFactor = ExtractCommonTermFun |
|
247 (open CancelFactorCommon |
|
248 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
249 val mk_bal = HOLogic.mk_binop @{const_name Divides.div} |
|
250 val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT |
|
251 val simplify_meta_eq = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if} |
|
252 ); |
|
253 |
|
254 structure IntModCancelFactor = ExtractCommonTermFun |
|
255 (open CancelFactorCommon |
|
256 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
257 val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} |
|
258 val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT |
|
259 val simplify_meta_eq = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1} |
|
260 ); |
|
261 |
|
262 structure IntDvdCancelFactor = ExtractCommonTermFun |
|
263 (open CancelFactorCommon |
|
264 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
265 val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} |
|
266 val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.intT |
|
267 val simplify_meta_eq = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj} |
|
268 ); |
|
269 |
|
270 (*Version for all fields, including unordered ones (type complex).*) |
|
271 structure DivideCancelFactor = ExtractCommonTermFun |
|
272 (open CancelFactorCommon |
|
273 val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
|
274 val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} |
|
275 val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT |
|
276 val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if} |
|
277 ); |
|
278 |
|
279 val cancel_factors = |
|
280 map Int_Numeral_Base_Simprocs.prep_simproc |
|
281 [("ring_eq_cancel_factor", |
|
282 ["(l::'a::{idom}) * m = n", |
|
283 "(l::'a::{idom}) = m * n"], |
|
284 K EqCancelFactor.proc), |
|
285 ("int_div_cancel_factor", |
|
286 ["((l::int) * m) div n", "(l::int) div (m * n)"], |
|
287 K IntDivCancelFactor.proc), |
|
288 ("int_mod_cancel_factor", |
|
289 ["((l::int) * m) mod n", "(l::int) mod (m * n)"], |
|
290 K IntModCancelFactor.proc), |
|
291 ("int_dvd_cancel_factor", |
|
292 ["((l::int) * m) dvd n", "(l::int) dvd (m * n)"], |
|
293 K IntDvdCancelFactor.proc), |
|
294 ("divide_cancel_factor", |
|
295 ["((l::'a::{division_by_zero,field}) * m) / n", |
|
296 "(l::'a::{division_by_zero,field}) / (m * n)"], |
|
297 K DivideCancelFactor.proc)]; |
|
298 |
|
299 end; |
|
300 |
|
301 Addsimprocs cancel_factors; |
|
302 |
|
303 |
|
304 (*examples: |
|
305 print_depth 22; |
|
306 set timing; |
|
307 set trace_simp; |
|
308 fun test s = (Goal s; by (Asm_simp_tac 1)); |
|
309 |
|
310 test "x*k = k*(y::int)"; |
|
311 test "k = k*(y::int)"; |
|
312 test "a*(b*c) = (b::int)"; |
|
313 test "a*(b*c) = d*(b::int)*(x*a)"; |
|
314 |
|
315 test "(x*k) div (k*(y::int)) = (uu::int)"; |
|
316 test "(k) div (k*(y::int)) = (uu::int)"; |
|
317 test "(a*(b*c)) div ((b::int)) = (uu::int)"; |
|
318 test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"; |
|
319 *) |
|
320 |
|
321 (*And the same examples for fields such as rat or real: |
|
322 print_depth 22; |
|
323 set timing; |
|
324 set trace_simp; |
|
325 fun test s = (Goal s; by (Asm_simp_tac 1)); |
|
326 |
|
327 test "x*k = k*(y::rat)"; |
|
328 test "k = k*(y::rat)"; |
|
329 test "a*(b*c) = (b::rat)"; |
|
330 test "a*(b*c) = d*(b::rat)*(x*a)"; |
|
331 |
|
332 |
|
333 test "(x*k) / (k*(y::rat)) = (uu::rat)"; |
|
334 test "(k) / (k*(y::rat)) = (uu::rat)"; |
|
335 test "(a*(b*c)) / ((b::rat)) = (uu::rat)"; |
|
336 test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"; |
|
337 |
|
338 (*FIXME: what do we do about this?*) |
|
339 test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"; |
|
340 *) |