src/HOL/Presburger.thy
changeset 23314 6894137e854a
parent 23253 b1f3f53c60b5
child 23333 ec5b4ab52026
     1.1 --- a/src/HOL/Presburger.thy	Mon Jun 11 11:05:59 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Mon Jun 11 11:06:00 2007 +0200
     1.3 @@ -1,629 +1,191 @@
     1.4  (*  Title:      HOL/Presburger.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen
     1.7 +    Author:     Amine Chaieb, TU Muenchen
     1.8  *)
     1.9  
    1.10 -header {* Presburger Arithmetic: Cooper's Algorithm *}
    1.11 -
    1.12  theory Presburger
    1.13  imports NatSimprocs SetInterval
    1.14 -uses
    1.15 -  ("Tools/Presburger/cooper_dec.ML")
    1.16 -  ("Tools/Presburger/cooper_proof.ML")
    1.17 -  ("Tools/Presburger/qelim.ML") 
    1.18 -  ("Tools/Presburger/reflected_presburger.ML")
    1.19 -  ("Tools/Presburger/reflected_cooper.ML")
    1.20 -  ("Tools/Presburger/presburger.ML")
    1.21 +  uses "Tools/Presburger/cooper_data" "Tools/Presburger/qelim" 
    1.22 +       "Tools/Presburger/generated_cooper.ML"
    1.23 +       ("Tools/Presburger/cooper.ML") ("Tools/Presburger/presburger.ML") 
    1.24 +       
    1.25  begin
    1.26 -
    1.27 -text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    1.28 -
    1.29 -theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
    1.30 -  apply (rule iffI)
    1.31 -  apply (erule exE)
    1.32 -  apply (rule_tac x = "l * x" in exI)
    1.33 -  apply simp
    1.34 -  apply (erule exE)
    1.35 -  apply (erule conjE)
    1.36 -  apply (erule dvdE)
    1.37 -  apply (rule_tac x = k in exI)
    1.38 -  apply simp
    1.39 -  done
    1.40 -
    1.41 -lemma uminus_dvd_conv: "(d dvd (t::int)) = (-d dvd t)"
    1.42 -apply(unfold dvd_def)
    1.43 -apply(rule iffI)
    1.44 -apply(clarsimp)
    1.45 -apply(rename_tac k)
    1.46 -apply(rule_tac x = "-k" in exI)
    1.47 -apply simp
    1.48 -apply(clarsimp)
    1.49 -apply(rename_tac k)
    1.50 -apply(rule_tac x = "-k" in exI)
    1.51 -apply simp
    1.52 -done
    1.53 +setup {* Cooper_Data.setup*}
    1.54  
    1.55 -lemma uminus_dvd_conv': "(d dvd (t::int)) = (d dvd -t)"
    1.56 -apply(unfold dvd_def)
    1.57 -apply(rule iffI)
    1.58 -apply(clarsimp)
    1.59 -apply(rule_tac x = "-k" in exI)
    1.60 -apply simp
    1.61 -apply(clarsimp)
    1.62 -apply(rule_tac x = "-k" in exI)
    1.63 -apply simp
    1.64 -done
    1.65 -
    1.66 -
    1.67 -
    1.68 -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}.*}
    1.69 -
    1.70 -theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    1.71 -  \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    1.72 -  \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
    1.73 -  apply (erule exE)+
    1.74 -  apply (rule_tac x = "min z1 z2" in exI)
    1.75 -  apply simp
    1.76 -  done
    1.77 -
    1.78 -
    1.79 -theorem eq_minf_disjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    1.80 -  \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    1.81 -  \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))"
    1.82 -
    1.83 -  apply (erule exE)+
    1.84 -  apply (rule_tac x = "min z1 z2" in exI)
    1.85 -  apply simp
    1.86 -  done
    1.87 -
    1.88 -
    1.89 -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}.*}
    1.90 +section{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
    1.91  
    1.92 -theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    1.93 -  \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    1.94 -  \<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
    1.95 -  apply (erule exE)+
    1.96 -  apply (rule_tac x = "max z1 z2" in exI)
    1.97 -  apply simp
    1.98 -  done
    1.99 -
   1.100 -
   1.101 -theorem eq_pinf_disjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
   1.102 -  \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
   1.103 -  \<exists>z::int. \<forall>x. z < x  \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))"
   1.104 -  apply (erule exE)+
   1.105 -  apply (rule_tac x = "max z1 z2" in exI)
   1.106 -  apply simp
   1.107 -  done
   1.108 -
   1.109 -text {*
   1.110 -  \medskip Theorems for the combination of proofs of the modulo @{text
   1.111 -  D} property for @{text "P plusinfinity"}
   1.112 -
   1.113 -  FIXME: This is THE SAME theorem as for the @{text minusinf} version,
   1.114 -  but with @{text "+k.."} instead of @{text "-k.."} In the future
   1.115 -  replace these both with only one. *}
   1.116 -
   1.117 -theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
   1.118 -  \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
   1.119 -  \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
   1.120 -  by simp
   1.121 -
   1.122 -theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
   1.123 -  \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
   1.124 -  \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
   1.125 -  by simp
   1.126 -
   1.127 -text {*
   1.128 -  This is one of the cases where the simplifed formula is prooved to
   1.129 -  habe some property (in relation to @{text P_m}) but we need to prove
   1.130 -  the property for the original formula (@{text P_m})
   1.131 -
   1.132 -  FIXME: This is exaclty the same thm as for @{text minusinf}. *}
   1.133 -
   1.134 -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)) "
   1.135 -  by blast
   1.136 -
   1.137 -
   1.138 -text {*
   1.139 -  \medskip Theorems for the combination of proofs of the modulo @{text D}
   1.140 -  property for @{text "P minusinfinity"} *}
   1.141 -
   1.142 -theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
   1.143 -  \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
   1.144 -  \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
   1.145 -  by simp
   1.146 -
   1.147 -theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
   1.148 -  \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
   1.149 -  \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
   1.150 -  by simp
   1.151 -
   1.152 -text {*
   1.153 -  This is one of the cases where the simplifed formula is prooved to
   1.154 -  have some property (in relation to @{text P_m}) but we need to
   1.155 -  prove the property for the original formula (@{text P_m}). *}
   1.156 -
   1.157 -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)) "
   1.158 -  by blast
   1.159 -
   1.160 -text {*
   1.161 -  Theorem needed for proving at runtime divide properties using the
   1.162 -  arithmetic tactic (which knows only about modulo = 0). *}
   1.163 -
   1.164 -lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   1.165 -  by(simp add:dvd_def zmod_eq_0_iff)
   1.166 +lemma minf:
   1.167 +  "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
   1.168 +     \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"
   1.169 +  "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
   1.170 +     \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<or> Q x) = (P' x \<or> Q' x)"
   1.171 +  "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x = t) = False"
   1.172 +  "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<noteq> t) = True"
   1.173 +  "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x < t) = True"
   1.174 +  "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
   1.175 +  "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
   1.176 +  "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
   1.177 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (d dvd x + s) = (d dvd x + s)"
   1.178 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   1.179 +  "\<exists>z.\<forall>x<z. F = F"
   1.180 +  by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
   1.181  
   1.182 -text {*
   1.183 -  \medskip Theorems used for the combination of proof for the
   1.184 -  backwards direction of Cooper's Theorem. They rely exclusively on
   1.185 -  Predicate calculus.*}
   1.186 -
   1.187 -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))
   1.188 -==>
   1.189 -(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
   1.190 -==>
   1.191 -(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))) "
   1.192 -  by blast
   1.193 -
   1.194 -
   1.195 -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))
   1.196 -==>
   1.197 -(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
   1.198 -==>
   1.199 -(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)
   1.200 -\<and> P2(x + d))) "
   1.201 -  by blast
   1.202 -
   1.203 -lemma not_ast_p_Q_elim: "
   1.204 -(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
   1.205 -==> ( P = Q )
   1.206 -==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
   1.207 -  by blast
   1.208 -
   1.209 -text {*
   1.210 -  \medskip Theorems used for the combination of proof for the
   1.211 -  backwards direction of Cooper's Theorem. They rely exclusively on
   1.212 -  Predicate calculus.*}
   1.213 -
   1.214 -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))
   1.215 -==>
   1.216 -(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d))
   1.217 -==>
   1.218 -(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)
   1.219 -\<or> P2(x-d))) "
   1.220 -  by blast
   1.221 -
   1.222 -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))
   1.223 -==>
   1.224 -(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d))
   1.225 -==>
   1.226 -(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)
   1.227 -\<and> P2(x-d))) "
   1.228 -  by blast
   1.229 -
   1.230 -lemma not_bst_p_Q_elim: "
   1.231 -(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) 
   1.232 -==> ( P = Q )
   1.233 -==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
   1.234 -  by blast
   1.235 -
   1.236 -text {* \medskip This is the first direction of Cooper's Theorem. *}
   1.237 -lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
   1.238 -  by blast
   1.239 -
   1.240 -text {*
   1.241 -  \medskip The full Cooper's Theorem in its equivalence Form. Given
   1.242 -  the premises it is trivial too, it relies exclusively on prediacte calculus.*}
   1.243 -lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
   1.244 ---> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
   1.245 -  by blast
   1.246 -
   1.247 -text {*
   1.248 -  \medskip Some of the atomic theorems generated each time the atom
   1.249 -  does not depend on @{text x}, they are trivial.*}
   1.250 -
   1.251 -lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
   1.252 -  by blast
   1.253 -
   1.254 -lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
   1.255 -  by blast
   1.256 +lemma pinf:
   1.257 +  "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> 
   1.258 +     \<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<and> Q x) = (P' x \<and> Q' x)"
   1.259 +  "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> 
   1.260 +     \<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<or> Q x) = (P' x \<or> Q' x)"
   1.261 +  "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x = t) = False"
   1.262 +  "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<noteq> t) = True"
   1.263 +  "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x < t) = False"
   1.264 +  "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
   1.265 +  "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
   1.266 +  "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
   1.267 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (d dvd x + s) = (d dvd x + s)"
   1.268 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   1.269 +  "\<exists>z.\<forall>x>z. F = F"
   1.270 +  by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
   1.271  
   1.272 -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"
   1.273 -  by blast
   1.274 -
   1.275 -lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
   1.276 -  by blast
   1.277 -
   1.278 -text {* The next two thms are the same as the @{text minusinf} version. *}
   1.279 -
   1.280 -lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
   1.281 -  by blast
   1.282 -
   1.283 -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"
   1.284 -  by blast
   1.285 -
   1.286 -text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
   1.287 -
   1.288 -lemma P_eqtrue: "(P=True) = P"
   1.289 -  by iprover
   1.290 -
   1.291 -lemma P_eqfalse: "(P=False) = (~P)"
   1.292 -  by iprover
   1.293 -
   1.294 -text {*
   1.295 -  \medskip Theorems for the generation of the bachwards direction of
   1.296 -  Cooper's Theorem.
   1.297 -
   1.298 -  These are the 6 interesting atomic cases which have to be proved relying on the
   1.299 -  properties of B-set and the arithmetic and contradiction proofs. *}
   1.300 -
   1.301 -lemma not_bst_p_lt: "0 < (d::int) ==>
   1.302 - 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 )"
   1.303 -  by arith
   1.304 -
   1.305 -lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
   1.306 - 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)"
   1.307 -apply clarsimp
   1.308 -apply(rule ccontr)
   1.309 -apply(drule_tac x = "x+a" in bspec)
   1.310 -apply(simp add:atLeastAtMost_iff)
   1.311 -apply(drule_tac x = "-a" in bspec)
   1.312 -apply assumption
   1.313 -apply(simp)
   1.314 -done
   1.315 -
   1.316 -lemma not_bst_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a - 1 \<rbrakk> \<Longrightarrow>
   1.317 - 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 )"
   1.318 -apply clarsimp
   1.319 -apply(subgoal_tac "x = -a")
   1.320 - prefer 2 apply arith
   1.321 -apply(drule_tac x = "1" in bspec)
   1.322 -apply(simp add:atLeastAtMost_iff)
   1.323 -apply(drule_tac x = "-a- 1" in bspec)
   1.324 -apply assumption
   1.325 -apply(simp)
   1.326 -done
   1.327 -
   1.328 -
   1.329 -lemma not_bst_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
   1.330 - 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)"
   1.331 -apply clarsimp
   1.332 -apply(subgoal_tac "x = -a+d")
   1.333 - prefer 2 apply arith
   1.334 -apply(drule_tac x = "d" in bspec)
   1.335 -apply(simp add:atLeastAtMost_iff)
   1.336 -apply(drule_tac x = "-a" in bspec)
   1.337 -apply assumption
   1.338 -apply(simp)
   1.339 -done
   1.340 -
   1.341 -
   1.342 -lemma not_bst_p_dvd: "(d1::int) dvd d ==>
   1.343 - 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 )"
   1.344 -apply(clarsimp simp add:dvd_def)
   1.345 -apply(rename_tac m)
   1.346 -apply(rule_tac x = "m - k" in exI)
   1.347 -apply(simp add:int_distrib)
   1.348 -done
   1.349 +lemma inf_period:
   1.350 +  "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
   1.351 +    \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
   1.352 +  "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
   1.353 +    \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
   1.354 +  "(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
   1.355 +  "(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
   1.356 +  "\<forall>x k. F = F"
   1.357 +by simp_all
   1.358 +  (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
   1.359 +    simp add: ring_eq_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_eq_simps)+
   1.360  
   1.361 -lemma not_bst_p_ndvd: "(d1::int) dvd d ==>
   1.362 - 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 ))"
   1.363 -apply(clarsimp simp add:dvd_def)
   1.364 -apply(rename_tac m)
   1.365 -apply(erule_tac x = "m + k" in allE)
   1.366 -apply(simp add:int_distrib)
   1.367 -done
   1.368 -
   1.369 -text {*
   1.370 -  \medskip Theorems for the generation of the bachwards direction of
   1.371 -  Cooper's Theorem.
   1.372 -
   1.373 -  These are the 6 interesting atomic cases which have to be proved
   1.374 -  relying on the properties of A-set ant the arithmetic and
   1.375 -  contradiction proofs. *}
   1.376 -
   1.377 -lemma not_ast_p_gt: "0 < (d::int) ==>
   1.378 - 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 )"
   1.379 -  by arith
   1.380 -
   1.381 -lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
   1.382 - 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)"
   1.383 -  apply clarsimp
   1.384 -  apply (rule ccontr)
   1.385 -  apply (drule_tac x = "t-x" in bspec)
   1.386 -  apply simp
   1.387 -  apply (drule_tac x = "t" in bspec)
   1.388 -  apply assumption
   1.389 -  apply simp
   1.390 -  done
   1.391 -
   1.392 -lemma not_ast_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t + 1 \<rbrakk> \<Longrightarrow>
   1.393 - 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 )"
   1.394 -  apply clarsimp
   1.395 -  apply (drule_tac x="1" in bspec)
   1.396 -  apply simp
   1.397 -  apply (drule_tac x="- t + 1" in bspec)
   1.398 -  apply assumption
   1.399 -  apply(subgoal_tac "x = -t")
   1.400 -  prefer 2 apply arith
   1.401 -  apply simp
   1.402 -  done
   1.403 -
   1.404 -lemma not_ast_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t \<rbrakk> \<Longrightarrow>
   1.405 - 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)"
   1.406 -  apply clarsimp
   1.407 -  apply (subgoal_tac "x = -t-d")
   1.408 -  prefer 2 apply arith
   1.409 -  apply (drule_tac x = "d" in bspec)
   1.410 -  apply simp
   1.411 -  apply (drule_tac x = "-t" in bspec)
   1.412 -  apply assumption
   1.413 -  apply simp
   1.414 -  done
   1.415 -
   1.416 -lemma not_ast_p_dvd: "(d1::int) dvd d ==>
   1.417 - 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 )"
   1.418 -  apply(clarsimp simp add:dvd_def)
   1.419 -  apply(rename_tac m)
   1.420 -  apply(rule_tac x = "m + k" in exI)
   1.421 -  apply(simp add:int_distrib)
   1.422 -  done
   1.423 -
   1.424 -lemma not_ast_p_ndvd: "(d1::int) dvd d ==>
   1.425 - 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 ))"
   1.426 -  apply(clarsimp simp add:dvd_def)
   1.427 -  apply(rename_tac m)
   1.428 -  apply(erule_tac x = "m - k" in allE)
   1.429 -  apply(simp add:int_distrib)
   1.430 -  done
   1.431 -
   1.432 -text {*
   1.433 -  \medskip These are the atomic cases for the proof generation for the
   1.434 -  modulo @{text D} property for @{text "P plusinfinity"}
   1.435 -
   1.436 -  They are fully based on arithmetics. *}
   1.437 -
   1.438 -lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
   1.439 - (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
   1.440 -  apply(clarsimp simp add:dvd_def)
   1.441 -  apply(rule iffI)
   1.442 -  apply(clarsimp)
   1.443 -  apply(rename_tac n m)
   1.444 -  apply(rule_tac x = "m + n*k" in exI)
   1.445 -  apply(simp add:int_distrib)
   1.446 -  apply(clarsimp)
   1.447 -  apply(rename_tac n m)
   1.448 -  apply(rule_tac x = "m - n*k" in exI)
   1.449 -  apply(simp add:int_distrib mult_ac)
   1.450 -  done
   1.451 -
   1.452 -lemma  not_dvd_modd_pinf: "((d::int) dvd d1) ==>
   1.453 - (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x+k*d1 + t))))"
   1.454 -  apply(clarsimp simp add:dvd_def)
   1.455 -  apply(rule iffI)
   1.456 -  apply(clarsimp)
   1.457 -  apply(rename_tac n m)
   1.458 -  apply(erule_tac x = "m - n*k" in allE)
   1.459 -  apply(simp add:int_distrib mult_ac)
   1.460 -  apply(clarsimp)
   1.461 -  apply(rename_tac n m)
   1.462 -  apply(erule_tac x = "m + n*k" in allE)
   1.463 -  apply(simp add:int_distrib mult_ac)
   1.464 -  done
   1.465 -
   1.466 -text {*
   1.467 -  \medskip These are the atomic cases for the proof generation for the
   1.468 -  equivalence of @{text P} and @{text "P plusinfinity"} for integers
   1.469 -  @{text x} greater than some integer @{text z}.
   1.470 -
   1.471 -  They are fully based on arithmetics. *}
   1.472 -
   1.473 -lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
   1.474 -  apply(rule_tac x = "-t" in exI)
   1.475 -  apply simp
   1.476 -  done
   1.477 -
   1.478 -lemma  neq_eq_pinf: "EX z::int. ALL x.  z < x --> ((~( 0 = x +t )) = True )"
   1.479 -  apply(rule_tac x = "-t" in exI)
   1.480 -  apply simp
   1.481 -  done
   1.482 -
   1.483 -lemma  le_eq_pinf: "EX z::int. ALL x.  z < x --> ( 0 < x +t  = True )"
   1.484 -  apply(rule_tac x = "-t" in exI)
   1.485 -  apply simp
   1.486 -  done
   1.487 -
   1.488 -lemma  len_eq_pinf: "EX z::int. ALL x. z < x  --> (0 < -x +t  = False )"
   1.489 -  apply(rule_tac x = "t" in exI)
   1.490 -  apply simp
   1.491 -  done
   1.492 -
   1.493 -lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
   1.494 -  by simp
   1.495 -
   1.496 -lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   1.497 -  by simp
   1.498 -
   1.499 -text {*
   1.500 -  \medskip These are the atomic cases for the proof generation for the
   1.501 -  modulo @{text D} property for @{text "P minusinfinity"}.
   1.502 -
   1.503 -  They are fully based on arithmetics. *}
   1.504 +section{* The A and B sets *}
   1.505 +lemma bset:
   1.506 +  "\<lbrakk>\<forall>x.(\<forall>j \<in> {1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x - D) ;
   1.507 +     \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow> 
   1.508 +  \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x - D) \<and> Q (x - D))"
   1.509 +  "\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x - D) ;
   1.510 +     \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow> 
   1.511 +  \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x - D) \<or> Q (x - D))"
   1.512 +  "\<lbrakk>D>0; t - 1\<in> B\<rbrakk> \<Longrightarrow> (\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x - D = t))"
   1.513 +  "\<lbrakk>D>0 ; t \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x - D \<noteq> t))"
   1.514 +  "D>0 \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x - D < t))"
   1.515 +  "D>0 \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x - D \<le> t))"
   1.516 +  "\<lbrakk>D>0 ; t \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x - D > t))"
   1.517 +  "\<lbrakk>D>0 ; t - 1 \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> t))"
   1.518 +  "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t))"
   1.519 +  "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not> d dvd (x - D) + t))"
   1.520 +  "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j) \<longrightarrow> F \<longrightarrow> F"
   1.521 +proof (blast, blast)
   1.522 +  assume dp: "D > 0" and tB: "t - 1\<in> B"
   1.523 +  show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x - D = t))" 
   1.524 +    apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"])
   1.525 +    using dp tB by simp_all
   1.526 +next
   1.527 +  assume dp: "D > 0" and tB: "t \<in> B"
   1.528 +  show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x - D \<noteq> t))" 
   1.529 +    apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"])
   1.530 +    using dp tB by simp_all
   1.531 +next
   1.532 +  assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x - D < t))" by arith
   1.533 +next
   1.534 +  assume dp: "D > 0" thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x - D \<le> t)" by arith
   1.535 +next
   1.536 +  assume dp: "D > 0" and tB:"t \<in> B"
   1.537 +  {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x > t" and ng: "\<not> (x - D) > t"
   1.538 +    hence "x -t \<le> D" and "1 \<le> x - t" by simp+
   1.539 +      hence "\<exists>j \<in> {1 .. D}. x - t = j" by auto
   1.540 +      hence "\<exists>j \<in> {1 .. D}. x = t + j" by (simp add: ring_eq_simps)
   1.541 +      with nob tB have "False" by simp}
   1.542 +  thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x - D > t)" by blast
   1.543 +next
   1.544 +  assume dp: "D > 0" and tB:"t - 1\<in> B"
   1.545 +  {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x \<ge> t" and ng: "\<not> (x - D) \<ge> t"
   1.546 +    hence "x - (t - 1) \<le> D" and "1 \<le> x - (t - 1)" by simp+
   1.547 +      hence "\<exists>j \<in> {1 .. D}. x - (t - 1) = j" by auto
   1.548 +      hence "\<exists>j \<in> {1 .. D}. x = (t - 1) + j" by (simp add: ring_eq_simps)
   1.549 +      with nob tB have "False" by simp}
   1.550 +  thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> t)" by blast
   1.551 +next
   1.552 +  assume d: "d dvd D"
   1.553 +  {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t"
   1.554 +      by (clarsimp simp add: dvd_def,rule_tac x= "ka - k" in exI,simp add: ring_eq_simps)}
   1.555 +  thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t)" by simp
   1.556 +next
   1.557 +  assume d: "d dvd D"
   1.558 +  {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x - D) + t"
   1.559 +      by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_eq_simps)}
   1.560 +  thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x - D) + t)" by auto
   1.561 +qed blast
   1.562  
   1.563 -lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
   1.564 - (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
   1.565 -apply(clarsimp simp add:dvd_def)
   1.566 -apply(rule iffI)
   1.567 -apply(clarsimp)
   1.568 -apply(rename_tac n m)
   1.569 -apply(rule_tac x = "m - n*k" in exI)
   1.570 -apply(simp add:int_distrib)
   1.571 -apply(clarsimp)
   1.572 -apply(rename_tac n m)
   1.573 -apply(rule_tac x = "m + n*k" in exI)
   1.574 -apply(simp add:int_distrib mult_ac)
   1.575 -done
   1.576 -
   1.577 -
   1.578 -lemma  not_dvd_modd_minf: "((d::int) dvd d1) ==>
   1.579 - (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x-k*d1 + t))))"
   1.580 -apply(clarsimp simp add:dvd_def)
   1.581 -apply(rule iffI)
   1.582 -apply(clarsimp)
   1.583 -apply(rename_tac n m)
   1.584 -apply(erule_tac x = "m + n*k" in allE)
   1.585 -apply(simp add:int_distrib mult_ac)
   1.586 -apply(clarsimp)
   1.587 -apply(rename_tac n m)
   1.588 -apply(erule_tac x = "m - n*k" in allE)
   1.589 -apply(simp add:int_distrib mult_ac)
   1.590 -done
   1.591 -
   1.592 -text {*
   1.593 -  \medskip These are the atomic cases for the proof generation for the
   1.594 -  equivalence of @{text P} and @{text "P minusinfinity"} for integers
   1.595 -  @{text x} less than some integer @{text z}.
   1.596 -
   1.597 -  They are fully based on arithmetics. *}
   1.598 -
   1.599 -lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
   1.600 -apply(rule_tac x = "-t" in exI)
   1.601 -apply simp
   1.602 -done
   1.603 -
   1.604 -lemma  neq_eq_minf: "EX z::int. ALL x. x < z --> ((~( 0 = x +t )) = True )"
   1.605 -apply(rule_tac x = "-t" in exI)
   1.606 -apply simp
   1.607 -done
   1.608 -
   1.609 -lemma  le_eq_minf: "EX z::int. ALL x. x < z --> ( 0 < x +t  = False )"
   1.610 -apply(rule_tac x = "-t" in exI)
   1.611 -apply simp
   1.612 -done
   1.613 -
   1.614 -
   1.615 -lemma  len_eq_minf: "EX z::int. ALL x. x < z --> (0 < -x +t  = True )"
   1.616 -apply(rule_tac x = "t" in exI)
   1.617 -apply simp
   1.618 -done
   1.619 -
   1.620 -lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
   1.621 -  by simp
   1.622 -
   1.623 -lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   1.624 -  by simp
   1.625 -
   1.626 -text {*
   1.627 -  \medskip This Theorem combines whithnesses about @{text "P
   1.628 -  minusinfinity"} to show one component of the equivalence proof for
   1.629 -  Cooper's Theorem.
   1.630 -
   1.631 -  FIXME: remove once they are part of the distribution. *}
   1.632 +lemma aset:
   1.633 +  "\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> P x \<longrightarrow> P(x + D) ;
   1.634 +     \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow> 
   1.635 +  \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x + D) \<and> Q (x + D))"
   1.636 +  "\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> P x \<longrightarrow> P(x + D) ;
   1.637 +     \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow> 
   1.638 +  \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x + D) \<or> Q (x + D))"
   1.639 +  "\<lbrakk>D>0; t + 1\<in> A\<rbrakk> \<Longrightarrow> (\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x = t) \<longrightarrow> (x + D = t))"
   1.640 +  "\<lbrakk>D>0 ; t \<in> A\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x + D \<noteq> t))"
   1.641 +  "\<lbrakk>D>0; t\<in> A\<rbrakk> \<Longrightarrow>(\<forall>(x::int). (\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t))"
   1.642 +  "\<lbrakk>D>0; t + 1 \<in> A\<rbrakk> \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t))"
   1.643 +  "D>0 \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x > t) \<longrightarrow> (x + D > t))"
   1.644 +  "D>0 \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x + D \<ge> t))"
   1.645 +  "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t))"
   1.646 +  "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not> d dvd (x + D) + t))"
   1.647 +  "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j) \<longrightarrow> F \<longrightarrow> F"
   1.648 +proof (blast, blast)
   1.649 +  assume dp: "D > 0" and tA: "t + 1 \<in> A"
   1.650 +  show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x = t) \<longrightarrow> (x + D = t))" 
   1.651 +    apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t + 1"])
   1.652 +    using dp tA by simp_all
   1.653 +next
   1.654 +  assume dp: "D > 0" and tA: "t \<in> A"
   1.655 +  show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x + D \<noteq> t))" 
   1.656 +    apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"])
   1.657 +    using dp tA by simp_all
   1.658 +next
   1.659 +  assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x > t) \<longrightarrow> (x + D > t))" by arith
   1.660 +next
   1.661 +  assume dp: "D > 0" thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x + D \<ge> t)" by arith
   1.662 +next
   1.663 +  assume dp: "D > 0" and tA:"t \<in> A"
   1.664 +  {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x < t" and ng: "\<not> (x + D) < t"
   1.665 +    hence "t - x \<le> D" and "1 \<le> t - x" by simp+
   1.666 +      hence "\<exists>j \<in> {1 .. D}. t - x = j" by auto
   1.667 +      hence "\<exists>j \<in> {1 .. D}. x = t - j" by (auto simp add: ring_eq_simps) 
   1.668 +      with nob tA have "False" by simp}
   1.669 +  thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t)" by blast
   1.670 +next
   1.671 +  assume dp: "D > 0" and tA:"t + 1\<in> A"
   1.672 +  {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x \<le> t" and ng: "\<not> (x + D) \<le> t"
   1.673 +    hence "(t + 1) - x \<le> D" and "1 \<le> (t + 1) - x" by (simp_all add: ring_eq_simps)
   1.674 +      hence "\<exists>j \<in> {1 .. D}. (t + 1) - x = j" by auto
   1.675 +      hence "\<exists>j \<in> {1 .. D}. x = (t + 1) - j" by (auto simp add: ring_eq_simps)
   1.676 +      with nob tA have "False" by simp}
   1.677 +  thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t)" by blast
   1.678 +next
   1.679 +  assume d: "d dvd D"
   1.680 +  {fix x assume H: "d dvd x + t" with d have "d dvd (x + D) + t"
   1.681 +      by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: ring_eq_simps)}
   1.682 +  thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t)" by simp
   1.683 +next
   1.684 +  assume d: "d dvd D"
   1.685 +  {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t"
   1.686 +      by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_eq_simps)}
   1.687 +  thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
   1.688 +qed blast
   1.689  
   1.690 -theorem int_ge_induct[consumes 1,case_names base step]:
   1.691 -  assumes ge: "k \<le> (i::int)" and
   1.692 -        base: "P(k)" and
   1.693 -        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
   1.694 -  shows "P i"
   1.695 -proof -
   1.696 -  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
   1.697 -    proof (induct n)
   1.698 -      case 0
   1.699 -      hence "i = k" by arith
   1.700 -      thus "P i" using base by simp
   1.701 -    next
   1.702 -      case (Suc n)
   1.703 -      hence "n = nat((i - 1) - k)" by arith
   1.704 -      moreover
   1.705 -      have ki1: "k \<le> i - 1" using Suc.prems by arith
   1.706 -      ultimately
   1.707 -      have "P(i - 1)" by(rule Suc.hyps)
   1.708 -      from step[OF ki1 this] show ?case by simp
   1.709 -    qed
   1.710 -  }
   1.711 -  from this ge show ?thesis by fast
   1.712 -qed
   1.713 -
   1.714 -theorem int_gr_induct[consumes 1,case_names base step]:
   1.715 -  assumes gr: "k < (i::int)" and
   1.716 -        base: "P(k+1)" and
   1.717 -        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
   1.718 -  shows "P i"
   1.719 -apply(rule int_ge_induct[of "k + 1"])
   1.720 -  using gr apply arith
   1.721 - apply(rule base)
   1.722 -apply(rule step)
   1.723 - apply simp+
   1.724 -done
   1.725 -
   1.726 -lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
   1.727 -apply(induct rule: int_gr_induct)
   1.728 - apply simp
   1.729 -apply (simp add:int_distrib)
   1.730 -done
   1.731 -
   1.732 -lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   1.733 -apply(induct rule: int_gr_induct)
   1.734 - apply simp
   1.735 -apply (simp add:int_distrib)
   1.736 -done
   1.737 +section{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *}
   1.738  
   1.739 -lemma  minusinfinity:
   1.740 -  assumes "0 < d" and
   1.741 -    P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and
   1.742 -    ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
   1.743 -  shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
   1.744 -proof
   1.745 -  assume eP1: "EX x. P1 x"
   1.746 -  then obtain x where P1: "P1 x" ..
   1.747 -  from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
   1.748 -  let ?w = "x - (abs(x-z)+1) * d"
   1.749 -  show "EX x. P x"
   1.750 -  proof
   1.751 -    have w: "?w < z" by(rule decr_lemma)
   1.752 -    have "P1 x = P1 ?w" using P1eqP1 by blast
   1.753 -    also have "\<dots> = P(?w)" using w P1eqP by blast
   1.754 -    finally show "P ?w" using P1 by blast
   1.755 -  qed
   1.756 -qed
   1.757 -
   1.758 -text {*
   1.759 -  \medskip This Theorem combines whithnesses about @{text "P
   1.760 -  minusinfinity"} to show one component of the equivalence proof for
   1.761 -  Cooper's Theorem. *}
   1.762 -
   1.763 -lemma plusinfinity:
   1.764 -  assumes "0 < d" and
   1.765 -    P1eqP1: "ALL (x::int) (k::int). P1 x = P1 (x + k * d)" and
   1.766 -    ePeqP1: "EX z::int. ALL x. z < x  --> (P x = P1 x)"
   1.767 -  shows "(EX x::int. P1 x) --> (EX x::int. P x)"
   1.768 -proof
   1.769 -  assume eP1: "EX x. P1 x"
   1.770 -  then obtain x where P1: "P1 x" ..
   1.771 -  from ePeqP1 obtain z where P1eqP: "ALL x. z < x \<longrightarrow> (P x = P1 x)" ..
   1.772 -  let ?w = "x + (abs(x-z)+1) * d"
   1.773 -  show "EX x. P x"
   1.774 -  proof
   1.775 -    have w: "z < ?w" by(rule incr_lemma)
   1.776 -    have "P1 x = P1 ?w" using P1eqP1 by blast
   1.777 -    also have "\<dots> = P(?w)" using w P1eqP by blast
   1.778 -    finally show "P ?w" using P1 by blast
   1.779 -  qed
   1.780 -qed
   1.781 - 
   1.782 -text {*
   1.783 -  \medskip Theorem for periodic function on discrete sets. *}
   1.784 -
   1.785 -lemma minf_vee:
   1.786 +subsection{* First some trivial facts about periodic sets or predicates *}
   1.787 +lemma periodic_finite_ex:
   1.788    assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   1.789    shows "(EX x. P x) = (EX j : {1..d}. P j)"
   1.790    (is "?LHS = ?RHS")
   1.791  proof
   1.792    assume ?LHS
   1.793    then obtain x where P: "P x" ..
   1.794 -  have "x mod d = x - (x div d)*d"
   1.795 -    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
   1.796 +  have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
   1.797    hence Pmod: "P x = P(x mod d)" using modd by simp
   1.798    show ?RHS
   1.799    proof (cases)
   1.800 @@ -644,425 +206,245 @@
   1.801      qed
   1.802      ultimately show ?RHS ..
   1.803    qed
   1.804 -next
   1.805 -  assume ?RHS thus ?LHS by blast
   1.806 -qed
   1.807 +qed auto
   1.808  
   1.809 -text {*
   1.810 -  \medskip Theorem for periodic function on discrete sets. *}
   1.811 +subsection{* The @{text "-\<infinity>"} Version*}
   1.812 +
   1.813 +lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
   1.814 +by(induct rule: int_gr_induct,simp_all add:int_distrib)
   1.815  
   1.816 -lemma pinf_vee:
   1.817 -  assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
   1.818 -  shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
   1.819 -  (is "?LHS = ?RHS")
   1.820 -proof
   1.821 -  assume ?LHS
   1.822 -  then obtain x where P: "P x" ..
   1.823 -  have "x mod d = x + (-(x div d))*d"
   1.824 -    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
   1.825 -  hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
   1.826 -  show ?RHS
   1.827 -  proof (cases)
   1.828 -    assume "x mod d = 0"
   1.829 -    hence "P 0" using P Pmod by simp
   1.830 -    moreover have "P 0 = P(0 + 1*d)" using modd by blast
   1.831 -    ultimately have "P d" by simp
   1.832 -    moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
   1.833 -    ultimately show ?RHS ..
   1.834 -  next
   1.835 -    assume not0: "x mod d \<noteq> 0"
   1.836 -    have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
   1.837 -    moreover have "x mod d : {1..d}"
   1.838 -    proof -
   1.839 -      have "0 \<le> x mod d" by(rule pos_mod_sign)
   1.840 -      moreover have "x mod d < d" by(rule pos_mod_bound)
   1.841 -      ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
   1.842 -    qed
   1.843 -    ultimately show ?RHS ..
   1.844 -  qed
   1.845 -next
   1.846 -  assume ?RHS thus ?LHS by blast
   1.847 +lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   1.848 +by(induct rule: int_gr_induct, simp_all add:int_distrib)
   1.849 +
   1.850 +theorem int_induct[case_names base step1 step2]:
   1.851 +  assumes 
   1.852 +  base: "P(k::int)" and step1: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" and
   1.853 +  step2: "\<And>i. \<lbrakk>k \<ge> i; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   1.854 +  shows "P i"
   1.855 +proof -
   1.856 +  have "i \<le> k \<or> i\<ge> k" by arith
   1.857 +  thus ?thesis using prems int_ge_induct[where P="P" and k="k" and i="i"] int_le_induct[where P="P" and k="k" and i="i"] by blast
   1.858  qed
   1.859  
   1.860  lemma decr_mult_lemma:
   1.861 -  assumes dpos: "(0::int) < d" and
   1.862 -          minus: "ALL x::int. P x \<longrightarrow> P(x - d)" and
   1.863 -          knneg: "0 <= k"
   1.864 +  assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k"
   1.865    shows "ALL x. P x \<longrightarrow> P(x - k*d)"
   1.866  using knneg
   1.867  proof (induct rule:int_ge_induct)
   1.868    case base thus ?case by simp
   1.869  next
   1.870    case (step i)
   1.871 -  show ?case
   1.872 -  proof
   1.873 -    fix x
   1.874 +  {fix x
   1.875      have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
   1.876 -    also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
   1.877 -      using minus[THEN spec, of "x - i * d"]
   1.878 +    also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)" using minus[THEN spec, of "x - i * d"]
   1.879        by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric])
   1.880 -    ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
   1.881 -  qed
   1.882 +    ultimately have "P x \<longrightarrow> P(x - (i + 1) * d)" by blast}
   1.883 +  thus ?case ..
   1.884 +qed
   1.885 +
   1.886 +lemma  minusinfinity:
   1.887 +  assumes "0 < d" and
   1.888 +    P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
   1.889 +  shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
   1.890 +proof
   1.891 +  assume eP1: "EX x. P1 x"
   1.892 +  then obtain x where P1: "P1 x" ..
   1.893 +  from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
   1.894 +  let ?w = "x - (abs(x-z)+1) * d"
   1.895 +  have w: "?w < z" by(rule decr_lemma)
   1.896 +  have "P1 x = P1 ?w" using P1eqP1 by blast
   1.897 +  also have "\<dots> = P(?w)" using w P1eqP by blast
   1.898 +  finally have "P ?w" using P1 by blast
   1.899 +  thus "EX x. P x" ..
   1.900 +qed
   1.901 +
   1.902 +lemma cpmi: 
   1.903 +  assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x< z. P x = P' x"
   1.904 +  and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> B. x \<noteq> b+j) --> P (x) --> P (x - D)"
   1.905 +  and pd: "\<forall> x k. P' x = P' (x-k*D)"
   1.906 +  shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j) | (\<exists> j \<in> {1..D}.\<exists> b\<in> B. P (b+j)))" 
   1.907 +         (is "?L = (?R1 \<or> ?R2)")
   1.908 +proof-
   1.909 + {assume "?R2" hence "?L"  by blast}
   1.910 + moreover
   1.911 + {assume H:"?R1" hence "?L" using minusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp}
   1.912 + moreover 
   1.913 + { fix x
   1.914 +   assume P: "P x" and H: "\<not> ?R2"
   1.915 +   {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j))" and P: "P y"
   1.916 +     hence "~(EX (j::int) : {1..D}. EX (b::int) : B. y = b+j)" by auto
   1.917 +     with nb P  have "P (y - D)" by auto }
   1.918 +   hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D)" by blast
   1.919 +   with H P have th: " \<forall>x. P x \<longrightarrow> P (x - D)" by auto
   1.920 +   from p1 obtain z where z: "ALL x. x < z --> (P x = P' x)" by blast
   1.921 +   let ?y = "x - (\<bar>x - z\<bar> + 1)*D"
   1.922 +   have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith
   1.923 +   from dp have yz: "?y < z" using decr_lemma[OF dp] by simp   
   1.924 +   from z[rule_format, OF yz] decr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto
   1.925 +   with periodic_finite_ex[OF dp pd]
   1.926 +   have "?R1" by blast}
   1.927 + ultimately show ?thesis by blast
   1.928 +qed
   1.929 +
   1.930 +subsection {* The @{text "+\<infinity>"} Version*}
   1.931 +
   1.932 +lemma  plusinfinity:
   1.933 +  assumes "(0::int) < d" and
   1.934 +    P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x"
   1.935 +  shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)"
   1.936 +proof
   1.937 +  assume eP1: "EX x. P' x"
   1.938 +  then obtain x where P1: "P' x" ..
   1.939 +  from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" ..
   1.940 +  let ?w' = "x + (abs(x-z)+1) * d"
   1.941 +  let ?w = "x - (-(abs(x-z) + 1))*d"
   1.942 +  have ww'[simp]: "?w = ?w'" by (simp add: ring_eq_simps)
   1.943 +  have w: "?w > z" by(simp only: ww', rule incr_lemma)
   1.944 +  hence "P' x = P' ?w" using P1eqP1 by blast
   1.945 +  also have "\<dots> = P(?w)" using w P1eqP by blast
   1.946 +  finally have "P ?w" using P1 by blast
   1.947 +  thus "EX x. P x" ..
   1.948  qed
   1.949  
   1.950  lemma incr_mult_lemma:
   1.951 -  assumes dpos: "(0::int) < d" and
   1.952 -          plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and
   1.953 -          knneg: "0 <= k"
   1.954 +  assumes dpos: "(0::int) < d" and plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and knneg: "0 <= k"
   1.955    shows "ALL x. P x \<longrightarrow> P(x + k*d)"
   1.956  using knneg
   1.957  proof (induct rule:int_ge_induct)
   1.958    case base thus ?case by simp
   1.959  next
   1.960    case (step i)
   1.961 -  show ?case
   1.962 -  proof
   1.963 -    fix x
   1.964 +  {fix x
   1.965      have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
   1.966 -    also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)"
   1.967 -      using plus[THEN spec, of "x + i * d"]
   1.968 +    also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
   1.969        by (simp add:int_distrib zadd_ac)
   1.970 -    ultimately show "P x \<longrightarrow> P(x + (i + 1) * d)" by blast
   1.971 -  qed
   1.972 +    ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
   1.973 +  thus ?case ..
   1.974  qed
   1.975  
   1.976 -lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
   1.977 -==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
   1.978 -==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
   1.979 -==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
   1.980 -apply(rule iffI)
   1.981 -prefer 2
   1.982 -apply(drule minusinfinity)
   1.983 -apply assumption+
   1.984 -apply(fastsimp)
   1.985 -apply clarsimp
   1.986 -apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
   1.987 -apply(frule_tac x = x and z=z in decr_lemma)
   1.988 -apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
   1.989 -prefer 2
   1.990 -apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
   1.991 -prefer 2 apply arith
   1.992 - apply fastsimp
   1.993 -apply(drule (1) minf_vee)
   1.994 -apply blast
   1.995 -apply(blast dest:decr_mult_lemma)
   1.996 -done
   1.997 -
   1.998 -text {* Cooper Theorem, plus infinity version. *}
   1.999 -lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
  1.1000 -==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
  1.1001 -==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
  1.1002 -==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)))"
  1.1003 -  apply(rule iffI)
  1.1004 -  prefer 2
  1.1005 -  apply(drule plusinfinity)
  1.1006 -  apply assumption+
  1.1007 -  apply(fastsimp)
  1.1008 -  apply clarsimp
  1.1009 -  apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x + k*D)")
  1.1010 -  apply(frule_tac x = x and z=z in incr_lemma)
  1.1011 -  apply(subgoal_tac "P1(x + (\<bar>x - z\<bar> + 1) * D)")
  1.1012 -  prefer 2
  1.1013 -  apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
  1.1014 -  prefer 2 apply arith
  1.1015 -  apply fastsimp
  1.1016 -  apply(drule (1) pinf_vee)
  1.1017 -  apply blast
  1.1018 -  apply(blast dest:incr_mult_lemma)
  1.1019 -  done
  1.1020 -
  1.1021 -
  1.1022 -text {*
  1.1023 -  \bigskip Theorems for the quantifier elminination Functions. *}
  1.1024 -
  1.1025 -lemma qe_ex_conj: "(EX (x::int). A x) = R
  1.1026 -		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
  1.1027 -		==> (EX (x::int). P x) = (Q & R)"
  1.1028 -by blast
  1.1029 -
  1.1030 -lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q)
  1.1031 -		==> (EX (x::int). P x) = Q"
  1.1032 -by blast
  1.1033 -
  1.1034 -lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)"
  1.1035 -by blast
  1.1036 -
  1.1037 -lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)"
  1.1038 -by blast
  1.1039 -
  1.1040 -lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)"
  1.1041 -by blast
  1.1042 -
  1.1043 -lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)"
  1.1044 -by blast
  1.1045 -
  1.1046 -lemma qe_Not: "P = Q ==> (~P) = (~Q)"
  1.1047 -by blast
  1.1048 -
  1.1049 -lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
  1.1050 -by blast
  1.1051 -
  1.1052 -text {* \bigskip Theorems for proving NNF *}
  1.1053 -
  1.1054 -lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
  1.1055 -by blast
  1.1056 -
  1.1057 -lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))"
  1.1058 -by blast
  1.1059 -
  1.1060 -lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)"
  1.1061 -  by blast
  1.1062 -lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))"
  1.1063 -by blast
  1.1064 -
  1.1065 -lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))"
  1.1066 -by blast
  1.1067 -lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))"
  1.1068 -by blast
  1.1069 -lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))"
  1.1070 -by blast
  1.1071 -lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))"
  1.1072 -by blast
  1.1073 -
  1.1074 -
  1.1075 -lemma qe_exI2: "A = B ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
  1.1076 -  by simp
  1.1077 -
  1.1078 -lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
  1.1079 -  by iprover
  1.1080 -
  1.1081 -lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
  1.1082 -  by iprover
  1.1083 -
  1.1084 -lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
  1.1085 -==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
  1.1086 -by blast
  1.1087 -
  1.1088 -lemma cppi_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j)))
  1.1089 -==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) "
  1.1090 -by blast
  1.1091 -
  1.1092 +lemma cppi: 
  1.1093 +  assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x> z. P x = P' x"
  1.1094 +  and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> A. x \<noteq> b - j) --> P (x) --> P (x + D)"
  1.1095 +  and pd: "\<forall> x k. P' x= P' (x-k*D)"
  1.1096 +  shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j) | (\<exists> j \<in> {1..D}.\<exists> b\<in> A. P (b - j)))" (is "?L = (?R1 \<or> ?R2)")
  1.1097 +proof-
  1.1098 + {assume "?R2" hence "?L"  by blast}
  1.1099 + moreover
  1.1100 + {assume H:"?R1" hence "?L" using plusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp}
  1.1101 + moreover 
  1.1102 + { fix x
  1.1103 +   assume P: "P x" and H: "\<not> ?R2"
  1.1104 +   {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>A. P (b - j))" and P: "P y"
  1.1105 +     hence "~(EX (j::int) : {1..D}. EX (b::int) : A. y = b - j)" by auto
  1.1106 +     with nb P  have "P (y + D)" by auto }
  1.1107 +   hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : A. P(b-j)) --> P (x) --> P (x + D)" by blast
  1.1108 +   with H P have th: " \<forall>x. P x \<longrightarrow> P (x + D)" by auto
  1.1109 +   from p1 obtain z where z: "ALL x. x > z --> (P x = P' x)" by blast
  1.1110 +   let ?y = "x + (\<bar>x - z\<bar> + 1)*D"
  1.1111 +   have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith
  1.1112 +   from dp have yz: "?y > z" using incr_lemma[OF dp] by simp
  1.1113 +   from z[rule_format, OF yz] incr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto
  1.1114 +   with periodic_finite_ex[OF dp pd]
  1.1115 +   have "?R1" by blast}
  1.1116 + ultimately show ?thesis by blast
  1.1117 +qed
  1.1118  
  1.1119  lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
  1.1120  apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
  1.1121  apply(fastsimp)
  1.1122  done
  1.1123  
  1.1124 -text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
  1.1125 -
  1.1126 -lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
  1.1127 -shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
  1.1128 -proof
  1.1129 -  assume ?P
  1.1130 -  thus ?Q
  1.1131 -    apply(simp add:dvd_def)
  1.1132 -    apply clarify
  1.1133 -    apply(rename_tac d)
  1.1134 -    apply(drule_tac f = "op * k" in arg_cong)
  1.1135 -    apply(simp only:int_distrib)
  1.1136 -    apply(rule_tac x = "d" in exI)
  1.1137 -    apply(simp only:mult_ac)
  1.1138 -    done
  1.1139 -next
  1.1140 -  assume ?Q
  1.1141 -  then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
  1.1142 -  hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
  1.1143 -  hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
  1.1144 -  hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
  1.1145 -  thus ?P by(simp add:dvd_def)
  1.1146 -qed
  1.1147 -
  1.1148 -lemma ac_lt_eq: assumes gr0: "0 < (k::int)"
  1.1149 -shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
  1.1150 -proof
  1.1151 -  assume P: ?P
  1.1152 -  show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
  1.1153 -next
  1.1154 -  assume ?Q
  1.1155 -  hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
  1.1156 -  with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
  1.1157 -  thus ?P by(simp)
  1.1158 -qed
  1.1159 +theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
  1.1160 +  apply (rule eq_reflection[symmetric])
  1.1161 +  apply (rule iffI)
  1.1162 +  defer
  1.1163 +  apply (erule exE)
  1.1164 +  apply (rule_tac x = "l * x" in exI)
  1.1165 +  apply (simp add: dvd_def)
  1.1166 +  apply (rule_tac x="x" in exI, simp)
  1.1167 +  apply (erule exE)
  1.1168 +  apply (erule conjE)
  1.1169 +  apply (erule dvdE)
  1.1170 +  apply (rule_tac x = k in exI)
  1.1171 +  apply simp
  1.1172 +  done
  1.1173  
  1.1174 -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")
  1.1175 -proof
  1.1176 -  assume ?P
  1.1177 -  thus ?Q
  1.1178 -    apply(drule_tac f = "op * k" in arg_cong)
  1.1179 -    apply(simp only:int_distrib)
  1.1180 -    done
  1.1181 -next
  1.1182 -  assume ?Q
  1.1183 -  hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
  1.1184 -  hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
  1.1185 -  thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
  1.1186 -qed
  1.1187 +lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0"
  1.1188 +shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" 
  1.1189 +  using not0 by (simp add: dvd_def)
  1.1190  
  1.1191 -lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
  1.1192 -proof -
  1.1193 -  have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
  1.1194 -  also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
  1.1195 -  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])
  1.1196 -  also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
  1.1197 -  finally show ?thesis .
  1.1198 -qed
  1.1199 -
  1.1200 -lemma binminus_uminus_conv: "(a::int) - b = a + (-b)"
  1.1201 -by arith
  1.1202 +lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))"
  1.1203 +by blast
  1.1204  
  1.1205 -lemma  linearize_dvd: "(t::int) = t1 ==> (d dvd t) = (d dvd t1)"
  1.1206 -by simp
  1.1207 -
  1.1208 -lemma lf_lt: "(l::int) = ll ==> (r::int) = lr ==> (l < r) =(ll < lr)"
  1.1209 -by simp
  1.1210 -
  1.1211 -lemma lf_eq: "(l::int) = ll ==> (r::int) = lr ==> (l = r) =(ll = lr)"
  1.1212 -by simp
  1.1213 -
  1.1214 -lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
  1.1215 -by simp
  1.1216 -
  1.1217 +lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
  1.1218 +  by simp_all
  1.1219  text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
  1.1220 -
  1.1221 -theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
  1.1222 +lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
  1.1223    by (simp split add: split_nat)
  1.1224  
  1.1225 +lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
  1.1226 +  by (auto split add: split_nat) 
  1.1227 +(rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
  1.1228  
  1.1229 -theorem zdiff_int_split: "P (int (x - y)) =
  1.1230 +lemma zdiff_int_split: "P (int (x - y)) =
  1.1231    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
  1.1232 -  apply (case_tac "y \<le> x")
  1.1233 -  apply (simp_all add: zdiff_int)
  1.1234 +  by (case_tac "y \<le> x",simp_all add: zdiff_int)
  1.1235 +
  1.1236 +lemma zdvd_int: "(x dvd y) = (int x dvd int y)"
  1.1237 +  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
  1.1238 +    nat_0_le cong add: conj_cong)
  1.1239 +  apply (rule iffI)
  1.1240 +  apply iprover
  1.1241 +  apply (erule exE)
  1.1242 +  apply (case_tac "x=0")
  1.1243 +  apply (rule_tac x=0 in exI)
  1.1244 +  apply simp
  1.1245 +  apply (case_tac "0 \<le> k")
  1.1246 +  apply iprover
  1.1247 +  apply (simp add: linorder_not_le)
  1.1248 +  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
  1.1249 +  apply assumption
  1.1250 +  apply (simp add: mult_ac)
  1.1251    done
  1.1252  
  1.1253 -
  1.1254 -theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
  1.1255 -  by simp
  1.1256 -
  1.1257 -theorem number_of2: "(0::int) <= Numeral0" by simp
  1.1258 -
  1.1259 -theorem Suc_plus1: "Suc n = n + 1" by simp
  1.1260 +lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
  1.1261 +lemma number_of2: "(0::int) <= Numeral0" by simp
  1.1262 +lemma Suc_plus1: "Suc n = n + 1" by simp
  1.1263  
  1.1264  text {*
  1.1265    \medskip Specific instances of congruence rules, to prevent
  1.1266    simplifier from looping. *}
  1.1267  
  1.1268 -theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
  1.1269 -  by simp
  1.1270 -
  1.1271 -theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
  1.1272 -  by (simp cong: conj_cong)
  1.1273 -
  1.1274 -    (* Theorems used in presburger.ML for the computation simpset*)
  1.1275 -    (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*)
  1.1276 +theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')" by simp
  1.1277  
  1.1278 -lemma lift_bool: "x \<Longrightarrow> x=True"
  1.1279 -  by simp
  1.1280 -
  1.1281 -lemma nlift_bool: "~x \<Longrightarrow> x=False"
  1.1282 -  by simp
  1.1283 -
  1.1284 -lemma not_false_eq_true: "(~ False) = True" by simp
  1.1285 -
  1.1286 -lemma not_true_eq_false: "(~ True) = False" by simp
  1.1287 -
  1.1288 -
  1.1289 +theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" 
  1.1290 +  by (simp cong: conj_cong)
  1.1291  lemma int_eq_number_of_eq:
  1.1292    "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
  1.1293    by simp
  1.1294 -lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
  1.1295 -  by (simp only: iszero_number_of_Pls)
  1.1296  
  1.1297 -lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
  1.1298 -  by simp
  1.1299 -
  1.1300 -lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
  1.1301 -  by simp
  1.1302 -
  1.1303 -lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
  1.1304 -  by simp
  1.1305 -
  1.1306 -lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
  1.1307 -  by simp
  1.1308 -
  1.1309 -lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
  1.1310 -  by simp
  1.1311 -
  1.1312 -lemma int_neg_number_of_Min: "neg (-1::int)"
  1.1313 -  by simp
  1.1314 -
  1.1315 -lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
  1.1316 -  by simp
  1.1317 -
  1.1318 -lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
  1.1319 -  by simp
  1.1320 -lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
  1.1321 -  by simp
  1.1322 -
  1.1323 -lemma int_number_of_diff_sym:
  1.1324 -  "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
  1.1325 -  by simp
  1.1326 -
  1.1327 -lemma int_number_of_mult_sym:
  1.1328 -  "((number_of v)::int) * number_of w = number_of (v * w)"
  1.1329 -  by simp
  1.1330 -
  1.1331 -lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
  1.1332 -  by simp
  1.1333 -lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
  1.1334 -  by simp
  1.1335  
  1.1336 -lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
  1.1337 -  by simp
  1.1338 -
  1.1339 -lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
  1.1340 -  by simp
  1.1341 -
  1.1342 -lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
  1.1343 -  by simp
  1.1344 -
  1.1345 -lemma int_pow_0: "(a::int)^(Numeral0) = 1"
  1.1346 -  by simp
  1.1347 -
  1.1348 -lemma int_pow_1: "(a::int)^(Numeral1) = a"
  1.1349 -  by simp
  1.1350 -
  1.1351 -lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
  1.1352 -  by simp
  1.1353 -
  1.1354 -lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
  1.1355 -  by simp
  1.1356 +use "Tools/Presburger/cooper.ML"
  1.1357 +oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
  1.1358  
  1.1359 -lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
  1.1360 -  by simp
  1.1361 -
  1.1362 -lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
  1.1363 -  by simp
  1.1364 -
  1.1365 -lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
  1.1366 -  by simp
  1.1367 -
  1.1368 -lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
  1.1369 -proof -
  1.1370 -  have 1:"((-1)::nat) = 0"
  1.1371 -    by simp
  1.1372 -  show ?thesis by (simp add: 1)
  1.1373 -qed
  1.1374 -
  1.1375 -use "Tools/Presburger/cooper_dec.ML"
  1.1376 -use "Tools/Presburger/reflected_presburger.ML" 
  1.1377 -use "Tools/Presburger/reflected_cooper.ML"
  1.1378 -oracle
  1.1379 -  presburger_oracle ("term") = ReflectedCooper.presburger_oracle
  1.1380 -
  1.1381 -use "Tools/Presburger/cooper_proof.ML"
  1.1382 -use "Tools/Presburger/qelim.ML"
  1.1383  use "Tools/Presburger/presburger.ML"
  1.1384  
  1.1385 -setup "Presburger.setup"
  1.1386 -
  1.1387 +setup {* 
  1.1388 +  arith_tactic_add 
  1.1389 +    (mk_arith_tactic "presburger" (fn i => fn st =>
  1.1390 +       (warning "Trying Presburger arithmetic ...";   
  1.1391 +    Presburger.cooper_tac true ((ProofContext.init o theory_of_thm) st) i st)))
  1.1392 +  (* FIXME!!!!!!! get the right context!!*)	
  1.1393 +*}
  1.1394 +method_setup presburger = {* Method.simple_args (Scan.optional (Args.$$$ "elim" >> K false) true)  
  1.1395 +  (fn q => fn ctxt =>  Method.SIMPLE_METHOD' (Presburger.cooper_tac q ctxt))*} ""
  1.1396 +(*
  1.1397 +method_setup presburger = {*
  1.1398 +  Method.ctxt_args (Method.SIMPLE_METHOD' o (Presburger.cooper_tac true))
  1.1399 +*} ""
  1.1400 +*)
  1.1401  
  1.1402  subsection {* Code generator setup *}
  1.1403 -
  1.1404  text {*
  1.1405    Presburger arithmetic is convenient to prove some
  1.1406    of the following code lemmas on integer numerals:
  1.1407 @@ -1243,7 +625,6 @@
  1.1408    "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
  1.1409    unfolding number_of_is_id ..
  1.1410  
  1.1411 -
  1.1412  lemmas pred_succ_numeral_code [code func] =
  1.1413    arith_simps(5-12)
  1.1414  
  1.1415 @@ -1277,4 +658,4 @@
  1.1416    less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
  1.1417    less_number_of
  1.1418  
  1.1419 -end
  1.1420 +end
  1.1421 \ No newline at end of file