src/HOL/Integ/Presburger.thy
changeset 14139 ca3dd7ed5ac5
parent 13876 68f4ed8311ac
child 14271 8ed6989228bb
     1.1 --- a/src/HOL/Integ/Presburger.thy	Thu Jul 31 14:01:04 2003 +0200
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Tue Aug 05 17:57:39 2003 +0200
     1.3 @@ -207,16 +207,7 @@
     1.4  ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
     1.5  by blast
     1.6  (*=============================================================================*)
     1.7 -(*The Theorem for the second proof step- about bset. it is trivial too. *)
     1.8 -lemma bst_thm: " (EX (j::int) : {1..d}. EX (b::int) : B. P (b+j) )--> (EX x::int. P (x)) "
     1.9 -by blast
    1.10  
    1.11 -(*The Theorem for the second proof step- about aset. it is trivial too. *)
    1.12 -lemma ast_thm: " (EX (j::int) : {1..d}. EX (a::int) : A. P (a - j) )--> (EX x::int. P (x)) "
    1.13 -by blast
    1.14 -
    1.15 -
    1.16 -(*=============================================================================*)
    1.17  (*This is the first direction of cooper's theorem*)
    1.18  lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
    1.19  by blast
    1.20 @@ -738,7 +729,6 @@
    1.21  qed
    1.22  
    1.23  lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
    1.24 -==> (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)) --> (EX (x::int). P x) 
    1.25  ==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
    1.26  ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
    1.27  ==> (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.28 @@ -762,7 +752,6 @@
    1.29  
    1.30  (* Cooper Thm `, plus infinity version*)
    1.31  lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
    1.32 -==> (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)) --> (EX (x::int). P x) 
    1.33  ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
    1.34  ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
    1.35  ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)))"