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