author | haftmann |
Fri, 08 May 2009 08:01:09 +0200 | |
changeset 31067 | fd7ec31f850c |
parent 30931 | 86ca651da03e |
permissions | -rw-r--r-- |
23164 | 1 |
(* Title: HOL/int_factor_simprocs.ML |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 2000 University of Cambridge |
|
4 |
||
5 |
Factor cancellation simprocs for the integers (and for fields). |
|
6 |
||
7 |
This file can't be combined with int_arith1 because it requires IntDiv.thy. |
|
8 |
*) |
|
9 |
||
10 |
||
11 |
(*To quote from Provers/Arith/cancel_numeral_factor.ML: |
|
12 |
||
13 |
Cancels common coefficients in balanced expressions: |
|
14 |
||
15 |
u*#m ~~ u'*#m' == #n*u ~~ #n'*u' |
|
16 |
||
17 |
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) |
|
18 |
and d = gcd(m,m') and n=m/d and n'=m'/d. |
|
19 |
*) |
|
20 |
||
29038 | 21 |
val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}]; |
23164 | 22 |
|
23 |
local |
|
24 |
open Int_Numeral_Simprocs |
|
25 |
in |
|
26 |
||
27 |
structure CancelNumeralFactorCommon = |
|
28 |
struct |
|
29 |
val mk_coeff = mk_coeff |
|
30 |
val dest_coeff = dest_coeff 1 |
|
30518 | 31 |
val trans_tac = K Arith_Data.trans_tac |
23164 | 32 |
|
33 |
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s |
|
34 |
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps |
|
23881 | 35 |
val norm_ss3 = HOL_ss addsimps @{thms mult_ac} |
23164 | 36 |
fun norm_tac ss = |
37 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
38 |
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
39 |
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
40 |
||
41 |
val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps |
|
42 |
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
30518 | 43 |
val simplify_meta_eq = Arith_Data.simplify_meta_eq |
23164 | 44 |
[@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left}, |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25481
diff
changeset
|
45 |
@{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}]; |
23164 | 46 |
end |
47 |
||
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
48 |
(*Version for semiring_div*) |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
49 |
structure DivCancelNumeralFactor = CancelNumeralFactorFun |
23164 | 50 |
(open CancelNumeralFactorCommon |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
51 |
val prove_conv = Arith_Data.prove_conv |
23164 | 52 |
val mk_bal = HOLogic.mk_binop @{const_name Divides.div} |
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
53 |
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
54 |
val cancel = @{thm div_mult_mult1} RS trans |
23164 | 55 |
val neg_exchanges = false |
56 |
) |
|
57 |
||
58 |
(*Version for fields*) |
|
59 |
structure DivideCancelNumeralFactor = CancelNumeralFactorFun |
|
60 |
(open CancelNumeralFactorCommon |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
61 |
val prove_conv = Arith_Data.prove_conv |
23164 | 62 |
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} |
63 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT |
|
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23401
diff
changeset
|
64 |
val cancel = @{thm mult_divide_mult_cancel_left} RS trans |
23164 | 65 |
val neg_exchanges = false |
66 |
) |
|
67 |
||
68 |
structure EqCancelNumeralFactor = CancelNumeralFactorFun |
|
69 |
(open CancelNumeralFactorCommon |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
70 |
val prove_conv = Arith_Data.prove_conv |
23164 | 71 |
val mk_bal = HOLogic.mk_eq |
72 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT |
|
73 |
val cancel = @{thm mult_cancel_left} RS trans |
|
74 |
val neg_exchanges = false |
|
75 |
) |
|
76 |
||
77 |
structure LessCancelNumeralFactor = CancelNumeralFactorFun |
|
78 |
(open CancelNumeralFactorCommon |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
79 |
val prove_conv = Arith_Data.prove_conv |
23881 | 80 |
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} |
81 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT |
|
23164 | 82 |
val cancel = @{thm mult_less_cancel_left} RS trans |
83 |
val neg_exchanges = true |
|
84 |
) |
|
85 |
||
86 |
structure LeCancelNumeralFactor = CancelNumeralFactorFun |
|
87 |
(open CancelNumeralFactorCommon |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
88 |
val prove_conv = Arith_Data.prove_conv |
23881 | 89 |
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} |
90 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT |
|
23164 | 91 |
val cancel = @{thm mult_le_cancel_left} RS trans |
92 |
val neg_exchanges = true |
|
93 |
) |
|
94 |
||
95 |
val cancel_numeral_factors = |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
96 |
map Arith_Data.prep_simproc |
23164 | 97 |
[("ring_eq_cancel_numeral_factor", |
98 |
["(l::'a::{idom,number_ring}) * m = n", |
|
99 |
"(l::'a::{idom,number_ring}) = m * n"], |
|
100 |
K EqCancelNumeralFactor.proc), |
|
101 |
("ring_less_cancel_numeral_factor", |
|
102 |
["(l::'a::{ordered_idom,number_ring}) * m < n", |
|
103 |
"(l::'a::{ordered_idom,number_ring}) < m * n"], |
|
104 |
K LessCancelNumeralFactor.proc), |
|
105 |
("ring_le_cancel_numeral_factor", |
|
106 |
["(l::'a::{ordered_idom,number_ring}) * m <= n", |
|
107 |
"(l::'a::{ordered_idom,number_ring}) <= m * n"], |
|
108 |
K LeCancelNumeralFactor.proc), |
|
109 |
("int_div_cancel_numeral_factors", |
|
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
110 |
["((l::'a::{semiring_div,number_ring}) * m) div n", |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
111 |
"(l::'a::{semiring_div,number_ring}) div (m * n)"], |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
112 |
K DivCancelNumeralFactor.proc), |
23164 | 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 = |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
121 |
map Arith_Data.prep_simproc |
23164 | 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 **) |
|
30518 | 218 |
val simplify_one = Arith_Data.simplify_meta_eq |
30031 | 219 |
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; |
23164 | 220 |
|
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
221 |
fun cancel_simplify_meta_eq ss cancel_th th = |
23164 | 222 |
simplify_one ss (([th, cancel_th]) MRS trans); |
223 |
||
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
224 |
local |
31067 | 225 |
val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop) |
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
226 |
fun Eq_True_elim Eq = |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
227 |
Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
228 |
in |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
229 |
fun sign_conv pos_th neg_th ss t = |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
230 |
let val T = fastype_of t; |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
231 |
val zero = Const(@{const_name HOL.zero}, T); |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
232 |
val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT); |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
233 |
val pos = less $ zero $ t and neg = less $ t $ zero |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
234 |
fun prove p = |
30685 | 235 |
Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p) |
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
236 |
handle THM _ => NONE |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
237 |
in case prove pos of |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
238 |
SOME th => SOME(th RS pos_th) |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
239 |
| NONE => (case prove neg of |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
240 |
SOME th => SOME(th RS neg_th) |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
241 |
| NONE => NONE) |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
242 |
end; |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
243 |
end |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
244 |
|
23164 | 245 |
structure CancelFactorCommon = |
246 |
struct |
|
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_t [] |
|
30518 | 252 |
val trans_tac = K Arith_Data.trans_tac |
23881 | 253 |
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} |
23164 | 254 |
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) |
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
255 |
val simplify_meta_eq = cancel_simplify_meta_eq |
23164 | 256 |
end; |
257 |
||
258 |
(*mult_cancel_left requires a ring with no zero divisors.*) |
|
259 |
structure EqCancelFactor = ExtractCommonTermFun |
|
260 |
(open CancelFactorCommon |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
261 |
val prove_conv = Arith_Data.prove_conv |
23164 | 262 |
val mk_bal = HOLogic.mk_eq |
263 |
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT |
|
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
264 |
val simp_conv = K (K (SOME @{thm mult_cancel_left})) |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
265 |
); |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
266 |
|
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
267 |
(*for ordered rings*) |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
268 |
structure LeCancelFactor = ExtractCommonTermFun |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
269 |
(open CancelFactorCommon |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
270 |
val prove_conv = Arith_Data.prove_conv |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
271 |
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
272 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
273 |
val simp_conv = sign_conv |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
274 |
@{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
275 |
); |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
276 |
|
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
277 |
(*for ordered rings*) |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
278 |
structure LessCancelFactor = ExtractCommonTermFun |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
279 |
(open CancelFactorCommon |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
280 |
val prove_conv = Arith_Data.prove_conv |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
281 |
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
282 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
283 |
val simp_conv = sign_conv |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
284 |
@{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} |
23164 | 285 |
); |
286 |
||
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
287 |
(*for semirings with division*) |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
288 |
structure DivCancelFactor = ExtractCommonTermFun |
23164 | 289 |
(open CancelFactorCommon |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
290 |
val prove_conv = Arith_Data.prove_conv |
23164 | 291 |
val mk_bal = HOLogic.mk_binop @{const_name Divides.div} |
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
292 |
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
293 |
val simp_conv = K (K (SOME @{thm div_mult_mult1_if})) |
23164 | 294 |
); |
295 |
||
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
296 |
structure ModCancelFactor = ExtractCommonTermFun |
24395 | 297 |
(open CancelFactorCommon |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
298 |
val prove_conv = Arith_Data.prove_conv |
24395 | 299 |
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} |
31067 | 300 |
val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT |
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
301 |
val simp_conv = K (K (SOME @{thm mod_mult_mult1})) |
24395 | 302 |
); |
303 |
||
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
304 |
(*for idoms*) |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
305 |
structure DvdCancelFactor = ExtractCommonTermFun |
23969 | 306 |
(open CancelFactorCommon |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
307 |
val prove_conv = Arith_Data.prove_conv |
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26086
diff
changeset
|
308 |
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} |
29981
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29038
diff
changeset
|
309 |
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT |
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
310 |
val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left})) |
23969 | 311 |
); |
312 |
||
23164 | 313 |
(*Version for all fields, including unordered ones (type complex).*) |
314 |
structure DivideCancelFactor = ExtractCommonTermFun |
|
315 |
(open CancelFactorCommon |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
316 |
val prove_conv = Arith_Data.prove_conv |
23164 | 317 |
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} |
318 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT |
|
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
319 |
val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if})) |
23164 | 320 |
); |
321 |
||
322 |
val cancel_factors = |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset
|
323 |
map Arith_Data.prep_simproc |
23164 | 324 |
[("ring_eq_cancel_factor", |
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
325 |
["(l::'a::idom) * m = n", |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
326 |
"(l::'a::idom) = m * n"], |
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
327 |
K EqCancelFactor.proc), |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
328 |
("ordered_ring_le_cancel_factor", |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
329 |
["(l::'a::ordered_ring) * m <= n", |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
330 |
"(l::'a::ordered_ring) <= m * n"], |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
331 |
K LeCancelFactor.proc), |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
332 |
("ordered_ring_less_cancel_factor", |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
333 |
["(l::'a::ordered_ring) * m < n", |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
334 |
"(l::'a::ordered_ring) < m * n"], |
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset
|
335 |
K LessCancelFactor.proc), |
23164 | 336 |
("int_div_cancel_factor", |
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
337 |
["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"], |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
338 |
K DivCancelFactor.proc), |
24395 | 339 |
("int_mod_cancel_factor", |
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
340 |
["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"], |
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
341 |
K ModCancelFactor.proc), |
29981
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29038
diff
changeset
|
342 |
("dvd_cancel_factor", |
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29038
diff
changeset
|
343 |
["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"], |
30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset
|
344 |
K DvdCancelFactor.proc), |
23164 | 345 |
("divide_cancel_factor", |
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23398
diff
changeset
|
346 |
["((l::'a::{division_by_zero,field}) * m) / n", |
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23398
diff
changeset
|
347 |
"(l::'a::{division_by_zero,field}) / (m * n)"], |
23164 | 348 |
K DivideCancelFactor.proc)]; |
349 |
||
350 |
end; |
|
351 |
||
352 |
Addsimprocs cancel_factors; |
|
353 |
||
354 |
||
355 |
(*examples: |
|
356 |
print_depth 22; |
|
357 |
set timing; |
|
358 |
set trace_simp; |
|
359 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
|
360 |
||
361 |
test "x*k = k*(y::int)"; |
|
362 |
test "k = k*(y::int)"; |
|
363 |
test "a*(b*c) = (b::int)"; |
|
364 |
test "a*(b*c) = d*(b::int)*(x*a)"; |
|
365 |
||
366 |
test "(x*k) div (k*(y::int)) = (uu::int)"; |
|
367 |
test "(k) div (k*(y::int)) = (uu::int)"; |
|
368 |
test "(a*(b*c)) div ((b::int)) = (uu::int)"; |
|
369 |
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"; |
|
370 |
*) |
|
371 |
||
372 |
(*And the same examples for fields such as rat or real: |
|
373 |
print_depth 22; |
|
374 |
set timing; |
|
375 |
set trace_simp; |
|
376 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
|
377 |
||
378 |
test "x*k = k*(y::rat)"; |
|
379 |
test "k = k*(y::rat)"; |
|
380 |
test "a*(b*c) = (b::rat)"; |
|
381 |
test "a*(b*c) = d*(b::rat)*(x*a)"; |
|
382 |
||
383 |
||
384 |
test "(x*k) / (k*(y::rat)) = (uu::rat)"; |
|
385 |
test "(k) / (k*(y::rat)) = (uu::rat)"; |
|
386 |
test "(a*(b*c)) / ((b::rat)) = (uu::rat)"; |
|
387 |
test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"; |
|
388 |
||
389 |
(*FIXME: what do we do about this?*) |
|
390 |
test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"; |
|
391 |
*) |