src/HOL/Integ/cooper_proof.ML
 changeset 14139 ca3dd7ed5ac5 parent 13905 3e496c70f2f3 child 14259 79f7d3451b1e
```     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Thu Jul 31 14:01:04 2003 +0200
1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Aug 05 17:57:39 2003 +0200
1.3 @@ -108,10 +108,6 @@
1.4  val modd_pinf_disjI = thm "modd_pinf_disjI";
1.5  val modd_pinf_conjI = thm "modd_pinf_conjI";
1.6
1.7 -(*A/B - set Theorem *)
1.8 -
1.9 -val bst_thm = thm "bst_thm";
1.10 -val ast_thm = thm "ast_thm";
1.11
1.12  (*Cooper Backwards...*)
1.13  (*Bset*)
1.14 @@ -684,8 +680,7 @@
1.15    (*"ss" like simplification with simpset*)
1.16    "ss" =>
1.17      let
1.18 -      val ss = presburger_ss addsimps
1.19 -        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
1.20 +      val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0]
1.21        val ct =  cert_Trueprop sg fm2
1.22      in
1.23        simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
1.24 @@ -1096,37 +1091,6 @@
1.25
1.26
1.27
1.28 -
1.29 -(* ------------------------------------------------------------------------- *)
1.30 -(* Here we generate the theorem for the Bset Property in the simple direction*)
1.31 -(* It is just an instantiation*)
1.32 -(* ------------------------------------------------------------------------- *)
1.33 -fun bsetproof_of sg (Bset(x as Free(xn,xT),fm,bs,dlcm))   =
1.34 -  let
1.35 -    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
1.36 -    val cdlcm = cterm_of sg dlcm
1.37 -    val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
1.38 -  in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
1.39 -    end;
1.40 -
1.41 -
1.42 -
1.43 -
1.44 -(* ------------------------------------------------------------------------- *)
1.45 -(* Here we generate the theorem for the Bset Property in the simple direction*)
1.46 -(* It is just an instantiation*)
1.47 -(* ------------------------------------------------------------------------- *)
1.48 -fun asetproof_of sg (Aset(x as Free(xn,xT),fm,ast,dlcm))   =
1.49 -  let
1.50 -    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
1.51 -    val cdlcm = cterm_of sg dlcm
1.52 -    val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
1.53 -  in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
1.54 -end;
1.55 -
1.56 -
1.57 -
1.58 -
1.59  (* ------------------------------------------------------------------------- *)
1.60  (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
1.61
1.62 @@ -1324,13 +1288,12 @@
1.63
1.64  fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
1.65    (* Get the Bset thm*)
1.66 -  let val bst = bsetproof_of sg bsprt
1.67 -      val (mit1,mit2) = minf_proof_of sg dlcm miprt
1.68 +  let val (mit1,mit2) = minf_proof_of sg dlcm miprt
1.69        val fm1 = norm_zero_one (simpl fm)
1.70        val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
1.71        val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
1.72      (* Return the four theorems needed to proove the whole Cooper Theorem*)
1.73 -  in (dpos,mit2,bst,nbstpthm,mit1)
1.74 +  in (dpos,mit2,nbstpthm,mit1)
1.75  end;
1.76
1.77
1.78 @@ -1340,12 +1303,11 @@
1.79
1.80
1.81  fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
1.82 -  let val ast = asetproof_of sg bsprt
1.83 -      val (mit1,mit2) = pinf_proof_of sg dlcm miprt
1.84 +  let val (mit1,mit2) = pinf_proof_of sg dlcm miprt
1.85        val fm1 = norm_zero_one (simpl fm)
1.86        val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
1.87        val nastpthm = not_ast_p_proof_of sg nast_p_prt
1.88 -  in (dpos,mit2,ast,nastpthm,mit1)
1.89 +  in (dpos,mit2,nastpthm,mit1)
1.90  end;
1.91
1.92
1.93 @@ -1357,12 +1319,12 @@
1.94
1.95  fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
1.96    "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
1.97 -	      val (dpsthm,th1,th2,nbpth,th3) = cooperpi_proof_of sg x prt
1.98 -		   in [dpsthm,th1,th2,nbpth,th3] MRS (cppi_eq)
1.99 +	      val (dpsthm,th1,nbpth,th3) = cooperpi_proof_of sg x prt
1.100 +		   in [dpsthm,th1,nbpth,th3] MRS (cppi_eq)
1.101             end
1.102    |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
1.103 -	       val (dpsthm,th1,th2,nbpth,th3) = coopermi_proof_of sg x prt
1.104 -		   in [dpsthm,th1,th2,nbpth,th3] MRS (cpmi_eq)
1.105 +	       val (dpsthm,th1,nbpth,th3) = coopermi_proof_of sg x prt
1.106 +		   in [dpsthm,th1,nbpth,th3] MRS (cpmi_eq)
1.107                  end
1.108   |_ => error "parameter error";
1.109
```