author nipkow Tue Aug 05 17:57:39 2003 +0200 (2003-08-05) changeset 14139 ca3dd7ed5ac5 parent 14138 ca5029d391d1 child 14140 ca089b9d13c4
cleaned up
 src/HOL/Integ/Presburger.thy file | annotate | diff | revisions src/HOL/Integ/cooper_proof.ML file | annotate | diff | revisions src/HOL/Presburger.thy file | annotate | diff | revisions src/HOL/Tools/Presburger/cooper_proof.ML file | annotate | diff | revisions
```     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
```