author | krauss |
Mon, 11 Feb 2008 15:40:21 +0100 | |
changeset 26056 | 6a0801279f4c |
parent 24893 | b8ef7afe3a6b |
child 26059 | b67a225b50fd |
permissions | -rw-r--r-- |
23146 | 1 |
(* Title: ZF/int_arith.ML |
2 |
ID: $Id$ |
|
3 |
Author: Larry Paulson |
|
4 |
Copyright 2000 University of Cambridge |
|
5 |
||
6 |
Simprocs for linear arithmetic. |
|
7 |
*) |
|
8 |
||
9 |
||
10 |
(** To simplify inequalities involving integer negation and literals, |
|
11 |
such as -x = #3 |
|
12 |
**) |
|
13 |
||
24893 | 14 |
Addsimps [inst "y" "integ_of(?w)" @{thm zminus_equation}, |
15 |
inst "x" "integ_of(?w)" @{thm equation_zminus}]; |
|
23146 | 16 |
|
24893 | 17 |
AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zless}, |
18 |
inst "x" "integ_of(?w)" @{thm zless_zminus}]; |
|
23146 | 19 |
|
24893 | 20 |
AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zle}, |
21 |
inst "x" "integ_of(?w)" @{thm zle_zminus}]; |
|
23146 | 22 |
|
24893 | 23 |
Addsimps [inst "s" "integ_of(?w)" @{thm Let_def}]; |
23146 | 24 |
|
25 |
(*** Simprocs for numeric literals ***) |
|
26 |
||
27 |
(** Combining of literal coefficients in sums of products **) |
|
28 |
||
29 |
Goal "(x $< y) <-> (x$-y $< #0)"; |
|
24893 | 30 |
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); |
23146 | 31 |
qed "zless_iff_zdiff_zless_0"; |
32 |
||
33 |
Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)"; |
|
24893 | 34 |
by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); |
23146 | 35 |
qed "eq_iff_zdiff_eq_0"; |
36 |
||
37 |
Goal "(x $<= y) <-> (x$-y $<= #0)"; |
|
24893 | 38 |
by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); |
23146 | 39 |
qed "zle_iff_zdiff_zle_0"; |
40 |
||
41 |
||
42 |
(** For combine_numerals **) |
|
43 |
||
44 |
Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"; |
|
24893 | 45 |
by (simp_tac (simpset() addsimps [@{thm zadd_zmult_distrib}]@ @{thms zadd_ac}) 1); |
23146 | 46 |
qed "left_zadd_zmult_distrib"; |
47 |
||
48 |
||
49 |
(** For cancel_numerals **) |
|
50 |
||
51 |
val rel_iff_rel_0_rls = map (inst "y" "?u$+?v") |
|
52 |
[zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, |
|
53 |
zle_iff_zdiff_zle_0] @ |
|
54 |
map (inst "y" "n") |
|
55 |
[zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, |
|
56 |
zle_iff_zdiff_zle_0]; |
|
57 |
||
58 |
Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"; |
|
24893 | 59 |
by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1); |
60 |
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); |
|
61 |
by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1); |
|
23146 | 62 |
qed "eq_add_iff1"; |
63 |
||
64 |
Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)"; |
|
24893 | 65 |
by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1); |
66 |
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); |
|
67 |
by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1); |
|
23146 | 68 |
qed "eq_add_iff2"; |
69 |
||
70 |
Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)"; |
|
24893 | 71 |
by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@ |
72 |
@{thms zadd_ac} @ rel_iff_rel_0_rls) 1); |
|
23146 | 73 |
qed "less_add_iff1"; |
74 |
||
75 |
Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)"; |
|
24893 | 76 |
by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@ |
77 |
@{thms zadd_ac} @ rel_iff_rel_0_rls) 1); |
|
23146 | 78 |
qed "less_add_iff2"; |
79 |
||
80 |
Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)"; |
|
24893 | 81 |
by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1); |
82 |
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); |
|
83 |
by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1); |
|
23146 | 84 |
qed "le_add_iff1"; |
85 |
||
86 |
Goal "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)"; |
|
24893 | 87 |
by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1); |
88 |
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); |
|
89 |
by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1); |
|
23146 | 90 |
qed "le_add_iff2"; |
91 |
||
92 |
||
93 |
structure Int_Numeral_Simprocs = |
|
94 |
struct |
|
95 |
||
96 |
(*Utilities*) |
|
97 |
||
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
98 |
val integ_of_const = Const (@{const_name "Bin.integ_of"}, iT --> iT); |
23146 | 99 |
|
100 |
fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n; |
|
101 |
||
102 |
(*Decodes a binary INTEGER*) |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
103 |
fun dest_numeral (Const(@{const_name "Bin.integ_of"}, _) $ w) = |
23146 | 104 |
(NumeralSyntax.dest_bin w |
105 |
handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w])) |
|
106 |
| dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]); |
|
107 |
||
108 |
fun find_first_numeral past (t::terms) = |
|
109 |
((dest_numeral t, rev past @ terms) |
|
110 |
handle TERM _ => find_first_numeral (t::past) terms) |
|
111 |
| find_first_numeral past [] = raise TERM("find_first_numeral", []); |
|
112 |
||
113 |
val zero = mk_numeral 0; |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
114 |
val mk_plus = FOLogic.mk_binop @{const_name "Int_ZF.zadd"}; |
23146 | 115 |
|
116 |
val iT = Ind_Syntax.iT; |
|
117 |
||
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
118 |
val zminus_const = Const (@{const_name "Int_ZF.zminus"}, iT --> iT); |
23146 | 119 |
|
120 |
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) |
|
121 |
fun mk_sum [] = zero |
|
122 |
| mk_sum [t,u] = mk_plus (t, u) |
|
123 |
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
124 |
||
125 |
(*this version ALWAYS includes a trailing zero*) |
|
126 |
fun long_mk_sum [] = zero |
|
127 |
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
128 |
||
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
129 |
val dest_plus = FOLogic.dest_bin @{const_name "Int_ZF.zadd"} iT; |
23146 | 130 |
|
131 |
(*decompose additions AND subtractions as a sum*) |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
132 |
fun dest_summing (pos, Const (@{const_name "Int_ZF.zadd"}, _) $ t $ u, ts) = |
23146 | 133 |
dest_summing (pos, t, dest_summing (pos, u, ts)) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
134 |
| dest_summing (pos, Const (@{const_name "Int_ZF.zdiff"}, _) $ t $ u, ts) = |
23146 | 135 |
dest_summing (pos, t, dest_summing (not pos, u, ts)) |
136 |
| dest_summing (pos, t, ts) = |
|
137 |
if pos then t::ts else zminus_const$t :: ts; |
|
138 |
||
139 |
fun dest_sum t = dest_summing (true, t, []); |
|
140 |
||
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
141 |
val mk_diff = FOLogic.mk_binop @{const_name "Int_ZF.zdiff"}; |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
142 |
val dest_diff = FOLogic.dest_bin @{const_name "Int_ZF.zdiff"} iT; |
23146 | 143 |
|
144 |
val one = mk_numeral 1; |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
145 |
val mk_times = FOLogic.mk_binop @{const_name "Int_ZF.zmult"}; |
23146 | 146 |
|
147 |
fun mk_prod [] = one |
|
148 |
| mk_prod [t] = t |
|
149 |
| mk_prod (t :: ts) = if t = one then mk_prod ts |
|
150 |
else mk_times (t, mk_prod ts); |
|
151 |
||
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
152 |
val dest_times = FOLogic.dest_bin @{const_name "Int_ZF.zmult"} iT; |
23146 | 153 |
|
154 |
fun dest_prod t = |
|
155 |
let val (t,u) = dest_times t |
|
156 |
in dest_prod t @ dest_prod u end |
|
157 |
handle TERM _ => [t]; |
|
158 |
||
159 |
(*DON'T do the obvious simplifications; that would create special cases*) |
|
160 |
fun mk_coeff (k, t) = mk_times (mk_numeral k, t); |
|
161 |
||
162 |
(*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
163 |
fun dest_coeff sign (Const (@{const_name "Int_ZF.zminus"}, _) $ t) = dest_coeff (~sign) t |
23146 | 164 |
| dest_coeff sign t = |
165 |
let val ts = sort Term.term_ord (dest_prod t) |
|
166 |
val (n, ts') = find_first_numeral [] ts |
|
167 |
handle TERM _ => (1, ts) |
|
168 |
in (sign*n, mk_prod ts') end; |
|
169 |
||
170 |
(*Find first coefficient-term THAT MATCHES u*) |
|
171 |
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
172 |
| find_first_coeff past u (t::terms) = |
|
173 |
let val (n,u') = dest_coeff 1 t |
|
174 |
in if u aconv u' then (n, rev past @ terms) |
|
175 |
else find_first_coeff (t::past) u terms |
|
176 |
end |
|
177 |
handle TERM _ => find_first_coeff (t::past) u terms; |
|
178 |
||
179 |
||
180 |
(*Simplify #1*n and n*#1 to n*) |
|
24893 | 181 |
val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}]; |
23146 | 182 |
|
24893 | 183 |
val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify}, |
184 |
@{thm zmult_minus1}, @{thm zmult_minus1_right}]; |
|
23146 | 185 |
|
24893 | 186 |
val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int}, |
187 |
@{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @ |
|
188 |
@{thms bin.intros}; |
|
189 |
val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2}, |
|
190 |
@{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2}, |
|
191 |
@{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}]; |
|
23146 | 192 |
|
193 |
(*To perform binary arithmetic*) |
|
24893 | 194 |
val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps}; |
23146 | 195 |
|
196 |
(*To evaluate binary negations of coefficients*) |
|
24893 | 197 |
val zminus_simps = @{thms NCons_simps} @ |
198 |
[@{thm integ_of_minus} RS sym, |
|
199 |
@{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min}, |
|
200 |
@{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}]; |
|
23146 | 201 |
|
202 |
(*To let us treat subtraction as addition*) |
|
24893 | 203 |
val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}]; |
23146 | 204 |
|
205 |
(*push the unary minus down: - x * y = x * - y *) |
|
206 |
val int_minus_mult_eq_1_to_2 = |
|
24893 | 207 |
[@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> standard; |
23146 | 208 |
|
209 |
(*to extract again any uncancelled minuses*) |
|
210 |
val int_minus_from_mult_simps = |
|
24893 | 211 |
[@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}]; |
23146 | 212 |
|
213 |
(*combine unary minus with numeric literals, however nested within a product*) |
|
214 |
val int_mult_minus_simps = |
|
24893 | 215 |
[@{thm zmult_assoc}, @{thm zmult_zminus} RS sym, int_minus_mult_eq_1_to_2]; |
23146 | 216 |
|
217 |
fun prep_simproc (name, pats, proc) = |
|
218 |
Simplifier.simproc (the_context ()) name pats proc; |
|
219 |
||
220 |
structure CancelNumeralsCommon = |
|
221 |
struct |
|
222 |
val mk_sum = (fn T:typ => mk_sum) |
|
223 |
val dest_sum = dest_sum |
|
224 |
val mk_coeff = mk_coeff |
|
225 |
val dest_coeff = dest_coeff 1 |
|
226 |
val find_first_coeff = find_first_coeff [] |
|
227 |
fun trans_tac _ = ArithData.gen_trans_tac iff_trans |
|
228 |
||
24893 | 229 |
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} |
23146 | 230 |
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys |
24893 | 231 |
val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys |
23146 | 232 |
fun norm_tac ss = |
233 |
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
234 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
235 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
236 |
||
237 |
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys |
|
238 |
fun numeral_simp_tac ss = |
|
239 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
240 |
THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset))) |
|
241 |
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) |
|
242 |
end; |
|
243 |
||
244 |
||
245 |
structure EqCancelNumerals = CancelNumeralsFun |
|
246 |
(open CancelNumeralsCommon |
|
247 |
val prove_conv = ArithData.prove_conv "inteq_cancel_numerals" |
|
248 |
val mk_bal = FOLogic.mk_eq |
|
249 |
val dest_bal = FOLogic.dest_eq |
|
250 |
val bal_add1 = eq_add_iff1 RS iff_trans |
|
251 |
val bal_add2 = eq_add_iff2 RS iff_trans |
|
252 |
); |
|
253 |
||
254 |
structure LessCancelNumerals = CancelNumeralsFun |
|
255 |
(open CancelNumeralsCommon |
|
256 |
val prove_conv = ArithData.prove_conv "intless_cancel_numerals" |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
257 |
val mk_bal = FOLogic.mk_binrel @{const_name "Int_ZF.zless"} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
258 |
val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zless"} iT |
23146 | 259 |
val bal_add1 = less_add_iff1 RS iff_trans |
260 |
val bal_add2 = less_add_iff2 RS iff_trans |
|
261 |
); |
|
262 |
||
263 |
structure LeCancelNumerals = CancelNumeralsFun |
|
264 |
(open CancelNumeralsCommon |
|
265 |
val prove_conv = ArithData.prove_conv "intle_cancel_numerals" |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
266 |
val mk_bal = FOLogic.mk_binrel @{const_name "Int_ZF.zle"} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset
|
267 |
val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zle"} iT |
23146 | 268 |
val bal_add1 = le_add_iff1 RS iff_trans |
269 |
val bal_add2 = le_add_iff2 RS iff_trans |
|
270 |
); |
|
271 |
||
272 |
val cancel_numerals = |
|
273 |
map prep_simproc |
|
274 |
[("inteq_cancel_numerals", |
|
275 |
["l $+ m = n", "l = m $+ n", |
|
276 |
"l $- m = n", "l = m $- n", |
|
277 |
"l $* m = n", "l = m $* n"], |
|
278 |
K EqCancelNumerals.proc), |
|
279 |
("intless_cancel_numerals", |
|
280 |
["l $+ m $< n", "l $< m $+ n", |
|
281 |
"l $- m $< n", "l $< m $- n", |
|
282 |
"l $* m $< n", "l $< m $* n"], |
|
283 |
K LessCancelNumerals.proc), |
|
284 |
("intle_cancel_numerals", |
|
285 |
["l $+ m $<= n", "l $<= m $+ n", |
|
286 |
"l $- m $<= n", "l $<= m $- n", |
|
287 |
"l $* m $<= n", "l $<= m $* n"], |
|
288 |
K LeCancelNumerals.proc)]; |
|
289 |
||
290 |
||
291 |
(*version without the hyps argument*) |
|
292 |
fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg []; |
|
293 |
||
294 |
structure CombineNumeralsData = |
|
295 |
struct |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
296 |
type coeff = int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
297 |
val iszero = (fn x => x = 0) |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
298 |
val add = op + |
23146 | 299 |
val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *) |
300 |
val dest_sum = dest_sum |
|
301 |
val mk_coeff = mk_coeff |
|
302 |
val dest_coeff = dest_coeff 1 |
|
303 |
val left_distrib = left_zadd_zmult_distrib RS trans |
|
304 |
val prove_conv = prove_conv_nohyps "int_combine_numerals" |
|
305 |
fun trans_tac _ = ArithData.gen_trans_tac trans |
|
306 |
||
24893 | 307 |
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys |
23146 | 308 |
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys |
24893 | 309 |
val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys |
23146 | 310 |
fun norm_tac ss = |
311 |
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
312 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
313 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
314 |
||
315 |
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys |
|
316 |
fun numeral_simp_tac ss = |
|
317 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
318 |
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) |
|
319 |
end; |
|
320 |
||
321 |
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); |
|
322 |
||
323 |
val combine_numerals = |
|
324 |
prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc); |
|
325 |
||
326 |
||
327 |
||
328 |
(** Constant folding for integer multiplication **) |
|
329 |
||
330 |
(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as |
|
331 |
the "sum" of #3, x, #4; the literals are then multiplied*) |
|
332 |
||
333 |
||
334 |
structure CombineNumeralsProdData = |
|
335 |
struct |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
336 |
type coeff = int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
337 |
val iszero = (fn x => x = 0) |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
338 |
val add = op * |
23146 | 339 |
val mk_sum = (fn T:typ => mk_prod) |
340 |
val dest_sum = dest_prod |
|
341 |
fun mk_coeff(k,t) = if t=one then mk_numeral k |
|
342 |
else raise TERM("mk_coeff", []) |
|
343 |
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*) |
|
24893 | 344 |
val left_distrib = @{thm zmult_assoc} RS sym RS trans |
23146 | 345 |
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" |
346 |
fun trans_tac _ = ArithData.gen_trans_tac trans |
|
347 |
||
348 |
||
349 |
||
350 |
val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps |
|
24893 | 351 |
val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS sym] @ |
352 |
bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys |
|
23146 | 353 |
fun norm_tac ss = |
354 |
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
355 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
356 |
||
357 |
val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys |
|
358 |
fun numeral_simp_tac ss = |
|
359 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
360 |
val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s); |
|
361 |
end; |
|
362 |
||
363 |
||
364 |
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); |
|
365 |
||
366 |
val combine_numerals_prod = |
|
367 |
prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc); |
|
368 |
||
369 |
end; |
|
370 |
||
371 |
||
372 |
Addsimprocs Int_Numeral_Simprocs.cancel_numerals; |
|
373 |
Addsimprocs [Int_Numeral_Simprocs.combine_numerals, |
|
374 |
Int_Numeral_Simprocs.combine_numerals_prod]; |
|
375 |
||
376 |
||
377 |
(*examples:*) |
|
378 |
(* |
|
379 |
print_depth 22; |
|
380 |
set timing; |
|
381 |
set trace_simp; |
|
382 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
|
383 |
val sg = #sign (rep_thm (topthm())); |
|
384 |
val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1)); |
|
385 |
val (t,_) = FOLogic.dest_eq t; |
|
386 |
||
387 |
(*combine_numerals_prod (products of separate literals) *) |
|
388 |
test "#5 $* x $* #3 = y"; |
|
389 |
||
390 |
test "y2 $+ ?x42 = y $+ y2"; |
|
391 |
||
392 |
test "oo : int ==> l $+ (l $+ #2) $+ oo = oo"; |
|
393 |
||
394 |
test "#9$*x $+ y = x$*#23 $+ z"; |
|
395 |
test "y $+ x = x $+ z"; |
|
396 |
||
397 |
test "x : int ==> x $+ y $+ z = x $+ z"; |
|
398 |
test "x : int ==> y $+ (z $+ x) = z $+ x"; |
|
399 |
test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)"; |
|
400 |
test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)"; |
|
401 |
||
402 |
test "#-3 $* x $+ y $<= x $* #2 $+ z"; |
|
403 |
test "y $+ x $<= x $+ z"; |
|
404 |
test "x $+ y $+ z $<= x $+ z"; |
|
405 |
||
406 |
test "y $+ (z $+ x) $< z $+ x"; |
|
407 |
test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)"; |
|
408 |
test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)"; |
|
409 |
||
410 |
test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu"; |
|
411 |
test "u : int ==> #2 $* u = u"; |
|
412 |
test "(i $+ j $+ #12 $+ k) $- #15 = y"; |
|
413 |
test "(i $+ j $+ #12 $+ k) $- #5 = y"; |
|
414 |
||
415 |
test "y $- b $< b"; |
|
416 |
test "y $- (#3 $* b $+ c) $< b $- #2 $* c"; |
|
417 |
||
418 |
test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w"; |
|
419 |
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w"; |
|
420 |
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w"; |
|
421 |
test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w"; |
|
422 |
||
423 |
test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y"; |
|
424 |
test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y"; |
|
425 |
||
426 |
test "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv"; |
|
427 |
||
428 |
test "a $+ $-(b$+c) $+ b = d"; |
|
429 |
test "a $+ $-(b$+c) $- b = d"; |
|
430 |
||
431 |
(*negative numerals*) |
|
432 |
test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz"; |
|
433 |
test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y"; |
|
434 |
test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y"; |
|
435 |
test "(i $+ j $+ #-12 $+ k) $- #15 = y"; |
|
436 |
test "(i $+ j $+ #12 $+ k) $- #-15 = y"; |
|
437 |
test "(i $+ j $+ #-12 $+ k) $- #-15 = y"; |
|
438 |
||
439 |
(*Multiplying separated numerals*) |
|
440 |
Goal "#6 $* ($# x $* #2) = uu"; |
|
441 |
Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) = uu"; |
|
442 |
*) |
|
443 |