src/HOL/Presburger.thy
 author chaieb Sat Jan 06 20:47:09 2007 +0100 (2007-01-06) changeset 22026 cc60e54aa7cb parent 21454 a1937c51ed88 child 22394 54ea68b5a92f permissions -rw-r--r--
A few theorems on integer divisibily.
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))"
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 )"
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 ))"
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
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 )"
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 ))"
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))))"
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)
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))))"
403   apply(rule iffI)
404   apply(clarsimp)
405   apply(rename_tac n m)
406   apply(erule_tac x = "m - n*k" in allE)
408   apply(clarsimp)
409   apply(rename_tac n m)
410   apply(erule_tac x = "m + n*k" in allE)
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))))"
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)
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))))"
471 apply(rule iffI)
472 apply(clarsimp)
473 apply(rename_tac n m)
474 apply(erule_tac x = "m + n*k" in allE)
476 apply(clarsimp)
477 apply(rename_tac n m)
478 apply(erule_tac x = "m - n*k" in allE)
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
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
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"
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"
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"]
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})"
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]])
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)
930 theorem zdiff_int_split: "P (int (x - y)) =
931   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
932   apply (case_tac "y \<le> x")
934   done
937 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
938   by simp
940 theorem number_of2: "(0::int) <= Numeral0" by simp
942 theorem Suc_plus1: "Suc n = n + 1" by simp
944 text {*
945   \medskip Specific instances of congruence rules, to prevent
946   simplifier from looping. *}
948 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
949   by simp
951 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
952   by (simp cong: conj_cong)
954     (* Theorems used in presburger.ML for the computation simpset*)
955     (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*)
957 lemma lift_bool: "x \<Longrightarrow> x=True"
958   by simp
960 lemma nlift_bool: "~x \<Longrightarrow> x=False"
961   by simp
963 lemma not_false_eq_true: "(~ False) = True" by simp
965 lemma not_true_eq_false: "(~ True) = False" by simp
968 lemma int_eq_number_of_eq:
969   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
970   by simp
971 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
972   by (simp only: iszero_number_of_Pls)
974 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
975   by simp
977 lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
978   by simp
980 lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
981   by simp
983 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
984   by simp
986 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
987   by simp
989 lemma int_neg_number_of_Min: "neg (-1::int)"
990   by simp
992 lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
993   by simp
995 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
996   by simp
997 lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
998   by simp
1000 lemma int_number_of_diff_sym:
1001   "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
1002   by simp
1004 lemma int_number_of_mult_sym:
1005   "((number_of v)::int) * number_of w = number_of (v * w)"
1006   by simp
1008 lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
1009   by simp
1011   by simp
1014   by simp
1016 lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
1017   by simp
1019 lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
1020   by simp
1022 lemma int_pow_0: "(a::int)^(Numeral0) = 1"
1023   by simp
1025 lemma int_pow_1: "(a::int)^(Numeral1) = a"
1026   by simp
1028 lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
1029   by simp
1031 lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
1032   by simp
1034 lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
1035   by simp
1037 lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
1038   by simp
1040 lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
1041   by simp
1043 lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
1044 proof -
1045   have 1:"((-1)::nat) = 0"
1046     by simp
1047   show ?thesis by (simp add: 1)
1048 qed
1050 use "cooper_dec.ML"
1051 use "reflected_presburger.ML"
1052 use "reflected_cooper.ML"
1053 oracle
1054   presburger_oracle ("term") = ReflectedCooper.presburger_oracle
1056 use "cooper_proof.ML"
1057 use "qelim.ML"
1058 use "presburger.ML"
1060 setup "Presburger.setup"
1062 text {* Code generator setup *}
1064 text {*
1065   Presburger arithmetic is necessary (at least convenient) to prove some
1066   of the following code lemmas on integer numerals.
1067 *}
1069 lemma eq_number_of [code func]:
1070   "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
1071   unfolding number_of_is_id ..
1073 lemma less_eq_number_of [code func]:
1074   "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l"
1075   unfolding number_of_is_id ..
1077 lemma eq_Pls_Pls:
1078   "Numeral.Pls = Numeral.Pls" ..
1080 lemma eq_Pls_Min:
1081   "Numeral.Pls \<noteq> Numeral.Min"
1082   unfolding Pls_def Min_def by auto
1084 lemma eq_Pls_Bit0:
1085   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
1086   unfolding Pls_def Bit_def bit.cases by auto
1088 lemma eq_Pls_Bit1:
1089   "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
1090   unfolding Pls_def Bit_def bit.cases by arith
1092 lemma eq_Min_Pls:
1093   "Numeral.Min \<noteq> Numeral.Pls"
1094   unfolding Pls_def Min_def by auto
1096 lemma eq_Min_Min:
1097   "Numeral.Min = Numeral.Min" ..
1099 lemma eq_Min_Bit0:
1100   "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
1101   unfolding Min_def Bit_def bit.cases by arith
1103 lemma eq_Min_Bit1:
1104   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
1105   unfolding Min_def Bit_def bit.cases by auto
1107 lemma eq_Bit0_Pls:
1108   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
1109   unfolding Pls_def Bit_def bit.cases by auto
1111 lemma eq_Bit1_Pls:
1112   "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
1113   unfolding Pls_def Bit_def bit.cases by arith
1115 lemma eq_Bit0_Min:
1116   "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
1117   unfolding Min_def Bit_def bit.cases by arith
1119 lemma eq_Bit1_Min:
1120   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
1121   unfolding Min_def Bit_def bit.cases by auto
1123 lemma eq_Bit_Bit:
1124   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
1125     v1 = v2 \<and> k1 = k2"
1126   unfolding Bit_def
1127   apply (cases v1)
1128   apply (cases v2)
1129   apply auto
1130   apply arith
1131   apply (cases v2)
1132   apply auto
1133   apply arith
1134   apply (cases v2)
1135   apply auto
1136 done
1138 lemmas eq_numeral_code [code func] =
1139   eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
1140   eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
1141   eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
1143 lemma less_eq_Pls_Pls:
1144   "Numeral.Pls \<le> Numeral.Pls" ..
1146 lemma less_eq_Pls_Min:
1147   "\<not> (Numeral.Pls \<le> Numeral.Min)"
1148   unfolding Pls_def Min_def by auto
1150 lemma less_eq_Pls_Bit:
1151   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
1152   unfolding Pls_def Bit_def by (cases v) auto
1154 lemma less_eq_Min_Pls:
1155   "Numeral.Min \<le> Numeral.Pls"
1156   unfolding Pls_def Min_def by auto
1158 lemma less_eq_Min_Min:
1159   "Numeral.Min \<le> Numeral.Min" ..
1161 lemma less_eq_Min_Bit0:
1162   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
1163   unfolding Min_def Bit_def by auto
1165 lemma less_eq_Min_Bit1:
1166   "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
1167   unfolding Min_def Bit_def by auto
1169 lemma less_eq_Bit0_Pls:
1170   "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
1171   unfolding Pls_def Bit_def by simp
1173 lemma less_eq_Bit1_Pls:
1174   "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
1175   unfolding Pls_def Bit_def by auto
1177 lemma less_eq_Bit_Min:
1178   "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
1179   unfolding Min_def Bit_def by (cases v) auto
1181 lemma less_eq_Bit0_Bit:
1182   "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
1183   unfolding Min_def Bit_def bit.cases by (cases v) auto
1185 lemma less_eq_Bit_Bit1:
1186   "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
1187   unfolding Min_def Bit_def bit.cases by (cases v) auto
1189 lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
1190   less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
1191   less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1
1193 end