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.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.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.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.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.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.317 +apply(rename_tac m)
1.318 +apply(rule_tac x = "m - k" in exI)
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.325 +apply(rename_tac m)
1.326 +apply(erule_tac x = "m + k" in allE)
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.379 +  apply(rename_tac m)
1.380 +  apply(rule_tac x = "m + k" in exI)
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.387 +  apply(rename_tac m)
1.388 +  apply(erule_tac x = "m - k" in allE)
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.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.407 +  apply(clarsimp)
1.408 +  apply(rename_tac n m)
1.409 +  apply(rule_tac x = "m - n*k" in exI)
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.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.421 +  apply(clarsimp)
1.422 +  apply(rename_tac n m)
1.423 +  apply(erule_tac x = "m + n*k" in allE)
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.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.474 +apply(clarsimp)
1.475 +apply(rename_tac n m)
1.476 +apply(rule_tac x = "m + n*k" in exI)
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.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.489 +apply(clarsimp)
1.490 +apply(rename_tac n m)
1.491 +apply(erule_tac x = "m - n*k" in allE)
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.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.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.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.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.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
```