author | wenzelm |
Wed, 03 Nov 2010 10:18:05 +0100 | |
changeset 40312 | dff9f73a3763 |
parent 38715 | 6513ea67d95d |
child 40313 | 54e8be8b4de0 |
permissions | -rw-r--r-- |
23146 | 1 |
(* Title: ZF/int_arith.ML |
2 |
Author: Larry Paulson |
|
3 |
||
4 |
Simprocs for linear arithmetic. |
|
5 |
*) |
|
6 |
||
40312
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
7 |
signature INT_NUMERAL_SIMPROCS = |
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
8 |
sig |
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
9 |
val cancel_numerals: simproc list |
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
10 |
val combine_numerals: simproc |
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
11 |
val combine_numerals_prod: simproc |
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
12 |
end |
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
13 |
|
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
14 |
structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS = |
23146 | 15 |
struct |
16 |
||
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
17 |
(* abstract syntax operations *) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
18 |
|
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
19 |
fun mk_bit 0 = @{term "0"} |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
20 |
| mk_bit 1 = @{term "succ(0)"} |
40312
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
21 |
| mk_bit _ = raise TERM ("mk_bit", []); |
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
22 |
|
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
23 |
fun dest_bit @{term "0"} = 0 |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
24 |
| dest_bit @{term "succ(0)"} = 1 |
40312
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
25 |
| dest_bit t = raise TERM ("dest_bit", [t]); |
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
26 |
|
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
27 |
fun mk_bin i = |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
28 |
let |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
29 |
fun term_of [] = @{term Pls} |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
30 |
| term_of [~1] = @{term Min} |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
31 |
| term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b; |
35123 | 32 |
in term_of (Numeral_Syntax.make_binary i) end; |
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
33 |
|
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
34 |
fun dest_bin tm = |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
35 |
let |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
36 |
fun bin_of @{term Pls} = [] |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
37 |
| bin_of @{term Min} = [~1] |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
38 |
| bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs |
40312
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
39 |
| bin_of _ = raise TERM ("dest_bin", [tm]); |
35123 | 40 |
in Numeral_Syntax.dest_binary (bin_of tm) end; |
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
41 |
|
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
42 |
|
23146 | 43 |
(*Utilities*) |
44 |
||
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset
|
45 |
fun mk_numeral i = @{const integ_of} $ mk_bin i; |
23146 | 46 |
|
40312
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
47 |
fun dest_numeral (Const(@{const_name integ_of}, _) $ w) = dest_bin w |
dff9f73a3763
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset
|
48 |
| dest_numeral t = raise TERM ("dest_numeral", [t]); |
23146 | 49 |
|
50 |
fun find_first_numeral past (t::terms) = |
|
51 |
((dest_numeral t, rev past @ terms) |
|
52 |
handle TERM _ => find_first_numeral (t::past) terms) |
|
53 |
| find_first_numeral past [] = raise TERM("find_first_numeral", []); |
|
54 |
||
55 |
val zero = mk_numeral 0; |
|
26059 | 56 |
val mk_plus = FOLogic.mk_binop @{const_name "zadd"}; |
23146 | 57 |
|
58 |
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) |
|
59 |
fun mk_sum [] = zero |
|
60 |
| mk_sum [t,u] = mk_plus (t, u) |
|
61 |
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
62 |
||
63 |
(*this version ALWAYS includes a trailing zero*) |
|
64 |
fun long_mk_sum [] = zero |
|
65 |
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
66 |
||
26190 | 67 |
val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i}; |
23146 | 68 |
|
69 |
(*decompose additions AND subtractions as a sum*) |
|
26059 | 70 |
fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) = |
23146 | 71 |
dest_summing (pos, t, dest_summing (pos, u, ts)) |
26059 | 72 |
| dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) = |
23146 | 73 |
dest_summing (pos, t, dest_summing (not pos, u, ts)) |
74 |
| dest_summing (pos, t, ts) = |
|
27237 | 75 |
if pos then t::ts else @{const zminus} $ t :: ts; |
23146 | 76 |
|
77 |
fun dest_sum t = dest_summing (true, t, []); |
|
78 |
||
26059 | 79 |
val mk_diff = FOLogic.mk_binop @{const_name "zdiff"}; |
26190 | 80 |
val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i}; |
23146 | 81 |
|
82 |
val one = mk_numeral 1; |
|
26059 | 83 |
val mk_times = FOLogic.mk_binop @{const_name "zmult"}; |
23146 | 84 |
|
85 |
fun mk_prod [] = one |
|
86 |
| mk_prod [t] = t |
|
87 |
| mk_prod (t :: ts) = if t = one then mk_prod ts |
|
88 |
else mk_times (t, mk_prod ts); |
|
89 |
||
26190 | 90 |
val dest_times = FOLogic.dest_bin @{const_name "zmult"} @{typ i}; |
23146 | 91 |
|
92 |
fun dest_prod t = |
|
93 |
let val (t,u) = dest_times t |
|
94 |
in dest_prod t @ dest_prod u end |
|
95 |
handle TERM _ => [t]; |
|
96 |
||
97 |
(*DON'T do the obvious simplifications; that would create special cases*) |
|
98 |
fun mk_coeff (k, t) = mk_times (mk_numeral k, t); |
|
99 |
||
100 |
(*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
26059 | 101 |
fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t |
23146 | 102 |
| dest_coeff sign t = |
35408 | 103 |
let val ts = sort Term_Ord.term_ord (dest_prod t) |
23146 | 104 |
val (n, ts') = find_first_numeral [] ts |
105 |
handle TERM _ => (1, ts) |
|
106 |
in (sign*n, mk_prod ts') end; |
|
107 |
||
108 |
(*Find first coefficient-term THAT MATCHES u*) |
|
109 |
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
110 |
| find_first_coeff past u (t::terms) = |
|
111 |
let val (n,u') = dest_coeff 1 t |
|
112 |
in if u aconv u' then (n, rev past @ terms) |
|
113 |
else find_first_coeff (t::past) u terms |
|
114 |
end |
|
115 |
handle TERM _ => find_first_coeff (t::past) u terms; |
|
116 |
||
117 |
||
118 |
(*Simplify #1*n and n*#1 to n*) |
|
24893 | 119 |
val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}]; |
23146 | 120 |
|
24893 | 121 |
val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify}, |
122 |
@{thm zmult_minus1}, @{thm zmult_minus1_right}]; |
|
23146 | 123 |
|
24893 | 124 |
val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int}, |
125 |
@{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @ |
|
126 |
@{thms bin.intros}; |
|
127 |
val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2}, |
|
128 |
@{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2}, |
|
129 |
@{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}]; |
|
23146 | 130 |
|
131 |
(*To perform binary arithmetic*) |
|
24893 | 132 |
val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps}; |
23146 | 133 |
|
134 |
(*To evaluate binary negations of coefficients*) |
|
24893 | 135 |
val zminus_simps = @{thms NCons_simps} @ |
35409 | 136 |
[@{thm integ_of_minus} RS @{thm sym}, |
24893 | 137 |
@{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min}, |
138 |
@{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}]; |
|
23146 | 139 |
|
140 |
(*To let us treat subtraction as addition*) |
|
24893 | 141 |
val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}]; |
23146 | 142 |
|
35020
862a20ffa8e2
prefer explicit @{lemma} over adhoc forward reasoning;
wenzelm
parents:
32957
diff
changeset
|
143 |
(*push the unary minus down*) |
862a20ffa8e2
prefer explicit @{lemma} over adhoc forward reasoning;
wenzelm
parents:
32957
diff
changeset
|
144 |
val int_minus_mult_eq_1_to_2 = @{lemma "$- w $* z = w $* $- z" by simp}; |
23146 | 145 |
|
146 |
(*to extract again any uncancelled minuses*) |
|
147 |
val int_minus_from_mult_simps = |
|
24893 | 148 |
[@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}]; |
23146 | 149 |
|
150 |
(*combine unary minus with numeric literals, however nested within a product*) |
|
151 |
val int_mult_minus_simps = |
|
35409 | 152 |
[@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2]; |
23146 | 153 |
|
32155 | 154 |
fun prep_simproc thy (name, pats, proc) = |
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
35409
diff
changeset
|
155 |
Simplifier.simproc_global thy name pats proc; |
23146 | 156 |
|
157 |
structure CancelNumeralsCommon = |
|
158 |
struct |
|
159 |
val mk_sum = (fn T:typ => mk_sum) |
|
160 |
val dest_sum = dest_sum |
|
161 |
val mk_coeff = mk_coeff |
|
162 |
val dest_coeff = dest_coeff 1 |
|
163 |
val find_first_coeff = find_first_coeff [] |
|
35409 | 164 |
fun trans_tac _ = ArithData.gen_trans_tac @{thm iff_trans} |
23146 | 165 |
|
24893 | 166 |
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} |
23146 | 167 |
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys |
24893 | 168 |
val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys |
23146 | 169 |
fun norm_tac ss = |
170 |
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
171 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
172 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
173 |
||
174 |
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys |
|
175 |
fun numeral_simp_tac ss = |
|
176 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents:
30607
diff
changeset
|
177 |
THEN ALLGOALS (asm_simp_tac (simpset_of (Simplifier.the_context ss))) |
23146 | 178 |
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) |
179 |
end; |
|
180 |
||
181 |
||
182 |
structure EqCancelNumerals = CancelNumeralsFun |
|
183 |
(open CancelNumeralsCommon |
|
184 |
val prove_conv = ArithData.prove_conv "inteq_cancel_numerals" |
|
185 |
val mk_bal = FOLogic.mk_eq |
|
186 |
val dest_bal = FOLogic.dest_eq |
|
35409 | 187 |
val bal_add1 = @{thm eq_add_iff1} RS @{thm iff_trans} |
188 |
val bal_add2 = @{thm eq_add_iff2} RS @{thm iff_trans} |
|
23146 | 189 |
); |
190 |
||
191 |
structure LessCancelNumerals = CancelNumeralsFun |
|
192 |
(open CancelNumeralsCommon |
|
193 |
val prove_conv = ArithData.prove_conv "intless_cancel_numerals" |
|
26059 | 194 |
val mk_bal = FOLogic.mk_binrel @{const_name "zless"} |
26190 | 195 |
val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i} |
35409 | 196 |
val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans} |
197 |
val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans} |
|
23146 | 198 |
); |
199 |
||
200 |
structure LeCancelNumerals = CancelNumeralsFun |
|
201 |
(open CancelNumeralsCommon |
|
202 |
val prove_conv = ArithData.prove_conv "intle_cancel_numerals" |
|
26059 | 203 |
val mk_bal = FOLogic.mk_binrel @{const_name "zle"} |
26190 | 204 |
val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i} |
35409 | 205 |
val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans} |
206 |
val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans} |
|
23146 | 207 |
); |
208 |
||
209 |
val cancel_numerals = |
|
32155 | 210 |
map (prep_simproc @{theory}) |
23146 | 211 |
[("inteq_cancel_numerals", |
212 |
["l $+ m = n", "l = m $+ n", |
|
213 |
"l $- m = n", "l = m $- n", |
|
214 |
"l $* m = n", "l = m $* n"], |
|
215 |
K EqCancelNumerals.proc), |
|
216 |
("intless_cancel_numerals", |
|
217 |
["l $+ m $< n", "l $< m $+ n", |
|
218 |
"l $- m $< n", "l $< m $- n", |
|
219 |
"l $* m $< n", "l $< m $* n"], |
|
220 |
K LessCancelNumerals.proc), |
|
221 |
("intle_cancel_numerals", |
|
222 |
["l $+ m $<= n", "l $<= m $+ n", |
|
223 |
"l $- m $<= n", "l $<= m $- n", |
|
224 |
"l $* m $<= n", "l $<= m $* n"], |
|
225 |
K LeCancelNumerals.proc)]; |
|
226 |
||
227 |
||
228 |
(*version without the hyps argument*) |
|
229 |
fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg []; |
|
230 |
||
231 |
structure CombineNumeralsData = |
|
232 |
struct |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
233 |
type coeff = int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
234 |
val iszero = (fn x => x = 0) |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
235 |
val add = op + |
23146 | 236 |
val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *) |
237 |
val dest_sum = dest_sum |
|
238 |
val mk_coeff = mk_coeff |
|
239 |
val dest_coeff = dest_coeff 1 |
|
35409 | 240 |
val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans} |
23146 | 241 |
val prove_conv = prove_conv_nohyps "int_combine_numerals" |
35409 | 242 |
fun trans_tac _ = ArithData.gen_trans_tac @{thm trans} |
23146 | 243 |
|
24893 | 244 |
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys |
23146 | 245 |
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys |
24893 | 246 |
val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys |
23146 | 247 |
fun norm_tac ss = |
248 |
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
249 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
250 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) |
|
251 |
||
252 |
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys |
|
253 |
fun numeral_simp_tac ss = |
|
254 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
255 |
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) |
|
256 |
end; |
|
257 |
||
258 |
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); |
|
259 |
||
260 |
val combine_numerals = |
|
32155 | 261 |
prep_simproc @{theory} |
262 |
("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc); |
|
23146 | 263 |
|
264 |
||
265 |
||
266 |
(** Constant folding for integer multiplication **) |
|
267 |
||
268 |
(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as |
|
269 |
the "sum" of #3, x, #4; the literals are then multiplied*) |
|
270 |
||
271 |
||
272 |
structure CombineNumeralsProdData = |
|
273 |
struct |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
274 |
type coeff = int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
275 |
val iszero = (fn x => x = 0) |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
276 |
val add = op * |
23146 | 277 |
val mk_sum = (fn T:typ => mk_prod) |
278 |
val dest_sum = dest_prod |
|
279 |
fun mk_coeff(k,t) = if t=one then mk_numeral k |
|
280 |
else raise TERM("mk_coeff", []) |
|
281 |
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*) |
|
35409 | 282 |
val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans} |
23146 | 283 |
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" |
35409 | 284 |
fun trans_tac _ = ArithData.gen_trans_tac @{thm trans} |
23146 | 285 |
|
286 |
||
287 |
||
288 |
val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps |
|
35409 | 289 |
val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @ |
24893 | 290 |
bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys |
23146 | 291 |
fun norm_tac ss = |
292 |
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) |
|
293 |
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) |
|
294 |
||
295 |
val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys |
|
296 |
fun numeral_simp_tac ss = |
|
297 |
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
|
298 |
val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s); |
|
299 |
end; |
|
300 |
||
301 |
||
302 |
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); |
|
303 |
||
304 |
val combine_numerals_prod = |
|
32155 | 305 |
prep_simproc @{theory} |
306 |
("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc); |
|
23146 | 307 |
|
308 |
end; |
|
309 |
||
310 |
||
311 |
Addsimprocs Int_Numeral_Simprocs.cancel_numerals; |
|
312 |
Addsimprocs [Int_Numeral_Simprocs.combine_numerals, |
|
313 |
Int_Numeral_Simprocs.combine_numerals_prod]; |
|
314 |
||
315 |
||
316 |
(*examples:*) |
|
317 |
(* |
|
318 |
print_depth 22; |
|
319 |
set timing; |
|
320 |
set trace_simp; |
|
321 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
|
322 |
val sg = #sign (rep_thm (topthm())); |
|
323 |
val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1)); |
|
324 |
val (t,_) = FOLogic.dest_eq t; |
|
325 |
||
326 |
(*combine_numerals_prod (products of separate literals) *) |
|
327 |
test "#5 $* x $* #3 = y"; |
|
328 |
||
329 |
test "y2 $+ ?x42 = y $+ y2"; |
|
330 |
||
331 |
test "oo : int ==> l $+ (l $+ #2) $+ oo = oo"; |
|
332 |
||
333 |
test "#9$*x $+ y = x$*#23 $+ z"; |
|
334 |
test "y $+ x = x $+ z"; |
|
335 |
||
336 |
test "x : int ==> x $+ y $+ z = x $+ z"; |
|
337 |
test "x : int ==> y $+ (z $+ x) = z $+ x"; |
|
338 |
test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)"; |
|
339 |
test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)"; |
|
340 |
||
341 |
test "#-3 $* x $+ y $<= x $* #2 $+ z"; |
|
342 |
test "y $+ x $<= x $+ z"; |
|
343 |
test "x $+ y $+ z $<= x $+ z"; |
|
344 |
||
345 |
test "y $+ (z $+ x) $< z $+ x"; |
|
346 |
test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)"; |
|
347 |
test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)"; |
|
348 |
||
349 |
test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu"; |
|
350 |
test "u : int ==> #2 $* u = u"; |
|
351 |
test "(i $+ j $+ #12 $+ k) $- #15 = y"; |
|
352 |
test "(i $+ j $+ #12 $+ k) $- #5 = y"; |
|
353 |
||
354 |
test "y $- b $< b"; |
|
355 |
test "y $- (#3 $* b $+ c) $< b $- #2 $* c"; |
|
356 |
||
357 |
test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w"; |
|
358 |
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w"; |
|
359 |
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w"; |
|
360 |
test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w"; |
|
361 |
||
362 |
test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y"; |
|
363 |
test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y"; |
|
364 |
||
365 |
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"; |
|
366 |
||
367 |
test "a $+ $-(b$+c) $+ b = d"; |
|
368 |
test "a $+ $-(b$+c) $- b = d"; |
|
369 |
||
370 |
(*negative numerals*) |
|
371 |
test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz"; |
|
372 |
test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y"; |
|
373 |
test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y"; |
|
374 |
test "(i $+ j $+ #-12 $+ k) $- #15 = y"; |
|
375 |
test "(i $+ j $+ #12 $+ k) $- #-15 = y"; |
|
376 |
test "(i $+ j $+ #-12 $+ k) $- #-15 = y"; |
|
377 |
||
378 |
(*Multiplying separated numerals*) |
|
379 |
Goal "#6 $* ($# x $* #2) = uu"; |
|
380 |
Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) = uu"; |
|
381 |
*) |
|
382 |