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 |
|
|
9 |
(*** Simprocs for numeric literals ***)
|
|
10 |
|
|
11 |
(** Combining of literal coefficients in sums of products **)
|
|
12 |
|
|
13 |
Goal "(x < y) = (x-y < (#0::int))";
|
|
14 |
by (simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
15 |
qed "zless_iff_zdiff_zless_0";
|
|
16 |
|
|
17 |
Goal "(x = y) = (x-y = (#0::int))";
|
|
18 |
by (simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
19 |
qed "eq_iff_zdiff_eq_0";
|
|
20 |
|
|
21 |
Goal "(x <= y) = (x-y <= (#0::int))";
|
|
22 |
by (simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
23 |
qed "zle_iff_zdiff_zle_0";
|
|
24 |
|
|
25 |
|
|
26 |
structure Int_CC_Data : COMBINE_COEFF_DATA =
|
|
27 |
struct
|
|
28 |
val ss = HOL_ss
|
|
29 |
val eq_reflection = eq_reflection
|
|
30 |
val thy = Bin.thy
|
|
31 |
val T = HOLogic.intT
|
|
32 |
|
|
33 |
val trans = trans
|
|
34 |
val add_ac = zadd_ac
|
|
35 |
val diff_def = zdiff_def
|
|
36 |
val minus_add_distrib = zminus_zadd_distrib
|
|
37 |
val minus_minus = zminus_zminus
|
|
38 |
val mult_commute = zmult_commute
|
|
39 |
val mult_1_right = zmult_1_right
|
|
40 |
val add_mult_distrib = zadd_zmult_distrib2
|
|
41 |
val diff_mult_distrib = zdiff_zmult_distrib2
|
|
42 |
val mult_minus_right = zmult_zminus_right
|
|
43 |
|
|
44 |
val rel_iff_rel_0_rls = [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
|
|
45 |
zle_iff_zdiff_zle_0]
|
|
46 |
fun dest_eqI th =
|
|
47 |
#1 (HOLogic.dest_bin "op =" HOLogic.boolT
|
|
48 |
(HOLogic.dest_Trueprop (concl_of th)))
|
|
49 |
|
|
50 |
end;
|
|
51 |
|
|
52 |
structure Int_CC = Combine_Coeff (Int_CC_Data);
|
|
53 |
|
|
54 |
Addsimprocs [Int_CC.sum_conv, Int_CC.rel_conv];
|
|
55 |
|
|
56 |
|
|
57 |
(** Constant folding for integer plus and times **)
|
|
58 |
|
|
59 |
(*We do not need
|
|
60 |
structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data);
|
|
61 |
because cancel_coeffs does the same thing*)
|
|
62 |
|
|
63 |
structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
|
|
64 |
struct
|
|
65 |
val ss = HOL_ss
|
|
66 |
val eq_reflection = eq_reflection
|
|
67 |
val thy = Bin.thy
|
|
68 |
val T = HOLogic.intT
|
|
69 |
val plus = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
|
|
70 |
val add_ac = zmult_ac
|
|
71 |
end;
|
|
72 |
|
|
73 |
structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data);
|
|
74 |
|
|
75 |
Addsimprocs [Int_Times_Assoc.conv];
|
|
76 |
|
|
77 |
|
|
78 |
(** The same for the naturals **)
|
|
79 |
|
|
80 |
structure Nat_Plus_Assoc_Data : ASSOC_FOLD_DATA =
|
|
81 |
struct
|
|
82 |
val ss = HOL_ss
|
|
83 |
val eq_reflection = eq_reflection
|
|
84 |
val thy = Bin.thy
|
|
85 |
val T = HOLogic.natT
|
|
86 |
val plus = Const ("op +", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
|
|
87 |
val add_ac = add_ac
|
|
88 |
end;
|
|
89 |
|
|
90 |
structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
|
|
91 |
|
|
92 |
structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
|
|
93 |
struct
|
|
94 |
val ss = HOL_ss
|
|
95 |
val eq_reflection = eq_reflection
|
|
96 |
val thy = Bin.thy
|
|
97 |
val T = HOLogic.natT
|
|
98 |
val plus = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
|
|
99 |
val add_ac = mult_ac
|
|
100 |
end;
|
|
101 |
|
|
102 |
structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data);
|
|
103 |
|
|
104 |
Addsimprocs [Nat_Plus_Assoc.conv, Nat_Times_Assoc.conv];
|
|
105 |
|
|
106 |
|
|
107 |
|
|
108 |
(*** decision procedure for linear arithmetic ***)
|
|
109 |
|
|
110 |
(*---------------------------------------------------------------------------*)
|
|
111 |
(* Linear arithmetic *)
|
|
112 |
(*---------------------------------------------------------------------------*)
|
|
113 |
|
|
114 |
(*
|
|
115 |
Instantiation of the generic linear arithmetic package for int.
|
|
116 |
FIXME: multiplication with constants (eg #2 * i) does not work yet.
|
|
117 |
Solution: the cancellation simprocs in Int_Cancel should be able to deal with
|
|
118 |
it (eg simplify #3 * i <= 2 * i to i <= #0) or `add_rules' below should
|
|
119 |
include rules for turning multiplication with constants into addition.
|
|
120 |
(The latter option is very inefficient!)
|
|
121 |
*)
|
|
122 |
|
|
123 |
(* Update parameters of arithmetic prover *)
|
|
124 |
let
|
|
125 |
|
|
126 |
(* reduce contradictory <= to False *)
|
|
127 |
val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
|
|
128 |
[int_0,zmult_0,zmult_0_right];
|
|
129 |
|
|
130 |
val simprocs = [Int_Cancel.sum_conv, Int_Cancel.rel_conv,
|
|
131 |
Int_CC.sum_conv, Int_CC.rel_conv];
|
|
132 |
|
|
133 |
val add_mono_thms =
|
|
134 |
map (fn s => prove_goal Int.thy s
|
|
135 |
(fn prems => [cut_facts_tac prems 1,
|
|
136 |
asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
|
|
137 |
["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
|
|
138 |
"(i = j) & (k <= l) ==> i + k <= j + (l::int)",
|
|
139 |
"(i <= j) & (k = l) ==> i + k <= j + (l::int)",
|
|
140 |
"(i = j) & (k = l) ==> i + k = j + (l::int)"
|
|
141 |
];
|
|
142 |
|
|
143 |
in
|
|
144 |
LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
|
|
145 |
LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2];
|
|
146 |
LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
|
|
147 |
addsimprocs simprocs;
|
|
148 |
LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)]
|
|
149 |
end;
|
|
150 |
|
|
151 |
let
|
|
152 |
val int_arith_simproc_pats =
|
|
153 |
map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT))
|
|
154 |
["(m::int) < n","(m::int) <= n", "(m::int) = n"];
|
|
155 |
|
|
156 |
val fast_int_arith_simproc = mk_simproc
|
|
157 |
"fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
|
|
158 |
in
|
|
159 |
Addsimprocs [fast_int_arith_simproc]
|
|
160 |
end;
|
|
161 |
|
|
162 |
(* Some test data
|
|
163 |
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
|
|
164 |
by (fast_arith_tac 1);
|
|
165 |
Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
|
|
166 |
by (fast_arith_tac 1);
|
|
167 |
Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
|
|
168 |
by (fast_arith_tac 1);
|
|
169 |
Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
|
|
170 |
by (fast_arith_tac 1);
|
|
171 |
Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
|
|
172 |
\ ==> a+a <= j+j";
|
|
173 |
by (fast_arith_tac 1);
|
|
174 |
Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
|
|
175 |
\ ==> a+a - - #-1 < j+j - #3";
|
|
176 |
by (fast_arith_tac 1);
|
|
177 |
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
|
|
178 |
by (arith_tac 1);
|
|
179 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
|
|
180 |
\ ==> a <= l";
|
|
181 |
by (fast_arith_tac 1);
|
|
182 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
|
|
183 |
\ ==> a+a+a+a <= l+l+l+l";
|
|
184 |
by (fast_arith_tac 1);
|
|
185 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
|
|
186 |
\ ==> a+a+a+a+a <= l+l+l+l+i";
|
|
187 |
by (fast_arith_tac 1);
|
|
188 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
|
|
189 |
\ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
|
|
190 |
by (fast_arith_tac 1);
|
|
191 |
*)
|
|
192 |
|
|
193 |
(*---------------------------------------------------------------------------*)
|
|
194 |
(* End of linear arithmetic *)
|
|
195 |
(*---------------------------------------------------------------------------*)
|
|
196 |
|
|
197 |
(** Simplification of arithmetic when nested to the right **)
|
|
198 |
|
|
199 |
Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)";
|
|
200 |
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
|
|
201 |
qed "add_number_of_left";
|
|
202 |
|
|
203 |
Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)";
|
|
204 |
by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
|
|
205 |
qed "mult_number_of_left";
|
|
206 |
|
|
207 |
Addsimps [add_number_of_left, mult_number_of_left];
|
|
208 |
|
|
209 |
(** Simplification of inequalities involving numerical constants **)
|
|
210 |
|
|
211 |
Goal "(w <= z + (#1::int)) = (w<=z | w = z + (#1::int))";
|
|
212 |
by (arith_tac 1);
|
|
213 |
qed "zle_add1_eq";
|
|
214 |
|
|
215 |
Goal "(w <= z - (#1::int)) = (w<(z::int))";
|
|
216 |
by (arith_tac 1);
|
|
217 |
qed "zle_diff1_eq";
|
|
218 |
Addsimps [zle_diff1_eq];
|
|
219 |
|
|
220 |
(*2nd premise can be proved automatically if v is a literal*)
|
|
221 |
Goal "[| w <= z; #0 <= v |] ==> w <= z + (v::int)";
|
|
222 |
by (fast_arith_tac 1);
|
|
223 |
qed "zle_imp_zle_zadd";
|
|
224 |
|
|
225 |
Goal "w <= z ==> w <= z + (#1::int)";
|
|
226 |
by (fast_arith_tac 1);
|
|
227 |
qed "zle_imp_zle_zadd1";
|
|
228 |
|
|
229 |
(*2nd premise can be proved automatically if v is a literal*)
|
|
230 |
Goal "[| w < z; #0 <= v |] ==> w < z + (v::int)";
|
|
231 |
by (fast_arith_tac 1);
|
|
232 |
qed "zless_imp_zless_zadd";
|
|
233 |
|
|
234 |
Goal "w < z ==> w < z + (#1::int)";
|
|
235 |
by (fast_arith_tac 1);
|
|
236 |
qed "zless_imp_zless_zadd1";
|
|
237 |
|
|
238 |
Goal "(w < z + #1) = (w<=(z::int))";
|
|
239 |
by (arith_tac 1);
|
|
240 |
qed "zle_add1_eq_le";
|
|
241 |
Addsimps [zle_add1_eq_le];
|
|
242 |
|
|
243 |
Goal "(z = z + w) = (w = (#0::int))";
|
|
244 |
by (arith_tac 1);
|
|
245 |
qed "zadd_left_cancel0";
|
|
246 |
Addsimps [zadd_left_cancel0];
|
|
247 |
|
|
248 |
(*LOOPS as a simprule!*)
|
|
249 |
Goal "[| w + v < z; #0 <= v |] ==> w < (z::int)";
|
|
250 |
by (fast_arith_tac 1);
|
|
251 |
qed "zless_zadd_imp_zless";
|
|
252 |
|
|
253 |
(*LOOPS as a simprule! Analogous to Suc_lessD*)
|
|
254 |
Goal "w + #1 < z ==> w < (z::int)";
|
|
255 |
by (fast_arith_tac 1);
|
|
256 |
qed "zless_zadd1_imp_zless";
|
|
257 |
|
|
258 |
Goal "w + #-1 = w - (#1::int)";
|
|
259 |
by (Simp_tac 1);
|
|
260 |
qed "zplus_minus1_conv";
|
|
261 |
|
|
262 |
|
|
263 |
(* nat *)
|
|
264 |
|
|
265 |
Goal "#0 <= z ==> int (nat z) = z";
|
|
266 |
by (asm_full_simp_tac
|
|
267 |
(simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1);
|
|
268 |
qed "nat_0_le";
|
|
269 |
|
|
270 |
Goal "z <= #0 ==> nat z = 0";
|
|
271 |
by (case_tac "z = #0" 1);
|
|
272 |
by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1);
|
|
273 |
by (asm_full_simp_tac
|
|
274 |
(simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
|
|
275 |
qed "nat_le_0";
|
|
276 |
|
|
277 |
Addsimps [nat_0_le, nat_le_0];
|
|
278 |
|
|
279 |
val [major,minor] = Goal "[| #0 <= z; !!m. z = int m ==> P |] ==> P";
|
|
280 |
by (rtac (major RS nat_0_le RS sym RS minor) 1);
|
|
281 |
qed "nonneg_eq_int";
|
|
282 |
|
|
283 |
Goal "#0 <= w ==> (nat w = m) = (w = int m)";
|
|
284 |
by Auto_tac;
|
|
285 |
qed "nat_eq_iff";
|
|
286 |
|
|
287 |
Goal "#0 <= w ==> (nat w < m) = (w < int m)";
|
|
288 |
by (rtac iffI 1);
|
|
289 |
by (asm_full_simp_tac
|
|
290 |
(simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
|
|
291 |
by (etac (nat_0_le RS subst) 1);
|
|
292 |
by (Simp_tac 1);
|
|
293 |
qed "nat_less_iff";
|
|
294 |
|
|
295 |
|
|
296 |
(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
|
|
297 |
Addsimps [int_0, int_Suc, symmetric zdiff_def];
|
|
298 |
|
|
299 |
Goal "nat #0 = 0";
|
|
300 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
|
|
301 |
qed "nat_0";
|
|
302 |
|
|
303 |
Goal "nat #1 = 1";
|
|
304 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
|
|
305 |
qed "nat_1";
|
|
306 |
|
|
307 |
Goal "nat #2 = 2";
|
|
308 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
|
|
309 |
qed "nat_2";
|
|
310 |
|
|
311 |
Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
|
|
312 |
by (case_tac "neg z" 1);
|
|
313 |
by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
|
|
314 |
by (auto_tac (claset() addIs [zless_trans],
|
|
315 |
simpset() addsimps [neg_eq_less_0, zle_def]));
|
|
316 |
qed "nat_less_eq_zless";
|
|
317 |
|
|
318 |
Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)";
|
|
319 |
by (auto_tac (claset(),
|
|
320 |
simpset() addsimps [linorder_not_less RS sym,
|
|
321 |
zless_nat_conj]));
|
|
322 |
qed "nat_le_eq_zle";
|
|
323 |
|
|
324 |
(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
|
|
325 |
Goal "n<=m --> int m - int n = int (m-n)";
|
|
326 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
|
|
327 |
by Auto_tac;
|
|
328 |
qed_spec_mp "zdiff_int";
|
|
329 |
|
|
330 |
|
|
331 |
(** Products of signs **)
|
|
332 |
|
|
333 |
Goal "(m::int) < #0 ==> (#0 < m*n) = (n < #0)";
|
|
334 |
by Auto_tac;
|
|
335 |
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
|
|
336 |
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
|
|
337 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
|
|
338 |
by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1_neg],
|
|
339 |
simpset()addsimps [order_le_less, zmult_commute]) 1);
|
|
340 |
qed "neg_imp_zmult_pos_iff";
|
|
341 |
|
|
342 |
Goal "(m::int) < #0 ==> (m*n < #0) = (#0 < n)";
|
|
343 |
by Auto_tac;
|
|
344 |
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
|
|
345 |
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
|
|
346 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
|
|
347 |
by (force_tac (claset() addDs [zmult_zless_mono1_neg],
|
|
348 |
simpset() addsimps [order_le_less]) 1);
|
|
349 |
qed "neg_imp_zmult_neg_iff";
|
|
350 |
|
|
351 |
Goal "#0 < (m::int) ==> (m*n < #0) = (n < #0)";
|
|
352 |
by Auto_tac;
|
|
353 |
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
|
|
354 |
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
|
|
355 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
|
|
356 |
by (force_tac (claset() addDs [zmult_zless_mono1],
|
|
357 |
simpset() addsimps [order_le_less]) 1);
|
|
358 |
qed "pos_imp_zmult_neg_iff";
|
|
359 |
|
|
360 |
Goal "#0 < (m::int) ==> (#0 < m*n) = (#0 < n)";
|
|
361 |
by Auto_tac;
|
|
362 |
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
|
|
363 |
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
|
|
364 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
|
|
365 |
by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1],
|
|
366 |
simpset() addsimps [order_le_less, zmult_commute]) 1);
|
|
367 |
qed "pos_imp_zmult_pos_iff";
|
|
368 |
|
|
369 |
(** <= versions of the theorems above **)
|
|
370 |
|
|
371 |
Goal "(m::int) < #0 ==> (m*n <= #0) = (#0 <= n)";
|
|
372 |
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
|
|
373 |
neg_imp_zmult_pos_iff]) 1);
|
|
374 |
qed "neg_imp_zmult_nonpos_iff";
|
|
375 |
|
|
376 |
Goal "(m::int) < #0 ==> (#0 <= m*n) = (n <= #0)";
|
|
377 |
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
|
|
378 |
neg_imp_zmult_neg_iff]) 1);
|
|
379 |
qed "neg_imp_zmult_nonneg_iff";
|
|
380 |
|
|
381 |
Goal "#0 < (m::int) ==> (m*n <= #0) = (n <= #0)";
|
|
382 |
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
|
|
383 |
pos_imp_zmult_pos_iff]) 1);
|
|
384 |
qed "pos_imp_zmult_nonpos_iff";
|
|
385 |
|
|
386 |
Goal "#0 < (m::int) ==> (#0 <= m*n) = (#0 <= n)";
|
|
387 |
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
|
|
388 |
pos_imp_zmult_neg_iff]) 1);
|
|
389 |
qed "pos_imp_zmult_nonneg_iff";
|