author | haftmann |
Wed, 06 Sep 2006 13:48:02 +0200 | |
changeset 20485 | 3078fd2eec7b |
parent 20044 | 92cc2f4c7335 |
child 21416 | f23e4e75dfd3 |
permissions | -rw-r--r-- |
10536 | 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 |
||
14390 | 6 |
Factor cancellation simprocs for the integers (and for fields). |
10536 | 7 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14113
diff
changeset
|
8 |
This file can't be combined with int_arith1 because it requires IntDiv.thy. |
10536 | 9 |
*) |
10 |
||
14390 | 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 /) **) |
|
10536 | 25 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
26 |
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)"; |
13462 | 27 |
by (stac zdiv_zmult_zmult1 1); |
28 |
by Auto_tac; |
|
10536 | 29 |
qed "int_mult_div_cancel1"; |
30 |
||
10703 | 31 |
(*For ExtractCommonTermFun, cancelling common factors*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
32 |
Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"; |
13462 | 33 |
by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1); |
10703 | 34 |
qed "int_mult_div_cancel_disj"; |
35 |
||
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14113
diff
changeset
|
36 |
|
10536 | 37 |
local |
38 |
open Int_Numeral_Simprocs |
|
39 |
in |
|
40 |
||
41 |
structure CancelNumeralFactorCommon = |
|
42 |
struct |
|
13462 | 43 |
val mk_coeff = mk_coeff |
44 |
val dest_coeff = dest_coeff 1 |
|
16973 | 45 |
val trans_tac = fn _ => trans_tac |
18328 | 46 |
|
47 |
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s |
|
20485 | 48 |
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps |
18328 | 49 |
val norm_ss3 = HOL_ss addsimps mult_ac |
16973 | 50 |
fun norm_tac ss = |
18328 | 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 |
||
20485 | 55 |
val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps |
18328 | 56 |
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
16973 | 57 |
val simplify_meta_eq = |
14390 | 58 |
Int_Numeral_Simprocs.simplify_meta_eq |
59 |
[add_0, add_0_right, |
|
20485 | 60 |
mult_zero_left, mult_zero_right, mult_num1, mult_1_right]; |
10536 | 61 |
end |
62 |
||
14390 | 63 |
(*Version for integer division*) |
10536 | 64 |
structure DivCancelNumeralFactor = CancelNumeralFactorFun |
65 |
(open CancelNumeralFactorCommon |
|
20485 | 66 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
10536 | 67 |
val mk_bal = HOLogic.mk_binop "Divides.op div" |
68 |
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT |
|
69 |
val cancel = int_mult_div_cancel1 RS trans |
|
70 |
val neg_exchanges = false |
|
71 |
) |
|
72 |
||
14390 | 73 |
(*Version for fields*) |
74 |
structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun |
|
75 |
(open CancelNumeralFactorCommon |
|
20485 | 76 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
14390 | 77 |
val mk_bal = HOLogic.mk_binop "HOL.divide" |
78 |
val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT |
|
79 |
val cancel = mult_divide_cancel_left RS trans |
|
80 |
val neg_exchanges = false |
|
81 |
) |
|
82 |
||
83 |
(*Version for ordered rings: mult_cancel_left requires an ordering*) |
|
10536 | 84 |
structure EqCancelNumeralFactor = CancelNumeralFactorFun |
85 |
(open CancelNumeralFactorCommon |
|
20485 | 86 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
10536 | 87 |
val mk_bal = HOLogic.mk_eq |
14390 | 88 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14113
diff
changeset
|
89 |
val cancel = mult_cancel_left RS trans |
10536 | 90 |
val neg_exchanges = false |
91 |
) |
|
92 |
||
14390 | 93 |
(*Version for (unordered) fields*) |
94 |
structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun |
|
95 |
(open CancelNumeralFactorCommon |
|
20485 | 96 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
14390 | 97 |
val mk_bal = HOLogic.mk_eq |
98 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT |
|
99 |
val cancel = field_mult_cancel_left RS trans |
|
100 |
val neg_exchanges = false |
|
101 |
) |
|
102 |
||
10536 | 103 |
structure LessCancelNumeralFactor = CancelNumeralFactorFun |
104 |
(open CancelNumeralFactorCommon |
|
20485 | 105 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
19277 | 106 |
val mk_bal = HOLogic.mk_binrel "Orderings.less" |
107 |
val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14113
diff
changeset
|
108 |
val cancel = mult_less_cancel_left RS trans |
10536 | 109 |
val neg_exchanges = true |
110 |
) |
|
111 |
||
112 |
structure LeCancelNumeralFactor = CancelNumeralFactorFun |
|
113 |
(open CancelNumeralFactorCommon |
|
20485 | 114 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
19277 | 115 |
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq" |
116 |
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14113
diff
changeset
|
117 |
val cancel = mult_le_cancel_left RS trans |
10536 | 118 |
val neg_exchanges = true |
119 |
) |
|
120 |
||
14390 | 121 |
val ring_cancel_numeral_factors = |
20485 | 122 |
map Int_Numeral_Base_Simprocs.prep_simproc |
14390 | 123 |
[("ring_eq_cancel_numeral_factor", |
14738 | 124 |
["(l::'a::{ordered_idom,number_ring}) * m = n", |
125 |
"(l::'a::{ordered_idom,number_ring}) = m * n"], |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
126 |
K EqCancelNumeralFactor.proc), |
14390 | 127 |
("ring_less_cancel_numeral_factor", |
14738 | 128 |
["(l::'a::{ordered_idom,number_ring}) * m < n", |
129 |
"(l::'a::{ordered_idom,number_ring}) < m * n"], |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
130 |
K LessCancelNumeralFactor.proc), |
14390 | 131 |
("ring_le_cancel_numeral_factor", |
14738 | 132 |
["(l::'a::{ordered_idom,number_ring}) * m <= n", |
133 |
"(l::'a::{ordered_idom,number_ring}) <= m * n"], |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
134 |
K LeCancelNumeralFactor.proc), |
14390 | 135 |
("int_div_cancel_numeral_factors", |
136 |
["((l::int) * m) div n", "(l::int) div (m * n)"], |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
137 |
K DivCancelNumeralFactor.proc)]; |
10536 | 138 |
|
14390 | 139 |
|
140 |
val field_cancel_numeral_factors = |
|
20485 | 141 |
map Int_Numeral_Base_Simprocs.prep_simproc |
14390 | 142 |
[("field_eq_cancel_numeral_factor", |
143 |
["(l::'a::{field,number_ring}) * m = n", |
|
144 |
"(l::'a::{field,number_ring}) = m * n"], |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
145 |
K FieldEqCancelNumeralFactor.proc), |
14390 | 146 |
("field_cancel_numeral_factor", |
14426 | 147 |
["((l::'a::{division_by_zero,field,number_ring}) * m) / n", |
148 |
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)", |
|
149 |
"((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
150 |
K FieldDivCancelNumeralFactor.proc)] |
14390 | 151 |
|
10536 | 152 |
end; |
153 |
||
14390 | 154 |
Addsimprocs ring_cancel_numeral_factors; |
155 |
Addsimprocs field_cancel_numeral_factors; |
|
10536 | 156 |
|
157 |
(*examples: |
|
158 |
print_depth 22; |
|
159 |
set timing; |
|
160 |
set trace_simp; |
|
13462 | 161 |
fun test s = (Goal s; by (Simp_tac 1)); |
10536 | 162 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
163 |
test "9*x = 12 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
164 |
test "(9*x) div (12 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
165 |
test "9*x < 12 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
166 |
test "9*x <= 12 * (y::int)"; |
10536 | 167 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
168 |
test "-99*x = 132 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
169 |
test "(-99*x) div (132 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
170 |
test "-99*x < 132 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
171 |
test "-99*x <= 132 * (y::int)"; |
10536 | 172 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
173 |
test "999*x = -396 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
174 |
test "(999*x) div (-396 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
175 |
test "999*x < -396 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
176 |
test "999*x <= -396 * (y::int)"; |
10536 | 177 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
178 |
test "-99*x = -81 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
179 |
test "(-99*x) div (-81 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
180 |
test "-99*x <= -81 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
181 |
test "-99*x < -81 * (y::int)"; |
10536 | 182 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
183 |
test "-2 * x = -1 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
184 |
test "-2 * x = -(y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
185 |
test "(-2 * x) div (-1 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
186 |
test "-2 * x < -(y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
187 |
test "-2 * x <= -1 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
188 |
test "-x < -23 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
189 |
test "-x <= -23 * (y::int)"; |
10536 | 190 |
*) |
191 |
||
14390 | 192 |
(*And the same examples for fields such as rat or real: |
193 |
test "0 <= (y::rat) * -2"; |
|
194 |
test "9*x = 12 * (y::rat)"; |
|
195 |
test "(9*x) / (12 * (y::rat)) = z"; |
|
196 |
test "9*x < 12 * (y::rat)"; |
|
197 |
test "9*x <= 12 * (y::rat)"; |
|
198 |
||
199 |
test "-99*x = 132 * (y::rat)"; |
|
200 |
test "(-99*x) / (132 * (y::rat)) = z"; |
|
201 |
test "-99*x < 132 * (y::rat)"; |
|
202 |
test "-99*x <= 132 * (y::rat)"; |
|
203 |
||
204 |
test "999*x = -396 * (y::rat)"; |
|
205 |
test "(999*x) / (-396 * (y::rat)) = z"; |
|
206 |
test "999*x < -396 * (y::rat)"; |
|
207 |
test "999*x <= -396 * (y::rat)"; |
|
208 |
||
209 |
test "(- ((2::rat) * x) <= 2 * y)"; |
|
210 |
test "-99*x = -81 * (y::rat)"; |
|
211 |
test "(-99*x) / (-81 * (y::rat)) = z"; |
|
212 |
test "-99*x <= -81 * (y::rat)"; |
|
213 |
test "-99*x < -81 * (y::rat)"; |
|
214 |
||
215 |
test "-2 * x = -1 * (y::rat)"; |
|
216 |
test "-2 * x = -(y::rat)"; |
|
217 |
test "(-2 * x) / (-1 * (y::rat)) = z"; |
|
218 |
test "-2 * x < -(y::rat)"; |
|
219 |
test "-2 * x <= -1 * (y::rat)"; |
|
220 |
test "-x < -23 * (y::rat)"; |
|
221 |
test "-x <= -23 * (y::rat)"; |
|
222 |
*) |
|
223 |
||
10703 | 224 |
|
225 |
(** Declarations for ExtractCommonTerm **) |
|
226 |
||
227 |
local |
|
228 |
open Int_Numeral_Simprocs |
|
229 |
in |
|
230 |
||
231 |
(*Find first term that matches u*) |
|
18442 | 232 |
fun find_first_t past u [] = raise TERM ("find_first_t", []) |
233 |
| find_first_t past u (t::terms) = |
|
13462 | 234 |
if u aconv t then (rev past @ terms) |
18442 | 235 |
else find_first_t (t::past) u terms |
236 |
handle TERM _ => find_first_t (t::past) u terms; |
|
10703 | 237 |
|
15271
3c32a26510c4
fixed some awkward problems with nat/int simprocs
paulson
parents:
14738
diff
changeset
|
238 |
(** Final simplification for the CancelFactor simprocs **) |
3c32a26510c4
fixed some awkward problems with nat/int simprocs
paulson
parents:
14738
diff
changeset
|
239 |
val simplify_one = |
3c32a26510c4
fixed some awkward problems with nat/int simprocs
paulson
parents:
14738
diff
changeset
|
240 |
Int_Numeral_Simprocs.simplify_meta_eq |
3c32a26510c4
fixed some awkward problems with nat/int simprocs
paulson
parents:
14738
diff
changeset
|
241 |
[mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1]; |
3c32a26510c4
fixed some awkward problems with nat/int simprocs
paulson
parents:
14738
diff
changeset
|
242 |
|
16973 | 243 |
fun cancel_simplify_meta_eq cancel_th ss th = |
244 |
simplify_one ss (([th, cancel_th]) MRS trans); |
|
10703 | 245 |
|
14426 | 246 |
(*At present, long_mk_prod creates Numeral1, so this requires the axclass |
247 |
number_ring*) |
|
10703 | 248 |
structure CancelFactorCommon = |
249 |
struct |
|
13462 | 250 |
val mk_sum = long_mk_prod |
251 |
val dest_sum = dest_prod |
|
252 |
val mk_coeff = mk_coeff |
|
253 |
val dest_coeff = dest_coeff |
|
18442 | 254 |
val find_first = find_first_t [] |
16973 | 255 |
val trans_tac = fn _ => trans_tac |
18328 | 256 |
val norm_ss = HOL_ss addsimps mult_1s @ mult_ac |
257 |
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) |
|
10703 | 258 |
end; |
259 |
||
14738 | 260 |
(*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
261 |
rat_arith.ML works for all fields.*) |
10703 | 262 |
structure EqCancelFactor = ExtractCommonTermFun |
263 |
(open CancelFactorCommon |
|
20485 | 264 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
10703 | 265 |
val mk_bal = HOLogic.mk_eq |
266 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14113
diff
changeset
|
267 |
val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left |
10703 | 268 |
); |
269 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
270 |
(*int_mult_div_cancel_disj is for integer division (div). The version in |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
271 |
rat_arith.ML works for all fields, using real division (/).*) |
10703 | 272 |
structure DivideCancelFactor = ExtractCommonTermFun |
273 |
(open CancelFactorCommon |
|
20485 | 274 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
10703 | 275 |
val mk_bal = HOLogic.mk_binop "Divides.op div" |
276 |
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT |
|
277 |
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj |
|
278 |
); |
|
279 |
||
13462 | 280 |
val int_cancel_factor = |
20485 | 281 |
map Int_Numeral_Base_Simprocs.prep_simproc |
15271
3c32a26510c4
fixed some awkward problems with nat/int simprocs
paulson
parents:
14738
diff
changeset
|
282 |
[("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], |
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
283 |
K EqCancelFactor.proc), |
14390 | 284 |
("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"], |
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
285 |
K DivideCancelFactor.proc)]; |
10703 | 286 |
|
14390 | 287 |
(** Versions for all fields, including unordered ones (type complex).*) |
288 |
||
289 |
structure FieldEqCancelFactor = ExtractCommonTermFun |
|
290 |
(open CancelFactorCommon |
|
20485 | 291 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
14390 | 292 |
val mk_bal = HOLogic.mk_eq |
293 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT |
|
294 |
val simplify_meta_eq = cancel_simplify_meta_eq field_mult_cancel_left |
|
295 |
); |
|
296 |
||
297 |
structure FieldDivideCancelFactor = ExtractCommonTermFun |
|
298 |
(open CancelFactorCommon |
|
20485 | 299 |
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv |
14390 | 300 |
val mk_bal = HOLogic.mk_binop "HOL.divide" |
301 |
val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT |
|
302 |
val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if |
|
303 |
); |
|
304 |
||
15271
3c32a26510c4
fixed some awkward problems with nat/int simprocs
paulson
parents:
14738
diff
changeset
|
305 |
(*The number_ring class is necessary because the simprocs refer to the |
14426 | 306 |
binary number 1. FIXME: probably they could use 1 instead.*) |
14390 | 307 |
val field_cancel_factor = |
20485 | 308 |
map Int_Numeral_Base_Simprocs.prep_simproc |
14390 | 309 |
[("field_eq_cancel_factor", |
14426 | 310 |
["(l::'a::{field,number_ring}) * m = n", |
15271
3c32a26510c4
fixed some awkward problems with nat/int simprocs
paulson
parents:
14738
diff
changeset
|
311 |
"(l::'a::{field,number_ring}) = m * n"], |
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
312 |
K FieldEqCancelFactor.proc), |
14390 | 313 |
("field_divide_cancel_factor", |
14426 | 314 |
["((l::'a::{division_by_zero,field,number_ring}) * m) / n", |
315 |
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)"], |
|
20044
92cc2f4c7335
simprocs: no theory argument -- use simpset context instead;
wenzelm
parents:
19277
diff
changeset
|
316 |
K FieldDivideCancelFactor.proc)]; |
14390 | 317 |
|
10703 | 318 |
end; |
319 |
||
320 |
Addsimprocs int_cancel_factor; |
|
14390 | 321 |
Addsimprocs field_cancel_factor; |
10703 | 322 |
|
323 |
||
324 |
(*examples: |
|
325 |
print_depth 22; |
|
326 |
set timing; |
|
327 |
set trace_simp; |
|
13462 | 328 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
10703 | 329 |
|
330 |
test "x*k = k*(y::int)"; |
|
13462 | 331 |
test "k = k*(y::int)"; |
10703 | 332 |
test "a*(b*c) = (b::int)"; |
333 |
test "a*(b*c) = d*(b::int)*(x*a)"; |
|
334 |
||
335 |
test "(x*k) div (k*(y::int)) = (uu::int)"; |
|
13462 | 336 |
test "(k) div (k*(y::int)) = (uu::int)"; |
10703 | 337 |
test "(a*(b*c)) div ((b::int)) = (uu::int)"; |
338 |
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"; |
|
339 |
*) |
|
340 |
||
14390 | 341 |
(*And the same examples for fields such as rat or real: |
342 |
print_depth 22; |
|
343 |
set timing; |
|
344 |
set trace_simp; |
|
345 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
|
346 |
||
347 |
test "x*k = k*(y::rat)"; |
|
348 |
test "k = k*(y::rat)"; |
|
349 |
test "a*(b*c) = (b::rat)"; |
|
350 |
test "a*(b*c) = d*(b::rat)*(x*a)"; |
|
351 |
||
352 |
||
353 |
test "(x*k) / (k*(y::rat)) = (uu::rat)"; |
|
354 |
test "(k) / (k*(y::rat)) = (uu::rat)"; |
|
355 |
test "(a*(b*c)) / ((b::rat)) = (uu::rat)"; |
|
356 |
test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"; |
|
357 |
||
358 |
(*FIXME: what do we do about this?*) |
|
359 |
test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"; |
|
360 |
*) |