19 qed "eq_iff_zdiff_eq_0"; |
18 qed "eq_iff_zdiff_eq_0"; |
20 |
19 |
21 Goal "(x <= y) = (x-y <= (#0::int))"; |
20 Goal "(x <= y) = (x-y <= (#0::int))"; |
22 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
21 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
23 qed "zle_iff_zdiff_zle_0"; |
22 qed "zle_iff_zdiff_zle_0"; |
|
23 |
|
24 |
|
25 (** For cancel_numerals **) |
|
26 |
|
27 Goal "!!i::int. ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"; |
|
28 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1); |
|
29 qed "diff_add_eq1"; |
|
30 |
|
31 Goal "!!i::int. ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"; |
|
32 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1); |
|
33 qed "diff_add_eq2"; |
|
34 |
|
35 val rel_iff_rel_0_rls = map (inst "y" "?u+?v") |
|
36 [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, |
|
37 zle_iff_zdiff_zle_0] @ |
|
38 map (inst "y" "n") |
|
39 [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, |
|
40 zle_iff_zdiff_zle_0]; |
|
41 |
|
42 Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; |
|
43 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
44 zadd_ac@rel_iff_rel_0_rls) 1); |
|
45 qed "eq_add_iff1"; |
|
46 |
|
47 Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; |
|
48 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
49 zadd_ac@rel_iff_rel_0_rls) 1); |
|
50 qed "eq_add_iff2"; |
|
51 |
|
52 Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)"; |
|
53 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
54 zadd_ac@rel_iff_rel_0_rls) 1); |
|
55 qed "less_add_iff1"; |
|
56 |
|
57 Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)"; |
|
58 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
59 zadd_ac@rel_iff_rel_0_rls) 1); |
|
60 qed "less_add_iff2"; |
|
61 |
|
62 Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; |
|
63 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
64 zadd_ac@rel_iff_rel_0_rls) 1); |
|
65 qed "le_add_iff1"; |
|
66 |
|
67 Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; |
|
68 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib] |
|
69 @zadd_ac@rel_iff_rel_0_rls) 1); |
|
70 qed "le_add_iff2"; |
|
71 |
|
72 |
|
73 structure Int_Numeral_Simprocs = |
|
74 struct |
|
75 |
|
76 (*Utilities*) |
|
77 |
|
78 fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ |
|
79 NumeralSyntax.mk_bin n; |
|
80 |
|
81 (*Decodes a binary INTEGER*) |
|
82 fun dest_numeral (Const("Numeral.number_of", _) $ w) = NumeralSyntax.dest_bin w |
|
83 | dest_numeral t = raise TERM("dest_numeral", [t]); |
|
84 |
|
85 fun find_first_numeral past (t::terms) = |
|
86 ((dest_numeral t, rev past @ terms) |
|
87 handle TERM _ => find_first_numeral (t::past) terms) |
|
88 | find_first_numeral past [] = raise TERM("find_first_numeral", []); |
|
89 |
|
90 val zero = mk_numeral 0; |
|
91 val mk_plus = HOLogic.mk_binop "op +"; |
|
92 |
|
93 val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT); |
|
94 |
|
95 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) |
|
96 fun mk_sum [] = zero |
|
97 | mk_sum [t,u] = mk_plus (t, u) |
|
98 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
99 |
|
100 val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT; |
|
101 |
|
102 (*decompose additions AND subtractions as a sum*) |
|
103 fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) = |
|
104 dest_summing (pos, t, dest_summing (pos, u, ts)) |
|
105 | dest_summing (pos, Const ("op -", _) $ t $ u, ts) = |
|
106 dest_summing (pos, t, dest_summing (not pos, u, ts)) |
|
107 | dest_summing (pos, t, ts) = |
|
108 if pos then t::ts else uminus_const$t :: ts; |
|
109 |
|
110 fun dest_sum t = dest_summing (true, t, []); |
|
111 |
|
112 val mk_diff = HOLogic.mk_binop "op -"; |
|
113 val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT; |
|
114 |
|
115 val one = mk_numeral 1; |
|
116 val mk_times = HOLogic.mk_binop "op *"; |
|
117 |
|
118 fun mk_prod [] = one |
|
119 | mk_prod [t] = t |
|
120 | mk_prod (t :: ts) = if t = one then mk_prod ts |
|
121 else mk_times (t, mk_prod ts); |
|
122 |
|
123 val dest_times = HOLogic.dest_bin "op *" HOLogic.intT; |
|
124 |
|
125 fun dest_prod t = |
|
126 let val (t,u) = dest_times t |
|
127 in dest_prod t @ dest_prod u end |
|
128 handle TERM _ => [t]; |
|
129 |
|
130 (*DON'T do the obvious simplifications; that would create special cases*) |
|
131 fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts); |
|
132 |
|
133 (*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
134 fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t |
|
135 | dest_coeff sign t = |
|
136 let val ts = sort Term.term_ord (dest_prod t) |
|
137 val (n, ts') = find_first_numeral [] ts |
|
138 handle TERM _ => (1, ts) |
|
139 in (sign*n, mk_prod ts') end; |
|
140 |
|
141 (*Find first coefficient-term THAT MATCHES u*) |
|
142 fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
143 | find_first_coeff past u (t::terms) = |
|
144 let val (n,u') = dest_coeff 1 t |
|
145 in if u aconv u' then (n, rev past @ terms) |
|
146 else find_first_coeff (t::past) u terms |
|
147 end |
|
148 handle TERM _ => find_first_coeff (t::past) u terms; |
|
149 |
|
150 |
|
151 (*Simplify #1*n and n*#1 to n*) |
|
152 val add_0s = [zadd_0, zadd_0_right]; |
|
153 val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right]; |
|
154 |
|
155 (*To perform binary arithmetic*) |
|
156 val bin_simps = [number_of_add RS sym, add_number_of_left] @ |
|
157 bin_arith_simps @ bin_rel_simps; |
|
158 |
|
159 (*To let us treat subtraction as addition*) |
|
160 val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus]; |
|
161 |
|
162 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
|
163 |
|
164 fun prove_conv tacs sg (t, u) = |
|
165 if t aconv u then None |
|
166 else |
|
167 Some |
|
168 (mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u))) |
|
169 (K tacs)) |
|
170 handle ERROR => error |
|
171 ("The error(s) above occurred while trying to prove " ^ |
|
172 (string_of_cterm (cterm_of sg (mk_eqv (t, u)))))); |
|
173 |
|
174 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; |
|
175 fun prep_pat s = Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.termT); |
|
176 val prep_pats = map prep_pat; |
|
177 |
|
178 structure CancelNumeralsCommon = |
|
179 struct |
|
180 val mk_sum = mk_sum |
|
181 val dest_sum = dest_sum |
|
182 val mk_coeff = mk_coeff |
|
183 val dest_coeff = dest_coeff 1 |
|
184 val find_first_coeff = find_first_coeff [] |
|
185 val prove_conv = prove_conv |
|
186 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@zadd_ac)) |
|
187 THEN ALLGOALS |
|
188 (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@bin_simps@zmult_ac)) |
|
189 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
|
190 end; |
|
191 |
|
192 |
|
193 (* int eq *) |
|
194 structure EqCancelNumerals = CancelNumeralsFun |
|
195 (open CancelNumeralsCommon |
|
196 val mk_bal = HOLogic.mk_eq |
|
197 val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT |
|
198 val bal_add1 = eq_add_iff1 RS trans |
|
199 val bal_add2 = eq_add_iff2 RS trans |
|
200 ); |
|
201 |
|
202 (* int less *) |
|
203 structure LessCancelNumerals = CancelNumeralsFun |
|
204 (open CancelNumeralsCommon |
|
205 val mk_bal = HOLogic.mk_binrel "op <" |
|
206 val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT |
|
207 val bal_add1 = less_add_iff1 RS trans |
|
208 val bal_add2 = less_add_iff2 RS trans |
|
209 ); |
|
210 |
|
211 (* int le *) |
|
212 structure LeCancelNumerals = CancelNumeralsFun |
|
213 (open CancelNumeralsCommon |
|
214 val mk_bal = HOLogic.mk_binrel "op <=" |
|
215 val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT |
|
216 val bal_add1 = le_add_iff1 RS trans |
|
217 val bal_add2 = le_add_iff2 RS trans |
|
218 ); |
|
219 |
|
220 (* int diff *) |
|
221 structure DiffCancelNumerals = CancelNumeralsFun |
|
222 (open CancelNumeralsCommon |
|
223 val mk_bal = HOLogic.mk_binop "op -" |
|
224 val dest_bal = HOLogic.dest_bin "op -" HOLogic.intT |
|
225 val bal_add1 = diff_add_eq1 RS trans |
|
226 val bal_add2 = diff_add_eq2 RS trans |
|
227 ); |
|
228 |
|
229 |
|
230 val cancel_numerals = |
|
231 map prep_simproc |
|
232 [("inteq_cancel_numerals", |
|
233 prep_pats ["(l::int) + m = n", "(l::int) = m + n", |
|
234 "(l::int) - m = n", "(l::int) = m - n", |
|
235 "(l::int) * m = n", "(l::int) = m * n"], |
|
236 EqCancelNumerals.proc), |
|
237 ("intless_cancel_numerals", |
|
238 prep_pats ["(l::int) + m < n", "(l::int) < m + n", |
|
239 "(l::int) - m < n", "(l::int) < m - n", |
|
240 "(l::int) * m < n", "(l::int) < m * n"], |
|
241 LessCancelNumerals.proc), |
|
242 ("intle_cancel_numerals", |
|
243 prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", |
|
244 "(l::int) - m <= n", "(l::int) <= m - n", |
|
245 "(l::int) * m <= n", "(l::int) <= m * n"], |
|
246 LeCancelNumerals.proc), |
|
247 ("intdiff_cancel_numerals", |
|
248 prep_pats ["((l::int) + m) - n", "(l::int) - (m + n)", |
|
249 "((l::int) - m) - n", "(l::int) - (m - n)", |
|
250 "(l::int) * m - n", "(l::int) - m * n"], |
|
251 DiffCancelNumerals.proc)]; |
|
252 |
|
253 end; |
|
254 |
|
255 |
|
256 Addsimprocs Int_Numeral_Simprocs.cancel_numerals; |
|
257 |
|
258 (*examples: |
|
259 print_depth 22; |
|
260 set proof_timing; |
|
261 set trace_simp; |
|
262 fun test s = (Goal s; by (Simp_tac 1)); |
|
263 |
|
264 test "#2*u = (u::int)"; |
|
265 test "(i + j + #12 + (k::int)) - #15 = y"; |
|
266 test "(i + j + #12 + (k::int)) - #5 = y"; |
|
267 |
|
268 test "y - b < (b::int)"; |
|
269 test "y - (#3*b + c) < (b::int) - #2*c"; |
|
270 |
|
271 test "(#2*x + (u*v) + y) - v*#3*u = (w::int)"; |
|
272 test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)"; |
|
273 test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)"; |
|
274 |
|
275 test "(i + j + #12 + (k::int)) = u + #15 + y"; |
|
276 test "(i + j*#2 + #12 + (k::int)) = j + #5 + y"; |
|
277 |
|
278 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::int)"; |
|
279 |
|
280 (*negative numerals*) |
|
281 test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz"; |
|
282 test "(i + j + #-3 + (k::int)) < u + #5 + y"; |
|
283 test "(i + j + #3 + (k::int)) < u + #-6 + y"; |
|
284 test "(i + j + #-12 + (k::int)) - #15 = y"; |
|
285 test "(i + j + #12 + (k::int)) - #-15 = y"; |
|
286 test "(i + j + #-12 + (k::int)) - #-15 = y"; |
|
287 *) |
|
288 |
|
289 |
|
290 |
|
291 (**************************************************************************************************************************************************************************************************************************************************************** |
24 |
292 |
25 |
293 |
26 structure Int_CC_Data : COMBINE_COEFF_DATA = |
294 structure Int_CC_Data : COMBINE_COEFF_DATA = |
27 struct |
295 struct |
28 val ss = HOL_ss |
296 val ss = HOL_ss |