src/HOL/Integ/Presburger.thy
changeset 13876 68f4ed8311ac
child 14139 ca3dd7ed5ac5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Tue Mar 25 09:47:05 2003 +0100
     1.3 @@ -0,0 +1,1002 @@
     1.4 +(*  Title:      HOL/Integ/Presburger.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +File containing necessary theorems for the proof
    1.10 +generation for Cooper Algorithm  
    1.11 +*)
    1.12 +
    1.13 +theory Presburger = NatSimprocs
    1.14 +files
    1.15 +  ("cooper_dec.ML")
    1.16 +  ("cooper_proof.ML")
    1.17 +  ("qelim.ML")
    1.18 +  ("presburger.ML"):
    1.19 +
    1.20 +(* Theorem for unitifying the coeffitients of x in an existential formula*)
    1.21 +
    1.22 +theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
    1.23 +  apply (rule iffI)
    1.24 +  apply (erule exE)
    1.25 +  apply (rule_tac x = "l * x" in exI)
    1.26 +  apply simp
    1.27 +  apply (erule exE)
    1.28 +  apply (erule conjE)
    1.29 +  apply (erule dvdE)
    1.30 +  apply (rule_tac x = k in exI)
    1.31 +  apply simp
    1.32 +  done
    1.33 +
    1.34 +lemma uminus_dvd_conv: "(d dvd (t::int)) = (-d dvd t)"
    1.35 +apply(unfold dvd_def)
    1.36 +apply(rule iffI)
    1.37 +apply(clarsimp)
    1.38 +apply(rename_tac k)
    1.39 +apply(rule_tac x = "-k" in exI)
    1.40 +apply simp
    1.41 +apply(clarsimp)
    1.42 +apply(rename_tac k)
    1.43 +apply(rule_tac x = "-k" in exI)
    1.44 +apply simp
    1.45 +done
    1.46 +
    1.47 +lemma uminus_dvd_conv': "(d dvd (t::int)) = (d dvd -t)"
    1.48 +apply(unfold dvd_def)
    1.49 +apply(rule iffI)
    1.50 +apply(clarsimp)
    1.51 +apply(rule_tac x = "-k" in exI)
    1.52 +apply simp
    1.53 +apply(clarsimp)
    1.54 +apply(rule_tac x = "-k" in exI)
    1.55 +apply simp
    1.56 +done
    1.57 +
    1.58 +
    1.59 +
    1.60 +(*Theorems for the combination of proofs of the equality of P and P_m for integers x less than some integer z.*)
    1.61 +
    1.62 +theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    1.63 +  \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    1.64 +  \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
    1.65 +  apply (erule exE)+
    1.66 +  apply (rule_tac x = "min z1 z2" in exI)
    1.67 +  apply simp
    1.68 +  done
    1.69 +
    1.70 +
    1.71 +theorem eq_minf_disjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    1.72 +  \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    1.73 +  \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))"
    1.74 +
    1.75 +  apply (erule exE)+
    1.76 +  apply (rule_tac x = "min z1 z2" in exI)
    1.77 +  apply simp
    1.78 +  done
    1.79 +
    1.80 +
    1.81 +(*Theorems for the combination of proofs of the equality of P and P_m for integers x greather than some integer z.*)
    1.82 +
    1.83 +theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    1.84 +  \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    1.85 +  \<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
    1.86 +  apply (erule exE)+
    1.87 +  apply (rule_tac x = "max z1 z2" in exI)
    1.88 +  apply simp
    1.89 +  done
    1.90 +
    1.91 +
    1.92 +theorem eq_pinf_disjI: "\<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 \<or> B1 x) = (A2 x \<or> 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 +(*Theorems for the combination of proofs of the modulo D property for P
   1.101 +pluusinfinity*)
   1.102 +(* FIXME : This is THE SAME theorem as for the minusinf version, but with +k.. instead of -k.. In the future replace these both with only one*)
   1.103 +
   1.104 +theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
   1.105 +  \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
   1.106 +  \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
   1.107 +  by simp
   1.108 +
   1.109 +
   1.110 +theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
   1.111 +  \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
   1.112 +  \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
   1.113 +  by simp
   1.114 +
   1.115 +(*=============================================================================*)
   1.116 +(*This is one of the cases where the simplifed formula is prooved to habe some property
   1.117 +(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
   1.118 +(*FIXME : This is exaclty the same thm as for minusinf.*)
   1.119 +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.120 +by blast
   1.121 +
   1.122 +
   1.123 +
   1.124 +(*=============================================================================*)
   1.125 +(*Theorems for the combination of proofs of the modulo D property for P
   1.126 +minusinfinity*)
   1.127 +
   1.128 +theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
   1.129 +  \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
   1.130 +  \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
   1.131 +  by simp
   1.132 +
   1.133 +
   1.134 +theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
   1.135 +  \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
   1.136 +  \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
   1.137 +  by simp
   1.138 +
   1.139 +(*=============================================================================*)
   1.140 +(*This is one of the cases where the simplifed formula is prooved to habe some property
   1.141 +(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
   1.142 +
   1.143 +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.144 +by blast
   1.145 +
   1.146 +(*=============================================================================*)
   1.147 +
   1.148 +(*theorem needed for prooving at runtime divide properties using the arithmetic tatic
   1.149 +(who knows only about modulo = 0)*)
   1.150 +
   1.151 +lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   1.152 +by(simp add:dvd_def zmod_eq_0_iff)
   1.153 +
   1.154 +(*=============================================================================*)
   1.155 +
   1.156 +
   1.157 +
   1.158 +(*Theorems used for the combination of proof for the backwards direction of cooper's
   1.159 +theorem. they rely exclusively on Predicate calculus.*)
   1.160 +
   1.161 +lemma not_ast_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P1(x) --> P1(x + d))
   1.162 +==>
   1.163 +(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
   1.164 +==>
   1.165 +(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<or> P2(x)) --> (P1(x + d) \<or> P2(x + d))) "
   1.166 +by blast
   1.167 +
   1.168 +
   1.169 +
   1.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))
   1.171 +==>
   1.172 +(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
   1.173 +==>
   1.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)
   1.175 +\<and> P2(x + d))) "
   1.176 +by blast
   1.177 +
   1.178 +lemma not_ast_p_Q_elim: "
   1.179 +(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
   1.180 +==> ( P = Q )
   1.181 +==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
   1.182 +by blast
   1.183 +(*=============================================================================*)
   1.184 +
   1.185 +
   1.186 +(*Theorems used for the combination of proof for the backwards direction of cooper's
   1.187 +theorem. they rely exclusively on Predicate calculus.*)
   1.188 +
   1.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))
   1.190 +==>
   1.191 +(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d))
   1.192 +==>
   1.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)
   1.194 +\<or> P2(x-d))) "
   1.195 +by blast
   1.196 +
   1.197 +
   1.198 +
   1.199 +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.200 +==>
   1.201 +(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d))
   1.202 +==>
   1.203 +(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.204 +\<and> P2(x-d))) "
   1.205 +by blast
   1.206 +
   1.207 +lemma not_bst_p_Q_elim: "
   1.208 +(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) 
   1.209 +==> ( P = Q )
   1.210 +==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
   1.211 +by blast
   1.212 +(*=============================================================================*)
   1.213 +(*The Theorem for the second proof step- about bset. it is trivial too. *)
   1.214 +lemma bst_thm: " (EX (j::int) : {1..d}. EX (b::int) : B. P (b+j) )--> (EX x::int. P (x)) "
   1.215 +by blast
   1.216 +
   1.217 +(*The Theorem for the second proof step- about aset. it is trivial too. *)
   1.218 +lemma ast_thm: " (EX (j::int) : {1..d}. EX (a::int) : A. P (a - j) )--> (EX x::int. P (x)) "
   1.219 +by blast
   1.220 +
   1.221 +
   1.222 +(*=============================================================================*)
   1.223 +(*This is the first direction of cooper's theorem*)
   1.224 +lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
   1.225 +by blast
   1.226 +
   1.227 +(*=============================================================================*)
   1.228 +(*The full cooper's theoorem in its equivalence Form- Given the premisses it is trivial
   1.229 +too, it relies exclusively on prediacte calculus.*)
   1.230 +lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
   1.231 +--> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
   1.232 +by blast
   1.233 +
   1.234 +(*=============================================================================*)
   1.235 +(*Some of the atomic theorems generated each time the atom does not depend on x, they
   1.236 +are trivial.*)
   1.237 +
   1.238 +lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
   1.239 +by blast
   1.240 +
   1.241 +lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
   1.242 +by blast
   1.243 +
   1.244 +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.245 +by blast
   1.246 +
   1.247 +
   1.248 +
   1.249 +lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
   1.250 +by blast
   1.251 +
   1.252 +(* The next 2 thms are the same as the minusinf version*)
   1.253 +lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
   1.254 +by blast
   1.255 +
   1.256 +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.257 +by blast
   1.258 +
   1.259 +
   1.260 +(* Theorems to be deleted from simpset when proving simplified formulaes*)
   1.261 +lemma P_eqtrue: "(P=True) = P"
   1.262 +  by rules
   1.263 +
   1.264 +lemma P_eqfalse: "(P=False) = (~P)"
   1.265 +  by rules
   1.266 +
   1.267 +(*=============================================================================*)
   1.268 +
   1.269 +(*Theorems for the generation of the bachwards direction of cooper's theorem*)
   1.270 +(*These are the 6 interesting atomic cases which have to be proved relying on the
   1.271 +properties of B-set ant the arithmetic and contradiction proofs*)
   1.272 +
   1.273 +lemma not_bst_p_lt: "0 < (d::int) ==>
   1.274 + 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.275 +by arith
   1.276 +
   1.277 +lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
   1.278 + 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.279 +apply clarsimp
   1.280 +apply(rule ccontr)
   1.281 +apply(drule_tac x = "x+a" in bspec)
   1.282 +apply(simp add:atLeastAtMost_iff)
   1.283 +apply(drule_tac x = "-a" in bspec)
   1.284 +apply assumption
   1.285 +apply(simp)
   1.286 +done
   1.287 +
   1.288 +lemma not_bst_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a - 1 \<rbrakk> \<Longrightarrow>
   1.289 + ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> (0 = x + a) --> (0 = (x - d) + a )"
   1.290 +apply clarsimp
   1.291 +apply(subgoal_tac "x = -a")
   1.292 + prefer 2 apply arith
   1.293 +apply(drule_tac x = "1" in bspec)
   1.294 +apply(simp add:atLeastAtMost_iff)
   1.295 +apply(drule_tac x = "-a- 1" in bspec)
   1.296 +apply assumption
   1.297 +apply(simp)
   1.298 +done
   1.299 +
   1.300 +
   1.301 +lemma not_bst_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
   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 +apply clarsimp
   1.304 +apply(subgoal_tac "x = -a+d")
   1.305 + prefer 2 apply arith
   1.306 +apply(drule_tac x = "d" in bspec)
   1.307 +apply(simp add:atLeastAtMost_iff)
   1.308 +apply(drule_tac x = "-a" in bspec)
   1.309 +apply assumption
   1.310 +apply(simp)
   1.311 +done
   1.312 +
   1.313 +
   1.314 +lemma not_bst_p_dvd: "(d1::int) dvd d ==>
   1.315 + 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.316 +apply(clarsimp simp add:dvd_def)
   1.317 +apply(rename_tac m)
   1.318 +apply(rule_tac x = "m - k" in exI)
   1.319 +apply(simp add:int_distrib)
   1.320 +done
   1.321 +
   1.322 +lemma not_bst_p_ndvd: "(d1::int) dvd d ==>
   1.323 + 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.324 +apply(clarsimp simp add:dvd_def)
   1.325 +apply(rename_tac m)
   1.326 +apply(erule_tac x = "m + k" in allE)
   1.327 +apply(simp add:int_distrib)
   1.328 +done
   1.329 +
   1.330 +
   1.331 +
   1.332 +(*Theorems for the generation of the bachwards direction of cooper's theorem*)
   1.333 +(*These are the 6 interesting atomic cases which have to be proved relying on the
   1.334 +properties of A-set ant the arithmetic and contradiction proofs*)
   1.335 +
   1.336 +lemma not_ast_p_gt: "0 < (d::int) ==>
   1.337 + 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.338 +by arith
   1.339 +
   1.340 +
   1.341 +lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
   1.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)"
   1.343 +  apply clarsimp
   1.344 +  apply (rule ccontr)
   1.345 +  apply (drule_tac x = "t-x" in bspec)
   1.346 +  apply simp
   1.347 +  apply (drule_tac x = "t" in bspec)
   1.348 +  apply assumption
   1.349 +  apply simp
   1.350 +  done
   1.351 +
   1.352 +lemma not_ast_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t + 1 \<rbrakk> \<Longrightarrow>
   1.353 + ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> (0 = x + t) --> (0 = (x + d) + t )"
   1.354 +  apply clarsimp
   1.355 +  apply (drule_tac x="1" in bspec)
   1.356 +  apply simp
   1.357 +  apply (drule_tac x="- t + 1" in bspec)
   1.358 +  apply assumption
   1.359 +  apply(subgoal_tac "x = -t")
   1.360 +  prefer 2 apply arith
   1.361 +  apply simp
   1.362 +  done
   1.363 +
   1.364 +lemma not_ast_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t \<rbrakk> \<Longrightarrow>
   1.365 + 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.366 +  apply clarsimp
   1.367 +  apply (subgoal_tac "x = -t-d")
   1.368 +  prefer 2 apply arith
   1.369 +  apply (drule_tac x = "d" in bspec)
   1.370 +  apply simp
   1.371 +  apply (drule_tac x = "-t" in bspec)
   1.372 +  apply assumption
   1.373 +  apply simp
   1.374 +  done
   1.375 +
   1.376 +lemma not_ast_p_dvd: "(d1::int) dvd d ==>
   1.377 + 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.378 +  apply(clarsimp simp add:dvd_def)
   1.379 +  apply(rename_tac m)
   1.380 +  apply(rule_tac x = "m + k" in exI)
   1.381 +  apply(simp add:int_distrib)
   1.382 +  done
   1.383 +
   1.384 +lemma not_ast_p_ndvd: "(d1::int) dvd d ==>
   1.385 + 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.386 +  apply(clarsimp simp add:dvd_def)
   1.387 +  apply(rename_tac m)
   1.388 +  apply(erule_tac x = "m - k" in allE)
   1.389 +  apply(simp add:int_distrib)
   1.390 +  done
   1.391 +
   1.392 +
   1.393 +
   1.394 +(*=============================================================================*)
   1.395 +(*These are the atomic cases for the proof generation for the modulo D property for P
   1.396 +plusinfinity*)
   1.397 +(*They are fully based on arithmetics*)
   1.398 +
   1.399 +lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
   1.400 + (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
   1.401 +  apply(clarsimp simp add:dvd_def)
   1.402 +  apply(rule iffI)
   1.403 +  apply(clarsimp)
   1.404 +  apply(rename_tac n m)
   1.405 +  apply(rule_tac x = "m + n*k" in exI)
   1.406 +  apply(simp add:int_distrib)
   1.407 +  apply(clarsimp)
   1.408 +  apply(rename_tac n m)
   1.409 +  apply(rule_tac x = "m - n*k" in exI)
   1.410 +  apply(simp add:int_distrib zmult_ac)
   1.411 +  done
   1.412 +
   1.413 +lemma  not_dvd_modd_pinf: "((d::int) dvd d1) ==>
   1.414 + (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x+k*d1 + t))))"
   1.415 +  apply(clarsimp simp add:dvd_def)
   1.416 +  apply(rule iffI)
   1.417 +  apply(clarsimp)
   1.418 +  apply(rename_tac n m)
   1.419 +  apply(erule_tac x = "m - n*k" in allE)
   1.420 +  apply(simp add:int_distrib zmult_ac)
   1.421 +  apply(clarsimp)
   1.422 +  apply(rename_tac n m)
   1.423 +  apply(erule_tac x = "m + n*k" in allE)
   1.424 +  apply(simp add:int_distrib zmult_ac)
   1.425 +  done
   1.426 +
   1.427 +(*=============================================================================*)
   1.428 +(*These are the atomic cases for the proof generation for the equivalence of P and P
   1.429 +plusinfinity for integers x greather than some integer z.*)
   1.430 +(*They are fully based on arithmetics*)
   1.431 +
   1.432 +lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
   1.433 +  apply(rule_tac x = "-t" in exI)
   1.434 +  apply simp
   1.435 +  done
   1.436 +
   1.437 +lemma  neq_eq_pinf: "EX z::int. ALL x.  z < x --> ((~( 0 = x +t )) = True )"
   1.438 +  apply(rule_tac x = "-t" in exI)
   1.439 +  apply simp
   1.440 +  done
   1.441 +
   1.442 +lemma  le_eq_pinf: "EX z::int. ALL x.  z < x --> ( 0 < x +t  = True )"
   1.443 +  apply(rule_tac x = "-t" in exI)
   1.444 +  apply simp
   1.445 +  done
   1.446 +
   1.447 +lemma  len_eq_pinf: "EX z::int. ALL x. z < x  --> (0 < -x +t  = False )"
   1.448 +  apply(rule_tac x = "t" in exI)
   1.449 +  apply simp
   1.450 +  done
   1.451 +
   1.452 +lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
   1.453 +by simp
   1.454 +
   1.455 +lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   1.456 +by simp
   1.457 +
   1.458 +
   1.459 +
   1.460 +
   1.461 +(*=============================================================================*)
   1.462 +(*These are the atomic cases for the proof generation for the modulo D property for P
   1.463 +minusinfinity*)
   1.464 +(*They are fully based on arithmetics*)
   1.465 +
   1.466 +lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
   1.467 + (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
   1.468 +apply(clarsimp simp add:dvd_def)
   1.469 +apply(rule iffI)
   1.470 +apply(clarsimp)
   1.471 +apply(rename_tac n m)
   1.472 +apply(rule_tac x = "m - n*k" in exI)
   1.473 +apply(simp add:int_distrib)
   1.474 +apply(clarsimp)
   1.475 +apply(rename_tac n m)
   1.476 +apply(rule_tac x = "m + n*k" in exI)
   1.477 +apply(simp add:int_distrib zmult_ac)
   1.478 +done
   1.479 +
   1.480 +
   1.481 +lemma  not_dvd_modd_minf: "((d::int) dvd d1) ==>
   1.482 + (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x-k*d1 + t))))"
   1.483 +apply(clarsimp simp add:dvd_def)
   1.484 +apply(rule iffI)
   1.485 +apply(clarsimp)
   1.486 +apply(rename_tac n m)
   1.487 +apply(erule_tac x = "m + n*k" in allE)
   1.488 +apply(simp add:int_distrib zmult_ac)
   1.489 +apply(clarsimp)
   1.490 +apply(rename_tac n m)
   1.491 +apply(erule_tac x = "m - n*k" in allE)
   1.492 +apply(simp add:int_distrib zmult_ac)
   1.493 +done
   1.494 +
   1.495 +
   1.496 +(*=============================================================================*)
   1.497 +(*These are the atomic cases for the proof generation for the equivalence of P and P
   1.498 +minusinfinity for integers x less than some integer z.*)
   1.499 +(*They are fully based on arithmetics*)
   1.500 +
   1.501 +lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
   1.502 +apply(rule_tac x = "-t" in exI)
   1.503 +apply simp
   1.504 +done
   1.505 +
   1.506 +lemma  neq_eq_minf: "EX z::int. ALL x. x < z --> ((~( 0 = x +t )) = True )"
   1.507 +apply(rule_tac x = "-t" in exI)
   1.508 +apply simp
   1.509 +done
   1.510 +
   1.511 +lemma  le_eq_minf: "EX z::int. ALL x. x < z --> ( 0 < x +t  = False )"
   1.512 +apply(rule_tac x = "-t" in exI)
   1.513 +apply simp
   1.514 +done
   1.515 +
   1.516 +
   1.517 +lemma  len_eq_minf: "EX z::int. ALL x. x < z --> (0 < -x +t  = True )"
   1.518 +apply(rule_tac x = "t" in exI)
   1.519 +apply simp
   1.520 +done
   1.521 +
   1.522 +lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
   1.523 +by simp
   1.524 +
   1.525 +lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   1.526 +by simp
   1.527 +
   1.528 +
   1.529 +(*=============================================================================*)
   1.530 +(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
   1.531 +equivalence proof for cooper's theorem*)
   1.532 +
   1.533 +(* FIXME: remove once they are part of the distribution *)
   1.534 +theorem int_ge_induct[consumes 1,case_names base step]:
   1.535 +  assumes ge: "k \<le> (i::int)" and
   1.536 +        base: "P(k)" and
   1.537 +        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
   1.538 +  shows "P i"
   1.539 +proof -
   1.540 +  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
   1.541 +    proof (induct n)
   1.542 +      case 0
   1.543 +      hence "i = k" by arith
   1.544 +      thus "P i" using base by simp
   1.545 +    next
   1.546 +      case (Suc n)
   1.547 +      hence "n = nat((i - 1) - k)" by arith
   1.548 +      moreover
   1.549 +      have ki1: "k \<le> i - 1" using Suc.prems by arith
   1.550 +      ultimately
   1.551 +      have "P(i - 1)" by(rule Suc.hyps)
   1.552 +      from step[OF ki1 this] show ?case by simp
   1.553 +    qed
   1.554 +  }
   1.555 +  from this ge show ?thesis by fast
   1.556 +qed
   1.557 +
   1.558 +theorem int_gr_induct[consumes 1,case_names base step]:
   1.559 +  assumes gr: "k < (i::int)" and
   1.560 +        base: "P(k+1)" and
   1.561 +        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
   1.562 +  shows "P i"
   1.563 +apply(rule int_ge_induct[of "k + 1"])
   1.564 +  using gr apply arith
   1.565 + apply(rule base)
   1.566 +apply(rule step)
   1.567 + apply simp+
   1.568 +done
   1.569 +
   1.570 +lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
   1.571 +apply(induct rule: int_gr_induct)
   1.572 + apply simp
   1.573 + apply arith
   1.574 +apply (simp add:int_distrib)
   1.575 +apply arith
   1.576 +done
   1.577 +
   1.578 +lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   1.579 +apply(induct rule: int_gr_induct)
   1.580 + apply simp
   1.581 + apply arith
   1.582 +apply (simp add:int_distrib)
   1.583 +apply arith
   1.584 +done
   1.585 +
   1.586 +lemma  minusinfinity:
   1.587 +  assumes "0 < d" and
   1.588 +    P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and
   1.589 +    ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
   1.590 +  shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
   1.591 +proof
   1.592 +  assume eP1: "EX x. P1 x"
   1.593 +  then obtain x where P1: "P1 x" ..
   1.594 +  from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
   1.595 +  let ?w = "x - (abs(x-z)+1) * d"
   1.596 +  show "EX x. P x"
   1.597 +  proof
   1.598 +    have w: "?w < z" by(rule decr_lemma)
   1.599 +    have "P1 x = P1 ?w" using P1eqP1 by blast
   1.600 +    also have "\<dots> = P(?w)" using w P1eqP by blast
   1.601 +    finally show "P ?w" using P1 by blast
   1.602 +  qed
   1.603 +qed
   1.604 +
   1.605 +(*=============================================================================*)
   1.606 +(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
   1.607 +equivalence proof for cooper's theorem*)
   1.608 +
   1.609 +lemma plusinfinity:
   1.610 +  assumes "0 < d" and
   1.611 +    P1eqP1: "ALL (x::int) (k::int). P1 x = P1 (x + k * d)" and
   1.612 +    ePeqP1: "EX z::int. ALL x. z < x  --> (P x = P1 x)"
   1.613 +  shows "(EX x::int. P1 x) --> (EX x::int. P x)"
   1.614 +proof
   1.615 +  assume eP1: "EX x. P1 x"
   1.616 +  then obtain x where P1: "P1 x" ..
   1.617 +  from ePeqP1 obtain z where P1eqP: "ALL x. z < x \<longrightarrow> (P x = P1 x)" ..
   1.618 +  let ?w = "x + (abs(x-z)+1) * d"
   1.619 +  show "EX x. P x"
   1.620 +  proof
   1.621 +    have w: "z < ?w" by(rule incr_lemma)
   1.622 +    have "P1 x = P1 ?w" using P1eqP1 by blast
   1.623 +    also have "\<dots> = P(?w)" using w P1eqP by blast
   1.624 +    finally show "P ?w" using P1 by blast
   1.625 +  qed
   1.626 +qed
   1.627 + 
   1.628 +
   1.629 +
   1.630 +(*=============================================================================*)
   1.631 +(*Theorem for periodic function on discrete sets*)
   1.632 +
   1.633 +lemma minf_vee:
   1.634 +  assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   1.635 +  shows "(EX x. P x) = (EX j : {1..d}. P j)"
   1.636 +  (is "?LHS = ?RHS")
   1.637 +proof
   1.638 +  assume ?LHS
   1.639 +  then obtain x where P: "P x" ..
   1.640 +  have "x mod d = x - (x div d)*d"
   1.641 +    by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
   1.642 +  hence Pmod: "P x = P(x mod d)" using modd by simp
   1.643 +  show ?RHS
   1.644 +  proof (cases)
   1.645 +    assume "x mod d = 0"
   1.646 +    hence "P 0" using P Pmod by simp
   1.647 +    moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
   1.648 +    ultimately have "P d" by simp
   1.649 +    moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
   1.650 +    ultimately show ?RHS ..
   1.651 +  next
   1.652 +    assume not0: "x mod d \<noteq> 0"
   1.653 +    have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
   1.654 +    moreover have "x mod d : {1..d}"
   1.655 +    proof -
   1.656 +      have "0 \<le> x mod d" by(rule pos_mod_sign)
   1.657 +      moreover have "x mod d < d" by(rule pos_mod_bound)
   1.658 +      ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
   1.659 +    qed
   1.660 +    ultimately show ?RHS ..
   1.661 +  qed
   1.662 +next
   1.663 +  assume ?RHS thus ?LHS by blast
   1.664 +qed
   1.665 +
   1.666 +(*=============================================================================*)
   1.667 +(*Theorem for periodic function on discrete sets*)
   1.668 +lemma pinf_vee:
   1.669 +  assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
   1.670 +  shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
   1.671 +  (is "?LHS = ?RHS")
   1.672 +proof
   1.673 +  assume ?LHS
   1.674 +  then obtain x where P: "P x" ..
   1.675 +  have "x mod d = x + (-(x div d))*d"
   1.676 +    by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
   1.677 +  hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
   1.678 +  show ?RHS
   1.679 +  proof (cases)
   1.680 +    assume "x mod d = 0"
   1.681 +    hence "P 0" using P Pmod by simp
   1.682 +    moreover have "P 0 = P(0 + 1*d)" using modd by blast
   1.683 +    ultimately have "P d" by simp
   1.684 +    moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
   1.685 +    ultimately show ?RHS ..
   1.686 +  next
   1.687 +    assume not0: "x mod d \<noteq> 0"
   1.688 +    have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
   1.689 +    moreover have "x mod d : {1..d}"
   1.690 +    proof -
   1.691 +      have "0 \<le> x mod d" by(rule pos_mod_sign)
   1.692 +      moreover have "x mod d < d" by(rule pos_mod_bound)
   1.693 +      ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
   1.694 +    qed
   1.695 +    ultimately show ?RHS ..
   1.696 +  qed
   1.697 +next
   1.698 +  assume ?RHS thus ?LHS by blast
   1.699 +qed
   1.700 +
   1.701 +lemma decr_mult_lemma:
   1.702 +  assumes dpos: "(0::int) < d" and
   1.703 +          minus: "ALL x::int. P x \<longrightarrow> P(x - d)" and
   1.704 +          knneg: "0 <= k"
   1.705 +  shows "ALL x. P x \<longrightarrow> P(x - k*d)"
   1.706 +using knneg
   1.707 +proof (induct rule:int_ge_induct)
   1.708 +  case base thus ?case by simp
   1.709 +next
   1.710 +  case (step i)
   1.711 +  show ?case
   1.712 +  proof
   1.713 +    fix x
   1.714 +    have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
   1.715 +    also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
   1.716 +      using minus[THEN spec, of "x - i * d"]
   1.717 +      by (simp add:int_distrib zdiff_zdiff_eq[symmetric])
   1.718 +    ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
   1.719 +  qed
   1.720 +qed
   1.721 +
   1.722 +lemma incr_mult_lemma:
   1.723 +  assumes dpos: "(0::int) < d" and
   1.724 +          plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and
   1.725 +          knneg: "0 <= k"
   1.726 +  shows "ALL x. P x \<longrightarrow> P(x + k*d)"
   1.727 +using knneg
   1.728 +proof (induct rule:int_ge_induct)
   1.729 +  case base thus ?case by simp
   1.730 +next
   1.731 +  case (step i)
   1.732 +  show ?case
   1.733 +  proof
   1.734 +    fix x
   1.735 +    have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
   1.736 +    also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)"
   1.737 +      using plus[THEN spec, of "x + i * d"]
   1.738 +      by (simp add:int_distrib zadd_ac)
   1.739 +    ultimately show "P x \<longrightarrow> P(x + (i + 1) * d)" by blast
   1.740 +  qed
   1.741 +qed
   1.742 +
   1.743 +lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
   1.744 +==> (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)) --> (EX (x::int). P x) 
   1.745 +==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
   1.746 +==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
   1.747 +==> (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.748 +apply(rule iffI)
   1.749 +prefer 2
   1.750 +apply(drule minusinfinity)
   1.751 +apply assumption+
   1.752 +apply(fastsimp)
   1.753 +apply clarsimp
   1.754 +apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
   1.755 +apply(frule_tac x = x and z=z in decr_lemma)
   1.756 +apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
   1.757 +prefer 2
   1.758 +apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
   1.759 +prefer 2 apply arith
   1.760 + apply fastsimp
   1.761 +apply(drule (1) minf_vee)
   1.762 +apply blast
   1.763 +apply(blast dest:decr_mult_lemma)
   1.764 +done
   1.765 +
   1.766 +(* Cooper Thm `, plus infinity version*)
   1.767 +lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
   1.768 +==> (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)) --> (EX (x::int). P x) 
   1.769 +==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
   1.770 +==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
   1.771 +==> (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.772 +  apply(rule iffI)
   1.773 +  prefer 2
   1.774 +  apply(drule plusinfinity)
   1.775 +  apply assumption+
   1.776 +  apply(fastsimp)
   1.777 +  apply clarsimp
   1.778 +  apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x + k*D)")
   1.779 +  apply(frule_tac x = x and z=z in incr_lemma)
   1.780 +  apply(subgoal_tac "P1(x + (\<bar>x - z\<bar> + 1) * D)")
   1.781 +  prefer 2
   1.782 +  apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
   1.783 +  prefer 2 apply arith
   1.784 +  apply fastsimp
   1.785 +  apply(drule (1) pinf_vee)
   1.786 +  apply blast
   1.787 +  apply(blast dest:incr_mult_lemma)
   1.788 +  done
   1.789 +
   1.790 +
   1.791 +(*=============================================================================*)
   1.792 +
   1.793 +(*Theorems for the quantifier elminination Functions.*)
   1.794 +
   1.795 +lemma qe_ex_conj: "(EX (x::int). A x) = R
   1.796 +		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
   1.797 +		==> (EX (x::int). P x) = (Q & R)"
   1.798 +by blast
   1.799 +
   1.800 +lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q)
   1.801 +		==> (EX (x::int). P x) = Q"
   1.802 +by blast
   1.803 +
   1.804 +lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)"
   1.805 +by blast
   1.806 +
   1.807 +lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)"
   1.808 +by blast
   1.809 +
   1.810 +lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)"
   1.811 +by blast
   1.812 +
   1.813 +lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)"
   1.814 +by blast
   1.815 +
   1.816 +lemma qe_Not: "P = Q ==> (~P) = (~Q)"
   1.817 +by blast
   1.818 +
   1.819 +lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
   1.820 +by blast
   1.821 +
   1.822 +(* Theorems for proving NNF *)
   1.823 +
   1.824 +lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
   1.825 +by blast
   1.826 +
   1.827 +lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))"
   1.828 +by blast
   1.829 +
   1.830 +lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)"
   1.831 +  by blast
   1.832 +lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))"
   1.833 +by blast
   1.834 +
   1.835 +lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))"
   1.836 +by blast
   1.837 +lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))"
   1.838 +by blast
   1.839 +lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))"
   1.840 +by blast
   1.841 +lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))"
   1.842 +by blast
   1.843 +
   1.844 +
   1.845 +lemma qe_exI2: "A = B ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
   1.846 +  by simp
   1.847 +
   1.848 +lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
   1.849 +  by rules
   1.850 +
   1.851 +lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
   1.852 +  by rules
   1.853 +
   1.854 +lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
   1.855 +==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
   1.856 +by blast
   1.857 +
   1.858 +lemma cppi_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j)))
   1.859 +==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) "
   1.860 +by blast
   1.861 +
   1.862 +
   1.863 +lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
   1.864 +apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
   1.865 +apply(fastsimp)
   1.866 +done
   1.867 +
   1.868 +(* Theorems required for the adjustcoeffitienteq*)
   1.869 +
   1.870 +lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
   1.871 +shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
   1.872 +proof
   1.873 +  assume ?P
   1.874 +  thus ?Q
   1.875 +    apply(simp add:dvd_def)
   1.876 +    apply clarify
   1.877 +    apply(rename_tac d)
   1.878 +    apply(drule_tac f = "op * k" in arg_cong)
   1.879 +    apply(simp only:int_distrib)
   1.880 +    apply(rule_tac x = "d" in exI)
   1.881 +    apply(simp only:zmult_ac)
   1.882 +    done
   1.883 +next
   1.884 +  assume ?Q
   1.885 +  then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
   1.886 +  hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib zmult_ac)
   1.887 +  hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
   1.888 +  hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
   1.889 +  thus ?P by(simp add:dvd_def)
   1.890 +qed
   1.891 +
   1.892 +lemma ac_lt_eq: assumes gr0: "0 < (k::int)"
   1.893 +shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
   1.894 +proof
   1.895 +  assume P: ?P
   1.896 +  show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib zmult_ac)
   1.897 +next
   1.898 +  assume ?Q
   1.899 +  hence "0 < k*(c*n + t - m)" by(simp add: int_distrib zmult_ac)
   1.900 +  with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
   1.901 +  thus ?P by(simp)
   1.902 +qed
   1.903 +
   1.904 +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.905 +proof
   1.906 +  assume ?P
   1.907 +  thus ?Q
   1.908 +    apply(drule_tac f = "op * k" in arg_cong)
   1.909 +    apply(simp only:int_distrib)
   1.910 +    done
   1.911 +next
   1.912 +  assume ?Q
   1.913 +  hence "m * k = (c*n + t) * k" by(simp add:int_distrib zmult_ac)
   1.914 +  hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
   1.915 +  thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
   1.916 +qed
   1.917 +
   1.918 +lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
   1.919 +proof -
   1.920 +  have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
   1.921 +  also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib zmult_ac)
   1.922 +  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.923 +  also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib zmult_ac)
   1.924 +  finally show ?thesis .
   1.925 +qed
   1.926 +
   1.927 +lemma binminus_uminus_conv: "(a::int) - b = a + (-b)"
   1.928 +by arith
   1.929 +
   1.930 +lemma  linearize_dvd: "(t::int) = t1 ==> (d dvd t) = (d dvd t1)"
   1.931 +by simp
   1.932 +
   1.933 +lemma lf_lt: "(l::int) = ll ==> (r::int) = lr ==> (l < r) =(ll < lr)"
   1.934 +by simp
   1.935 +
   1.936 +lemma lf_eq: "(l::int) = ll ==> (r::int) = lr ==> (l = r) =(ll = lr)"
   1.937 +by simp
   1.938 +
   1.939 +lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
   1.940 +by simp
   1.941 +
   1.942 +(* Theorems for transforming predicates on nat to predicates on int*)
   1.943 +
   1.944 +theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   1.945 +  by (simp split add: split_nat)
   1.946 +
   1.947 +theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
   1.948 +  apply (simp split add: split_nat)
   1.949 +  apply (rule iffI)
   1.950 +  apply (erule exE)
   1.951 +  apply (rule_tac x = "int x" in exI)
   1.952 +  apply simp
   1.953 +  apply (erule exE)
   1.954 +  apply (rule_tac x = "nat x" in exI)
   1.955 +  apply (erule conjE)
   1.956 +  apply (erule_tac x = "nat x" in allE)
   1.957 +  apply simp
   1.958 +  done
   1.959 +
   1.960 +theorem zdiff_int_split: "P (int (x - y)) =
   1.961 +  ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   1.962 +  apply (case_tac "y \<le> x")
   1.963 +  apply (simp_all add: zdiff_int)
   1.964 +  done
   1.965 +
   1.966 +theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
   1.967 +  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
   1.968 +    nat_0_le cong add: conj_cong)
   1.969 +  apply (rule iffI)
   1.970 +  apply rules
   1.971 +  apply (erule exE)
   1.972 +  apply (case_tac "x=0")
   1.973 +  apply (rule_tac x=0 in exI)
   1.974 +  apply simp
   1.975 +  apply (case_tac "0 \<le> k")
   1.976 +  apply rules
   1.977 +  apply (simp add: linorder_not_le)
   1.978 +  apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
   1.979 +  apply assumption
   1.980 +  apply (simp add: zmult_ac)
   1.981 +  done
   1.982 +
   1.983 +theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
   1.984 +  by simp
   1.985 +
   1.986 +theorem number_of2: "(0::int) <= number_of bin.Pls" by simp
   1.987 +
   1.988 +theorem Suc_plus1: "Suc n = n + 1" by simp
   1.989 +
   1.990 +(* specific instances of congruence rules, to prevent simplifier from looping *)
   1.991 +
   1.992 +theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
   1.993 +  by simp
   1.994 +
   1.995 +theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<and> P) = (0 <= x \<and> P')"
   1.996 +  by simp
   1.997 +
   1.998 +use "cooper_dec.ML"
   1.999 +use "cooper_proof.ML"
  1.1000 +use "qelim.ML"
  1.1001 +use "presburger.ML"
  1.1002 +
  1.1003 +setup "Presburger.setup"
  1.1004 +
  1.1005 +end