src/HOL/Integ/Presburger.thy
author chaieb
Wed May 19 11:23:59 2004 +0200 (2004-05-19)
changeset 14758 af3b71a46a1c
parent 14738 83f1a514dcb4
child 14941 1edb674e0c33
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
     1 (*  Title:      HOL/Integ/Presburger.thy
     2     ID:         $Id$
     3     Author:     Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 File containing necessary theorems for the proof
     7 generation for Cooper Algorithm  
     8 *)
     9 
    10 header {* Presburger Arithmetic: Cooper Algorithm *}
    11 
    12 theory Presburger = NatSimprocs + SetInterval
    13 files
    14   ("cooper_dec.ML")
    15   ("cooper_proof.ML")
    16   ("qelim.ML")
    17   ("presburger.ML"):
    18 
    19 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    20 
    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
    32 
    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
    45 
    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
    56 
    57 
    58 
    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}.*}
    60 
    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
    68 
    69 
    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))"
    73 
    74   apply (erule exE)+
    75   apply (rule_tac x = "min z1 z2" in exI)
    76   apply simp
    77   done
    78 
    79 
    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}.*}
    81 
    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
    89 
    90 
    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
    98 
    99 text {*
   100   \medskip Theorems for the combination of proofs of the modulo @{text
   101   D} property for @{text "P plusinfinity"}
   102 
   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. *}
   106 
   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
   111 
   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
   116 
   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})
   121 
   122   FIXME: This is exaclty the same thm as for @{text minusinf}. *}
   123 
   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
   126 
   127 
   128 text {*
   129   \medskip Theorems for the combination of proofs of the modulo @{text D}
   130   property for @{text "P minusinfinity"} *}
   131 
   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
   136 
   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
   141 
   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}). *}
   146 
   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
   149 
   150 text {*
   151   Theorem needed for proving at runtime divide properties using the
   152   arithmetic tactic (which knows only about modulo = 0). *}
   153 
   154 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   155   by(simp add:dvd_def zmod_eq_0_iff)
   156 
   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.*}
   161 
   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
   168 
   169 
   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
   177 
   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
   183 
   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.*}
   188 
   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
   196 
   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
   204 
   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
   210 
   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
   214 
   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
   221 
   222 text {*
   223   \medskip Some of the atomic theorems generated each time the atom
   224   does not depend on @{text x}, they are trivial.*}
   225 
   226 lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
   227   by blast
   228 
   229 lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
   230   by blast
   231 
   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
   234 
   235 lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
   236   by blast
   237 
   238 text {* The next two thms are the same as the @{text minusinf} version. *}
   239 
   240 lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
   241   by blast
   242 
   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
   245 
   246 text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
   247 
   248 lemma P_eqtrue: "(P=True) = P"
   249   by rules
   250 
   251 lemma P_eqfalse: "(P=False) = (~P)"
   252   by rules
   253 
   254 text {*
   255   \medskip Theorems for the generation of the bachwards direction of
   256   Cooper's Theorem.
   257 
   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. *}
   260 
   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
   264 
   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)
   270 apply(simp add:atLeastAtMost_iff)
   271 apply(drule_tac x = "-a" in bspec)
   272 apply assumption
   273 apply(simp)
   274 done
   275 
   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)
   282 apply(simp add:atLeastAtMost_iff)
   283 apply(drule_tac x = "-a- 1" in bspec)
   284 apply assumption
   285 apply(simp)
   286 done
   287 
   288 
   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)
   295 apply(simp add:atLeastAtMost_iff)
   296 apply(drule_tac x = "-a" in bspec)
   297 apply assumption
   298 apply(simp)
   299 done
   300 
   301 
   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 )"
   304 apply(clarsimp simp add:dvd_def)
   305 apply(rename_tac m)
   306 apply(rule_tac x = "m - k" in exI)
   307 apply(simp add:int_distrib)
   308 done
   309 
   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 ))"
   312 apply(clarsimp simp add:dvd_def)
   313 apply(rename_tac m)
   314 apply(erule_tac x = "m + k" in allE)
   315 apply(simp add:int_distrib)
   316 done
   317 
   318 text {*
   319   \medskip Theorems for the generation of the bachwards direction of
   320   Cooper's Theorem.
   321 
   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
   324   contradiction proofs. *}
   325 
   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
   329 
   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
   340 
   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
   352 
   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
   364 
   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 )"
   367   apply(clarsimp simp add:dvd_def)
   368   apply(rename_tac m)
   369   apply(rule_tac x = "m + k" in exI)
   370   apply(simp add:int_distrib)
   371   done
   372 
   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 ))"
   375   apply(clarsimp simp add:dvd_def)
   376   apply(rename_tac m)
   377   apply(erule_tac x = "m - k" in allE)
   378   apply(simp add:int_distrib)
   379   done
   380 
   381 text {*
   382   \medskip These are the atomic cases for the proof generation for the
   383   modulo @{text D} property for @{text "P plusinfinity"}
   384 
   385   They are fully based on arithmetics. *}
   386 
   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))))"
   389   apply(clarsimp simp add:dvd_def)
   390   apply(rule iffI)
   391   apply(clarsimp)
   392   apply(rename_tac n m)
   393   apply(rule_tac x = "m + n*k" in exI)
   394   apply(simp add:int_distrib)
   395   apply(clarsimp)
   396   apply(rename_tac n m)
   397   apply(rule_tac x = "m - n*k" in exI)
   398   apply(simp add:int_distrib mult_ac)
   399   done
   400 
   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))))"
   403   apply(clarsimp simp add:dvd_def)
   404   apply(rule iffI)
   405   apply(clarsimp)
   406   apply(rename_tac n m)
   407   apply(erule_tac x = "m - n*k" in allE)
   408   apply(simp add:int_distrib mult_ac)
   409   apply(clarsimp)
   410   apply(rename_tac n m)
   411   apply(erule_tac x = "m + n*k" in allE)
   412   apply(simp add:int_distrib mult_ac)
   413   done
   414 
   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}.
   419 
   420   They are fully based on arithmetics. *}
   421 
   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
   426 
   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
   431 
   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
   436 
   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
   441 
   442 lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
   443   by simp
   444 
   445 lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   446   by simp
   447 
   448 text {*
   449   \medskip These are the atomic cases for the proof generation for the
   450   modulo @{text D} property for @{text "P minusinfinity"}.
   451 
   452   They are fully based on arithmetics. *}
   453 
   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))))"
   456 apply(clarsimp simp add:dvd_def)
   457 apply(rule iffI)
   458 apply(clarsimp)
   459 apply(rename_tac n m)
   460 apply(rule_tac x = "m - n*k" in exI)
   461 apply(simp add:int_distrib)
   462 apply(clarsimp)
   463 apply(rename_tac n m)
   464 apply(rule_tac x = "m + n*k" in exI)
   465 apply(simp add:int_distrib mult_ac)
   466 done
   467 
   468 
   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))))"
   471 apply(clarsimp simp add:dvd_def)
   472 apply(rule iffI)
   473 apply(clarsimp)
   474 apply(rename_tac n m)
   475 apply(erule_tac x = "m + n*k" in allE)
   476 apply(simp add:int_distrib mult_ac)
   477 apply(clarsimp)
   478 apply(rename_tac n m)
   479 apply(erule_tac x = "m - n*k" in allE)
   480 apply(simp add:int_distrib mult_ac)
   481 done
   482 
   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}.
   487 
   488   They are fully based on arithmetics. *}
   489 
   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
   494 
   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
   499 
   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
   504 
   505 
   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
   510 
   511 lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
   512   by simp
   513 
   514 lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   515   by simp
   516 
   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.
   521 
   522   FIXME: remove once they are part of the distribution. *}
   523 
   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
   547 
   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
   559 
   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
   563  apply arith
   564 apply (simp add:int_distrib)
   565 apply arith
   566 done
   567 
   568 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   569 apply(induct rule: int_gr_induct)
   570  apply simp
   571  apply arith
   572 apply (simp add:int_distrib)
   573 apply arith
   574 done
   575 
   576 lemma  minusinfinity:
   577   assumes "0 < d" and
   578     P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and
   579     ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
   580   shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
   581 proof
   582   assume eP1: "EX x. P1 x"
   583   then obtain x where P1: "P1 x" ..
   584   from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
   585   let ?w = "x - (abs(x-z)+1) * d"
   586   show "EX x. P x"
   587   proof
   588     have w: "?w < z" by(rule decr_lemma)
   589     have "P1 x = P1 ?w" using P1eqP1 by blast
   590     also have "\<dots> = P(?w)" using w P1eqP by blast
   591     finally show "P ?w" using P1 by blast
   592   qed
   593 qed
   594 
   595 text {*
   596   \medskip This Theorem combines whithnesses about @{text "P
   597   minusinfinity"} to show one component of the equivalence proof for
   598   Cooper's Theorem. *}
   599 
   600 lemma plusinfinity:
   601   assumes "0 < d" and
   602     P1eqP1: "ALL (x::int) (k::int). P1 x = P1 (x + k * d)" and
   603     ePeqP1: "EX z::int. ALL x. z < x  --> (P x = P1 x)"
   604   shows "(EX x::int. P1 x) --> (EX x::int. P x)"
   605 proof
   606   assume eP1: "EX x. P1 x"
   607   then obtain x where P1: "P1 x" ..
   608   from ePeqP1 obtain z where P1eqP: "ALL x. z < x \<longrightarrow> (P x = P1 x)" ..
   609   let ?w = "x + (abs(x-z)+1) * d"
   610   show "EX x. P x"
   611   proof
   612     have w: "z < ?w" by(rule incr_lemma)
   613     have "P1 x = P1 ?w" using P1eqP1 by blast
   614     also have "\<dots> = P(?w)" using w P1eqP by blast
   615     finally show "P ?w" using P1 by blast
   616   qed
   617 qed
   618  
   619 text {*
   620   \medskip Theorem for periodic function on discrete sets. *}
   621 
   622 lemma minf_vee:
   623   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   624   shows "(EX x. P x) = (EX j : {1..d}. P j)"
   625   (is "?LHS = ?RHS")
   626 proof
   627   assume ?LHS
   628   then obtain x where P: "P x" ..
   629   have "x mod d = x - (x div d)*d"
   630     by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
   631   hence Pmod: "P x = P(x mod d)" using modd by simp
   632   show ?RHS
   633   proof (cases)
   634     assume "x mod d = 0"
   635     hence "P 0" using P Pmod by simp
   636     moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
   637     ultimately have "P d" by simp
   638     moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
   639     ultimately show ?RHS ..
   640   next
   641     assume not0: "x mod d \<noteq> 0"
   642     have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
   643     moreover have "x mod d : {1..d}"
   644     proof -
   645       have "0 \<le> x mod d" by(rule pos_mod_sign)
   646       moreover have "x mod d < d" by(rule pos_mod_bound)
   647       ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
   648     qed
   649     ultimately show ?RHS ..
   650   qed
   651 next
   652   assume ?RHS thus ?LHS by blast
   653 qed
   654 
   655 text {*
   656   \medskip Theorem for periodic function on discrete sets. *}
   657 
   658 lemma pinf_vee:
   659   assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
   660   shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
   661   (is "?LHS = ?RHS")
   662 proof
   663   assume ?LHS
   664   then obtain x where P: "P x" ..
   665   have "x mod d = x + (-(x div d))*d"
   666     by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
   667   hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
   668   show ?RHS
   669   proof (cases)
   670     assume "x mod d = 0"
   671     hence "P 0" using P Pmod by simp
   672     moreover have "P 0 = P(0 + 1*d)" using modd by blast
   673     ultimately have "P d" by simp
   674     moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
   675     ultimately show ?RHS ..
   676   next
   677     assume not0: "x mod d \<noteq> 0"
   678     have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
   679     moreover have "x mod d : {1..d}"
   680     proof -
   681       have "0 \<le> x mod d" by(rule pos_mod_sign)
   682       moreover have "x mod d < d" by(rule pos_mod_bound)
   683       ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
   684     qed
   685     ultimately show ?RHS ..
   686   qed
   687 next
   688   assume ?RHS thus ?LHS by blast
   689 qed
   690 
   691 lemma decr_mult_lemma:
   692   assumes dpos: "(0::int) < d" and
   693           minus: "ALL x::int. P x \<longrightarrow> P(x - d)" and
   694           knneg: "0 <= k"
   695   shows "ALL x. P x \<longrightarrow> P(x - k*d)"
   696 using knneg
   697 proof (induct rule:int_ge_induct)
   698   case base thus ?case by simp
   699 next
   700   case (step i)
   701   show ?case
   702   proof
   703     fix x
   704     have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
   705     also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
   706       using minus[THEN spec, of "x - i * d"]
   707       by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric])
   708     ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
   709   qed
   710 qed
   711 
   712 lemma incr_mult_lemma:
   713   assumes dpos: "(0::int) < d" and
   714           plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and
   715           knneg: "0 <= k"
   716   shows "ALL x. P x \<longrightarrow> P(x + k*d)"
   717 using knneg
   718 proof (induct rule:int_ge_induct)
   719   case base thus ?case by simp
   720 next
   721   case (step i)
   722   show ?case
   723   proof
   724     fix x
   725     have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
   726     also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)"
   727       using plus[THEN spec, of "x + i * d"]
   728       by (simp add:int_distrib zadd_ac)
   729     ultimately show "P x \<longrightarrow> P(x + (i + 1) * d)" by blast
   730   qed
   731 qed
   732 
   733 lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
   734 ==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
   735 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
   736 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
   737 apply(rule iffI)
   738 prefer 2
   739 apply(drule minusinfinity)
   740 apply assumption+
   741 apply(fastsimp)
   742 apply clarsimp
   743 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
   744 apply(frule_tac x = x and z=z in decr_lemma)
   745 apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
   746 prefer 2
   747 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
   748 prefer 2 apply arith
   749  apply fastsimp
   750 apply(drule (1) minf_vee)
   751 apply blast
   752 apply(blast dest:decr_mult_lemma)
   753 done
   754 
   755 text {* Cooper Theorem, plus infinity version. *}
   756 lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
   757 ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
   758 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
   759 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)))"
   760   apply(rule iffI)
   761   prefer 2
   762   apply(drule plusinfinity)
   763   apply assumption+
   764   apply(fastsimp)
   765   apply clarsimp
   766   apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x + k*D)")
   767   apply(frule_tac x = x and z=z in incr_lemma)
   768   apply(subgoal_tac "P1(x + (\<bar>x - z\<bar> + 1) * D)")
   769   prefer 2
   770   apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
   771   prefer 2 apply arith
   772   apply fastsimp
   773   apply(drule (1) pinf_vee)
   774   apply blast
   775   apply(blast dest:incr_mult_lemma)
   776   done
   777 
   778 
   779 text {*
   780   \bigskip Theorems for the quantifier elminination Functions. *}
   781 
   782 lemma qe_ex_conj: "(EX (x::int). A x) = R
   783 		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
   784 		==> (EX (x::int). P x) = (Q & R)"
   785 by blast
   786 
   787 lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q)
   788 		==> (EX (x::int). P x) = Q"
   789 by blast
   790 
   791 lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)"
   792 by blast
   793 
   794 lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)"
   795 by blast
   796 
   797 lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)"
   798 by blast
   799 
   800 lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)"
   801 by blast
   802 
   803 lemma qe_Not: "P = Q ==> (~P) = (~Q)"
   804 by blast
   805 
   806 lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
   807 by blast
   808 
   809 text {* \bigskip Theorems for proving NNF *}
   810 
   811 lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
   812 by blast
   813 
   814 lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))"
   815 by blast
   816 
   817 lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)"
   818   by blast
   819 lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))"
   820 by blast
   821 
   822 lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))"
   823 by blast
   824 lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))"
   825 by blast
   826 lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))"
   827 by blast
   828 lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))"
   829 by blast
   830 
   831 
   832 lemma qe_exI2: "A = B ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
   833   by simp
   834 
   835 lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
   836   by rules
   837 
   838 lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
   839   by rules
   840 
   841 lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
   842 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
   843 by blast
   844 
   845 lemma cppi_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j)))
   846 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) "
   847 by blast
   848 
   849 
   850 lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
   851 apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
   852 apply(fastsimp)
   853 done
   854 
   855 text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
   856 
   857 lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
   858 shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
   859 proof
   860   assume ?P
   861   thus ?Q
   862     apply(simp add:dvd_def)
   863     apply clarify
   864     apply(rename_tac d)
   865     apply(drule_tac f = "op * k" in arg_cong)
   866     apply(simp only:int_distrib)
   867     apply(rule_tac x = "d" in exI)
   868     apply(simp only:mult_ac)
   869     done
   870 next
   871   assume ?Q
   872   then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
   873   hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
   874   hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
   875   hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
   876   thus ?P by(simp add:dvd_def)
   877 qed
   878 
   879 lemma ac_lt_eq: assumes gr0: "0 < (k::int)"
   880 shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
   881 proof
   882   assume P: ?P
   883   show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
   884 next
   885   assume ?Q
   886   hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
   887   with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
   888   thus ?P by(simp)
   889 qed
   890 
   891 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")
   892 proof
   893   assume ?P
   894   thus ?Q
   895     apply(drule_tac f = "op * k" in arg_cong)
   896     apply(simp only:int_distrib)
   897     done
   898 next
   899   assume ?Q
   900   hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
   901   hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
   902   thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
   903 qed
   904 
   905 lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
   906 proof -
   907   have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
   908   also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
   909   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])
   910   also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
   911   finally show ?thesis .
   912 qed
   913 
   914 lemma binminus_uminus_conv: "(a::int) - b = a + (-b)"
   915 by arith
   916 
   917 lemma  linearize_dvd: "(t::int) = t1 ==> (d dvd t) = (d dvd t1)"
   918 by simp
   919 
   920 lemma lf_lt: "(l::int) = ll ==> (r::int) = lr ==> (l < r) =(ll < lr)"
   921 by simp
   922 
   923 lemma lf_eq: "(l::int) = ll ==> (r::int) = lr ==> (l = r) =(ll = lr)"
   924 by simp
   925 
   926 lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
   927 by simp
   928 
   929 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
   930 
   931 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   932   by (simp split add: split_nat)
   933 
   934 theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
   935   apply (simp split add: split_nat)
   936   apply (rule iffI)
   937   apply (erule exE)
   938   apply (rule_tac x = "int x" in exI)
   939   apply simp
   940   apply (erule exE)
   941   apply (rule_tac x = "nat x" in exI)
   942   apply (erule conjE)
   943   apply (erule_tac x = "nat x" in allE)
   944   apply simp
   945   done
   946 
   947 theorem zdiff_int_split: "P (int (x - y)) =
   948   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   949   apply (case_tac "y \<le> x")
   950   apply (simp_all add: zdiff_int)
   951   done
   952 
   953 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
   954   apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
   955     nat_0_le cong add: conj_cong)
   956   apply (rule iffI)
   957   apply rules
   958   apply (erule exE)
   959   apply (case_tac "x=0")
   960   apply (rule_tac x=0 in exI)
   961   apply simp
   962   apply (case_tac "0 \<le> k")
   963   apply rules
   964   apply (simp add: linorder_not_le)
   965   apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   966   apply assumption
   967   apply (simp add: mult_ac)
   968   done
   969 
   970 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
   971   by simp
   972 
   973 theorem number_of2: "(0::int) <= number_of bin.Pls" by simp
   974 
   975 theorem Suc_plus1: "Suc n = n + 1" by simp
   976 
   977 text {*
   978   \medskip Specific instances of congruence rules, to prevent
   979   simplifier from looping. *}
   980 
   981 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
   982   by simp
   983 
   984 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
   985   by (simp cong: conj_cong)
   986 
   987 use "cooper_dec.ML"
   988 use "cooper_proof.ML"
   989 use "qelim.ML"
   990 use "presburger.ML"
   991 
   992 setup "Presburger.setup"
   993 
   994 end