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