# HG changeset patch
# User nipkow
# Date 1060099059 -7200
# Node ID ca3dd7ed5ac52806488332c7dec26c7e0cae9302
# Parent  ca5029d391d1e7632fe0bfbd16fcc35b15dc884f
cleaned up

diff -r ca5029d391d1 -r ca3dd7ed5ac5 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Thu Jul 31 14:01:04 2003 +0200
+++ b/src/HOL/Integ/Presburger.thy	Tue Aug 05 17:57:39 2003 +0200
@@ -207,16 +207,7 @@
 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
 by blast
 (*=============================================================================*)
-(*The Theorem for the second proof step- about bset. it is trivial too. *)
-lemma bst_thm: " (EX (j::int) : {1..d}. EX (b::int) : B. P (b+j) )--> (EX x::int. P (x)) "
-by blast
 
-(*The Theorem for the second proof step- about aset. it is trivial too. *)
-lemma ast_thm: " (EX (j::int) : {1..d}. EX (a::int) : A. P (a - j) )--> (EX x::int. P (x)) "
-by blast
-
-
-(*=============================================================================*)
 (*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
@@ -738,7 +729,6 @@
 qed
 
 lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
-==> (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)) --> (EX (x::int). P 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)))"
@@ -762,7 +752,6 @@
 
 (* Cooper Thm `, plus infinity version*)
 lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
-==> (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)) --> (EX (x::int). P 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)))"
diff -r ca5029d391d1 -r ca3dd7ed5ac5 src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Thu Jul 31 14:01:04 2003 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Tue Aug 05 17:57:39 2003 +0200
@@ -108,10 +108,6 @@
 val modd_pinf_disjI = thm "modd_pinf_disjI";
 val modd_pinf_conjI = thm "modd_pinf_conjI";
 
-(*A/B - set Theorem *)
-
-val bst_thm = thm "bst_thm";
-val ast_thm = thm "ast_thm";
 
 (*Cooper Backwards...*)
 (*Bset*)
@@ -684,8 +680,7 @@
   (*"ss" like simplification with simpset*)
   "ss" =>
     let
-      val ss = presburger_ss addsimps
-        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
+      val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0]
       val ct =  cert_Trueprop sg fm2
     in 
       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
@@ -1096,37 +1091,6 @@
 				 
 
 
-
-(* ------------------------------------------------------------------------- *)
-(* Here we generate the theorem for the Bset Property in the simple direction*)
-(* It is just an instantiation*)
-(* ------------------------------------------------------------------------- *)
-fun bsetproof_of sg (Bset(x as Free(xn,xT),fm,bs,dlcm))   = 
-  let
-    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
-    val cdlcm = cterm_of sg dlcm
-    val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
-  in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
-    end;
-
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* Here we generate the theorem for the Bset Property in the simple direction*)
-(* It is just an instantiation*)
-(* ------------------------------------------------------------------------- *)
-fun asetproof_of sg (Aset(x as Free(xn,xT),fm,ast,dlcm))   = 
-  let
-    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
-    val cdlcm = cterm_of sg dlcm
-    val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
-  in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
-end;
-
-
-
-
 (* ------------------------------------------------------------------------- *)    
 (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
 
@@ -1324,13 +1288,12 @@
 
 fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
   (* Get the Bset thm*)
-  let val bst = bsetproof_of sg bsprt
-      val (mit1,mit2) = minf_proof_of sg dlcm miprt
+  let val (mit1,mit2) = minf_proof_of sg dlcm miprt
       val fm1 = norm_zero_one (simpl fm) 
       val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
       val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
     (* Return the four theorems needed to proove the whole Cooper Theorem*)
-  in (dpos,mit2,bst,nbstpthm,mit1)
+  in (dpos,mit2,nbstpthm,mit1)
 end;
 
 
@@ -1340,12 +1303,11 @@
 
 
 fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
-  let val ast = asetproof_of sg bsprt
-      val (mit1,mit2) = pinf_proof_of sg dlcm miprt
+  let val (mit1,mit2) = pinf_proof_of sg dlcm miprt
       val fm1 = norm_zero_one (simpl fm) 
       val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
       val nastpthm = not_ast_p_proof_of sg nast_p_prt
-  in (dpos,mit2,ast,nastpthm,mit1)
+  in (dpos,mit2,nastpthm,mit1)
 end;
 
 
@@ -1357,12 +1319,12 @@
 
 fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
   "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
-	      val (dpsthm,th1,th2,nbpth,th3) = cooperpi_proof_of sg x prt
-		   in [dpsthm,th1,th2,nbpth,th3] MRS (cppi_eq)
+	      val (dpsthm,th1,nbpth,th3) = cooperpi_proof_of sg x prt
+		   in [dpsthm,th1,nbpth,th3] MRS (cppi_eq)
            end
   |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
-	       val (dpsthm,th1,th2,nbpth,th3) = coopermi_proof_of sg x prt
-		   in [dpsthm,th1,th2,nbpth,th3] MRS (cpmi_eq)
+	       val (dpsthm,th1,nbpth,th3) = coopermi_proof_of sg x prt
+		   in [dpsthm,th1,nbpth,th3] MRS (cpmi_eq)
                 end
  |_ => error "parameter error";
 
diff -r ca5029d391d1 -r ca3dd7ed5ac5 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Jul 31 14:01:04 2003 +0200
+++ b/src/HOL/Presburger.thy	Tue Aug 05 17:57:39 2003 +0200
@@ -207,16 +207,7 @@
 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
 by blast
 (*=============================================================================*)
-(*The Theorem for the second proof step- about bset. it is trivial too. *)
-lemma bst_thm: " (EX (j::int) : {1..d}. EX (b::int) : B. P (b+j) )--> (EX x::int. P (x)) "
-by blast
 
-(*The Theorem for the second proof step- about aset. it is trivial too. *)
-lemma ast_thm: " (EX (j::int) : {1..d}. EX (a::int) : A. P (a - j) )--> (EX x::int. P (x)) "
-by blast
-
-
-(*=============================================================================*)
 (*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
@@ -738,7 +729,6 @@
 qed
 
 lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
-==> (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)) --> (EX (x::int). P 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)))"
@@ -762,7 +752,6 @@
 
 (* Cooper Thm `, plus infinity version*)
 lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
-==> (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)) --> (EX (x::int). P 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)))"
diff -r ca5029d391d1 -r ca3dd7ed5ac5 src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Thu Jul 31 14:01:04 2003 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Aug 05 17:57:39 2003 +0200
@@ -108,10 +108,6 @@
 val modd_pinf_disjI = thm "modd_pinf_disjI";
 val modd_pinf_conjI = thm "modd_pinf_conjI";
 
-(*A/B - set Theorem *)
-
-val bst_thm = thm "bst_thm";
-val ast_thm = thm "ast_thm";
 
 (*Cooper Backwards...*)
 (*Bset*)
@@ -684,8 +680,7 @@
   (*"ss" like simplification with simpset*)
   "ss" =>
     let
-      val ss = presburger_ss addsimps
-        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
+      val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0]
       val ct =  cert_Trueprop sg fm2
     in 
       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
@@ -1096,37 +1091,6 @@
 				 
 
 
-
-(* ------------------------------------------------------------------------- *)
-(* Here we generate the theorem for the Bset Property in the simple direction*)
-(* It is just an instantiation*)
-(* ------------------------------------------------------------------------- *)
-fun bsetproof_of sg (Bset(x as Free(xn,xT),fm,bs,dlcm))   = 
-  let
-    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
-    val cdlcm = cterm_of sg dlcm
-    val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
-  in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
-    end;
-
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* Here we generate the theorem for the Bset Property in the simple direction*)
-(* It is just an instantiation*)
-(* ------------------------------------------------------------------------- *)
-fun asetproof_of sg (Aset(x as Free(xn,xT),fm,ast,dlcm))   = 
-  let
-    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
-    val cdlcm = cterm_of sg dlcm
-    val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
-  in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
-end;
-
-
-
-
 (* ------------------------------------------------------------------------- *)    
 (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
 
@@ -1324,13 +1288,12 @@
 
 fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
   (* Get the Bset thm*)
-  let val bst = bsetproof_of sg bsprt
-      val (mit1,mit2) = minf_proof_of sg dlcm miprt
+  let val (mit1,mit2) = minf_proof_of sg dlcm miprt
       val fm1 = norm_zero_one (simpl fm) 
       val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
       val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
     (* Return the four theorems needed to proove the whole Cooper Theorem*)
-  in (dpos,mit2,bst,nbstpthm,mit1)
+  in (dpos,mit2,nbstpthm,mit1)
 end;
 
 
@@ -1340,12 +1303,11 @@
 
 
 fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
-  let val ast = asetproof_of sg bsprt
-      val (mit1,mit2) = pinf_proof_of sg dlcm miprt
+  let val (mit1,mit2) = pinf_proof_of sg dlcm miprt
       val fm1 = norm_zero_one (simpl fm) 
       val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
       val nastpthm = not_ast_p_proof_of sg nast_p_prt
-  in (dpos,mit2,ast,nastpthm,mit1)
+  in (dpos,mit2,nastpthm,mit1)
 end;
 
 
@@ -1357,12 +1319,12 @@
 
 fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
   "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
-	      val (dpsthm,th1,th2,nbpth,th3) = cooperpi_proof_of sg x prt
-		   in [dpsthm,th1,th2,nbpth,th3] MRS (cppi_eq)
+	      val (dpsthm,th1,nbpth,th3) = cooperpi_proof_of sg x prt
+		   in [dpsthm,th1,nbpth,th3] MRS (cppi_eq)
            end
   |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
-	       val (dpsthm,th1,th2,nbpth,th3) = coopermi_proof_of sg x prt
-		   in [dpsthm,th1,th2,nbpth,th3] MRS (cpmi_eq)
+	       val (dpsthm,th1,nbpth,th3) = coopermi_proof_of sg x prt
+		   in [dpsthm,th1,nbpth,th3] MRS (cpmi_eq)
                 end
  |_ => error "parameter error";