1 (* Title: HOL/Integ/IntArith.thy |
1 (* Title: HOL/Integ/IntArith.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Authors: Larry Paulson and Tobias Nipkow |
3 Authors: Larry Paulson and Tobias Nipkow |
4 |
|
5 Simprocs and decision procedure for linear arithmetic. |
|
6 *) |
4 *) |
7 |
|
8 (*** Simprocs for numeric literals ***) |
|
9 |
|
10 (** Combining of literal coefficients in sums of products **) |
|
11 |
|
12 Goal "(x < y) = (x-y < (#0::int))"; |
|
13 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
|
14 qed "zless_iff_zdiff_zless_0"; |
|
15 |
|
16 Goal "(x = y) = (x-y = (#0::int))"; |
|
17 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
|
18 qed "eq_iff_zdiff_eq_0"; |
|
19 |
|
20 Goal "(x <= y) = (x-y <= (#0::int))"; |
|
21 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
|
22 qed "zle_iff_zdiff_zle_0"; |
|
23 |
|
24 |
|
25 (** For combine_numerals **) |
|
26 |
|
27 Goal "i*u + (j*u + k) = (i+j)*u + (k::int)"; |
|
28 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); |
|
29 qed "left_zadd_zmult_distrib"; |
|
30 |
|
31 |
|
32 (** For cancel_numerals **) |
|
33 |
|
34 val rel_iff_rel_0_rls = map (inst "y" "?u+?v") |
|
35 [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, |
|
36 zle_iff_zdiff_zle_0] @ |
|
37 map (inst "y" "n") |
|
38 [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, |
|
39 zle_iff_zdiff_zle_0]; |
|
40 |
|
41 Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; |
|
42 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
43 zadd_ac@rel_iff_rel_0_rls) 1); |
|
44 qed "eq_add_iff1"; |
|
45 |
|
46 Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; |
|
47 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
48 zadd_ac@rel_iff_rel_0_rls) 1); |
|
49 qed "eq_add_iff2"; |
|
50 |
|
51 Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)"; |
|
52 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
53 zadd_ac@rel_iff_rel_0_rls) 1); |
|
54 qed "less_add_iff1"; |
|
55 |
|
56 Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)"; |
|
57 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
58 zadd_ac@rel_iff_rel_0_rls) 1); |
|
59 qed "less_add_iff2"; |
|
60 |
|
61 Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; |
|
62 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ |
|
63 zadd_ac@rel_iff_rel_0_rls) 1); |
|
64 qed "le_add_iff1"; |
|
65 |
|
66 Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; |
|
67 by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib] |
|
68 @zadd_ac@rel_iff_rel_0_rls) 1); |
|
69 qed "le_add_iff2"; |
|
70 |
|
71 (*To tidy up the result of a simproc. Only the RHS will be simplified.*) |
|
72 Goal "u = u' ==> (t==u) == (t==u')"; |
|
73 by Auto_tac; |
|
74 qed "eq_cong2"; |
|
75 |
|
76 |
|
77 structure Int_Numeral_Simprocs = |
|
78 struct |
|
79 |
|
80 (*Utilities*) |
|
81 |
|
82 fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ |
|
83 NumeralSyntax.mk_bin n; |
|
84 |
|
85 (*Decodes a binary INTEGER*) |
|
86 fun dest_numeral (Const("Numeral.number_of", _) $ w) = |
|
87 (NumeralSyntax.dest_bin w |
|
88 handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w])) |
|
89 | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]); |
|
90 |
|
91 fun find_first_numeral past (t::terms) = |
|
92 ((dest_numeral t, rev past @ terms) |
|
93 handle TERM _ => find_first_numeral (t::past) terms) |
|
94 | find_first_numeral past [] = raise TERM("find_first_numeral", []); |
|
95 |
|
96 val zero = mk_numeral 0; |
|
97 val mk_plus = HOLogic.mk_binop "op +"; |
|
98 |
|
99 val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT); |
|
100 |
|
101 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) |
|
102 fun mk_sum [] = zero |
|
103 | mk_sum [t,u] = mk_plus (t, u) |
|
104 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
105 |
|
106 (*this version ALWAYS includes a trailing zero*) |
|
107 fun long_mk_sum [] = zero |
|
108 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
109 |
|
110 val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT; |
|
111 |
|
112 (*decompose additions AND subtractions as a sum*) |
|
113 fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) = |
|
114 dest_summing (pos, t, dest_summing (pos, u, ts)) |
|
115 | dest_summing (pos, Const ("op -", _) $ t $ u, ts) = |
|
116 dest_summing (pos, t, dest_summing (not pos, u, ts)) |
|
117 | dest_summing (pos, t, ts) = |
|
118 if pos then t::ts else uminus_const$t :: ts; |
|
119 |
|
120 fun dest_sum t = dest_summing (true, t, []); |
|
121 |
|
122 val mk_diff = HOLogic.mk_binop "op -"; |
|
123 val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT; |
|
124 |
|
125 val one = mk_numeral 1; |
|
126 val mk_times = HOLogic.mk_binop "op *"; |
|
127 |
|
128 fun mk_prod [] = one |
|
129 | mk_prod [t] = t |
|
130 | mk_prod (t :: ts) = if t = one then mk_prod ts |
|
131 else mk_times (t, mk_prod ts); |
|
132 |
|
133 val dest_times = HOLogic.dest_bin "op *" HOLogic.intT; |
|
134 |
|
135 fun dest_prod t = |
|
136 let val (t,u) = dest_times t |
|
137 in dest_prod t @ dest_prod u end |
|
138 handle TERM _ => [t]; |
|
139 |
|
140 (*DON'T do the obvious simplifications; that would create special cases*) |
|
141 fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts); |
|
142 |
|
143 (*Express t as a product of (possibly) a numeral with other sorted terms*) |
|
144 fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t |
|
145 | dest_coeff sign t = |
|
146 let val ts = sort Term.term_ord (dest_prod t) |
|
147 val (n, ts') = find_first_numeral [] ts |
|
148 handle TERM _ => (1, ts) |
|
149 in (sign*n, mk_prod ts') end; |
|
150 |
|
151 (*Find first coefficient-term THAT MATCHES u*) |
|
152 fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
|
153 | find_first_coeff past u (t::terms) = |
|
154 let val (n,u') = dest_coeff 1 t |
|
155 in if u aconv u' then (n, rev past @ terms) |
|
156 else find_first_coeff (t::past) u terms |
|
157 end |
|
158 handle TERM _ => find_first_coeff (t::past) u terms; |
|
159 |
|
160 |
|
161 (*Simplify #1*n and n*#1 to n*) |
|
162 val add_0s = [zadd_0, zadd_0_right]; |
|
163 val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right]; |
|
164 |
|
165 (*To perform binary arithmetic*) |
|
166 val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps; |
|
167 |
|
168 (*To evaluate binary negations of coefficients*) |
|
169 val zminus_simps = NCons_simps @ |
|
170 [number_of_minus RS sym, |
|
171 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
|
172 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; |
|
173 |
|
174 (*To let us treat subtraction as addition*) |
|
175 val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus]; |
|
176 |
|
177 (*Apply the given rewrite (if present) just once*) |
|
178 fun trans_tac None = all_tac |
|
179 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); |
|
180 |
|
181 fun prove_conv name tacs sg (t, u) = |
|
182 if t aconv u then None |
|
183 else |
|
184 let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))) |
|
185 in Some |
|
186 (prove_goalw_cterm [] ct (K tacs) |
|
187 handle ERROR => error |
|
188 ("The error(s) above occurred while trying to prove " ^ |
|
189 string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) |
|
190 end; |
|
191 |
|
192 fun simplify_meta_eq rules = |
|
193 mk_meta_eq o |
|
194 simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) |
|
195 |
|
196 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; |
|
197 fun prep_pat s = Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.termT); |
|
198 val prep_pats = map prep_pat; |
|
199 |
|
200 structure CancelNumeralsCommon = |
|
201 struct |
|
202 val mk_sum = mk_sum |
|
203 val dest_sum = dest_sum |
|
204 val mk_coeff = mk_coeff |
|
205 val dest_coeff = dest_coeff 1 |
|
206 val find_first_coeff = find_first_coeff [] |
|
207 val trans_tac = trans_tac |
|
208 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
|
209 zminus_simps@zadd_ac)) |
|
210 THEN ALLGOALS |
|
211 (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ |
|
212 bin_simps@zadd_ac@zmult_ac)) |
|
213 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
|
214 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
|
215 end; |
|
216 |
|
217 |
|
218 structure EqCancelNumerals = CancelNumeralsFun |
|
219 (open CancelNumeralsCommon |
|
220 val prove_conv = prove_conv "inteq_cancel_numerals" |
|
221 val mk_bal = HOLogic.mk_eq |
|
222 val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT |
|
223 val bal_add1 = eq_add_iff1 RS trans |
|
224 val bal_add2 = eq_add_iff2 RS trans |
|
225 ); |
|
226 |
|
227 structure LessCancelNumerals = CancelNumeralsFun |
|
228 (open CancelNumeralsCommon |
|
229 val prove_conv = prove_conv "intless_cancel_numerals" |
|
230 val mk_bal = HOLogic.mk_binrel "op <" |
|
231 val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT |
|
232 val bal_add1 = less_add_iff1 RS trans |
|
233 val bal_add2 = less_add_iff2 RS trans |
|
234 ); |
|
235 |
|
236 structure LeCancelNumerals = CancelNumeralsFun |
|
237 (open CancelNumeralsCommon |
|
238 val prove_conv = prove_conv "intle_cancel_numerals" |
|
239 val mk_bal = HOLogic.mk_binrel "op <=" |
|
240 val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT |
|
241 val bal_add1 = le_add_iff1 RS trans |
|
242 val bal_add2 = le_add_iff2 RS trans |
|
243 ); |
|
244 |
|
245 val cancel_numerals = |
|
246 map prep_simproc |
|
247 [("inteq_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 EqCancelNumerals.proc), |
|
252 ("intless_cancel_numerals", |
|
253 prep_pats ["(l::int) + m < n", "(l::int) < m + n", |
|
254 "(l::int) - m < n", "(l::int) < m - n", |
|
255 "(l::int) * m < n", "(l::int) < m * n"], |
|
256 LessCancelNumerals.proc), |
|
257 ("intle_cancel_numerals", |
|
258 prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", |
|
259 "(l::int) - m <= n", "(l::int) <= m - n", |
|
260 "(l::int) * m <= n", "(l::int) <= m * n"], |
|
261 LeCancelNumerals.proc)]; |
|
262 |
|
263 |
|
264 structure CombineNumeralsData = |
|
265 struct |
|
266 val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) |
|
267 val dest_sum = dest_sum |
|
268 val mk_coeff = mk_coeff |
|
269 val dest_coeff = dest_coeff 1 |
|
270 val left_distrib = left_zadd_zmult_distrib RS trans |
|
271 val prove_conv = prove_conv "int_combine_numerals" |
|
272 val trans_tac = trans_tac |
|
273 val norm_tac = ALLGOALS |
|
274 (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
|
275 zminus_simps@zadd_ac)) |
|
276 THEN ALLGOALS |
|
277 (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ |
|
278 bin_simps@zadd_ac@zmult_ac)) |
|
279 val numeral_simp_tac = ALLGOALS |
|
280 (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
|
281 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
|
282 end; |
|
283 |
|
284 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); |
|
285 |
|
286 val combine_numerals = |
|
287 prep_simproc ("int_combine_numerals", |
|
288 prep_pats ["(i::int) + j", "(i::int) - j"], |
|
289 CombineNumerals.proc); |
|
290 |
|
291 end; |
|
292 |
|
293 |
|
294 Addsimprocs Int_Numeral_Simprocs.cancel_numerals; |
|
295 Addsimprocs [Int_Numeral_Simprocs.combine_numerals]; |
|
296 |
|
297 (*The Abel_Cancel simprocs are now obsolete*) |
|
298 Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; |
|
299 |
|
300 (*examples: |
|
301 print_depth 22; |
|
302 set timing; |
|
303 set trace_simp; |
|
304 fun test s = (Goal s; by (Simp_tac 1)); |
|
305 |
|
306 test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)"; |
|
307 |
|
308 test "#2*u = (u::int)"; |
|
309 test "(i + j + #12 + (k::int)) - #15 = y"; |
|
310 test "(i + j + #12 + (k::int)) - #5 = y"; |
|
311 |
|
312 test "y - b < (b::int)"; |
|
313 test "y - (#3*b + c) < (b::int) - #2*c"; |
|
314 |
|
315 test "(#2*x - (u*v) + y) - v*#3*u = (w::int)"; |
|
316 test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)"; |
|
317 test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)"; |
|
318 test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)"; |
|
319 |
|
320 test "(i + j + #12 + (k::int)) = u + #15 + y"; |
|
321 test "(i + j*#2 + #12 + (k::int)) = j + #5 + y"; |
|
322 |
|
323 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)"; |
|
324 |
|
325 test "a + -(b+c) + b = (d::int)"; |
|
326 test "a + -(b+c) - b = (d::int)"; |
|
327 |
|
328 (*negative numerals*) |
|
329 test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz"; |
|
330 test "(i + j + #-3 + (k::int)) < u + #5 + y"; |
|
331 test "(i + j + #3 + (k::int)) < u + #-6 + y"; |
|
332 test "(i + j + #-12 + (k::int)) - #15 = y"; |
|
333 test "(i + j + #12 + (k::int)) - #-15 = y"; |
|
334 test "(i + j + #-12 + (k::int)) - #-15 = y"; |
|
335 *) |
|
336 |
|
337 |
|
338 (** Constant folding for integer plus and times **) |
|
339 |
|
340 (*We do not need |
|
341 structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data); |
|
342 structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data); |
|
343 because combine_numerals does the same thing*) |
|
344 |
|
345 structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA = |
|
346 struct |
|
347 val ss = HOL_ss |
|
348 val eq_reflection = eq_reflection |
|
349 val thy = Bin.thy |
|
350 val T = HOLogic.intT |
|
351 val plus = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT); |
|
352 val add_ac = zmult_ac |
|
353 end; |
|
354 |
|
355 structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data); |
|
356 |
|
357 Addsimprocs [Int_Times_Assoc.conv]; |
|
358 |
|
359 |
|
360 (** The same for the naturals **) |
|
361 |
|
362 structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA = |
|
363 struct |
|
364 val ss = HOL_ss |
|
365 val eq_reflection = eq_reflection |
|
366 val thy = Bin.thy |
|
367 val T = HOLogic.natT |
|
368 val plus = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT); |
|
369 val add_ac = mult_ac |
|
370 end; |
|
371 |
|
372 structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data); |
|
373 |
|
374 Addsimprocs [Nat_Times_Assoc.conv]; |
|
375 |
|
376 |
|
377 |
|
378 (*** decision procedure for linear arithmetic ***) |
|
379 |
|
380 (*---------------------------------------------------------------------------*) |
|
381 (* Linear arithmetic *) |
|
382 (*---------------------------------------------------------------------------*) |
|
383 |
|
384 (* |
|
385 Instantiation of the generic linear arithmetic package for int. |
|
386 *) |
|
387 |
|
388 (* Update parameters of arithmetic prover *) |
|
389 let |
|
390 |
|
391 (* reduce contradictory <= to False *) |
|
392 val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @ |
|
393 [int_0, zadd_0, zadd_0_right, zdiff_def, |
|
394 zadd_zminus_inverse, zadd_zminus_inverse2, |
|
395 zmult_0, zmult_0_right, |
|
396 zmult_1, zmult_1_right, |
|
397 zmult_minus1, zmult_minus1_right, |
|
398 zminus_zadd_distrib, zminus_zminus]; |
|
399 |
|
400 val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@ |
|
401 Int_Numeral_Simprocs.cancel_numerals; |
|
402 |
|
403 val add_mono_thms = |
|
404 map (fn s => prove_goal Int.thy s |
|
405 (fn prems => [cut_facts_tac prems 1, |
|
406 asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) |
|
407 ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", |
|
408 "(i = j) & (k <= l) ==> i + k <= j + (l::int)", |
|
409 "(i <= j) & (k = l) ==> i + k <= j + (l::int)", |
|
410 "(i = j) & (k = l) ==> i + k = j + (l::int)" |
|
411 ]; |
|
412 |
|
413 in |
|
414 LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms; |
|
415 LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2]; |
|
416 LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules |
|
417 addsimprocs simprocs |
|
418 addcongs [if_weak_cong]; |
|
419 LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)] |
|
420 end; |
|
421 |
|
422 let |
|
423 val int_arith_simproc_pats = |
|
424 map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT)) |
|
425 ["(m::int) < n","(m::int) <= n", "(m::int) = n"]; |
|
426 |
|
427 val fast_int_arith_simproc = mk_simproc |
|
428 "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover; |
|
429 in |
|
430 Addsimprocs [fast_int_arith_simproc] |
|
431 end; |
|
432 |
|
433 (* Some test data |
|
434 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
|
435 by (fast_arith_tac 1); |
|
436 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)"; |
|
437 by (fast_arith_tac 1); |
|
438 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d"; |
|
439 by (fast_arith_tac 1); |
|
440 Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; |
|
441 by (fast_arith_tac 1); |
|
442 Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ |
|
443 \ ==> a+a <= j+j"; |
|
444 by (fast_arith_tac 1); |
|
445 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \ |
|
446 \ ==> a+a - - #-1 < j+j - #3"; |
|
447 by (fast_arith_tac 1); |
|
448 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; |
|
449 by (arith_tac 1); |
|
450 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
451 \ ==> a <= l"; |
|
452 by (fast_arith_tac 1); |
|
453 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
454 \ ==> a+a+a+a <= l+l+l+l"; |
|
455 by (fast_arith_tac 1); |
|
456 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
457 \ ==> a+a+a+a+a <= l+l+l+l+i"; |
|
458 by (fast_arith_tac 1); |
|
459 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
460 \ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; |
|
461 by (fast_arith_tac 1); |
|
462 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
463 \ ==> #6*a <= #5*l+i"; |
|
464 by (fast_arith_tac 1); |
|
465 *) |
|
466 |
|
467 (*---------------------------------------------------------------------------*) |
|
468 (* End of linear arithmetic *) |
|
469 (*---------------------------------------------------------------------------*) |
|
470 |
|
471 (** Simplification of inequalities involving numerical constants **) |
|
472 |
|
473 Goal "(w <= z - (#1::int)) = (w<(z::int))"; |
|
474 by (arith_tac 1); |
|
475 qed "zle_diff1_eq"; |
|
476 Addsimps [zle_diff1_eq]; |
|
477 |
|
478 Goal "(w < z + #1) = (w<=(z::int))"; |
|
479 by (arith_tac 1); |
|
480 qed "zle_add1_eq_le"; |
|
481 Addsimps [zle_add1_eq_le]; |
|
482 |
|
483 Goal "(z = z + w) = (w = (#0::int))"; |
|
484 by (arith_tac 1); |
|
485 qed "zadd_left_cancel0"; |
|
486 Addsimps [zadd_left_cancel0]; |
|
487 |
|
488 |
|
489 (* nat *) |
|
490 |
|
491 Goal "#0 <= z ==> int (nat z) = z"; |
|
492 by (asm_full_simp_tac |
|
493 (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); |
|
494 qed "nat_0_le"; |
|
495 |
|
496 Goal "z <= #0 ==> nat z = 0"; |
|
497 by (case_tac "z = #0" 1); |
|
498 by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); |
|
499 by (asm_full_simp_tac |
|
500 (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1); |
|
501 qed "nat_le_0"; |
|
502 |
|
503 Addsimps [nat_0_le, nat_le_0]; |
|
504 |
|
505 val [major,minor] = Goal "[| #0 <= z; !!m. z = int m ==> P |] ==> P"; |
|
506 by (rtac (major RS nat_0_le RS sym RS minor) 1); |
|
507 qed "nonneg_eq_int"; |
|
508 |
|
509 Goal "#0 <= w ==> (nat w = m) = (w = int m)"; |
|
510 by Auto_tac; |
|
511 qed "nat_eq_iff"; |
|
512 |
|
513 Goal "#0 <= w ==> (m = nat w) = (w = int m)"; |
|
514 by Auto_tac; |
|
515 qed "nat_eq_iff2"; |
|
516 |
|
517 Goal "#0 <= w ==> (nat w < m) = (w < int m)"; |
|
518 by (rtac iffI 1); |
|
519 by (asm_full_simp_tac |
|
520 (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); |
|
521 by (etac (nat_0_le RS subst) 1); |
|
522 by (Simp_tac 1); |
|
523 qed "nat_less_iff"; |
|
524 |
|
525 |
|
526 (*Users don't want to see (int 0), int(Suc 0) or w + - z*) |
|
527 Addsimps [int_0, int_Suc, symmetric zdiff_def]; |
|
528 |
|
529 Goal "nat #0 = 0"; |
|
530 by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
|
531 qed "nat_0"; |
|
532 |
|
533 Goal "nat #1 = 1"; |
|
534 by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
|
535 qed "nat_1"; |
|
536 |
|
537 Goal "nat #2 = 2"; |
|
538 by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
|
539 qed "nat_2"; |
|
540 |
|
541 Goal "#0 <= w ==> (nat w < nat z) = (w<z)"; |
|
542 by (case_tac "neg z" 1); |
|
543 by (auto_tac (claset(), simpset() addsimps [nat_less_iff])); |
|
544 by (auto_tac (claset() addIs [zless_trans], |
|
545 simpset() addsimps [neg_eq_less_0, zle_def])); |
|
546 qed "nat_less_eq_zless"; |
|
547 |
|
548 Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)"; |
|
549 by (auto_tac (claset(), |
|
550 simpset() addsimps [linorder_not_less RS sym, |
|
551 zless_nat_conj])); |
|
552 qed "nat_le_eq_zle"; |
|
553 |
|
554 (*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*) |
|
555 Goal "n<=m --> int m - int n = int (m-n)"; |
|
556 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
557 by Auto_tac; |
|
558 qed_spec_mp "zdiff_int"; |
|
559 |
|
560 |
|
561 (*** abs: absolute value, as an integer ****) |
|
562 |
|
563 (* Simpler: use zabs_def as rewrite rule; |
|
564 but arith_tac is not parameterized by such simp rules |
|
565 *) |
|
566 Goalw [zabs_def] |
|
567 "P(abs(i::int)) = ((#0 <= i --> P i) & (i < #0 --> P(-i)))"; |
|
568 by(Simp_tac 1); |
|
569 qed "zabs_split"; |
|
570 |
|
571 arith_tac_split_thms := !arith_tac_split_thms @ [zabs_split]; |
|
572 |
5 |
573 Goal "abs(abs(x::int)) = abs(x)"; |
6 Goal "abs(abs(x::int)) = abs(x)"; |
574 by(arith_tac 1); |
7 by(arith_tac 1); |
575 qed "abs_abs"; |
8 qed "abs_abs"; |
576 Addsimps [abs_abs]; |
9 Addsimps [abs_abs]; |