author | nipkow |
Thu, 06 Jul 2000 15:38:26 +0200 | |
changeset 9269 | b62d5265b959 |
parent 9214 | 9454f30eacc7 |
child 9436 | 62bb04ab4b01 |
permissions | -rw-r--r-- |
7707 | 1 |
(* Title: HOL/Integ/IntArith.thy |
2 |
ID: $Id$ |
|
3 |
Authors: Larry Paulson and Tobias Nipkow |
|
4 |
||
5 |
Simprocs and decision procedure for linear arithmetic. |
|
6 |
*) |
|
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 |
||
8785 | 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 |
||
8763 | 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 |
||
8799 | 71 |
(*To tidy up the result of a simproc. Only the RHS will be simplified.*) |
8834 | 72 |
Goal "u = u' ==> (t==u) == (t==u')"; |
8799 | 73 |
by Auto_tac; |
74 |
qed "eq_cong2"; |
|
75 |
||
8763 | 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*) |
|
8785 | 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]); |
|
8763 | 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 |
||
8785 | 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 |
||
8763 | 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*) |
|
9063 | 166 |
val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps; |
8763 | 167 |
|
8787 | 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 |
||
8763 | 174 |
(*To let us treat subtraction as addition*) |
175 |
val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus]; |
|
176 |
||
8776 | 177 |
(*Apply the given rewrite (if present) just once*) |
8799 | 178 |
fun trans_tac None = all_tac |
179 |
| trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); |
|
8763 | 180 |
|
8776 | 181 |
fun prove_conv name tacs sg (t, u) = |
8763 | 182 |
if t aconv u then None |
183 |
else |
|
8799 | 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) |
|
8763 | 187 |
handle ERROR => error |
188 |
("The error(s) above occurred while trying to prove " ^ |
|
8799 | 189 |
string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) |
190 |
end; |
|
191 |
||
192 |
fun simplify_meta_eq rules = |
|
193 |
mk_meta_eq o |
|
8834 | 194 |
simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) |
8763 | 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 [] |
|
8799 | 207 |
val trans_tac = trans_tac |
8776 | 208 |
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
8787 | 209 |
zminus_simps@zadd_ac)) |
8763 | 210 |
THEN ALLGOALS |
8776 | 211 |
(simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ |
212 |
bin_simps@zadd_ac@zmult_ac)) |
|
8763 | 213 |
val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
8799 | 214 |
val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
8763 | 215 |
end; |
216 |
||
217 |
||
218 |
structure EqCancelNumerals = CancelNumeralsFun |
|
219 |
(open CancelNumeralsCommon |
|
8776 | 220 |
val prove_conv = prove_conv "inteq_cancel_numerals" |
8763 | 221 |
val mk_bal = HOLogic.mk_eq |
222 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT |
|
8776 | 223 |
val bal_add1 = eq_add_iff1 RS trans |
224 |
val bal_add2 = eq_add_iff2 RS trans |
|
8763 | 225 |
); |
226 |
||
227 |
structure LessCancelNumerals = CancelNumeralsFun |
|
228 |
(open CancelNumeralsCommon |
|
8776 | 229 |
val prove_conv = prove_conv "intless_cancel_numerals" |
8763 | 230 |
val mk_bal = HOLogic.mk_binrel "op <" |
231 |
val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT |
|
8776 | 232 |
val bal_add1 = less_add_iff1 RS trans |
233 |
val bal_add2 = less_add_iff2 RS trans |
|
8763 | 234 |
); |
235 |
||
236 |
structure LeCancelNumerals = CancelNumeralsFun |
|
237 |
(open CancelNumeralsCommon |
|
8776 | 238 |
val prove_conv = prove_conv "intle_cancel_numerals" |
8763 | 239 |
val mk_bal = HOLogic.mk_binrel "op <=" |
240 |
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT |
|
8776 | 241 |
val bal_add1 = le_add_iff1 RS trans |
242 |
val bal_add2 = le_add_iff2 RS trans |
|
8763 | 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"], |
|
8787 | 261 |
LeCancelNumerals.proc)]; |
8763 | 262 |
|
8785 | 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" |
|
8799 | 272 |
val trans_tac = trans_tac |
8785 | 273 |
val norm_tac = ALLGOALS |
274 |
(simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
|
8787 | 275 |
zminus_simps@zadd_ac)) |
8785 | 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)) |
|
8799 | 281 |
val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
8785 | 282 |
end; |
283 |
||
284 |
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); |
|
285 |
||
286 |
val combine_numerals = |
|
287 |
prep_simproc ("int_combine_numerals", |
|
8787 | 288 |
prep_pats ["(i::int) + j", "(i::int) - j"], |
8785 | 289 |
CombineNumerals.proc); |
290 |
||
8763 | 291 |
end; |
292 |
||
293 |
||
294 |
Addsimprocs Int_Numeral_Simprocs.cancel_numerals; |
|
8785 | 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]; |
|
8763 | 299 |
|
300 |
(*examples: |
|
301 |
print_depth 22; |
|
9000 | 302 |
set timing; |
8763 | 303 |
set trace_simp; |
304 |
fun test s = (Goal s; by (Simp_tac 1)); |
|
305 |
||
8785 | 306 |
test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)"; |
307 |
||
8763 | 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 |
||
8785 | 315 |
test "(#2*x - (u*v) + y) - v*#3*u = (w::int)"; |
8763 | 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)"; |
|
8785 | 318 |
test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)"; |
8763 | 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 |
||
8785 | 325 |
test "a + -(b+c) + b = (d::int)"; |
326 |
test "a + -(b+c) - b = (d::int)"; |
|
327 |
||
8763 | 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 |
||
7707 | 338 |
(** Constant folding for integer plus and times **) |
339 |
||
340 |
(*We do not need |
|
8785 | 341 |
structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data); |
7707 | 342 |
structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data); |
8785 | 343 |
because combine_numerals does the same thing*) |
7707 | 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 |
||
8785 | 374 |
Addsimprocs [Nat_Times_Assoc.conv]; |
7707 | 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 @ |
|
8785 | 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, |
|
9079
8e9b7095bf59
some missing simprules for integer linear arithmetic
paulson
parents:
9063
diff
changeset
|
397 |
zmult_minus1, zmult_minus1_right, |
8e9b7095bf59
some missing simprules for integer linear arithmetic
paulson
parents:
9063
diff
changeset
|
398 |
zminus_zadd_distrib, zminus_zminus]; |
7707 | 399 |
|
8785 | 400 |
val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@ |
401 |
Int_Numeral_Simprocs.cancel_numerals; |
|
7707 | 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 |
|
8796 | 417 |
addsimprocs simprocs |
418 |
addcongs [if_weak_cong]; |
|
7707 | 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); |
|
8257 | 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); |
|
7707 | 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 |
||
8796 | 513 |
Goal "#0 <= w ==> (m = nat w) = (w = int m)"; |
514 |
by Auto_tac; |
|
515 |
qed "nat_eq_iff2"; |
|
516 |
||
7707 | 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 |
||
9214 | 561 |
(*** abs: absolute value, as an integer ****) |
562 |
||
9269 | 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)))"; |
|
9214 | 568 |
by(Simp_tac 1); |
9269 | 569 |
qed "zabs_split"; |
570 |
||
571 |
arith_tac_split_thms := !arith_tac_split_thms @ [zabs_split]; |
|
572 |
||
573 |
Goal "abs(abs(x::int)) = abs(x)"; |
|
574 |
by(arith_tac 1); |
|
9214 | 575 |
qed "abs_abs"; |
576 |
Addsimps [abs_abs]; |
|
577 |
||
9269 | 578 |
Goal "abs(-(x::int)) = abs(x)"; |
579 |
by(arith_tac 1); |
|
9214 | 580 |
qed "abs_minus"; |
581 |
Addsimps [abs_minus]; |
|
582 |
||
9269 | 583 |
Goal "abs(x+y) <= abs(x) + abs(y::int)"; |
584 |
by(arith_tac 1); |
|
585 |
qed "triangle_ineq"; |
|
586 |
||
9214 | 587 |
|
9063 | 588 |
(*** Some convenient biconditionals for products of signs ***) |
7707 | 589 |
|
9063 | 590 |
Goal "[| (#0::int) < i; #0 < j |] ==> #0 < i*j"; |
591 |
by (dtac zmult_zless_mono1 1); |
|
592 |
by Auto_tac; |
|
593 |
qed "zmult_pos"; |
|
7707 | 594 |
|
9063 | 595 |
Goal "[| i < (#0::int); j < #0 |] ==> #0 < i*j"; |
596 |
by (dtac zmult_zless_mono1_neg 1); |
|
597 |
by Auto_tac; |
|
598 |
qed "zmult_neg"; |
|
7707 | 599 |
|
9063 | 600 |
Goal "[| (#0::int) < i; j < #0 |] ==> i*j < #0"; |
601 |
by (dtac zmult_zless_mono1_neg 1); |
|
602 |
by Auto_tac; |
|
603 |
qed "zmult_pos_neg"; |
|
7707 | 604 |
|
9063 | 605 |
Goal "((#0::int) < x*y) = (#0 < x & #0 < y | x < #0 & y < #0)"; |
606 |
by (auto_tac (claset(), |
|
607 |
simpset() addsimps [order_le_less, linorder_not_less, |
|
608 |
zmult_pos, zmult_neg])); |
|
609 |
by (ALLGOALS (rtac ccontr)); |
|
610 |
by (auto_tac (claset(), |
|
611 |
simpset() addsimps [order_le_less, linorder_not_less])); |
|
612 |
by (ALLGOALS (etac rev_mp)); |
|
613 |
by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac)); |
|
614 |
by (auto_tac (claset() addDs [order_less_not_sym], |
|
615 |
simpset() addsimps [zmult_commute])); |
|
616 |
qed "int_0_less_mult_iff"; |
|
7707 | 617 |
|
9063 | 618 |
Goal "((#0::int) <= x*y) = (#0 <= x & #0 <= y | x <= #0 & y <= #0)"; |
619 |
by (auto_tac (claset(), |
|
620 |
simpset() addsimps [order_le_less, linorder_not_less, |
|
621 |
int_0_less_mult_iff])); |
|
622 |
qed "int_0_le_mult_iff"; |
|
7707 | 623 |
|
9063 | 624 |
Goal "(x*y < (#0::int)) = (#0 < x & y < #0 | x < #0 & #0 < y)"; |
625 |
by (auto_tac (claset(), |
|
626 |
simpset() addsimps [int_0_le_mult_iff, |
|
627 |
linorder_not_le RS sym])); |
|
628 |
by (auto_tac (claset() addDs [order_less_not_sym], |
|
629 |
simpset() addsimps [linorder_not_le])); |
|
630 |
qed "zmult_less_0_iff"; |
|
7707 | 631 |
|
9063 | 632 |
Goal "(x*y <= (#0::int)) = (#0 <= x & y <= #0 | x <= #0 & #0 <= y)"; |
633 |
by (auto_tac (claset() addDs [order_less_not_sym], |
|
634 |
simpset() addsimps [int_0_less_mult_iff, |
|
635 |
linorder_not_less RS sym])); |
|
636 |
qed "zmult_le_0_iff"; |
|
637 |