cleaned up
authornipkow
Tue Aug 05 17:57:39 2003 +0200 (2003-08-05)
changeset 14139ca3dd7ed5ac5
parent 14138 ca5029d391d1
child 14140 ca089b9d13c4
cleaned up
src/HOL/Integ/Presburger.thy
src/HOL/Integ/cooper_proof.ML
src/HOL/Presburger.thy
src/HOL/Tools/Presburger/cooper_proof.ML
     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)))"
     2.1 --- a/src/HOL/Integ/cooper_proof.ML	Thu Jul 31 14:01:04 2003 +0200
     2.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Aug 05 17:57:39 2003 +0200
     2.3 @@ -108,10 +108,6 @@
     2.4  val modd_pinf_disjI = thm "modd_pinf_disjI";
     2.5  val modd_pinf_conjI = thm "modd_pinf_conjI";
     2.6  
     2.7 -(*A/B - set Theorem *)
     2.8 -
     2.9 -val bst_thm = thm "bst_thm";
    2.10 -val ast_thm = thm "ast_thm";
    2.11  
    2.12  (*Cooper Backwards...*)
    2.13  (*Bset*)
    2.14 @@ -684,8 +680,7 @@
    2.15    (*"ss" like simplification with simpset*)
    2.16    "ss" =>
    2.17      let
    2.18 -      val ss = presburger_ss addsimps
    2.19 -        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
    2.20 +      val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0]
    2.21        val ct =  cert_Trueprop sg fm2
    2.22      in 
    2.23        simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
    2.24 @@ -1096,37 +1091,6 @@
    2.25  				 
    2.26  
    2.27  
    2.28 -
    2.29 -(* ------------------------------------------------------------------------- *)
    2.30 -(* Here we generate the theorem for the Bset Property in the simple direction*)
    2.31 -(* It is just an instantiation*)
    2.32 -(* ------------------------------------------------------------------------- *)
    2.33 -fun bsetproof_of sg (Bset(x as Free(xn,xT),fm,bs,dlcm))   = 
    2.34 -  let
    2.35 -    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
    2.36 -    val cdlcm = cterm_of sg dlcm
    2.37 -    val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
    2.38 -  in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
    2.39 -    end;
    2.40 -
    2.41 -
    2.42 -
    2.43 -
    2.44 -(* ------------------------------------------------------------------------- *)
    2.45 -(* Here we generate the theorem for the Bset Property in the simple direction*)
    2.46 -(* It is just an instantiation*)
    2.47 -(* ------------------------------------------------------------------------- *)
    2.48 -fun asetproof_of sg (Aset(x as Free(xn,xT),fm,ast,dlcm))   = 
    2.49 -  let
    2.50 -    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
    2.51 -    val cdlcm = cterm_of sg dlcm
    2.52 -    val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
    2.53 -  in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
    2.54 -end;
    2.55 -
    2.56 -
    2.57 -
    2.58 -
    2.59  (* ------------------------------------------------------------------------- *)    
    2.60  (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
    2.61  
    2.62 @@ -1324,13 +1288,12 @@
    2.63  
    2.64  fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
    2.65    (* Get the Bset thm*)
    2.66 -  let val bst = bsetproof_of sg bsprt
    2.67 -      val (mit1,mit2) = minf_proof_of sg dlcm miprt
    2.68 +  let val (mit1,mit2) = minf_proof_of sg dlcm miprt
    2.69        val fm1 = norm_zero_one (simpl fm) 
    2.70        val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
    2.71        val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
    2.72      (* Return the four theorems needed to proove the whole Cooper Theorem*)
    2.73 -  in (dpos,mit2,bst,nbstpthm,mit1)
    2.74 +  in (dpos,mit2,nbstpthm,mit1)
    2.75  end;
    2.76  
    2.77  
    2.78 @@ -1340,12 +1303,11 @@
    2.79  
    2.80  
    2.81  fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
    2.82 -  let val ast = asetproof_of sg bsprt
    2.83 -      val (mit1,mit2) = pinf_proof_of sg dlcm miprt
    2.84 +  let val (mit1,mit2) = pinf_proof_of sg dlcm miprt
    2.85        val fm1 = norm_zero_one (simpl fm) 
    2.86        val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
    2.87        val nastpthm = not_ast_p_proof_of sg nast_p_prt
    2.88 -  in (dpos,mit2,ast,nastpthm,mit1)
    2.89 +  in (dpos,mit2,nastpthm,mit1)
    2.90  end;
    2.91  
    2.92  
    2.93 @@ -1357,12 +1319,12 @@
    2.94  
    2.95  fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
    2.96    "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
    2.97 -	      val (dpsthm,th1,th2,nbpth,th3) = cooperpi_proof_of sg x prt
    2.98 -		   in [dpsthm,th1,th2,nbpth,th3] MRS (cppi_eq)
    2.99 +	      val (dpsthm,th1,nbpth,th3) = cooperpi_proof_of sg x prt
   2.100 +		   in [dpsthm,th1,nbpth,th3] MRS (cppi_eq)
   2.101             end
   2.102    |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
   2.103 -	       val (dpsthm,th1,th2,nbpth,th3) = coopermi_proof_of sg x prt
   2.104 -		   in [dpsthm,th1,th2,nbpth,th3] MRS (cpmi_eq)
   2.105 +	       val (dpsthm,th1,nbpth,th3) = coopermi_proof_of sg x prt
   2.106 +		   in [dpsthm,th1,nbpth,th3] MRS (cpmi_eq)
   2.107                  end
   2.108   |_ => error "parameter error";
   2.109  
     3.1 --- a/src/HOL/Presburger.thy	Thu Jul 31 14:01:04 2003 +0200
     3.2 +++ b/src/HOL/Presburger.thy	Tue Aug 05 17:57:39 2003 +0200
     3.3 @@ -207,16 +207,7 @@
     3.4  ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
     3.5  by blast
     3.6  (*=============================================================================*)
     3.7 -(*The Theorem for the second proof step- about bset. it is trivial too. *)
     3.8 -lemma bst_thm: " (EX (j::int) : {1..d}. EX (b::int) : B. P (b+j) )--> (EX x::int. P (x)) "
     3.9 -by blast
    3.10  
    3.11 -(*The Theorem for the second proof step- about aset. it is trivial too. *)
    3.12 -lemma ast_thm: " (EX (j::int) : {1..d}. EX (a::int) : A. P (a - j) )--> (EX x::int. P (x)) "
    3.13 -by blast
    3.14 -
    3.15 -
    3.16 -(*=============================================================================*)
    3.17  (*This is the first direction of cooper's theorem*)
    3.18  lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
    3.19  by blast
    3.20 @@ -738,7 +729,6 @@
    3.21  qed
    3.22  
    3.23  lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
    3.24 -==> (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)) --> (EX (x::int). P x) 
    3.25  ==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
    3.26  ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
    3.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)))"
    3.28 @@ -762,7 +752,6 @@
    3.29  
    3.30  (* Cooper Thm `, plus infinity version*)
    3.31  lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
    3.32 -==> (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)) --> (EX (x::int). P x) 
    3.33  ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
    3.34  ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
    3.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)))"
     4.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Thu Jul 31 14:01:04 2003 +0200
     4.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Aug 05 17:57:39 2003 +0200
     4.3 @@ -108,10 +108,6 @@
     4.4  val modd_pinf_disjI = thm "modd_pinf_disjI";
     4.5  val modd_pinf_conjI = thm "modd_pinf_conjI";
     4.6  
     4.7 -(*A/B - set Theorem *)
     4.8 -
     4.9 -val bst_thm = thm "bst_thm";
    4.10 -val ast_thm = thm "ast_thm";
    4.11  
    4.12  (*Cooper Backwards...*)
    4.13  (*Bset*)
    4.14 @@ -684,8 +680,7 @@
    4.15    (*"ss" like simplification with simpset*)
    4.16    "ss" =>
    4.17      let
    4.18 -      val ss = presburger_ss addsimps
    4.19 -        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
    4.20 +      val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0]
    4.21        val ct =  cert_Trueprop sg fm2
    4.22      in 
    4.23        simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
    4.24 @@ -1096,37 +1091,6 @@
    4.25  				 
    4.26  
    4.27  
    4.28 -
    4.29 -(* ------------------------------------------------------------------------- *)
    4.30 -(* Here we generate the theorem for the Bset Property in the simple direction*)
    4.31 -(* It is just an instantiation*)
    4.32 -(* ------------------------------------------------------------------------- *)
    4.33 -fun bsetproof_of sg (Bset(x as Free(xn,xT),fm,bs,dlcm))   = 
    4.34 -  let
    4.35 -    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
    4.36 -    val cdlcm = cterm_of sg dlcm
    4.37 -    val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
    4.38 -  in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
    4.39 -    end;
    4.40 -
    4.41 -
    4.42 -
    4.43 -
    4.44 -(* ------------------------------------------------------------------------- *)
    4.45 -(* Here we generate the theorem for the Bset Property in the simple direction*)
    4.46 -(* It is just an instantiation*)
    4.47 -(* ------------------------------------------------------------------------- *)
    4.48 -fun asetproof_of sg (Aset(x as Free(xn,xT),fm,ast,dlcm))   = 
    4.49 -  let
    4.50 -    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
    4.51 -    val cdlcm = cterm_of sg dlcm
    4.52 -    val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
    4.53 -  in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
    4.54 -end;
    4.55 -
    4.56 -
    4.57 -
    4.58 -
    4.59  (* ------------------------------------------------------------------------- *)    
    4.60  (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
    4.61  
    4.62 @@ -1324,13 +1288,12 @@
    4.63  
    4.64  fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
    4.65    (* Get the Bset thm*)
    4.66 -  let val bst = bsetproof_of sg bsprt
    4.67 -      val (mit1,mit2) = minf_proof_of sg dlcm miprt
    4.68 +  let val (mit1,mit2) = minf_proof_of sg dlcm miprt
    4.69        val fm1 = norm_zero_one (simpl fm) 
    4.70        val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
    4.71        val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
    4.72      (* Return the four theorems needed to proove the whole Cooper Theorem*)
    4.73 -  in (dpos,mit2,bst,nbstpthm,mit1)
    4.74 +  in (dpos,mit2,nbstpthm,mit1)
    4.75  end;
    4.76  
    4.77  
    4.78 @@ -1340,12 +1303,11 @@
    4.79  
    4.80  
    4.81  fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
    4.82 -  let val ast = asetproof_of sg bsprt
    4.83 -      val (mit1,mit2) = pinf_proof_of sg dlcm miprt
    4.84 +  let val (mit1,mit2) = pinf_proof_of sg dlcm miprt
    4.85        val fm1 = norm_zero_one (simpl fm) 
    4.86        val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
    4.87        val nastpthm = not_ast_p_proof_of sg nast_p_prt
    4.88 -  in (dpos,mit2,ast,nastpthm,mit1)
    4.89 +  in (dpos,mit2,nastpthm,mit1)
    4.90  end;
    4.91  
    4.92  
    4.93 @@ -1357,12 +1319,12 @@
    4.94  
    4.95  fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
    4.96    "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
    4.97 -	      val (dpsthm,th1,th2,nbpth,th3) = cooperpi_proof_of sg x prt
    4.98 -		   in [dpsthm,th1,th2,nbpth,th3] MRS (cppi_eq)
    4.99 +	      val (dpsthm,th1,nbpth,th3) = cooperpi_proof_of sg x prt
   4.100 +		   in [dpsthm,th1,nbpth,th3] MRS (cppi_eq)
   4.101             end
   4.102    |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
   4.103 -	       val (dpsthm,th1,th2,nbpth,th3) = coopermi_proof_of sg x prt
   4.104 -		   in [dpsthm,th1,th2,nbpth,th3] MRS (cpmi_eq)
   4.105 +	       val (dpsthm,th1,nbpth,th3) = coopermi_proof_of sg x prt
   4.106 +		   in [dpsthm,th1,nbpth,th3] MRS (cpmi_eq)
   4.107                  end
   4.108   |_ => error "parameter error";
   4.109