author | wenzelm |
Thu, 08 Aug 2002 23:50:23 +0200 | |
changeset 13485 | acf39e924091 |
parent 13462 | 56610e2ba220 |
child 14113 | 7b3513ba0f86 |
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 |
||
6 |
Factor cancellation simprocs for the integers. |
|
7 |
||
8 |
This file can't be combined with int_arith1,2 because it requires IntDiv.thy. |
|
9 |
*) |
|
10 |
||
11 |
(** Factor cancellation theorems for "int" **) |
|
12 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
13 |
Goal "!!k::int. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))"; |
10536 | 14 |
by (stac zmult_zle_cancel1 1); |
13462 | 15 |
by Auto_tac; |
10536 | 16 |
qed "int_mult_le_cancel1"; |
17 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
18 |
Goal "!!k::int. (k*m < k*n) = ((0 < k & m<n) | (k < 0 & n<m))"; |
10536 | 19 |
by (stac zmult_zless_cancel1 1); |
13462 | 20 |
by Auto_tac; |
10536 | 21 |
qed "int_mult_less_cancel1"; |
22 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
23 |
Goal "!!k::int. (k*m = k*n) = (k = 0 | m=n)"; |
13462 | 24 |
by Auto_tac; |
10536 | 25 |
qed "int_mult_eq_cancel1"; |
26 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
27 |
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)"; |
13462 | 28 |
by (stac zdiv_zmult_zmult1 1); |
29 |
by Auto_tac; |
|
10536 | 30 |
qed "int_mult_div_cancel1"; |
31 |
||
10703 | 32 |
(*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
|
33 |
Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"; |
13462 | 34 |
by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1); |
10703 | 35 |
qed "int_mult_div_cancel_disj"; |
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 |
|
10536 | 45 |
val trans_tac = trans_tac |
13462 | 46 |
val norm_tac = |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11868
diff
changeset
|
47 |
ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s)) |
10713
69c9fc1d11f2
simproc bug fix: negative literals and large terms
paulson
parents:
10703
diff
changeset
|
48 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps)) |
69c9fc1d11f2
simproc bug fix: negative literals and large terms
paulson
parents:
10703
diff
changeset
|
49 |
THEN ALLGOALS |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11868
diff
changeset
|
50 |
(simp_tac (HOL_ss addsimps zmult_ac)) |
13462 | 51 |
val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps)) |
10536 | 52 |
val simplify_meta_eq = simplify_meta_eq mult_1s |
53 |
end |
|
54 |
||
55 |
structure DivCancelNumeralFactor = CancelNumeralFactorFun |
|
56 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
57 |
val prove_conv = Bin_Simprocs.prove_conv |
10536 | 58 |
val mk_bal = HOLogic.mk_binop "Divides.op div" |
59 |
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT |
|
60 |
val cancel = int_mult_div_cancel1 RS trans |
|
61 |
val neg_exchanges = false |
|
62 |
) |
|
63 |
||
64 |
structure EqCancelNumeralFactor = CancelNumeralFactorFun |
|
65 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
66 |
val prove_conv = Bin_Simprocs.prove_conv |
10536 | 67 |
val mk_bal = HOLogic.mk_eq |
68 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT |
|
69 |
val cancel = int_mult_eq_cancel1 RS trans |
|
70 |
val neg_exchanges = false |
|
71 |
) |
|
72 |
||
73 |
structure LessCancelNumeralFactor = CancelNumeralFactorFun |
|
74 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
75 |
val prove_conv = Bin_Simprocs.prove_conv |
10536 | 76 |
val mk_bal = HOLogic.mk_binrel "op <" |
77 |
val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT |
|
78 |
val cancel = int_mult_less_cancel1 RS trans |
|
79 |
val neg_exchanges = true |
|
80 |
) |
|
81 |
||
82 |
structure LeCancelNumeralFactor = CancelNumeralFactorFun |
|
83 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
84 |
val prove_conv = Bin_Simprocs.prove_conv |
10536 | 85 |
val mk_bal = HOLogic.mk_binrel "op <=" |
86 |
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT |
|
87 |
val cancel = int_mult_le_cancel1 RS trans |
|
88 |
val neg_exchanges = true |
|
89 |
) |
|
90 |
||
13462 | 91 |
val int_cancel_numeral_factors = |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
92 |
map Bin_Simprocs.prep_simproc |
13462 | 93 |
[("inteq_cancel_numeral_factors", ["(l::int) * m = n", "(l::int) = m * n"], |
10536 | 94 |
EqCancelNumeralFactor.proc), |
13462 | 95 |
("intless_cancel_numeral_factors", ["(l::int) * m < n", "(l::int) < m * n"], |
10536 | 96 |
LessCancelNumeralFactor.proc), |
13462 | 97 |
("intle_cancel_numeral_factors", ["(l::int) * m <= n", "(l::int) <= m * n"], |
10536 | 98 |
LeCancelNumeralFactor.proc), |
13462 | 99 |
("intdiv_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"], |
10536 | 100 |
DivCancelNumeralFactor.proc)]; |
101 |
||
102 |
end; |
|
103 |
||
104 |
Addsimprocs int_cancel_numeral_factors; |
|
105 |
||
106 |
||
107 |
(*examples: |
|
108 |
print_depth 22; |
|
109 |
set timing; |
|
110 |
set trace_simp; |
|
13462 | 111 |
fun test s = (Goal s; by (Simp_tac 1)); |
10536 | 112 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
113 |
test "9*x = 12 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
114 |
test "(9*x) div (12 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
115 |
test "9*x < 12 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
116 |
test "9*x <= 12 * (y::int)"; |
10536 | 117 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
118 |
test "-99*x = 132 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
119 |
test "(-99*x) div (132 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
120 |
test "-99*x < 132 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
121 |
test "-99*x <= 132 * (y::int)"; |
10536 | 122 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
123 |
test "999*x = -396 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
124 |
test "(999*x) div (-396 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
125 |
test "999*x < -396 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
126 |
test "999*x <= -396 * (y::int)"; |
10536 | 127 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
128 |
test "-99*x = -81 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
129 |
test "(-99*x) div (-81 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
130 |
test "-99*x <= -81 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
131 |
test "-99*x < -81 * (y::int)"; |
10536 | 132 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
133 |
test "-2 * x = -1 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
134 |
test "-2 * x = -(y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
135 |
test "(-2 * x) div (-1 * (y::int)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
136 |
test "-2 * x < -(y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
137 |
test "-2 * x <= -1 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
138 |
test "-x < -23 * (y::int)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
139 |
test "-x <= -23 * (y::int)"; |
10536 | 140 |
*) |
141 |
||
10703 | 142 |
|
143 |
(** Declarations for ExtractCommonTerm **) |
|
144 |
||
145 |
local |
|
146 |
open Int_Numeral_Simprocs |
|
147 |
in |
|
148 |
||
149 |
||
150 |
(*this version ALWAYS includes a trailing one*) |
|
151 |
fun long_mk_prod [] = one |
|
152 |
| long_mk_prod (t :: ts) = mk_times (t, mk_prod ts); |
|
153 |
||
154 |
(*Find first term that matches u*) |
|
13462 | 155 |
fun find_first past u [] = raise TERM("find_first", []) |
10703 | 156 |
| find_first past u (t::terms) = |
13462 | 157 |
if u aconv t then (rev past @ terms) |
10703 | 158 |
else find_first (t::past) u terms |
13462 | 159 |
handle TERM _ => find_first (t::past) u terms; |
10703 | 160 |
|
161 |
(*Final simplification: cancel + and * *) |
|
13462 | 162 |
fun cancel_simplify_meta_eq cancel_th th = |
163 |
Int_Numeral_Simprocs.simplify_meta_eq |
|
164 |
[zmult_1, zmult_1_right] |
|
10703 | 165 |
(([th, cancel_th]) MRS trans); |
166 |
||
167 |
structure CancelFactorCommon = |
|
168 |
struct |
|
13462 | 169 |
val mk_sum = long_mk_prod |
170 |
val dest_sum = dest_prod |
|
171 |
val mk_coeff = mk_coeff |
|
172 |
val dest_coeff = dest_coeff |
|
173 |
val find_first = find_first [] |
|
10703 | 174 |
val trans_tac = trans_tac |
175 |
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac)) |
|
176 |
end; |
|
177 |
||
178 |
structure EqCancelFactor = ExtractCommonTermFun |
|
179 |
(open CancelFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
180 |
val prove_conv = Bin_Simprocs.prove_conv |
10703 | 181 |
val mk_bal = HOLogic.mk_eq |
182 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT |
|
183 |
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_eq_cancel1 |
|
184 |
); |
|
185 |
||
186 |
structure DivideCancelFactor = ExtractCommonTermFun |
|
187 |
(open CancelFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
188 |
val prove_conv = Bin_Simprocs.prove_conv |
10703 | 189 |
val mk_bal = HOLogic.mk_binop "Divides.op div" |
190 |
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT |
|
191 |
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj |
|
192 |
); |
|
193 |
||
13462 | 194 |
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
|
195 |
map Bin_Simprocs.prep_simproc |
13462 | 196 |
[("int_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc), |
197 |
("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"], |
|
10703 | 198 |
DivideCancelFactor.proc)]; |
199 |
||
200 |
end; |
|
201 |
||
202 |
Addsimprocs int_cancel_factor; |
|
203 |
||
204 |
||
205 |
(*examples: |
|
206 |
print_depth 22; |
|
207 |
set timing; |
|
208 |
set trace_simp; |
|
13462 | 209 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
10703 | 210 |
|
211 |
test "x*k = k*(y::int)"; |
|
13462 | 212 |
test "k = k*(y::int)"; |
10703 | 213 |
test "a*(b*c) = (b::int)"; |
214 |
test "a*(b*c) = d*(b::int)*(x*a)"; |
|
215 |
||
216 |
test "(x*k) div (k*(y::int)) = (uu::int)"; |
|
13462 | 217 |
test "(k) div (k*(y::int)) = (uu::int)"; |
10703 | 218 |
test "(a*(b*c)) div ((b::int)) = (uu::int)"; |
219 |
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"; |
|
220 |
*) |
|
221 |