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