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