src/HOL/Presburger.thy
 author wenzelm Tue Jun 05 16:26:06 2007 +0200 (2007-06-05) changeset 23253 b1f3f53c60b5 parent 23164 69e55066dbca child 23314 6894137e854a permissions -rw-r--r--
1 (*  Title:      HOL/Presburger.thy
2     ID:         \$Id\$
3     Author:     Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen
4 *)
6 header {* Presburger Arithmetic: Cooper's Algorithm *}
8 theory Presburger
9 imports NatSimprocs SetInterval
10 uses
11   ("Tools/Presburger/cooper_dec.ML")
12   ("Tools/Presburger/cooper_proof.ML")
13   ("Tools/Presburger/qelim.ML")
14   ("Tools/Presburger/reflected_presburger.ML")
15   ("Tools/Presburger/reflected_cooper.ML")
16   ("Tools/Presburger/presburger.ML")
17 begin
19 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
21 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
22   apply (rule iffI)
23   apply (erule exE)
24   apply (rule_tac x = "l * x" in exI)
25   apply simp
26   apply (erule exE)
27   apply (erule conjE)
28   apply (erule dvdE)
29   apply (rule_tac x = k in exI)
30   apply simp
31   done
33 lemma uminus_dvd_conv: "(d dvd (t::int)) = (-d dvd t)"
34 apply(unfold dvd_def)
35 apply(rule iffI)
36 apply(clarsimp)
37 apply(rename_tac k)
38 apply(rule_tac x = "-k" in exI)
39 apply simp
40 apply(clarsimp)
41 apply(rename_tac k)
42 apply(rule_tac x = "-k" in exI)
43 apply simp
44 done
46 lemma uminus_dvd_conv': "(d dvd (t::int)) = (d dvd -t)"
47 apply(unfold dvd_def)
48 apply(rule iffI)
49 apply(clarsimp)
50 apply(rule_tac x = "-k" in exI)
51 apply simp
52 apply(clarsimp)
53 apply(rule_tac x = "-k" in exI)
54 apply simp
55 done
59 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}.*}
61 theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
62   \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
63   \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
64   apply (erule exE)+
65   apply (rule_tac x = "min z1 z2" in exI)
66   apply simp
67   done
70 theorem eq_minf_disjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
71   \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
72   \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))"
74   apply (erule exE)+
75   apply (rule_tac x = "min z1 z2" in exI)
76   apply simp
77   done
80 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}.*}
82 theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
83   \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
84   \<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
85   apply (erule exE)+
86   apply (rule_tac x = "max z1 z2" in exI)
87   apply simp
88   done
91 theorem eq_pinf_disjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
92   \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
93   \<exists>z::int. \<forall>x. z < x  \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))"
94   apply (erule exE)+
95   apply (rule_tac x = "max z1 z2" in exI)
96   apply simp
97   done
99 text {*
100   \medskip Theorems for the combination of proofs of the modulo @{text
101   D} property for @{text "P plusinfinity"}
103   FIXME: This is THE SAME theorem as for the @{text minusinf} version,
104   but with @{text "+k.."} instead of @{text "-k.."} In the future
105   replace these both with only one. *}
107 theorem modd_pinf_conjI: "\<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 \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
110   by simp
112 theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
113   \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
114   \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
115   by simp
117 text {*
118   This is one of the cases where the simplifed formula is prooved to
119   habe some property (in relation to @{text P_m}) but we need to prove
120   the property for the original formula (@{text P_m})
122   FIXME: This is exaclty the same thm as for @{text minusinf}. *}
124 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)) "
125   by blast
128 text {*
129   \medskip Theorems for the combination of proofs of the modulo @{text D}
130   property for @{text "P minusinfinity"} *}
132 theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
133   \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
134   \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
135   by simp
137 theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
138   \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
139   \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
140   by simp
142 text {*
143   This is one of the cases where the simplifed formula is prooved to
144   have some property (in relation to @{text P_m}) but we need to
145   prove the property for the original formula (@{text P_m}). *}
147 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)) "
148   by blast
150 text {*
151   Theorem needed for proving at runtime divide properties using the
152   arithmetic tactic (which knows only about modulo = 0). *}
154 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
157 text {*
158   \medskip Theorems used for the combination of proof for the
159   backwards direction of Cooper's Theorem. They rely exclusively on
160   Predicate calculus.*}
162 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))
163 ==>
164 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
165 ==>
166 (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))) "
167   by blast
170 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))
171 ==>
172 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
173 ==>
174 (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)
175 \<and> P2(x + d))) "
176   by blast
178 lemma not_ast_p_Q_elim: "
179 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
180 ==> ( P = Q )
181 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
182   by blast
184 text {*
185   \medskip Theorems used for the combination of proof for the
186   backwards direction of Cooper's Theorem. They rely exclusively on
187   Predicate calculus.*}
189 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))
190 ==>
191 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d))
192 ==>
193 (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)
194 \<or> P2(x-d))) "
195   by blast
197 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))
198 ==>
199 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d))
200 ==>
201 (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)
202 \<and> P2(x-d))) "
203   by blast
205 lemma not_bst_p_Q_elim: "
206 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d))
207 ==> ( P = Q )
208 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
209   by blast
211 text {* \medskip This is the first direction of Cooper's Theorem. *}
212 lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
213   by blast
215 text {*
216   \medskip The full Cooper's Theorem in its equivalence Form. Given
217   the premises it is trivial too, it relies exclusively on prediacte calculus.*}
218 lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
219 --> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
220   by blast
222 text {*
223   \medskip Some of the atomic theorems generated each time the atom
224   does not depend on @{text x}, they are trivial.*}
226 lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
227   by blast
229 lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
230   by blast
232 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"
233   by blast
235 lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
236   by blast
238 text {* The next two thms are the same as the @{text minusinf} version. *}
240 lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
241   by blast
243 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"
244   by blast
246 text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
248 lemma P_eqtrue: "(P=True) = P"
249   by iprover
251 lemma P_eqfalse: "(P=False) = (~P)"
252   by iprover
254 text {*
255   \medskip Theorems for the generation of the bachwards direction of
256   Cooper's Theorem.
258   These are the 6 interesting atomic cases which have to be proved relying on the
259   properties of B-set and the arithmetic and contradiction proofs. *}
261 lemma not_bst_p_lt: "0 < (d::int) ==>
262  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 )"
263   by arith
265 lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
266  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)"
267 apply clarsimp
268 apply(rule ccontr)
269 apply(drule_tac x = "x+a" in bspec)
271 apply(drule_tac x = "-a" in bspec)
272 apply assumption
273 apply(simp)
274 done
276 lemma not_bst_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a - 1 \<rbrakk> \<Longrightarrow>
277  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 )"
278 apply clarsimp
279 apply(subgoal_tac "x = -a")
280  prefer 2 apply arith
281 apply(drule_tac x = "1" in bspec)
283 apply(drule_tac x = "-a- 1" in bspec)
284 apply assumption
285 apply(simp)
286 done
289 lemma not_bst_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
290  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)"
291 apply clarsimp
292 apply(subgoal_tac "x = -a+d")
293  prefer 2 apply arith
294 apply(drule_tac x = "d" in bspec)
296 apply(drule_tac x = "-a" in bspec)
297 apply assumption
298 apply(simp)
299 done
302 lemma not_bst_p_dvd: "(d1::int) dvd d ==>
303  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 )"
305 apply(rename_tac m)
306 apply(rule_tac x = "m - k" in exI)
308 done
310 lemma not_bst_p_ndvd: "(d1::int) dvd d ==>
311  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(rename_tac m)
314 apply(erule_tac x = "m + k" in allE)
316 done
318 text {*
319   \medskip Theorems for the generation of the bachwards direction of
320   Cooper's Theorem.
322   These are the 6 interesting atomic cases which have to be proved
323   relying on the properties of A-set ant the arithmetic and
326 lemma not_ast_p_gt: "0 < (d::int) ==>
327  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 )"
328   by arith
330 lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
331  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)"
332   apply clarsimp
333   apply (rule ccontr)
334   apply (drule_tac x = "t-x" in bspec)
335   apply simp
336   apply (drule_tac x = "t" in bspec)
337   apply assumption
338   apply simp
339   done
341 lemma not_ast_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t + 1 \<rbrakk> \<Longrightarrow>
342  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 )"
343   apply clarsimp
344   apply (drule_tac x="1" in bspec)
345   apply simp
346   apply (drule_tac x="- t + 1" in bspec)
347   apply assumption
348   apply(subgoal_tac "x = -t")
349   prefer 2 apply arith
350   apply simp
351   done
353 lemma not_ast_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t \<rbrakk> \<Longrightarrow>
354  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)"
355   apply clarsimp
356   apply (subgoal_tac "x = -t-d")
357   prefer 2 apply arith
358   apply (drule_tac x = "d" in bspec)
359   apply simp
360   apply (drule_tac x = "-t" in bspec)
361   apply assumption
362   apply simp
363   done
365 lemma not_ast_p_dvd: "(d1::int) dvd d ==>
366  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 )"
368   apply(rename_tac m)
369   apply(rule_tac x = "m + k" in exI)
371   done
373 lemma not_ast_p_ndvd: "(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 ))"
376   apply(rename_tac m)
377   apply(erule_tac x = "m - k" in allE)
379   done
381 text {*
382   \medskip These are the atomic cases for the proof generation for the
383   modulo @{text D} property for @{text "P plusinfinity"}
385   They are fully based on arithmetics. *}
387 lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
388  (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
390   apply(rule iffI)
391   apply(clarsimp)
392   apply(rename_tac n m)
393   apply(rule_tac x = "m + n*k" in exI)
395   apply(clarsimp)
396   apply(rename_tac n m)
397   apply(rule_tac x = "m - n*k" in exI)
399   done
401 lemma  not_dvd_modd_pinf: "((d::int) dvd d1) ==>
402  (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x+k*d1 + t))))"
404   apply(rule iffI)
405   apply(clarsimp)
406   apply(rename_tac n m)
407   apply(erule_tac x = "m - n*k" in allE)
409   apply(clarsimp)
410   apply(rename_tac n m)
411   apply(erule_tac x = "m + n*k" in allE)
413   done
415 text {*
416   \medskip These are the atomic cases for the proof generation for the
417   equivalence of @{text P} and @{text "P plusinfinity"} for integers
418   @{text x} greater than some integer @{text z}.
420   They are fully based on arithmetics. *}
422 lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
423   apply(rule_tac x = "-t" in exI)
424   apply simp
425   done
427 lemma  neq_eq_pinf: "EX z::int. ALL x.  z < x --> ((~( 0 = x +t )) = True )"
428   apply(rule_tac x = "-t" in exI)
429   apply simp
430   done
432 lemma  le_eq_pinf: "EX z::int. ALL x.  z < x --> ( 0 < x +t  = True )"
433   apply(rule_tac x = "-t" in exI)
434   apply simp
435   done
437 lemma  len_eq_pinf: "EX z::int. ALL x. z < x  --> (0 < -x +t  = False )"
438   apply(rule_tac x = "t" in exI)
439   apply simp
440   done
442 lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
443   by simp
445 lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
446   by simp
448 text {*
449   \medskip These are the atomic cases for the proof generation for the
450   modulo @{text D} property for @{text "P minusinfinity"}.
452   They are fully based on arithmetics. *}
454 lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
455  (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
457 apply(rule iffI)
458 apply(clarsimp)
459 apply(rename_tac n m)
460 apply(rule_tac x = "m - n*k" in exI)
462 apply(clarsimp)
463 apply(rename_tac n m)
464 apply(rule_tac x = "m + n*k" in exI)
466 done
469 lemma  not_dvd_modd_minf: "((d::int) dvd d1) ==>
470  (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x-k*d1 + t))))"
472 apply(rule iffI)
473 apply(clarsimp)
474 apply(rename_tac n m)
475 apply(erule_tac x = "m + n*k" in allE)
477 apply(clarsimp)
478 apply(rename_tac n m)
479 apply(erule_tac x = "m - n*k" in allE)
481 done
483 text {*
484   \medskip These are the atomic cases for the proof generation for the
485   equivalence of @{text P} and @{text "P minusinfinity"} for integers
486   @{text x} less than some integer @{text z}.
488   They are fully based on arithmetics. *}
490 lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
491 apply(rule_tac x = "-t" in exI)
492 apply simp
493 done
495 lemma  neq_eq_minf: "EX z::int. ALL x. x < z --> ((~( 0 = x +t )) = True )"
496 apply(rule_tac x = "-t" in exI)
497 apply simp
498 done
500 lemma  le_eq_minf: "EX z::int. ALL x. x < z --> ( 0 < x +t  = False )"
501 apply(rule_tac x = "-t" in exI)
502 apply simp
503 done
506 lemma  len_eq_minf: "EX z::int. ALL x. x < z --> (0 < -x +t  = True )"
507 apply(rule_tac x = "t" in exI)
508 apply simp
509 done
511 lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
512   by simp
514 lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
515   by simp
517 text {*
518   \medskip This Theorem combines whithnesses about @{text "P
519   minusinfinity"} to show one component of the equivalence proof for
520   Cooper's Theorem.
522   FIXME: remove once they are part of the distribution. *}
524 theorem int_ge_induct[consumes 1,case_names base step]:
525   assumes ge: "k \<le> (i::int)" and
526         base: "P(k)" and
527         step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
528   shows "P i"
529 proof -
530   { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
531     proof (induct n)
532       case 0
533       hence "i = k" by arith
534       thus "P i" using base by simp
535     next
536       case (Suc n)
537       hence "n = nat((i - 1) - k)" by arith
538       moreover
539       have ki1: "k \<le> i - 1" using Suc.prems by arith
540       ultimately
541       have "P(i - 1)" by(rule Suc.hyps)
542       from step[OF ki1 this] show ?case by simp
543     qed
544   }
545   from this ge show ?thesis by fast
546 qed
548 theorem int_gr_induct[consumes 1,case_names base step]:
549   assumes gr: "k < (i::int)" and
550         base: "P(k+1)" and
551         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
552   shows "P i"
553 apply(rule int_ge_induct[of "k + 1"])
554   using gr apply arith
555  apply(rule base)
556 apply(rule step)
557  apply simp+
558 done
560 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
561 apply(induct rule: int_gr_induct)
562  apply simp
564 done
566 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
567 apply(induct rule: int_gr_induct)
568  apply simp
570 done
572 lemma  minusinfinity:
573   assumes "0 < d" and
574     P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and
575     ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
576   shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
577 proof
578   assume eP1: "EX x. P1 x"
579   then obtain x where P1: "P1 x" ..
580   from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
581   let ?w = "x - (abs(x-z)+1) * d"
582   show "EX x. P x"
583   proof
584     have w: "?w < z" by(rule decr_lemma)
585     have "P1 x = P1 ?w" using P1eqP1 by blast
586     also have "\<dots> = P(?w)" using w P1eqP by blast
587     finally show "P ?w" using P1 by blast
588   qed
589 qed
591 text {*
592   \medskip This Theorem combines whithnesses about @{text "P
593   minusinfinity"} to show one component of the equivalence proof for
594   Cooper's Theorem. *}
596 lemma plusinfinity:
597   assumes "0 < d" and
598     P1eqP1: "ALL (x::int) (k::int). P1 x = P1 (x + k * d)" and
599     ePeqP1: "EX z::int. ALL x. z < x  --> (P x = P1 x)"
600   shows "(EX x::int. P1 x) --> (EX x::int. P x)"
601 proof
602   assume eP1: "EX x. P1 x"
603   then obtain x where P1: "P1 x" ..
604   from ePeqP1 obtain z where P1eqP: "ALL x. z < x \<longrightarrow> (P x = P1 x)" ..
605   let ?w = "x + (abs(x-z)+1) * d"
606   show "EX x. P x"
607   proof
608     have w: "z < ?w" by(rule incr_lemma)
609     have "P1 x = P1 ?w" using P1eqP1 by blast
610     also have "\<dots> = P(?w)" using w P1eqP by blast
611     finally show "P ?w" using P1 by blast
612   qed
613 qed
615 text {*
616   \medskip Theorem for periodic function on discrete sets. *}
618 lemma minf_vee:
619   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
620   shows "(EX x. P x) = (EX j : {1..d}. P j)"
621   (is "?LHS = ?RHS")
622 proof
623   assume ?LHS
624   then obtain x where P: "P x" ..
625   have "x mod d = x - (x div d)*d"
627   hence Pmod: "P x = P(x mod d)" using modd by simp
628   show ?RHS
629   proof (cases)
630     assume "x mod d = 0"
631     hence "P 0" using P Pmod by simp
632     moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
633     ultimately have "P d" by simp
634     moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
635     ultimately show ?RHS ..
636   next
637     assume not0: "x mod d \<noteq> 0"
638     have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
639     moreover have "x mod d : {1..d}"
640     proof -
641       have "0 \<le> x mod d" by(rule pos_mod_sign)
642       moreover have "x mod d < d" by(rule pos_mod_bound)
643       ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
644     qed
645     ultimately show ?RHS ..
646   qed
647 next
648   assume ?RHS thus ?LHS by blast
649 qed
651 text {*
652   \medskip Theorem for periodic function on discrete sets. *}
654 lemma pinf_vee:
655   assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
656   shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
657   (is "?LHS = ?RHS")
658 proof
659   assume ?LHS
660   then obtain x where P: "P x" ..
661   have "x mod d = x + (-(x div d))*d"
663   hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
664   show ?RHS
665   proof (cases)
666     assume "x mod d = 0"
667     hence "P 0" using P Pmod by simp
668     moreover have "P 0 = P(0 + 1*d)" using modd by blast
669     ultimately have "P d" by simp
670     moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
671     ultimately show ?RHS ..
672   next
673     assume not0: "x mod d \<noteq> 0"
674     have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
675     moreover have "x mod d : {1..d}"
676     proof -
677       have "0 \<le> x mod d" by(rule pos_mod_sign)
678       moreover have "x mod d < d" by(rule pos_mod_bound)
679       ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
680     qed
681     ultimately show ?RHS ..
682   qed
683 next
684   assume ?RHS thus ?LHS by blast
685 qed
687 lemma decr_mult_lemma:
688   assumes dpos: "(0::int) < d" and
689           minus: "ALL x::int. P x \<longrightarrow> P(x - d)" and
690           knneg: "0 <= k"
691   shows "ALL x. P x \<longrightarrow> P(x - k*d)"
692 using knneg
693 proof (induct rule:int_ge_induct)
694   case base thus ?case by simp
695 next
696   case (step i)
697   show ?case
698   proof
699     fix x
700     have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
701     also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
702       using minus[THEN spec, of "x - i * d"]
704     ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
705   qed
706 qed
708 lemma incr_mult_lemma:
709   assumes dpos: "(0::int) < d" and
710           plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and
711           knneg: "0 <= k"
712   shows "ALL x. P x \<longrightarrow> P(x + k*d)"
713 using knneg
714 proof (induct rule:int_ge_induct)
715   case base thus ?case by simp
716 next
717   case (step i)
718   show ?case
719   proof
720     fix x
721     have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
722     also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)"
723       using plus[THEN spec, of "x + i * d"]
725     ultimately show "P x \<longrightarrow> P(x + (i + 1) * d)" by blast
726   qed
727 qed
729 lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
730 ==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D)
731 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
732 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
733 apply(rule iffI)
734 prefer 2
735 apply(drule minusinfinity)
736 apply assumption+
737 apply(fastsimp)
738 apply clarsimp
739 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
740 apply(frule_tac x = x and z=z in decr_lemma)
741 apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
742 prefer 2
743 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
744 prefer 2 apply arith
745  apply fastsimp
746 apply(drule (1) minf_vee)
747 apply blast
748 apply(blast dest:decr_mult_lemma)
749 done
751 text {* Cooper Theorem, plus infinity version. *}
752 lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
753 ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D)
754 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
755 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)))"
756   apply(rule iffI)
757   prefer 2
758   apply(drule plusinfinity)
759   apply assumption+
760   apply(fastsimp)
761   apply clarsimp
762   apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x + k*D)")
763   apply(frule_tac x = x and z=z in incr_lemma)
764   apply(subgoal_tac "P1(x + (\<bar>x - z\<bar> + 1) * D)")
765   prefer 2
766   apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
767   prefer 2 apply arith
768   apply fastsimp
769   apply(drule (1) pinf_vee)
770   apply blast
771   apply(blast dest:incr_mult_lemma)
772   done
775 text {*
776   \bigskip Theorems for the quantifier elminination Functions. *}
778 lemma qe_ex_conj: "(EX (x::int). A x) = R
779 		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
780 		==> (EX (x::int). P x) = (Q & R)"
781 by blast
783 lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q)
784 		==> (EX (x::int). P x) = Q"
785 by blast
787 lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)"
788 by blast
790 lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)"
791 by blast
793 lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)"
794 by blast
796 lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)"
797 by blast
799 lemma qe_Not: "P = Q ==> (~P) = (~Q)"
800 by blast
802 lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
803 by blast
805 text {* \bigskip Theorems for proving NNF *}
807 lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
808 by blast
810 lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))"
811 by blast
813 lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)"
814   by blast
815 lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))"
816 by blast
818 lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))"
819 by blast
820 lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))"
821 by blast
822 lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))"
823 by blast
824 lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))"
825 by blast
828 lemma qe_exI2: "A = B ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
829   by simp
831 lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
832   by iprover
834 lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
835   by iprover
837 lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
838 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
839 by blast
841 lemma cppi_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j)))
842 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) "
843 by blast
846 lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
848 apply(fastsimp)
849 done
851 text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
853 lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
854 shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
855 proof
856   assume ?P
857   thus ?Q
859     apply clarify
860     apply(rename_tac d)
861     apply(drule_tac f = "op * k" in arg_cong)
862     apply(simp only:int_distrib)
863     apply(rule_tac x = "d" in exI)
864     apply(simp only:mult_ac)
865     done
866 next
867   assume ?Q
868   then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
869   hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
870   hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
871   hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
873 qed
875 lemma ac_lt_eq: assumes gr0: "0 < (k::int)"
876 shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
877 proof
878   assume P: ?P
879   show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
880 next
881   assume ?Q
882   hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
883   with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
884   thus ?P by(simp)
885 qed
887 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")
888 proof
889   assume ?P
890   thus ?Q
891     apply(drule_tac f = "op * k" in arg_cong)
892     apply(simp only:int_distrib)
893     done
894 next
895   assume ?Q
896   hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
897   hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
898   thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
899 qed
901 lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
902 proof -
903   have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
904   also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
905   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])
906   also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
907   finally show ?thesis .
908 qed
910 lemma binminus_uminus_conv: "(a::int) - b = a + (-b)"
911 by arith
913 lemma  linearize_dvd: "(t::int) = t1 ==> (d dvd t) = (d dvd t1)"
914 by simp
916 lemma lf_lt: "(l::int) = ll ==> (r::int) = lr ==> (l < r) =(ll < lr)"
917 by simp
919 lemma lf_eq: "(l::int) = ll ==> (r::int) = lr ==> (l = r) =(ll = lr)"
920 by simp
922 lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
923 by simp
925 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
927 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
928   by (simp split add: split_nat)
931 theorem zdiff_int_split: "P (int (x - y)) =
932   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
933   apply (case_tac "y \<le> x")
935   done
938 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
939   by simp
941 theorem number_of2: "(0::int) <= Numeral0" by simp
943 theorem Suc_plus1: "Suc n = n + 1" by simp
945 text {*
946   \medskip Specific instances of congruence rules, to prevent
947   simplifier from looping. *}
949 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
950   by simp
952 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
953   by (simp cong: conj_cong)
955     (* Theorems used in presburger.ML for the computation simpset*)
956     (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*)
958 lemma lift_bool: "x \<Longrightarrow> x=True"
959   by simp
961 lemma nlift_bool: "~x \<Longrightarrow> x=False"
962   by simp
964 lemma not_false_eq_true: "(~ False) = True" by simp
966 lemma not_true_eq_false: "(~ True) = False" by simp
969 lemma int_eq_number_of_eq:
970   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
971   by simp
972 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
973   by (simp only: iszero_number_of_Pls)
975 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
976   by simp
978 lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
979   by simp
981 lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
982   by simp
984 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
985   by simp
987 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
988   by simp
990 lemma int_neg_number_of_Min: "neg (-1::int)"
991   by simp
993 lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
994   by simp
996 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
997   by simp
998 lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
999   by simp
1001 lemma int_number_of_diff_sym:
1002   "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
1003   by simp
1005 lemma int_number_of_mult_sym:
1006   "((number_of v)::int) * number_of w = number_of (v * w)"
1007   by simp
1009 lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
1010   by simp
1012   by simp
1015   by simp
1017 lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
1018   by simp
1020 lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
1021   by simp
1023 lemma int_pow_0: "(a::int)^(Numeral0) = 1"
1024   by simp
1026 lemma int_pow_1: "(a::int)^(Numeral1) = a"
1027   by simp
1029 lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
1030   by simp
1032 lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
1033   by simp
1035 lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
1036   by simp
1038 lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
1039   by simp
1041 lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
1042   by simp
1044 lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
1045 proof -
1046   have 1:"((-1)::nat) = 0"
1047     by simp
1048   show ?thesis by (simp add: 1)
1049 qed
1051 use "Tools/Presburger/cooper_dec.ML"
1052 use "Tools/Presburger/reflected_presburger.ML"
1053 use "Tools/Presburger/reflected_cooper.ML"
1054 oracle
1055   presburger_oracle ("term") = ReflectedCooper.presburger_oracle
1057 use "Tools/Presburger/cooper_proof.ML"
1058 use "Tools/Presburger/qelim.ML"
1059 use "Tools/Presburger/presburger.ML"
1061 setup "Presburger.setup"
1064 subsection {* Code generator setup *}
1066 text {*
1067   Presburger arithmetic is convenient to prove some
1068   of the following code lemmas on integer numerals:
1069 *}
1071 lemma eq_Pls_Pls:
1072   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
1074 lemma eq_Pls_Min:
1075   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
1076   unfolding Pls_def Min_def by auto
1078 lemma eq_Pls_Bit0:
1079   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
1080   unfolding Pls_def Bit_def bit.cases by auto
1082 lemma eq_Pls_Bit1:
1083   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
1084   unfolding Pls_def Bit_def bit.cases by arith
1086 lemma eq_Min_Pls:
1087   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
1088   unfolding Pls_def Min_def by auto
1090 lemma eq_Min_Min:
1091   "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
1093 lemma eq_Min_Bit0:
1094   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
1095   unfolding Min_def Bit_def bit.cases by arith
1097 lemma eq_Min_Bit1:
1098   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
1099   unfolding Min_def Bit_def bit.cases by auto
1101 lemma eq_Bit0_Pls:
1102   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
1103   unfolding Pls_def Bit_def bit.cases by auto
1105 lemma eq_Bit1_Pls:
1106   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
1107   unfolding Pls_def Bit_def bit.cases by arith
1109 lemma eq_Bit0_Min:
1110   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
1111   unfolding Min_def Bit_def bit.cases by arith
1113 lemma eq_Bit1_Min:
1114   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
1115   unfolding Min_def Bit_def bit.cases by auto
1117 lemma eq_Bit_Bit:
1118   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
1119     v1 = v2 \<and> k1 = k2"
1120   unfolding Bit_def
1121   apply (cases v1)
1122   apply (cases v2)
1123   apply auto
1124   apply arith
1125   apply (cases v2)
1126   apply auto
1127   apply arith
1128   apply (cases v2)
1129   apply auto
1130 done
1132 lemma eq_number_of:
1133   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
1134   unfolding number_of_is_id ..
1137 lemma less_eq_Pls_Pls:
1138   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
1140 lemma less_eq_Pls_Min:
1141   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
1142   unfolding Pls_def Min_def by auto
1144 lemma less_eq_Pls_Bit:
1145   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
1146   unfolding Pls_def Bit_def by (cases v) auto
1148 lemma less_eq_Min_Pls:
1149   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
1150   unfolding Pls_def Min_def by auto
1152 lemma less_eq_Min_Min:
1153   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
1155 lemma less_eq_Min_Bit0:
1156   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
1157   unfolding Min_def Bit_def by auto
1159 lemma less_eq_Min_Bit1:
1160   "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
1161   unfolding Min_def Bit_def by auto
1163 lemma less_eq_Bit0_Pls:
1164   "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
1165   unfolding Pls_def Bit_def by simp
1167 lemma less_eq_Bit1_Pls:
1168   "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
1169   unfolding Pls_def Bit_def by auto
1171 lemma less_eq_Bit_Min:
1172   "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
1173   unfolding Min_def Bit_def by (cases v) auto
1175 lemma less_eq_Bit0_Bit:
1176   "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
1177   unfolding Bit_def bit.cases by (cases v) auto
1179 lemma less_eq_Bit_Bit1:
1180   "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
1181   unfolding Bit_def bit.cases by (cases v) auto
1183 lemma less_eq_Bit1_Bit0:
1184   "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
1185   unfolding Bit_def by (auto split: bit.split)
1187 lemma less_eq_number_of:
1188   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
1189   unfolding number_of_is_id ..
1192 lemma less_Pls_Pls:
1193   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
1195 lemma less_Pls_Min:
1196   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
1197   unfolding Pls_def Min_def by auto
1199 lemma less_Pls_Bit0:
1200   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
1201   unfolding Pls_def Bit_def by auto
1203 lemma less_Pls_Bit1:
1204   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
1205   unfolding Pls_def Bit_def by auto
1207 lemma less_Min_Pls:
1208   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
1209   unfolding Pls_def Min_def by auto
1211 lemma less_Min_Min:
1212   "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
1214 lemma less_Min_Bit:
1215   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
1216   unfolding Min_def Bit_def by (auto split: bit.split)
1218 lemma less_Bit_Pls:
1219   "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
1220   unfolding Pls_def Bit_def by (auto split: bit.split)
1222 lemma less_Bit0_Min:
1223   "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
1224   unfolding Min_def Bit_def by auto
1226 lemma less_Bit1_Min:
1227   "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
1228   unfolding Min_def Bit_def by auto
1230 lemma less_Bit_Bit0:
1231   "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
1232   unfolding Bit_def by (auto split: bit.split)
1234 lemma less_Bit1_Bit:
1235   "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
1236   unfolding Bit_def by (auto split: bit.split)
1238 lemma less_Bit0_Bit1:
1239   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
1240   unfolding Bit_def bit.cases by auto
1242 lemma less_number_of:
1243   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
1244   unfolding number_of_is_id ..
1247 lemmas pred_succ_numeral_code [code func] =
1248   arith_simps(5-12)
1250 lemmas plus_numeral_code [code func] =
1251   arith_simps(13-17)
1252   arith_simps(26-27)
1253   arith_extra_simps(1) [where 'a = int]
1255 lemmas minus_numeral_code [code func] =
1256   arith_simps(18-21)
1257   arith_extra_simps(2) [where 'a = int]
1258   arith_extra_simps(5) [where 'a = int]
1260 lemmas times_numeral_code [code func] =
1261   arith_simps(22-25)
1262   arith_extra_simps(4) [where 'a = int]
1264 lemmas eq_numeral_code [code func] =
1265   eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
1266   eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
1267   eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
1268   eq_number_of
1270 lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
1271   less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
1272   less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
1273   less_eq_number_of
1275 lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
1276   less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
1277   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
1278   less_number_of
1280 end