src/HOL/Presburger.thy

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

(*  Title:      HOL/Integ/Presburger.thy
    ID:         $Id$
    Author:     Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

File containing necessary theorems for the proof
generation for Cooper Algorithm  
*)

header {* Presburger Arithmetic: Cooper Algorithm *}

theory Presburger = NatSimprocs + SetInterval
files
  ("cooper_dec.ML")
  ("cooper_proof.ML")
  ("qelim.ML")
  ("presburger.ML"):

text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}

theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
  apply (rule iffI)
  apply (erule exE)
  apply (rule_tac x = "l * x" in exI)
  apply simp
  apply (erule exE)
  apply (erule conjE)
  apply (erule dvdE)
  apply (rule_tac x = k in exI)
  apply simp
  done

lemma uminus_dvd_conv: "(d dvd (t::int)) = (-d dvd t)"
apply(unfold dvd_def)
apply(rule iffI)
apply(clarsimp)
apply(rename_tac k)
apply(rule_tac x = "-k" in exI)
apply simp
apply(clarsimp)
apply(rename_tac k)
apply(rule_tac x = "-k" in exI)
apply simp
done

lemma uminus_dvd_conv': "(d dvd (t::int)) = (d dvd -t)"
apply(unfold dvd_def)
apply(rule iffI)
apply(clarsimp)
apply(rule_tac x = "-k" in exI)
apply simp
apply(clarsimp)
apply(rule_tac x = "-k" in exI)
apply simp
done



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}.*}

theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
  \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
  \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
  apply (erule exE)+
  apply (rule_tac x = "min z1 z2" in exI)
  apply simp
  done


theorem eq_minf_disjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
  \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
  \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))"

  apply (erule exE)+
  apply (rule_tac x = "min z1 z2" in exI)
  apply simp
  done


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}.*}

theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
  \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
  \<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))"
  apply (erule exE)+
  apply (rule_tac x = "max z1 z2" in exI)
  apply simp
  done


theorem eq_pinf_disjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
  \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
  \<exists>z::int. \<forall>x. z < x  \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))"
  apply (erule exE)+
  apply (rule_tac x = "max z1 z2" in exI)
  apply simp
  done

text {*
  \medskip Theorems for the combination of proofs of the modulo @{text
  D} property for @{text "P plusinfinity"}

  FIXME: This is THE SAME theorem as for the @{text minusinf} version,
  but with @{text "+k.."} instead of @{text "-k.."} In the future
  replace these both with only one. *}

theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
  \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
  \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
  by simp

theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
  \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
  \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
  by simp

text {*
  This is one of the cases where the simplifed formula is prooved to
  habe some property (in relation to @{text P_m}) but we need to prove
  the property for the original formula (@{text P_m})

  FIXME: This is exaclty the same thm as for @{text minusinf}. *}

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)) "
  by blast


text {*
  \medskip Theorems for the combination of proofs of the modulo @{text D}
  property for @{text "P minusinfinity"} *}

theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
  \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
  \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
  by simp

theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
  \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
  \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
  by simp

text {*
  This is one of the cases where the simplifed formula is prooved to
  have some property (in relation to @{text P_m}) but we need to
  prove the property for the original formula (@{text P_m}). *}

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)) "
  by blast

text {*
  Theorem needed for proving at runtime divide properties using the
  arithmetic tactic (which knows only about modulo = 0). *}

lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
  by(simp add:dvd_def zmod_eq_0_iff)

text {*
  \medskip Theorems used for the combination of proof for the
  backwards direction of Cooper's Theorem. They rely exclusively on
  Predicate calculus.*}

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))
==>
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
==>
(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))) "
  by blast


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))
==>
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
==>
(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)
\<and> P2(x + d))) "
  by blast

lemma not_ast_p_Q_elim: "
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
==> ( P = Q )
==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
  by blast

text {*
  \medskip Theorems used for the combination of proof for the
  backwards direction of Cooper's Theorem. They rely exclusively on
  Predicate calculus.*}

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))
==>
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d))
==>
(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)
\<or> P2(x-d))) "
  by blast

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))
==>
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d))
==>
(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)
\<and> P2(x-d))) "
  by blast

lemma not_bst_p_Q_elim: "
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) 
==> ( P = Q )
==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
  by blast

text {* \medskip This is the first direction of Cooper's Theorem. *}
lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
  by blast

text {*
  \medskip The full Cooper's Theorem in its equivalence Form. Given
  the premises it is trivial too, it relies exclusively on prediacte calculus.*}
lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
--> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
  by blast

text {*
  \medskip Some of the atomic theorems generated each time the atom
  does not depend on @{text x}, they are trivial.*}

lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
  by blast

lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
  by blast

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"
  by blast

lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
  by blast

text {* The next two thms are the same as the @{text minusinf} version. *}

lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
  by blast

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"
  by blast

text {* Theorems to be deleted from simpset when proving simplified formulaes. *}

lemma P_eqtrue: "(P=True) = P"
  by rules

lemma P_eqfalse: "(P=False) = (~P)"
  by rules

text {*
  \medskip Theorems for the generation of the bachwards direction of
  Cooper's Theorem.

  These are the 6 interesting atomic cases which have to be proved relying on the
  properties of B-set and the arithmetic and contradiction proofs. *}

lemma not_bst_p_lt: "0 < (d::int) ==>
 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 )"
  by arith

lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
 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)"
apply clarsimp
apply(rule ccontr)
apply(drule_tac x = "x+a" in bspec)
apply(simp add:atLeastAtMost_iff)
apply(drule_tac x = "-a" in bspec)
apply assumption
apply(simp)
done

lemma not_bst_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a - 1 \<rbrakk> \<Longrightarrow>
 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 )"
apply clarsimp
apply(subgoal_tac "x = -a")
 prefer 2 apply arith
apply(drule_tac x = "1" in bspec)
apply(simp add:atLeastAtMost_iff)
apply(drule_tac x = "-a- 1" in bspec)
apply assumption
apply(simp)
done


lemma not_bst_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
 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)"
apply clarsimp
apply(subgoal_tac "x = -a+d")
 prefer 2 apply arith
apply(drule_tac x = "d" in bspec)
apply(simp add:atLeastAtMost_iff)
apply(drule_tac x = "-a" in bspec)
apply assumption
apply(simp)
done


lemma not_bst_p_dvd: "(d1::int) dvd d ==>
 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 )"
apply(clarsimp simp add:dvd_def)
apply(rename_tac m)
apply(rule_tac x = "m - k" in exI)
apply(simp add:int_distrib)
done

lemma not_bst_p_ndvd: "(d1::int) dvd d ==>
 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 ))"
apply(clarsimp simp add:dvd_def)
apply(rename_tac m)
apply(erule_tac x = "m + k" in allE)
apply(simp add:int_distrib)
done

text {*
  \medskip Theorems for the generation of the bachwards direction of
  Cooper's Theorem.

  These are the 6 interesting atomic cases which have to be proved
  relying on the properties of A-set ant the arithmetic and
  contradiction proofs. *}

lemma not_ast_p_gt: "0 < (d::int) ==>
 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 )"
  by arith

lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
 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)"
  apply clarsimp
  apply (rule ccontr)
  apply (drule_tac x = "t-x" in bspec)
  apply simp
  apply (drule_tac x = "t" in bspec)
  apply assumption
  apply simp
  done

lemma not_ast_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t + 1 \<rbrakk> \<Longrightarrow>
 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 )"
  apply clarsimp
  apply (drule_tac x="1" in bspec)
  apply simp
  apply (drule_tac x="- t + 1" in bspec)
  apply assumption
  apply(subgoal_tac "x = -t")
  prefer 2 apply arith
  apply simp
  done

lemma not_ast_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t \<rbrakk> \<Longrightarrow>
 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)"
  apply clarsimp
  apply (subgoal_tac "x = -t-d")
  prefer 2 apply arith
  apply (drule_tac x = "d" in bspec)
  apply simp
  apply (drule_tac x = "-t" in bspec)
  apply assumption
  apply simp
  done

lemma not_ast_p_dvd: "(d1::int) dvd d ==>
 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 )"
  apply(clarsimp simp add:dvd_def)
  apply(rename_tac m)
  apply(rule_tac x = "m + k" in exI)
  apply(simp add:int_distrib)
  done

lemma not_ast_p_ndvd: "(d1::int) dvd d ==>
 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 ))"
  apply(clarsimp simp add:dvd_def)
  apply(rename_tac m)
  apply(erule_tac x = "m - k" in allE)
  apply(simp add:int_distrib)
  done

text {*
  \medskip These are the atomic cases for the proof generation for the
  modulo @{text D} property for @{text "P plusinfinity"}

  They are fully based on arithmetics. *}

lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
 (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
  apply(clarsimp simp add:dvd_def)
  apply(rule iffI)
  apply(clarsimp)
  apply(rename_tac n m)
  apply(rule_tac x = "m + n*k" in exI)
  apply(simp add:int_distrib)
  apply(clarsimp)
  apply(rename_tac n m)
  apply(rule_tac x = "m - n*k" in exI)
  apply(simp add:int_distrib mult_ac)
  done

lemma  not_dvd_modd_pinf: "((d::int) dvd d1) ==>
 (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x+k*d1 + t))))"
  apply(clarsimp simp add:dvd_def)
  apply(rule iffI)
  apply(clarsimp)
  apply(rename_tac n m)
  apply(erule_tac x = "m - n*k" in allE)
  apply(simp add:int_distrib mult_ac)
  apply(clarsimp)
  apply(rename_tac n m)
  apply(erule_tac x = "m + n*k" in allE)
  apply(simp add:int_distrib mult_ac)
  done

text {*
  \medskip These are the atomic cases for the proof generation for the
  equivalence of @{text P} and @{text "P plusinfinity"} for integers
  @{text x} greater than some integer @{text z}.

  They are fully based on arithmetics. *}

lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
  apply(rule_tac x = "-t" in exI)
  apply simp
  done

lemma  neq_eq_pinf: "EX z::int. ALL x.  z < x --> ((~( 0 = x +t )) = True )"
  apply(rule_tac x = "-t" in exI)
  apply simp
  done

lemma  le_eq_pinf: "EX z::int. ALL x.  z < x --> ( 0 < x +t  = True )"
  apply(rule_tac x = "-t" in exI)
  apply simp
  done

lemma  len_eq_pinf: "EX z::int. ALL x. z < x  --> (0 < -x +t  = False )"
  apply(rule_tac x = "t" in exI)
  apply simp
  done

lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
  by simp

lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
  by simp

text {*
  \medskip These are the atomic cases for the proof generation for the
  modulo @{text D} property for @{text "P minusinfinity"}.

  They are fully based on arithmetics. *}

lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
 (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
apply(clarsimp simp add:dvd_def)
apply(rule iffI)
apply(clarsimp)
apply(rename_tac n m)
apply(rule_tac x = "m - n*k" in exI)
apply(simp add:int_distrib)
apply(clarsimp)
apply(rename_tac n m)
apply(rule_tac x = "m + n*k" in exI)
apply(simp add:int_distrib mult_ac)
done


lemma  not_dvd_modd_minf: "((d::int) dvd d1) ==>
 (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x-k*d1 + t))))"
apply(clarsimp simp add:dvd_def)
apply(rule iffI)
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m + n*k" in allE)
apply(simp add:int_distrib mult_ac)
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m - n*k" in allE)
apply(simp add:int_distrib mult_ac)
done

text {*
  \medskip These are the atomic cases for the proof generation for the
  equivalence of @{text P} and @{text "P minusinfinity"} for integers
  @{text x} less than some integer @{text z}.

  They are fully based on arithmetics. *}

lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
apply(rule_tac x = "-t" in exI)
apply simp
done

lemma  neq_eq_minf: "EX z::int. ALL x. x < z --> ((~( 0 = x +t )) = True )"
apply(rule_tac x = "-t" in exI)
apply simp
done

lemma  le_eq_minf: "EX z::int. ALL x. x < z --> ( 0 < x +t  = False )"
apply(rule_tac x = "-t" in exI)
apply simp
done


lemma  len_eq_minf: "EX z::int. ALL x. x < z --> (0 < -x +t  = True )"
apply(rule_tac x = "t" in exI)
apply simp
done

lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
  by simp

lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
  by simp

text {*
  \medskip This Theorem combines whithnesses about @{text "P
  minusinfinity"} to show one component of the equivalence proof for
  Cooper's Theorem.

  FIXME: remove once they are part of the distribution. *}

theorem int_ge_induct[consumes 1,case_names base step]:
  assumes ge: "k \<le> (i::int)" and
        base: "P(k)" and
        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
  shows "P i"
proof -
  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
    proof (induct n)
      case 0
      hence "i = k" by arith
      thus "P i" using base by simp
    next
      case (Suc n)
      hence "n = nat((i - 1) - k)" by arith
      moreover
      have ki1: "k \<le> i - 1" using Suc.prems by arith
      ultimately
      have "P(i - 1)" by(rule Suc.hyps)
      from step[OF ki1 this] show ?case by simp
    qed
  }
  from this ge show ?thesis by fast
qed

theorem int_gr_induct[consumes 1,case_names base step]:
  assumes gr: "k < (i::int)" and
        base: "P(k+1)" and
        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
  shows "P i"
apply(rule int_ge_induct[of "k + 1"])
  using gr apply arith
 apply(rule base)
apply(rule step)
 apply simp+
done

lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
apply(induct rule: int_gr_induct)
 apply simp
 apply arith
apply (simp add:int_distrib)
apply arith
done

lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
apply(induct rule: int_gr_induct)
 apply simp
 apply arith
apply (simp add:int_distrib)
apply arith
done

lemma  minusinfinity:
  assumes "0 < d" and
    P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and
    ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
  shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
proof
  assume eP1: "EX x. P1 x"
  then obtain x where P1: "P1 x" ..
  from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
  let ?w = "x - (abs(x-z)+1) * d"
  show "EX x. P x"
  proof
    have w: "?w < z" by(rule decr_lemma)
    have "P1 x = P1 ?w" using P1eqP1 by blast
    also have "\<dots> = P(?w)" using w P1eqP by blast
    finally show "P ?w" using P1 by blast
  qed
qed

text {*
  \medskip This Theorem combines whithnesses about @{text "P
  minusinfinity"} to show one component of the equivalence proof for
  Cooper's Theorem. *}

lemma plusinfinity:
  assumes "0 < d" and
    P1eqP1: "ALL (x::int) (k::int). P1 x = P1 (x + k * d)" and
    ePeqP1: "EX z::int. ALL x. z < x  --> (P x = P1 x)"
  shows "(EX x::int. P1 x) --> (EX x::int. P x)"
proof
  assume eP1: "EX x. P1 x"
  then obtain x where P1: "P1 x" ..
  from ePeqP1 obtain z where P1eqP: "ALL x. z < x \<longrightarrow> (P x = P1 x)" ..
  let ?w = "x + (abs(x-z)+1) * d"
  show "EX x. P x"
  proof
    have w: "z < ?w" by(rule incr_lemma)
    have "P1 x = P1 ?w" using P1eqP1 by blast
    also have "\<dots> = P(?w)" using w P1eqP by blast
    finally show "P ?w" using P1 by blast
  qed
qed
 
text {*
  \medskip Theorem for periodic function on discrete sets. *}

lemma minf_vee:
  assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
  shows "(EX x. P x) = (EX j : {1..d}. P j)"
  (is "?LHS = ?RHS")
proof
  assume ?LHS
  then obtain x where P: "P x" ..
  have "x mod d = x - (x div d)*d"
    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
  hence Pmod: "P x = P(x mod d)" using modd by simp
  show ?RHS
  proof (cases)
    assume "x mod d = 0"
    hence "P 0" using P Pmod by simp
    moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
    ultimately have "P d" by simp
    moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
    ultimately show ?RHS ..
  next
    assume not0: "x mod d \<noteq> 0"
    have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
    moreover have "x mod d : {1..d}"
    proof -
      have "0 \<le> x mod d" by(rule pos_mod_sign)
      moreover have "x mod d < d" by(rule pos_mod_bound)
      ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
    qed
    ultimately show ?RHS ..
  qed
next
  assume ?RHS thus ?LHS by blast
qed

text {*
  \medskip Theorem for periodic function on discrete sets. *}

lemma pinf_vee:
  assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
  shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
  (is "?LHS = ?RHS")
proof
  assume ?LHS
  then obtain x where P: "P x" ..
  have "x mod d = x + (-(x div d))*d"
    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
  hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
  show ?RHS
  proof (cases)
    assume "x mod d = 0"
    hence "P 0" using P Pmod by simp
    moreover have "P 0 = P(0 + 1*d)" using modd by blast
    ultimately have "P d" by simp
    moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
    ultimately show ?RHS ..
  next
    assume not0: "x mod d \<noteq> 0"
    have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
    moreover have "x mod d : {1..d}"
    proof -
      have "0 \<le> x mod d" by(rule pos_mod_sign)
      moreover have "x mod d < d" by(rule pos_mod_bound)
      ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
    qed
    ultimately show ?RHS ..
  qed
next
  assume ?RHS thus ?LHS by blast
qed

lemma decr_mult_lemma:
  assumes dpos: "(0::int) < d" and
          minus: "ALL x::int. P x \<longrightarrow> P(x - d)" and
          knneg: "0 <= k"
  shows "ALL x. P x \<longrightarrow> P(x - k*d)"
using knneg
proof (induct rule:int_ge_induct)
  case base thus ?case by simp
next
  case (step i)
  show ?case
  proof
    fix x
    have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
    also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
      using minus[THEN spec, of "x - i * d"]
      by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric])
    ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
  qed
qed

lemma incr_mult_lemma:
  assumes dpos: "(0::int) < d" and
          plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and
          knneg: "0 <= k"
  shows "ALL x. P x \<longrightarrow> P(x + k*d)"
using knneg
proof (induct rule:int_ge_induct)
  case base thus ?case by simp
next
  case (step i)
  show ?case
  proof
    fix x
    have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
    also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)"
      using plus[THEN spec, of "x + i * d"]
      by (simp add:int_distrib zadd_ac)
    ultimately show "P x \<longrightarrow> P(x + (i + 1) * d)" by blast
  qed
qed

lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
apply(rule iffI)
prefer 2
apply(drule minusinfinity)
apply assumption+
apply(fastsimp)
apply clarsimp
apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
apply(frule_tac x = x and z=z in decr_lemma)
apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
prefer 2
apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
prefer 2 apply arith
 apply fastsimp
apply(drule (1) minf_vee)
apply blast
apply(blast dest:decr_mult_lemma)
done

text {* Cooper Theorem, plus infinity version. *}
lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)))"
  apply(rule iffI)
  prefer 2
  apply(drule plusinfinity)
  apply assumption+
  apply(fastsimp)
  apply clarsimp
  apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x + k*D)")
  apply(frule_tac x = x and z=z in incr_lemma)
  apply(subgoal_tac "P1(x + (\<bar>x - z\<bar> + 1) * D)")
  prefer 2
  apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
  prefer 2 apply arith
  apply fastsimp
  apply(drule (1) pinf_vee)
  apply blast
  apply(blast dest:incr_mult_lemma)
  done


text {*
  \bigskip Theorems for the quantifier elminination Functions. *}

lemma qe_ex_conj: "(EX (x::int). A x) = R
		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
		==> (EX (x::int). P x) = (Q & R)"
by blast

lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q)
		==> (EX (x::int). P x) = Q"
by blast

lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)"
by blast

lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)"
by blast

lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)"
by blast

lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)"
by blast

lemma qe_Not: "P = Q ==> (~P) = (~Q)"
by blast

lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
by blast

text {* \bigskip Theorems for proving NNF *}

lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
by blast

lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))"
by blast

lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)"
  by blast
lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))"
by blast

lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))"
by blast
lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))"
by blast
lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))"
by blast
lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))"
by blast


lemma qe_exI2: "A = B ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
  by simp

lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
  by rules

lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
  by rules

lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
by blast

lemma cppi_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j)))
==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) "
by blast


lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
apply(fastsimp)
done

text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}

lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
proof
  assume ?P
  thus ?Q
    apply(simp add:dvd_def)
    apply clarify
    apply(rename_tac d)
    apply(drule_tac f = "op * k" in arg_cong)
    apply(simp only:int_distrib)
    apply(rule_tac x = "d" in exI)
    apply(simp only:mult_ac)
    done
next
  assume ?Q
  then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
  hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
  hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
  hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
  thus ?P by(simp add:dvd_def)
qed

lemma ac_lt_eq: assumes gr0: "0 < (k::int)"
shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
proof
  assume P: ?P
  show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
next
  assume ?Q
  hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
  with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
  thus ?P by(simp)
qed

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")
proof
  assume ?P
  thus ?Q
    apply(drule_tac f = "op * k" in arg_cong)
    apply(simp only:int_distrib)
    done
next
  assume ?Q
  hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
  hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
  thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
qed

lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
proof -
  have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
  also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
  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])
  also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
  finally show ?thesis .
qed

lemma binminus_uminus_conv: "(a::int) - b = a + (-b)"
by arith

lemma  linearize_dvd: "(t::int) = t1 ==> (d dvd t) = (d dvd t1)"
by simp

lemma lf_lt: "(l::int) = ll ==> (r::int) = lr ==> (l < r) =(ll < lr)"
by simp

lemma lf_eq: "(l::int) = ll ==> (r::int) = lr ==> (l = r) =(ll = lr)"
by simp

lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
by simp

text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}

theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
  by (simp split add: split_nat)

theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
  apply (simp split add: split_nat)
  apply (rule iffI)
  apply (erule exE)
  apply (rule_tac x = "int x" in exI)
  apply simp
  apply (erule exE)
  apply (rule_tac x = "nat x" in exI)
  apply (erule conjE)
  apply (erule_tac x = "nat x" in allE)
  apply simp
  done

theorem zdiff_int_split: "P (int (x - y)) =
  ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
  apply (case_tac "y \<le> x")
  apply (simp_all add: zdiff_int)
  done

theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
    nat_0_le cong add: conj_cong)
  apply (rule iffI)
  apply rules
  apply (erule exE)
  apply (case_tac "x=0")
  apply (rule_tac x=0 in exI)
  apply simp
  apply (case_tac "0 \<le> k")
  apply rules
  apply (simp add: linorder_not_le)
  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
  apply assumption
  apply (simp add: mult_ac)
  done

theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
  by simp

theorem number_of2: "(0::int) <= number_of bin.Pls" by simp

theorem Suc_plus1: "Suc n = n + 1" by simp

text {*
  \medskip Specific instances of congruence rules, to prevent
  simplifier from looping. *}

theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
  by simp

theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
  by (simp cong: conj_cong)

use "cooper_dec.ML"
use "cooper_proof.ML"
use "qelim.ML"
use "presburger.ML"

setup "Presburger.setup"

end