src/HOL/Presburger.thy
 author krauss Fri Nov 24 13:44:51 2006 +0100 (2006-11-24) changeset 21512 3786eb1b69d6 parent 21454 a1937c51ed88 child 22026 cc60e54aa7cb permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
1 (*  Title:      HOL/Integ/Presburger.thy
2     ID:         \$Id\$
3     Author:     Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen
5 File containing necessary theorems for the proof
6 generation for Cooper Algorithm
7 *)
9 header {* Presburger Arithmetic: Cooper's Algorithm *}
11 theory Presburger
12 imports NatSimprocs
13 uses
14   ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML")
15   ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
16 begin
18 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
20 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
21   apply (rule iffI)
22   apply (erule exE)
23   apply (rule_tac x = "l * x" in exI)
24   apply simp
25   apply (erule exE)
26   apply (erule conjE)
27   apply (erule dvdE)
28   apply (rule_tac x = k in exI)
29   apply simp
30   done
32 lemma uminus_dvd_conv: "(d dvd (t::int)) = (-d dvd t)"
33 apply(unfold dvd_def)
34 apply(rule iffI)
35 apply(clarsimp)
36 apply(rename_tac k)
37 apply(rule_tac x = "-k" in exI)
38 apply simp
39 apply(clarsimp)
40 apply(rename_tac k)
41 apply(rule_tac x = "-k" in exI)
42 apply simp
43 done
45 lemma uminus_dvd_conv': "(d dvd (t::int)) = (d dvd -t)"
46 apply(unfold dvd_def)
47 apply(rule iffI)
48 apply(clarsimp)
49 apply(rule_tac x = "-k" in exI)
50 apply simp
51 apply(clarsimp)
52 apply(rule_tac x = "-k" in exI)
53 apply simp
54 done
58 text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} less than some integer @{text z}.*}
60 theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
61   \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
62   \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
63   apply (erule exE)+
64   apply (rule_tac x = "min z1 z2" in exI)
65   apply simp
66   done
69 theorem eq_minf_disjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
70   \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
71   \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))"
73   apply (erule exE)+
74   apply (rule_tac x = "min z1 z2" in exI)
75   apply simp
76   done
79 text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} greather than some integer @{text z}.*}
81 theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
82   \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
83   \<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
84   apply (erule exE)+
85   apply (rule_tac x = "max z1 z2" in exI)
86   apply simp
87   done
90 theorem eq_pinf_disjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
91   \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
92   \<exists>z::int. \<forall>x. z < x  \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))"
93   apply (erule exE)+
94   apply (rule_tac x = "max z1 z2" in exI)
95   apply simp
96   done
98 text {*
99   \medskip Theorems for the combination of proofs of the modulo @{text
100   D} property for @{text "P plusinfinity"}
102   FIXME: This is THE SAME theorem as for the @{text minusinf} version,
103   but with @{text "+k.."} instead of @{text "-k.."} In the future
104   replace these both with only one. *}
106 theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
107   \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
108   \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
109   by simp
111 theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
112   \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
113   \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
114   by simp
116 text {*
117   This is one of the cases where the simplifed formula is prooved to
118   habe some property (in relation to @{text P_m}) but we need to prove
119   the property for the original formula (@{text P_m})
121   FIXME: This is exaclty the same thm as for @{text minusinf}. *}
123 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)) "
124   by blast
127 text {*
128   \medskip Theorems for the combination of proofs of the modulo @{text D}
129   property for @{text "P minusinfinity"} *}
131 theorem modd_minf_conjI: "\<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 \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
134   by simp
136 theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
137   \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
138   \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
139   by simp
141 text {*
142   This is one of the cases where the simplifed formula is prooved to
143   have some property (in relation to @{text P_m}) but we need to
144   prove the property for the original formula (@{text P_m}). *}
146 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)) "
147   by blast
149 text {*
150   Theorem needed for proving at runtime divide properties using the
151   arithmetic tactic (which knows only about modulo = 0). *}
153 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
154   by(simp add:dvd_def zmod_eq_0_iff)
156 text {*
157   \medskip Theorems used for the combination of proof for the
158   backwards direction of Cooper's Theorem. They rely exclusively on
159   Predicate calculus.*}
161 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))
162 ==>
163 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
164 ==>
165 (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))) "
166   by blast
169 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))
170 ==>
171 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
172 ==>
173 (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)
174 \<and> P2(x + d))) "
175   by blast
177 lemma not_ast_p_Q_elim: "
178 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
179 ==> ( P = Q )
180 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
181   by blast
183 text {*
184   \medskip Theorems used for the combination of proof for the
185   backwards direction of Cooper's Theorem. They rely exclusively on
186   Predicate calculus.*}
188 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))
189 ==>
190 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d))
191 ==>
192 (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)
193 \<or> P2(x-d))) "
194   by blast
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
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
210 text {* \medskip This is the first direction of Cooper's Theorem. *}
211 lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
212   by blast
214 text {*
215   \medskip The full Cooper's Theorem in its equivalence Form. Given
216   the premises it is trivial too, it relies exclusively on prediacte calculus.*}
217 lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
218 --> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
219   by blast
221 text {*
222   \medskip Some of the atomic theorems generated each time the atom
223   does not depend on @{text x}, they are trivial.*}
225 lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
226   by blast
228 lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
229   by blast
231 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"
232   by blast
234 lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
235   by blast
237 text {* The next two thms are the same as the @{text minusinf} version. *}
239 lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
240   by blast
242 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"
243   by blast
245 text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
247 lemma P_eqtrue: "(P=True) = P"
248   by iprover
250 lemma P_eqfalse: "(P=False) = (~P)"
251   by iprover
253 text {*
254   \medskip Theorems for the generation of the bachwards direction of
255   Cooper's Theorem.
257   These are the 6 interesting atomic cases which have to be proved relying on the
258   properties of B-set and the arithmetic and contradiction proofs. *}
260 lemma not_bst_p_lt: "0 < (d::int) ==>
261  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 )"
262   by arith
264 lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
265  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)"
266 apply clarsimp
267 apply(rule ccontr)
268 apply(drule_tac x = "x+a" in bspec)
270 apply(drule_tac x = "-a" in bspec)
271 apply assumption
272 apply(simp)
273 done
275 lemma not_bst_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a - 1 \<rbrakk> \<Longrightarrow>
276  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 )"
277 apply clarsimp
278 apply(subgoal_tac "x = -a")
279  prefer 2 apply arith
280 apply(drule_tac x = "1" in bspec)
282 apply(drule_tac x = "-a- 1" in bspec)
283 apply assumption
284 apply(simp)
285 done
288 lemma not_bst_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
289  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)"
290 apply clarsimp
291 apply(subgoal_tac "x = -a+d")
292  prefer 2 apply arith
293 apply(drule_tac x = "d" in bspec)
295 apply(drule_tac x = "-a" in bspec)
296 apply assumption
297 apply(simp)
298 done
301 lemma not_bst_p_dvd: "(d1::int) dvd d ==>
302  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 )"
303 apply(clarsimp simp add:dvd_def)
304 apply(rename_tac m)
305 apply(rule_tac x = "m - k" in exI)
307 done
309 lemma not_bst_p_ndvd: "(d1::int) dvd d ==>
310  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 ))"
311 apply(clarsimp simp add:dvd_def)
312 apply(rename_tac m)
313 apply(erule_tac x = "m + k" in allE)
315 done
317 text {*
318   \medskip Theorems for the generation of the bachwards direction of
319   Cooper's Theorem.
321   These are the 6 interesting atomic cases which have to be proved
322   relying on the properties of A-set ant the arithmetic and
323   contradiction proofs. *}
325 lemma not_ast_p_gt: "0 < (d::int) ==>
326  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 )"
327   by arith
329 lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
330  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)"
331   apply clarsimp
332   apply (rule ccontr)
333   apply (drule_tac x = "t-x" in bspec)
334   apply simp
335   apply (drule_tac x = "t" in bspec)
336   apply assumption
337   apply simp
338   done
340 lemma not_ast_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t + 1 \<rbrakk> \<Longrightarrow>
341  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 )"
342   apply clarsimp
343   apply (drule_tac x="1" in bspec)
344   apply simp
345   apply (drule_tac x="- t + 1" in bspec)
346   apply assumption
347   apply(subgoal_tac "x = -t")
348   prefer 2 apply arith
349   apply simp
350   done
352 lemma not_ast_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t \<rbrakk> \<Longrightarrow>
353  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)"
354   apply clarsimp
355   apply (subgoal_tac "x = -t-d")
356   prefer 2 apply arith
357   apply (drule_tac x = "d" in bspec)
358   apply simp
359   apply (drule_tac x = "-t" in bspec)
360   apply assumption
361   apply simp
362   done
364 lemma not_ast_p_dvd: "(d1::int) dvd d ==>
365  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 )"
366   apply(clarsimp simp add:dvd_def)
367   apply(rename_tac m)
368   apply(rule_tac x = "m + k" in exI)
370   done
372 lemma not_ast_p_ndvd: "(d1::int) dvd d ==>
373  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 ))"
374   apply(clarsimp simp add:dvd_def)
375   apply(rename_tac m)
376   apply(erule_tac x = "m - k" in allE)
378   done
380 text {*
381   \medskip These are the atomic cases for the proof generation for the
382   modulo @{text D} property for @{text "P plusinfinity"}
384   They are fully based on arithmetics. *}
386 lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
387  (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
388   apply(clarsimp simp add:dvd_def)
389   apply(rule iffI)
390   apply(clarsimp)
391   apply(rename_tac n m)
392   apply(rule_tac x = "m + n*k" in exI)
394   apply(clarsimp)
395   apply(rename_tac n m)
396   apply(rule_tac x = "m - n*k" in exI)
397   apply(simp add:int_distrib mult_ac)
398   done
400 lemma  not_dvd_modd_pinf: "((d::int) dvd d1) ==>
401  (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x+k*d1 + t))))"
402   apply(clarsimp simp add:dvd_def)
403   apply(rule iffI)
404   apply(clarsimp)
405   apply(rename_tac n m)
406   apply(erule_tac x = "m - n*k" in allE)
407   apply(simp add:int_distrib mult_ac)
408   apply(clarsimp)
409   apply(rename_tac n m)
410   apply(erule_tac x = "m + n*k" in allE)
411   apply(simp add:int_distrib mult_ac)
412   done
414 text {*
415   \medskip These are the atomic cases for the proof generation for the
416   equivalence of @{text P} and @{text "P plusinfinity"} for integers
417   @{text x} greater than some integer @{text z}.
419   They are fully based on arithmetics. *}
421 lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
422   apply(rule_tac x = "-t" in exI)
423   apply simp
424   done
426 lemma  neq_eq_pinf: "EX z::int. ALL x.  z < x --> ((~( 0 = x +t )) = True )"
427   apply(rule_tac x = "-t" in exI)
428   apply simp
429   done
431 lemma  le_eq_pinf: "EX z::int. ALL x.  z < x --> ( 0 < x +t  = True )"
432   apply(rule_tac x = "-t" in exI)
433   apply simp
434   done
436 lemma  len_eq_pinf: "EX z::int. ALL x. z < x  --> (0 < -x +t  = False )"
437   apply(rule_tac x = "t" in exI)
438   apply simp
439   done
441 lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
442   by simp
444 lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
445   by simp
447 text {*
448   \medskip These are the atomic cases for the proof generation for the
449   modulo @{text D} property for @{text "P minusinfinity"}.
451   They are fully based on arithmetics. *}
453 lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
454  (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
455 apply(clarsimp simp add:dvd_def)
456 apply(rule iffI)
457 apply(clarsimp)
458 apply(rename_tac n m)
459 apply(rule_tac x = "m - n*k" in exI)
461 apply(clarsimp)
462 apply(rename_tac n m)
463 apply(rule_tac x = "m + n*k" in exI)
464 apply(simp add:int_distrib mult_ac)
465 done
468 lemma  not_dvd_modd_minf: "((d::int) dvd d1) ==>
469  (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x-k*d1 + t))))"
470 apply(clarsimp simp add:dvd_def)
471 apply(rule iffI)
472 apply(clarsimp)
473 apply(rename_tac n m)
474 apply(erule_tac x = "m + n*k" in allE)
475 apply(simp add:int_distrib mult_ac)
476 apply(clarsimp)
477 apply(rename_tac n m)
478 apply(erule_tac x = "m - n*k" in allE)
479 apply(simp add:int_distrib mult_ac)
480 done
482 text {*
483   \medskip These are the atomic cases for the proof generation for the
484   equivalence of @{text P} and @{text "P minusinfinity"} for integers
485   @{text x} less than some integer @{text z}.
487   They are fully based on arithmetics. *}
489 lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
490 apply(rule_tac x = "-t" in exI)
491 apply simp
492 done
494 lemma  neq_eq_minf: "EX z::int. ALL x. x < z --> ((~( 0 = x +t )) = True )"
495 apply(rule_tac x = "-t" in exI)
496 apply simp
497 done
499 lemma  le_eq_minf: "EX z::int. ALL x. x < z --> ( 0 < x +t  = False )"
500 apply(rule_tac x = "-t" in exI)
501 apply simp
502 done
505 lemma  len_eq_minf: "EX z::int. ALL x. x < z --> (0 < -x +t  = True )"
506 apply(rule_tac x = "t" in exI)
507 apply simp
508 done
510 lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
511   by simp
513 lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
514   by simp
516 text {*
517   \medskip This Theorem combines whithnesses about @{text "P
518   minusinfinity"} to show one component of the equivalence proof for
519   Cooper's Theorem.
521   FIXME: remove once they are part of the distribution. *}
523 theorem int_ge_induct[consumes 1,case_names base step]:
524   assumes ge: "k \<le> (i::int)" and
525         base: "P(k)" and
526         step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
527   shows "P i"
528 proof -
529   { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
530     proof (induct n)
531       case 0
532       hence "i = k" by arith
533       thus "P i" using base by simp
534     next
535       case (Suc n)
536       hence "n = nat((i - 1) - k)" by arith
537       moreover
538       have ki1: "k \<le> i - 1" using Suc.prems by arith
539       ultimately
540       have "P(i - 1)" by(rule Suc.hyps)
541       from step[OF ki1 this] show ?case by simp
542     qed
543   }
544   from this ge show ?thesis by fast
545 qed
547 theorem int_gr_induct[consumes 1,case_names base step]:
548   assumes gr: "k < (i::int)" and
549         base: "P(k+1)" and
550         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
551   shows "P i"
552 apply(rule int_ge_induct[of "k + 1"])
553   using gr apply arith
554  apply(rule base)
555 apply(rule step)
556  apply simp+
557 done
559 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
560 apply(induct rule: int_gr_induct)
561  apply simp
562 apply (simp add:int_distrib)
563 done
565 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
566 apply(induct rule: int_gr_induct)
567  apply simp
568 apply (simp add:int_distrib)
569 done
571 lemma  minusinfinity:
572   assumes "0 < d" and
573     P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and
574     ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
575   shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
576 proof
577   assume eP1: "EX x. P1 x"
578   then obtain x where P1: "P1 x" ..
579   from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
580   let ?w = "x - (abs(x-z)+1) * d"
581   show "EX x. P x"
582   proof
583     have w: "?w < z" by(rule decr_lemma)
584     have "P1 x = P1 ?w" using P1eqP1 by blast
585     also have "\<dots> = P(?w)" using w P1eqP by blast
586     finally show "P ?w" using P1 by blast
587   qed
588 qed
590 text {*
591   \medskip This Theorem combines whithnesses about @{text "P
592   minusinfinity"} to show one component of the equivalence proof for
593   Cooper's Theorem. *}
595 lemma plusinfinity:
596   assumes "0 < d" and
597     P1eqP1: "ALL (x::int) (k::int). P1 x = P1 (x + k * d)" and
598     ePeqP1: "EX z::int. ALL x. z < x  --> (P x = P1 x)"
599   shows "(EX x::int. P1 x) --> (EX x::int. P x)"
600 proof
601   assume eP1: "EX x. P1 x"
602   then obtain x where P1: "P1 x" ..
603   from ePeqP1 obtain z where P1eqP: "ALL x. z < x \<longrightarrow> (P x = P1 x)" ..
604   let ?w = "x + (abs(x-z)+1) * d"
605   show "EX x. P x"
606   proof
607     have w: "z < ?w" by(rule incr_lemma)
608     have "P1 x = P1 ?w" using P1eqP1 by blast
609     also have "\<dots> = P(?w)" using w P1eqP by blast
610     finally show "P ?w" using P1 by blast
611   qed
612 qed
614 text {*
615   \medskip Theorem for periodic function on discrete sets. *}
617 lemma minf_vee:
618   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
619   shows "(EX x. P x) = (EX j : {1..d}. P j)"
620   (is "?LHS = ?RHS")
621 proof
622   assume ?LHS
623   then obtain x where P: "P x" ..
624   have "x mod d = x - (x div d)*d"
625     by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
626   hence Pmod: "P x = P(x mod d)" using modd by simp
627   show ?RHS
628   proof (cases)
629     assume "x mod d = 0"
630     hence "P 0" using P Pmod by simp
631     moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
632     ultimately have "P d" by simp
633     moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
634     ultimately show ?RHS ..
635   next
636     assume not0: "x mod d \<noteq> 0"
637     have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
638     moreover have "x mod d : {1..d}"
639     proof -
640       have "0 \<le> x mod d" by(rule pos_mod_sign)
641       moreover have "x mod d < d" by(rule pos_mod_bound)
642       ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
643     qed
644     ultimately show ?RHS ..
645   qed
646 next
647   assume ?RHS thus ?LHS by blast
648 qed
650 text {*
651   \medskip Theorem for periodic function on discrete sets. *}
653 lemma pinf_vee:
654   assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
655   shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
656   (is "?LHS = ?RHS")
657 proof
658   assume ?LHS
659   then obtain x where P: "P x" ..
660   have "x mod d = x + (-(x div d))*d"
661     by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
662   hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
663   show ?RHS
664   proof (cases)
665     assume "x mod d = 0"
666     hence "P 0" using P Pmod by simp
667     moreover have "P 0 = P(0 + 1*d)" using modd by blast
668     ultimately have "P d" by simp
669     moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
670     ultimately show ?RHS ..
671   next
672     assume not0: "x mod d \<noteq> 0"
673     have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
674     moreover have "x mod d : {1..d}"
675     proof -
676       have "0 \<le> x mod d" by(rule pos_mod_sign)
677       moreover have "x mod d < d" by(rule pos_mod_bound)
678       ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
679     qed
680     ultimately show ?RHS ..
681   qed
682 next
683   assume ?RHS thus ?LHS by blast
684 qed
686 lemma decr_mult_lemma:
687   assumes dpos: "(0::int) < d" and
688           minus: "ALL x::int. P x \<longrightarrow> P(x - d)" and
689           knneg: "0 <= k"
690   shows "ALL x. P x \<longrightarrow> P(x - k*d)"
691 using knneg
692 proof (induct rule:int_ge_induct)
693   case base thus ?case by simp
694 next
695   case (step i)
696   show ?case
697   proof
698     fix x
699     have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
700     also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
701       using minus[THEN spec, of "x - i * d"]
702       by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric])
703     ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
704   qed
705 qed
707 lemma incr_mult_lemma:
708   assumes dpos: "(0::int) < d" and
709           plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and
710           knneg: "0 <= k"
711   shows "ALL x. P x \<longrightarrow> P(x + k*d)"
712 using knneg
713 proof (induct rule:int_ge_induct)
714   case base thus ?case by simp
715 next
716   case (step i)
717   show ?case
718   proof
719     fix x
720     have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
721     also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)"
722       using plus[THEN spec, of "x + i * d"]
724     ultimately show "P x \<longrightarrow> P(x + (i + 1) * d)" by blast
725   qed
726 qed
728 lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
729 ==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D)
730 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
731 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
732 apply(rule iffI)
733 prefer 2
734 apply(drule minusinfinity)
735 apply assumption+
736 apply(fastsimp)
737 apply clarsimp
738 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
739 apply(frule_tac x = x and z=z in decr_lemma)
740 apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
741 prefer 2
742 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
743 prefer 2 apply arith
744  apply fastsimp
745 apply(drule (1) minf_vee)
746 apply blast
747 apply(blast dest:decr_mult_lemma)
748 done
750 text {* Cooper Theorem, plus infinity version. *}
751 lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
752 ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D)
753 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
754 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)))"
755   apply(rule iffI)
756   prefer 2
757   apply(drule plusinfinity)
758   apply assumption+
759   apply(fastsimp)
760   apply clarsimp
761   apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x + k*D)")
762   apply(frule_tac x = x and z=z in incr_lemma)
763   apply(subgoal_tac "P1(x + (\<bar>x - z\<bar> + 1) * D)")
764   prefer 2
765   apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
766   prefer 2 apply arith
767   apply fastsimp
768   apply(drule (1) pinf_vee)
769   apply blast
770   apply(blast dest:incr_mult_lemma)
771   done
774 text {*
775   \bigskip Theorems for the quantifier elminination Functions. *}
777 lemma qe_ex_conj: "(EX (x::int). A x) = R
778 		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
779 		==> (EX (x::int). P x) = (Q & R)"
780 by blast
782 lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q)
783 		==> (EX (x::int). P x) = Q"
784 by blast
786 lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)"
787 by blast
789 lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)"
790 by blast
792 lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)"
793 by blast
795 lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)"
796 by blast
798 lemma qe_Not: "P = Q ==> (~P) = (~Q)"
799 by blast
801 lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
802 by blast
804 text {* \bigskip Theorems for proving NNF *}
806 lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
807 by blast
809 lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))"
810 by blast
812 lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)"
813   by blast
814 lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))"
815 by blast
817 lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))"
818 by blast
819 lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))"
820 by blast
821 lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))"
822 by blast
823 lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))"
824 by blast
827 lemma qe_exI2: "A = B ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
828   by simp
830 lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
831   by iprover
833 lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
834   by iprover
836 lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
837 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
838 by blast
840 lemma cppi_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j)))
841 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) "
842 by blast
845 lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
846 apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
847 apply(fastsimp)
848 done
850 text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
852 lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
853 shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
854 proof
855   assume ?P
856   thus ?Q
858     apply clarify
859     apply(rename_tac d)
860     apply(drule_tac f = "op * k" in arg_cong)
861     apply(simp only:int_distrib)
862     apply(rule_tac x = "d" in exI)
863     apply(simp only:mult_ac)
864     done
865 next
866   assume ?Q
867   then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
868   hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
869   hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
870   hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
871   thus ?P by(simp add:dvd_def)
872 qed
874 lemma ac_lt_eq: assumes gr0: "0 < (k::int)"
875 shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
876 proof
877   assume P: ?P
878   show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
879 next
880   assume ?Q
881   hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
882   with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
883   thus ?P by(simp)
884 qed
886 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")
887 proof
888   assume ?P
889   thus ?Q
890     apply(drule_tac f = "op * k" in arg_cong)
891     apply(simp only:int_distrib)
892     done
893 next
894   assume ?Q
895   hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
896   hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
897   thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
898 qed
900 lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
901 proof -
902   have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
903   also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
904   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])
905   also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
906   finally show ?thesis .
907 qed
909 lemma binminus_uminus_conv: "(a::int) - b = a + (-b)"
910 by arith
912 lemma  linearize_dvd: "(t::int) = t1 ==> (d dvd t) = (d dvd t1)"
913 by simp
915 lemma lf_lt: "(l::int) = ll ==> (r::int) = lr ==> (l < r) =(ll < lr)"
916 by simp
918 lemma lf_eq: "(l::int) = ll ==> (r::int) = lr ==> (l = r) =(ll = lr)"
919 by simp
921 lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
922 by simp
924 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
926 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
927   by (simp split add: split_nat)
929 theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
930   apply (simp split add: split_nat)
931   apply (rule iffI)
932   apply (erule exE)
933   apply (rule_tac x = "int x" in exI)
934   apply simp
935   apply (erule exE)
936   apply (rule_tac x = "nat x" in exI)
937   apply (erule conjE)
938   apply (erule_tac x = "nat x" in allE)
939   apply simp
940   done
942 theorem zdiff_int_split: "P (int (x - y)) =
943   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
944   apply (case_tac "y \<le> x")
945   apply (simp_all add: zdiff_int)
946   done
948 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
949   apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
950     nat_0_le cong add: conj_cong)
951   apply (rule iffI)
952   apply iprover
953   apply (erule exE)
954   apply (case_tac "x=0")
955   apply (rule_tac x=0 in exI)
956   apply simp
957   apply (case_tac "0 \<le> k")
958   apply iprover
959   apply (simp add: linorder_not_le)
960   apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
961   apply assumption
962   apply (simp add: mult_ac)
963   done
965 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
966   by simp
968 theorem number_of2: "(0::int) <= Numeral0" by simp
970 theorem Suc_plus1: "Suc n = n + 1" by simp
972 text {*
973   \medskip Specific instances of congruence rules, to prevent
974   simplifier from looping. *}
976 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
977   by simp
979 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
980   by (simp cong: conj_cong)
982     (* Theorems used in presburger.ML for the computation simpset*)
983     (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*)
985 lemma lift_bool: "x \<Longrightarrow> x=True"
986   by simp
988 lemma nlift_bool: "~x \<Longrightarrow> x=False"
989   by simp
991 lemma not_false_eq_true: "(~ False) = True" by simp
993 lemma not_true_eq_false: "(~ True) = False" by simp
996 lemma int_eq_number_of_eq:
997   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
998   by simp
999 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
1000   by (simp only: iszero_number_of_Pls)
1002 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
1003   by simp
1005 lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
1006   by simp
1008 lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
1009   by simp
1011 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
1012   by simp
1014 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
1015   by simp
1017 lemma int_neg_number_of_Min: "neg (-1::int)"
1018   by simp
1020 lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
1021   by simp
1023 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
1024   by simp
1025 lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
1026   by simp
1028 lemma int_number_of_diff_sym:
1029   "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
1030   by simp
1032 lemma int_number_of_mult_sym:
1033   "((number_of v)::int) * number_of w = number_of (v * w)"
1034   by simp
1036 lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
1037   by simp
1038 lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
1039   by simp
1041 lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
1042   by simp
1044 lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
1045   by simp
1047 lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
1048   by simp
1050 lemma int_pow_0: "(a::int)^(Numeral0) = 1"
1051   by simp
1053 lemma int_pow_1: "(a::int)^(Numeral1) = a"
1054   by simp
1056 lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
1057   by simp
1059 lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
1060   by simp
1062 lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
1063   by simp
1065 lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
1066   by simp
1068 lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
1069   by simp
1071 lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
1072 proof -
1073   have 1:"((-1)::nat) = 0"
1074     by simp
1075   show ?thesis by (simp add: 1)
1076 qed
1078 use "cooper_dec.ML"
1079 use "reflected_presburger.ML"
1080 use "reflected_cooper.ML"
1081 oracle
1082   presburger_oracle ("term") = ReflectedCooper.presburger_oracle
1084 use "cooper_proof.ML"
1085 use "qelim.ML"
1086 use "presburger.ML"
1088 setup "Presburger.setup"
1090 text {* Code generator setup *}
1092 text {*
1093   Presburger arithmetic is necessary (at least convenient) to prove some
1094   of the following code lemmas on integer numerals.
1095 *}
1097 lemma eq_number_of [code func]:
1098   "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
1099   unfolding number_of_is_id ..
1101 lemma less_eq_number_of [code func]:
1102   "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l"
1103   unfolding number_of_is_id ..
1105 lemma eq_Pls_Pls:
1106   "Numeral.Pls = Numeral.Pls" ..
1108 lemma eq_Pls_Min:
1109   "Numeral.Pls \<noteq> Numeral.Min"
1110   unfolding Pls_def Min_def by auto
1112 lemma eq_Pls_Bit0:
1113   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
1114   unfolding Pls_def Bit_def bit.cases by auto
1116 lemma eq_Pls_Bit1:
1117   "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
1118   unfolding Pls_def Bit_def bit.cases by arith
1120 lemma eq_Min_Pls:
1121   "Numeral.Min \<noteq> Numeral.Pls"
1122   unfolding Pls_def Min_def by auto
1124 lemma eq_Min_Min:
1125   "Numeral.Min = Numeral.Min" ..
1127 lemma eq_Min_Bit0:
1128   "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
1129   unfolding Min_def Bit_def bit.cases by arith
1131 lemma eq_Min_Bit1:
1132   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
1133   unfolding Min_def Bit_def bit.cases by auto
1135 lemma eq_Bit0_Pls:
1136   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
1137   unfolding Pls_def Bit_def bit.cases by auto
1139 lemma eq_Bit1_Pls:
1140   "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
1141   unfolding Pls_def Bit_def bit.cases by arith
1143 lemma eq_Bit0_Min:
1144   "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
1145   unfolding Min_def Bit_def bit.cases by arith
1147 lemma eq_Bit1_Min:
1148   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
1149   unfolding Min_def Bit_def bit.cases by auto
1151 lemma eq_Bit_Bit:
1152   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
1153     v1 = v2 \<and> k1 = k2"
1154   unfolding Bit_def
1155   apply (cases v1)
1156   apply (cases v2)
1157   apply auto
1158   apply arith
1159   apply (cases v2)
1160   apply auto
1161   apply arith
1162   apply (cases v2)
1163   apply auto
1164 done
1166 lemmas eq_numeral_code [code func] =
1167   eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
1168   eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
1169   eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
1171 lemma less_eq_Pls_Pls:
1172   "Numeral.Pls \<le> Numeral.Pls" ..
1174 lemma less_eq_Pls_Min:
1175   "\<not> (Numeral.Pls \<le> Numeral.Min)"
1176   unfolding Pls_def Min_def by auto
1178 lemma less_eq_Pls_Bit:
1179   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
1180   unfolding Pls_def Bit_def by (cases v) auto
1182 lemma less_eq_Min_Pls:
1183   "Numeral.Min \<le> Numeral.Pls"
1184   unfolding Pls_def Min_def by auto
1186 lemma less_eq_Min_Min:
1187   "Numeral.Min \<le> Numeral.Min" ..
1189 lemma less_eq_Min_Bit0:
1190   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
1191   unfolding Min_def Bit_def by auto
1193 lemma less_eq_Min_Bit1:
1194   "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
1195   unfolding Min_def Bit_def by auto
1197 lemma less_eq_Bit0_Pls:
1198   "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
1199   unfolding Pls_def Bit_def by simp
1201 lemma less_eq_Bit1_Pls:
1202   "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
1203   unfolding Pls_def Bit_def by auto
1205 lemma less_eq_Bit_Min:
1206   "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
1207   unfolding Min_def Bit_def by (cases v) auto
1209 lemma less_eq_Bit0_Bit:
1210   "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
1211   unfolding Min_def Bit_def bit.cases by (cases v) auto
1213 lemma less_eq_Bit_Bit1:
1214   "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
1215   unfolding Min_def Bit_def bit.cases by (cases v) auto
1217 lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
1218   less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
1219   less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1
1221 end