|
1 (* Title: HOL/Integ/Presburger.thy |
|
2 ID: $Id$ |
|
3 Author: Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 File containing necessary theorems for the proof |
|
7 generation for Cooper Algorithm |
|
8 *) |
|
9 |
|
10 theory Presburger = NatSimprocs |
|
11 files |
|
12 ("cooper_dec.ML") |
|
13 ("cooper_proof.ML") |
|
14 ("qelim.ML") |
|
15 ("presburger.ML"): |
|
16 |
|
17 (* Theorem for unitifying the coeffitients of x in an existential formula*) |
|
18 |
|
19 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)" |
|
20 apply (rule iffI) |
|
21 apply (erule exE) |
|
22 apply (rule_tac x = "l * x" in exI) |
|
23 apply simp |
|
24 apply (erule exE) |
|
25 apply (erule conjE) |
|
26 apply (erule dvdE) |
|
27 apply (rule_tac x = k in exI) |
|
28 apply simp |
|
29 done |
|
30 |
|
31 lemma uminus_dvd_conv: "(d dvd (t::int)) = (-d dvd t)" |
|
32 apply(unfold dvd_def) |
|
33 apply(rule iffI) |
|
34 apply(clarsimp) |
|
35 apply(rename_tac k) |
|
36 apply(rule_tac x = "-k" in exI) |
|
37 apply simp |
|
38 apply(clarsimp) |
|
39 apply(rename_tac k) |
|
40 apply(rule_tac x = "-k" in exI) |
|
41 apply simp |
|
42 done |
|
43 |
|
44 lemma uminus_dvd_conv': "(d dvd (t::int)) = (d dvd -t)" |
|
45 apply(unfold dvd_def) |
|
46 apply(rule iffI) |
|
47 apply(clarsimp) |
|
48 apply(rule_tac x = "-k" in exI) |
|
49 apply simp |
|
50 apply(clarsimp) |
|
51 apply(rule_tac x = "-k" in exI) |
|
52 apply simp |
|
53 done |
|
54 |
|
55 |
|
56 |
|
57 (*Theorems for the combination of proofs of the equality of P and P_m for integers x less than some integer z.*) |
|
58 |
|
59 theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
|
60 \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
|
61 \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))" |
|
62 apply (erule exE)+ |
|
63 apply (rule_tac x = "min z1 z2" in exI) |
|
64 apply simp |
|
65 done |
|
66 |
|
67 |
|
68 theorem eq_minf_disjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
|
69 \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
|
70 \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))" |
|
71 |
|
72 apply (erule exE)+ |
|
73 apply (rule_tac x = "min z1 z2" in exI) |
|
74 apply simp |
|
75 done |
|
76 |
|
77 |
|
78 (*Theorems for the combination of proofs of the equality of P and P_m for integers x greather than some integer z.*) |
|
79 |
|
80 theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
|
81 \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
|
82 \<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))" |
|
83 apply (erule exE)+ |
|
84 apply (rule_tac x = "max z1 z2" in exI) |
|
85 apply simp |
|
86 done |
|
87 |
|
88 |
|
89 theorem eq_pinf_disjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
|
90 \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
|
91 \<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))" |
|
92 apply (erule exE)+ |
|
93 apply (rule_tac x = "max z1 z2" in exI) |
|
94 apply simp |
|
95 done |
|
96 (*=============================================================================*) |
|
97 (*Theorems for the combination of proofs of the modulo D property for P |
|
98 pluusinfinity*) |
|
99 (* FIXME : This is THE SAME theorem as for the minusinf version, but with +k.. instead of -k.. In the future replace these both with only one*) |
|
100 |
|
101 theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow> |
|
102 \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow> |
|
103 \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))" |
|
104 by simp |
|
105 |
|
106 |
|
107 theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow> |
|
108 \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow> |
|
109 \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))" |
|
110 by simp |
|
111 |
|
112 (*=============================================================================*) |
|
113 (*This is one of the cases where the simplifed formula is prooved to habe some property |
|
114 (in relation to P_m) but we need to proove the property for the original formula (P_m)*) |
|
115 (*FIXME : This is exaclty the same thm as for minusinf.*) |
|
116 lemma pinf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x)) ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) " |
|
117 by blast |
|
118 |
|
119 |
|
120 |
|
121 (*=============================================================================*) |
|
122 (*Theorems for the combination of proofs of the modulo D property for P |
|
123 minusinfinity*) |
|
124 |
|
125 theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow> |
|
126 \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow> |
|
127 \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))" |
|
128 by simp |
|
129 |
|
130 |
|
131 theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow> |
|
132 \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow> |
|
133 \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))" |
|
134 by simp |
|
135 |
|
136 (*=============================================================================*) |
|
137 (*This is one of the cases where the simplifed formula is prooved to habe some property |
|
138 (in relation to P_m) but we need to proove the property for the original formula (P_m)*) |
|
139 |
|
140 lemma minf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x)) ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) " |
|
141 by blast |
|
142 |
|
143 (*=============================================================================*) |
|
144 |
|
145 (*theorem needed for prooving at runtime divide properties using the arithmetic tatic |
|
146 (who knows only about modulo = 0)*) |
|
147 |
|
148 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
|
149 by(simp add:dvd_def zmod_eq_0_iff) |
|
150 |
|
151 (*=============================================================================*) |
|
152 |
|
153 |
|
154 |
|
155 (*Theorems used for the combination of proof for the backwards direction of cooper's |
|
156 theorem. they rely exclusively on Predicate calculus.*) |
|
157 |
|
158 lemma not_ast_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P1(x) --> P1(x + d)) |
|
159 ==> |
|
160 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d)) |
|
161 ==> |
|
162 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<or> P2(x)) --> (P1(x + d) \<or> P2(x + d))) " |
|
163 by blast |
|
164 |
|
165 |
|
166 |
|
167 lemma not_ast_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a- j)) --> P1(x) --> P1(x + d)) |
|
168 ==> |
|
169 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d)) |
|
170 ==> |
|
171 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<and> P2(x)) --> (P1(x + d) |
|
172 \<and> P2(x + d))) " |
|
173 by blast |
|
174 |
|
175 lemma not_ast_p_Q_elim: " |
|
176 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d)) |
|
177 ==> ( P = Q ) |
|
178 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))" |
|
179 by blast |
|
180 (*=============================================================================*) |
|
181 |
|
182 |
|
183 (*Theorems used for the combination of proof for the backwards direction of cooper's |
|
184 theorem. they rely exclusively on Predicate calculus.*) |
|
185 |
|
186 lemma not_bst_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d)) |
|
187 ==> |
|
188 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d)) |
|
189 ==> |
|
190 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<or> P2(x)) --> (P1(x - d) |
|
191 \<or> P2(x-d))) " |
|
192 by blast |
|
193 |
|
194 |
|
195 |
|
196 lemma not_bst_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d)) |
|
197 ==> |
|
198 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d)) |
|
199 ==> |
|
200 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<and> P2(x)) --> (P1(x - d) |
|
201 \<and> P2(x-d))) " |
|
202 by blast |
|
203 |
|
204 lemma not_bst_p_Q_elim: " |
|
205 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) |
|
206 ==> ( P = Q ) |
|
207 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))" |
|
208 by blast |
|
209 (*=============================================================================*) |
|
210 (*The Theorem for the second proof step- about bset. it is trivial too. *) |
|
211 lemma bst_thm: " (EX (j::int) : {1..d}. EX (b::int) : B. P (b+j) )--> (EX x::int. P (x)) " |
|
212 by blast |
|
213 |
|
214 (*The Theorem for the second proof step- about aset. it is trivial too. *) |
|
215 lemma ast_thm: " (EX (j::int) : {1..d}. EX (a::int) : A. P (a - j) )--> (EX x::int. P (x)) " |
|
216 by blast |
|
217 |
|
218 |
|
219 (*=============================================================================*) |
|
220 (*This is the first direction of cooper's theorem*) |
|
221 lemma cooper_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((R|Q) --> (EX x::int. P x )) " |
|
222 by blast |
|
223 |
|
224 (*=============================================================================*) |
|
225 (*The full cooper's theoorem in its equivalence Form- Given the premisses it is trivial |
|
226 too, it relies exclusively on prediacte calculus.*) |
|
227 lemma cooper_eq_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((~Q) |
|
228 --> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q " |
|
229 by blast |
|
230 |
|
231 (*=============================================================================*) |
|
232 (*Some of the atomic theorems generated each time the atom does not depend on x, they |
|
233 are trivial.*) |
|
234 |
|
235 lemma fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) " |
|
236 by blast |
|
237 |
|
238 lemma fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)" |
|
239 by blast |
|
240 |
|
241 lemma not_bst_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> fm --> fm" |
|
242 by blast |
|
243 |
|
244 |
|
245 |
|
246 lemma fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) " |
|
247 by blast |
|
248 |
|
249 (* The next 2 thms are the same as the minusinf version*) |
|
250 lemma fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)" |
|
251 by blast |
|
252 |
|
253 lemma not_ast_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> fm --> fm" |
|
254 by blast |
|
255 |
|
256 |
|
257 (* Theorems to be deleted from simpset when proving simplified formulaes*) |
|
258 lemma P_eqtrue: "(P=True) = P" |
|
259 by rules |
|
260 |
|
261 lemma P_eqfalse: "(P=False) = (~P)" |
|
262 by rules |
|
263 |
|
264 (*=============================================================================*) |
|
265 |
|
266 (*Theorems for the generation of the bachwards direction of cooper's theorem*) |
|
267 (*These are the 6 interesting atomic cases which have to be proved relying on the |
|
268 properties of B-set ant the arithmetic and contradiction proofs*) |
|
269 |
|
270 lemma not_bst_p_lt: "0 < (d::int) ==> |
|
271 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> ( 0 < -x + a) --> (0 < -(x - d) + a )" |
|
272 by arith |
|
273 |
|
274 lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow> |
|
275 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> (0 < (x) + a) --> ( 0 < (x - d) + a)" |
|
276 apply clarsimp |
|
277 apply(rule ccontr) |
|
278 apply(drule_tac x = "x+a" in bspec) |
|
279 apply(simp add:atLeastAtMost_iff) |
|
280 apply(drule_tac x = "-a" in bspec) |
|
281 apply assumption |
|
282 apply(simp) |
|
283 done |
|
284 |
|
285 lemma not_bst_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a - 1 \<rbrakk> \<Longrightarrow> |
|
286 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> (0 = x + a) --> (0 = (x - d) + a )" |
|
287 apply clarsimp |
|
288 apply(subgoal_tac "x = -a") |
|
289 prefer 2 apply arith |
|
290 apply(drule_tac x = "1" in bspec) |
|
291 apply(simp add:atLeastAtMost_iff) |
|
292 apply(drule_tac x = "-a- 1" in bspec) |
|
293 apply assumption |
|
294 apply(simp) |
|
295 done |
|
296 |
|
297 |
|
298 lemma not_bst_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow> |
|
299 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> ~(0 = x + a) --> ~(0 = (x - d) + a)" |
|
300 apply clarsimp |
|
301 apply(subgoal_tac "x = -a+d") |
|
302 prefer 2 apply arith |
|
303 apply(drule_tac x = "d" in bspec) |
|
304 apply(simp add:atLeastAtMost_iff) |
|
305 apply(drule_tac x = "-a" in bspec) |
|
306 apply assumption |
|
307 apply(simp) |
|
308 done |
|
309 |
|
310 |
|
311 lemma not_bst_p_dvd: "(d1::int) dvd d ==> |
|
312 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> d1 dvd (x + a) --> d1 dvd ((x - d) + a )" |
|
313 apply(clarsimp simp add:dvd_def) |
|
314 apply(rename_tac m) |
|
315 apply(rule_tac x = "m - k" in exI) |
|
316 apply(simp add:int_distrib) |
|
317 done |
|
318 |
|
319 lemma not_bst_p_ndvd: "(d1::int) dvd d ==> |
|
320 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> ~(d1 dvd (x + a)) --> ~(d1 dvd ((x - d) + a ))" |
|
321 apply(clarsimp simp add:dvd_def) |
|
322 apply(rename_tac m) |
|
323 apply(erule_tac x = "m + k" in allE) |
|
324 apply(simp add:int_distrib) |
|
325 done |
|
326 |
|
327 |
|
328 |
|
329 (*Theorems for the generation of the bachwards direction of cooper's theorem*) |
|
330 (*These are the 6 interesting atomic cases which have to be proved relying on the |
|
331 properties of A-set ant the arithmetic and contradiction proofs*) |
|
332 |
|
333 lemma not_ast_p_gt: "0 < (d::int) ==> |
|
334 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> ( 0 < x + t) --> (0 < (x + d) + t )" |
|
335 by arith |
|
336 |
|
337 |
|
338 lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow> |
|
339 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> (0 < -x + t) --> ( 0 < -(x + d) + t)" |
|
340 apply clarsimp |
|
341 apply (rule ccontr) |
|
342 apply (drule_tac x = "t-x" in bspec) |
|
343 apply simp |
|
344 apply (drule_tac x = "t" in bspec) |
|
345 apply assumption |
|
346 apply simp |
|
347 done |
|
348 |
|
349 lemma not_ast_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t + 1 \<rbrakk> \<Longrightarrow> |
|
350 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> (0 = x + t) --> (0 = (x + d) + t )" |
|
351 apply clarsimp |
|
352 apply (drule_tac x="1" in bspec) |
|
353 apply simp |
|
354 apply (drule_tac x="- t + 1" in bspec) |
|
355 apply assumption |
|
356 apply(subgoal_tac "x = -t") |
|
357 prefer 2 apply arith |
|
358 apply simp |
|
359 done |
|
360 |
|
361 lemma not_ast_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t \<rbrakk> \<Longrightarrow> |
|
362 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> ~(0 = x + t) --> ~(0 = (x + d) + t)" |
|
363 apply clarsimp |
|
364 apply (subgoal_tac "x = -t-d") |
|
365 prefer 2 apply arith |
|
366 apply (drule_tac x = "d" in bspec) |
|
367 apply simp |
|
368 apply (drule_tac x = "-t" in bspec) |
|
369 apply assumption |
|
370 apply simp |
|
371 done |
|
372 |
|
373 lemma not_ast_p_dvd: "(d1::int) dvd d ==> |
|
374 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> d1 dvd (x + t) --> d1 dvd ((x + d) + t )" |
|
375 apply(clarsimp simp add:dvd_def) |
|
376 apply(rename_tac m) |
|
377 apply(rule_tac x = "m + k" in exI) |
|
378 apply(simp add:int_distrib) |
|
379 done |
|
380 |
|
381 lemma not_ast_p_ndvd: "(d1::int) dvd d ==> |
|
382 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> ~(d1 dvd (x + t)) --> ~(d1 dvd ((x + d) + t ))" |
|
383 apply(clarsimp simp add:dvd_def) |
|
384 apply(rename_tac m) |
|
385 apply(erule_tac x = "m - k" in allE) |
|
386 apply(simp add:int_distrib) |
|
387 done |
|
388 |
|
389 |
|
390 |
|
391 (*=============================================================================*) |
|
392 (*These are the atomic cases for the proof generation for the modulo D property for P |
|
393 plusinfinity*) |
|
394 (*They are fully based on arithmetics*) |
|
395 |
|
396 lemma dvd_modd_pinf: "((d::int) dvd d1) ==> |
|
397 (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))" |
|
398 apply(clarsimp simp add:dvd_def) |
|
399 apply(rule iffI) |
|
400 apply(clarsimp) |
|
401 apply(rename_tac n m) |
|
402 apply(rule_tac x = "m + n*k" in exI) |
|
403 apply(simp add:int_distrib) |
|
404 apply(clarsimp) |
|
405 apply(rename_tac n m) |
|
406 apply(rule_tac x = "m - n*k" in exI) |
|
407 apply(simp add:int_distrib zmult_ac) |
|
408 done |
|
409 |
|
410 lemma not_dvd_modd_pinf: "((d::int) dvd d1) ==> |
|
411 (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x+k*d1 + t))))" |
|
412 apply(clarsimp simp add:dvd_def) |
|
413 apply(rule iffI) |
|
414 apply(clarsimp) |
|
415 apply(rename_tac n m) |
|
416 apply(erule_tac x = "m - n*k" in allE) |
|
417 apply(simp add:int_distrib zmult_ac) |
|
418 apply(clarsimp) |
|
419 apply(rename_tac n m) |
|
420 apply(erule_tac x = "m + n*k" in allE) |
|
421 apply(simp add:int_distrib zmult_ac) |
|
422 done |
|
423 |
|
424 (*=============================================================================*) |
|
425 (*These are the atomic cases for the proof generation for the equivalence of P and P |
|
426 plusinfinity for integers x greather than some integer z.*) |
|
427 (*They are fully based on arithmetics*) |
|
428 |
|
429 lemma eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )" |
|
430 apply(rule_tac x = "-t" in exI) |
|
431 apply simp |
|
432 done |
|
433 |
|
434 lemma neq_eq_pinf: "EX z::int. ALL x. z < x --> ((~( 0 = x +t )) = True )" |
|
435 apply(rule_tac x = "-t" in exI) |
|
436 apply simp |
|
437 done |
|
438 |
|
439 lemma le_eq_pinf: "EX z::int. ALL x. z < x --> ( 0 < x +t = True )" |
|
440 apply(rule_tac x = "-t" in exI) |
|
441 apply simp |
|
442 done |
|
443 |
|
444 lemma len_eq_pinf: "EX z::int. ALL x. z < x --> (0 < -x +t = False )" |
|
445 apply(rule_tac x = "t" in exI) |
|
446 apply simp |
|
447 done |
|
448 |
|
449 lemma dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((d dvd (x + t)) = (d dvd (x + t))) " |
|
450 by simp |
|
451 |
|
452 lemma not_dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) " |
|
453 by simp |
|
454 |
|
455 |
|
456 |
|
457 |
|
458 (*=============================================================================*) |
|
459 (*These are the atomic cases for the proof generation for the modulo D property for P |
|
460 minusinfinity*) |
|
461 (*They are fully based on arithmetics*) |
|
462 |
|
463 lemma dvd_modd_minf: "((d::int) dvd d1) ==> |
|
464 (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))" |
|
465 apply(clarsimp simp add:dvd_def) |
|
466 apply(rule iffI) |
|
467 apply(clarsimp) |
|
468 apply(rename_tac n m) |
|
469 apply(rule_tac x = "m - n*k" in exI) |
|
470 apply(simp add:int_distrib) |
|
471 apply(clarsimp) |
|
472 apply(rename_tac n m) |
|
473 apply(rule_tac x = "m + n*k" in exI) |
|
474 apply(simp add:int_distrib zmult_ac) |
|
475 done |
|
476 |
|
477 |
|
478 lemma not_dvd_modd_minf: "((d::int) dvd d1) ==> |
|
479 (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x-k*d1 + t))))" |
|
480 apply(clarsimp simp add:dvd_def) |
|
481 apply(rule iffI) |
|
482 apply(clarsimp) |
|
483 apply(rename_tac n m) |
|
484 apply(erule_tac x = "m + n*k" in allE) |
|
485 apply(simp add:int_distrib zmult_ac) |
|
486 apply(clarsimp) |
|
487 apply(rename_tac n m) |
|
488 apply(erule_tac x = "m - n*k" in allE) |
|
489 apply(simp add:int_distrib zmult_ac) |
|
490 done |
|
491 |
|
492 |
|
493 (*=============================================================================*) |
|
494 (*These are the atomic cases for the proof generation for the equivalence of P and P |
|
495 minusinfinity for integers x less than some integer z.*) |
|
496 (*They are fully based on arithmetics*) |
|
497 |
|
498 lemma eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )" |
|
499 apply(rule_tac x = "-t" in exI) |
|
500 apply simp |
|
501 done |
|
502 |
|
503 lemma neq_eq_minf: "EX z::int. ALL x. x < z --> ((~( 0 = x +t )) = True )" |
|
504 apply(rule_tac x = "-t" in exI) |
|
505 apply simp |
|
506 done |
|
507 |
|
508 lemma le_eq_minf: "EX z::int. ALL x. x < z --> ( 0 < x +t = False )" |
|
509 apply(rule_tac x = "-t" in exI) |
|
510 apply simp |
|
511 done |
|
512 |
|
513 |
|
514 lemma len_eq_minf: "EX z::int. ALL x. x < z --> (0 < -x +t = True )" |
|
515 apply(rule_tac x = "t" in exI) |
|
516 apply simp |
|
517 done |
|
518 |
|
519 lemma dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) " |
|
520 by simp |
|
521 |
|
522 lemma not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) " |
|
523 by simp |
|
524 |
|
525 |
|
526 (*=============================================================================*) |
|
527 (*This Theorem combines whithnesses about P minusinfinity to schow one component of the |
|
528 equivalence proof for cooper's theorem*) |
|
529 |
|
530 (* FIXME: remove once they are part of the distribution *) |
|
531 theorem int_ge_induct[consumes 1,case_names base step]: |
|
532 assumes ge: "k \<le> (i::int)" and |
|
533 base: "P(k)" and |
|
534 step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" |
|
535 shows "P i" |
|
536 proof - |
|
537 { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i" |
|
538 proof (induct n) |
|
539 case 0 |
|
540 hence "i = k" by arith |
|
541 thus "P i" using base by simp |
|
542 next |
|
543 case (Suc n) |
|
544 hence "n = nat((i - 1) - k)" by arith |
|
545 moreover |
|
546 have ki1: "k \<le> i - 1" using Suc.prems by arith |
|
547 ultimately |
|
548 have "P(i - 1)" by(rule Suc.hyps) |
|
549 from step[OF ki1 this] show ?case by simp |
|
550 qed |
|
551 } |
|
552 from this ge show ?thesis by fast |
|
553 qed |
|
554 |
|
555 theorem int_gr_induct[consumes 1,case_names base step]: |
|
556 assumes gr: "k < (i::int)" and |
|
557 base: "P(k+1)" and |
|
558 step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)" |
|
559 shows "P i" |
|
560 apply(rule int_ge_induct[of "k + 1"]) |
|
561 using gr apply arith |
|
562 apply(rule base) |
|
563 apply(rule step) |
|
564 apply simp+ |
|
565 done |
|
566 |
|
567 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z" |
|
568 apply(induct rule: int_gr_induct) |
|
569 apply simp |
|
570 apply arith |
|
571 apply (simp add:int_distrib) |
|
572 apply arith |
|
573 done |
|
574 |
|
575 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d" |
|
576 apply(induct rule: int_gr_induct) |
|
577 apply simp |
|
578 apply arith |
|
579 apply (simp add:int_distrib) |
|
580 apply arith |
|
581 done |
|
582 |
|
583 lemma minusinfinity: |
|
584 assumes "0 < d" and |
|
585 P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and |
|
586 ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)" |
|
587 shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)" |
|
588 proof |
|
589 assume eP1: "EX x. P1 x" |
|
590 then obtain x where P1: "P1 x" .. |
|
591 from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" .. |
|
592 let ?w = "x - (abs(x-z)+1) * d" |
|
593 show "EX x. P x" |
|
594 proof |
|
595 have w: "?w < z" by(rule decr_lemma) |
|
596 have "P1 x = P1 ?w" using P1eqP1 by blast |
|
597 also have "\<dots> = P(?w)" using w P1eqP by blast |
|
598 finally show "P ?w" using P1 by blast |
|
599 qed |
|
600 qed |
|
601 |
|
602 (*=============================================================================*) |
|
603 (*This Theorem combines whithnesses about P minusinfinity to schow one component of the |
|
604 equivalence proof for cooper's theorem*) |
|
605 |
|
606 lemma plusinfinity: |
|
607 assumes "0 < d" and |
|
608 P1eqP1: "ALL (x::int) (k::int). P1 x = P1 (x + k * d)" and |
|
609 ePeqP1: "EX z::int. ALL x. z < x --> (P x = P1 x)" |
|
610 shows "(EX x::int. P1 x) --> (EX x::int. P x)" |
|
611 proof |
|
612 assume eP1: "EX x. P1 x" |
|
613 then obtain x where P1: "P1 x" .. |
|
614 from ePeqP1 obtain z where P1eqP: "ALL x. z < x \<longrightarrow> (P x = P1 x)" .. |
|
615 let ?w = "x + (abs(x-z)+1) * d" |
|
616 show "EX x. P x" |
|
617 proof |
|
618 have w: "z < ?w" by(rule incr_lemma) |
|
619 have "P1 x = P1 ?w" using P1eqP1 by blast |
|
620 also have "\<dots> = P(?w)" using w P1eqP by blast |
|
621 finally show "P ?w" using P1 by blast |
|
622 qed |
|
623 qed |
|
624 |
|
625 |
|
626 |
|
627 (*=============================================================================*) |
|
628 (*Theorem for periodic function on discrete sets*) |
|
629 |
|
630 lemma minf_vee: |
|
631 assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)" |
|
632 shows "(EX x. P x) = (EX j : {1..d}. P j)" |
|
633 (is "?LHS = ?RHS") |
|
634 proof |
|
635 assume ?LHS |
|
636 then obtain x where P: "P x" .. |
|
637 have "x mod d = x - (x div d)*d" |
|
638 by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq) |
|
639 hence Pmod: "P x = P(x mod d)" using modd by simp |
|
640 show ?RHS |
|
641 proof (cases) |
|
642 assume "x mod d = 0" |
|
643 hence "P 0" using P Pmod by simp |
|
644 moreover have "P 0 = P(0 - (-1)*d)" using modd by blast |
|
645 ultimately have "P d" by simp |
|
646 moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff) |
|
647 ultimately show ?RHS .. |
|
648 next |
|
649 assume not0: "x mod d \<noteq> 0" |
|
650 have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) |
|
651 moreover have "x mod d : {1..d}" |
|
652 proof - |
|
653 have "0 \<le> x mod d" by(rule pos_mod_sign) |
|
654 moreover have "x mod d < d" by(rule pos_mod_bound) |
|
655 ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) |
|
656 qed |
|
657 ultimately show ?RHS .. |
|
658 qed |
|
659 next |
|
660 assume ?RHS thus ?LHS by blast |
|
661 qed |
|
662 |
|
663 (*=============================================================================*) |
|
664 (*Theorem for periodic function on discrete sets*) |
|
665 lemma pinf_vee: |
|
666 assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)" |
|
667 shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)" |
|
668 (is "?LHS = ?RHS") |
|
669 proof |
|
670 assume ?LHS |
|
671 then obtain x where P: "P x" .. |
|
672 have "x mod d = x + (-(x div d))*d" |
|
673 by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq) |
|
674 hence Pmod: "P x = P(x mod d)" using modd by (simp only:) |
|
675 show ?RHS |
|
676 proof (cases) |
|
677 assume "x mod d = 0" |
|
678 hence "P 0" using P Pmod by simp |
|
679 moreover have "P 0 = P(0 + 1*d)" using modd by blast |
|
680 ultimately have "P d" by simp |
|
681 moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff) |
|
682 ultimately show ?RHS .. |
|
683 next |
|
684 assume not0: "x mod d \<noteq> 0" |
|
685 have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) |
|
686 moreover have "x mod d : {1..d}" |
|
687 proof - |
|
688 have "0 \<le> x mod d" by(rule pos_mod_sign) |
|
689 moreover have "x mod d < d" by(rule pos_mod_bound) |
|
690 ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) |
|
691 qed |
|
692 ultimately show ?RHS .. |
|
693 qed |
|
694 next |
|
695 assume ?RHS thus ?LHS by blast |
|
696 qed |
|
697 |
|
698 lemma decr_mult_lemma: |
|
699 assumes dpos: "(0::int) < d" and |
|
700 minus: "ALL x::int. P x \<longrightarrow> P(x - d)" and |
|
701 knneg: "0 <= k" |
|
702 shows "ALL x. P x \<longrightarrow> P(x - k*d)" |
|
703 using knneg |
|
704 proof (induct rule:int_ge_induct) |
|
705 case base thus ?case by simp |
|
706 next |
|
707 case (step i) |
|
708 show ?case |
|
709 proof |
|
710 fix x |
|
711 have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast |
|
712 also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)" |
|
713 using minus[THEN spec, of "x - i * d"] |
|
714 by (simp add:int_distrib zdiff_zdiff_eq[symmetric]) |
|
715 ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast |
|
716 qed |
|
717 qed |
|
718 |
|
719 lemma incr_mult_lemma: |
|
720 assumes dpos: "(0::int) < d" and |
|
721 plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and |
|
722 knneg: "0 <= k" |
|
723 shows "ALL x. P x \<longrightarrow> P(x + k*d)" |
|
724 using knneg |
|
725 proof (induct rule:int_ge_induct) |
|
726 case base thus ?case by simp |
|
727 next |
|
728 case (step i) |
|
729 show ?case |
|
730 proof |
|
731 fix x |
|
732 have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast |
|
733 also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" |
|
734 using plus[THEN spec, of "x + i * d"] |
|
735 by (simp add:int_distrib zadd_ac) |
|
736 ultimately show "P x \<longrightarrow> P(x + (i + 1) * d)" by blast |
|
737 qed |
|
738 qed |
|
739 |
|
740 lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x)) |
|
741 ==> (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)) --> (EX (x::int). P x) |
|
742 ==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) |
|
743 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D)))) |
|
744 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))" |
|
745 apply(rule iffI) |
|
746 prefer 2 |
|
747 apply(drule minusinfinity) |
|
748 apply assumption+ |
|
749 apply(fastsimp) |
|
750 apply clarsimp |
|
751 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)") |
|
752 apply(frule_tac x = x and z=z in decr_lemma) |
|
753 apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)") |
|
754 prefer 2 |
|
755 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)") |
|
756 prefer 2 apply arith |
|
757 apply fastsimp |
|
758 apply(drule (1) minf_vee) |
|
759 apply blast |
|
760 apply(blast dest:decr_mult_lemma) |
|
761 done |
|
762 |
|
763 (* Cooper Thm `, plus infinity version*) |
|
764 lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x)) |
|
765 ==> (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)) --> (EX (x::int). P x) |
|
766 ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) |
|
767 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D)))) |
|
768 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)))" |
|
769 apply(rule iffI) |
|
770 prefer 2 |
|
771 apply(drule plusinfinity) |
|
772 apply assumption+ |
|
773 apply(fastsimp) |
|
774 apply clarsimp |
|
775 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x + k*D)") |
|
776 apply(frule_tac x = x and z=z in incr_lemma) |
|
777 apply(subgoal_tac "P1(x + (\<bar>x - z\<bar> + 1) * D)") |
|
778 prefer 2 |
|
779 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)") |
|
780 prefer 2 apply arith |
|
781 apply fastsimp |
|
782 apply(drule (1) pinf_vee) |
|
783 apply blast |
|
784 apply(blast dest:incr_mult_lemma) |
|
785 done |
|
786 |
|
787 |
|
788 (*=============================================================================*) |
|
789 |
|
790 (*Theorems for the quantifier elminination Functions.*) |
|
791 |
|
792 lemma qe_ex_conj: "(EX (x::int). A x) = R |
|
793 ==> (EX (x::int). P x) = (Q & (EX x::int. A x)) |
|
794 ==> (EX (x::int). P x) = (Q & R)" |
|
795 by blast |
|
796 |
|
797 lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q) |
|
798 ==> (EX (x::int). P x) = Q" |
|
799 by blast |
|
800 |
|
801 lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)" |
|
802 by blast |
|
803 |
|
804 lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)" |
|
805 by blast |
|
806 |
|
807 lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)" |
|
808 by blast |
|
809 |
|
810 lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)" |
|
811 by blast |
|
812 |
|
813 lemma qe_Not: "P = Q ==> (~P) = (~Q)" |
|
814 by blast |
|
815 |
|
816 lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)" |
|
817 by blast |
|
818 |
|
819 (* Theorems for proving NNF *) |
|
820 |
|
821 lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))" |
|
822 by blast |
|
823 |
|
824 lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))" |
|
825 by blast |
|
826 |
|
827 lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)" |
|
828 by blast |
|
829 lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))" |
|
830 by blast |
|
831 |
|
832 lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))" |
|
833 by blast |
|
834 lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))" |
|
835 by blast |
|
836 lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))" |
|
837 by blast |
|
838 lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))" |
|
839 by blast |
|
840 |
|
841 |
|
842 lemma qe_exI2: "A = B ==> (EX (x::int). A(x)) = (EX (x::int). B(x))" |
|
843 by simp |
|
844 |
|
845 lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))" |
|
846 by rules |
|
847 |
|
848 lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))" |
|
849 by rules |
|
850 |
|
851 lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) |
|
852 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) " |
|
853 by blast |
|
854 |
|
855 lemma cppi_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) |
|
856 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) " |
|
857 by blast |
|
858 |
|
859 |
|
860 lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})" |
|
861 apply(simp add:atLeastAtMost_def atLeast_def atMost_def) |
|
862 apply(fastsimp) |
|
863 done |
|
864 |
|
865 (* Theorems required for the adjustcoeffitienteq*) |
|
866 |
|
867 lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)" |
|
868 shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q") |
|
869 proof |
|
870 assume ?P |
|
871 thus ?Q |
|
872 apply(simp add:dvd_def) |
|
873 apply clarify |
|
874 apply(rename_tac d) |
|
875 apply(drule_tac f = "op * k" in arg_cong) |
|
876 apply(simp only:int_distrib) |
|
877 apply(rule_tac x = "d" in exI) |
|
878 apply(simp only:zmult_ac) |
|
879 done |
|
880 next |
|
881 assume ?Q |
|
882 then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def) |
|
883 hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib zmult_ac) |
|
884 hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"]) |
|
885 hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]]) |
|
886 thus ?P by(simp add:dvd_def) |
|
887 qed |
|
888 |
|
889 lemma ac_lt_eq: assumes gr0: "0 < (k::int)" |
|
890 shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q") |
|
891 proof |
|
892 assume P: ?P |
|
893 show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib zmult_ac) |
|
894 next |
|
895 assume ?Q |
|
896 hence "0 < k*(c*n + t - m)" by(simp add: int_distrib zmult_ac) |
|
897 with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff) |
|
898 thus ?P by(simp) |
|
899 qed |
|
900 |
|
901 lemma ac_eq_eq : assumes not0: "0 ~= (k::int)" shows "((m::int) = (c*n+t)) = (k*m =((k*c)*n+(k*t)) )" (is "?P = ?Q") |
|
902 proof |
|
903 assume ?P |
|
904 thus ?Q |
|
905 apply(drule_tac f = "op * k" in arg_cong) |
|
906 apply(simp only:int_distrib) |
|
907 done |
|
908 next |
|
909 assume ?Q |
|
910 hence "m * k = (c*n + t) * k" by(simp add:int_distrib zmult_ac) |
|
911 hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"]) |
|
912 thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]]) |
|
913 qed |
|
914 |
|
915 lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))" |
|
916 proof - |
|
917 have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith |
|
918 also have "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib zmult_ac) |
|
919 also have "0<(-1*c)*n + (-t+1) = (0 < (k*(-1*c)*n) + (k*(-t+1)))" by(rule ac_lt_eq[of _ 0,OF gr0,simplified]) |
|
920 also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib zmult_ac) |
|
921 finally show ?thesis . |
|
922 qed |
|
923 |
|
924 lemma binminus_uminus_conv: "(a::int) - b = a + (-b)" |
|
925 by arith |
|
926 |
|
927 lemma linearize_dvd: "(t::int) = t1 ==> (d dvd t) = (d dvd t1)" |
|
928 by simp |
|
929 |
|
930 lemma lf_lt: "(l::int) = ll ==> (r::int) = lr ==> (l < r) =(ll < lr)" |
|
931 by simp |
|
932 |
|
933 lemma lf_eq: "(l::int) = ll ==> (r::int) = lr ==> (l = r) =(ll = lr)" |
|
934 by simp |
|
935 |
|
936 lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)" |
|
937 by simp |
|
938 |
|
939 (* Theorems for transforming predicates on nat to predicates on int*) |
|
940 |
|
941 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))" |
|
942 by (simp split add: split_nat) |
|
943 |
|
944 theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))" |
|
945 apply (simp split add: split_nat) |
|
946 apply (rule iffI) |
|
947 apply (erule exE) |
|
948 apply (rule_tac x = "int x" in exI) |
|
949 apply simp |
|
950 apply (erule exE) |
|
951 apply (rule_tac x = "nat x" in exI) |
|
952 apply (erule conjE) |
|
953 apply (erule_tac x = "nat x" in allE) |
|
954 apply simp |
|
955 done |
|
956 |
|
957 theorem zdiff_int_split: "P (int (x - y)) = |
|
958 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))" |
|
959 apply (case_tac "y \<le> x") |
|
960 apply (simp_all add: zdiff_int) |
|
961 done |
|
962 |
|
963 theorem zdvd_int: "(x dvd y) = (int x dvd int y)" |
|
964 apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric] |
|
965 nat_0_le cong add: conj_cong) |
|
966 apply (rule iffI) |
|
967 apply rules |
|
968 apply (erule exE) |
|
969 apply (case_tac "x=0") |
|
970 apply (rule_tac x=0 in exI) |
|
971 apply simp |
|
972 apply (case_tac "0 \<le> k") |
|
973 apply rules |
|
974 apply (simp add: linorder_not_le) |
|
975 apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]]) |
|
976 apply assumption |
|
977 apply (simp add: zmult_ac) |
|
978 done |
|
979 |
|
980 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" |
|
981 by simp |
|
982 |
|
983 theorem number_of2: "(0::int) <= number_of bin.Pls" by simp |
|
984 |
|
985 theorem Suc_plus1: "Suc n = n + 1" by simp |
|
986 |
|
987 (* specific instances of congruence rules, to prevent simplifier from looping *) |
|
988 |
|
989 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')" |
|
990 by simp |
|
991 |
|
992 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<and> P) = (0 <= x \<and> P')" |
|
993 by simp |
|
994 |
|
995 use "cooper_dec.ML" |
|
996 use "cooper_proof.ML" |
|
997 use "qelim.ML" |
|
998 use "presburger.ML" |
|
999 |
|
1000 setup "Presburger.setup" |
|
1001 |
|
1002 end |