1.1 --- a/src/HOL/UNITY/Project.ML	Fri Nov 05 12:47:29 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Project.ML	Fri Nov 05 16:41:56 1999 +0100
     1.3 @@ -570,32 +570,6 @@
     1.4  qed "transient_extend_set_imp_project_transient";
     1.5  
     1.6  
     1.7 -(*UNUSED.  WHY??
     1.8 -  Converse of the above...it requires a strong assumption about actions
     1.9 -  being enabled for all possible values of the new variables.*)
    1.10 -Goalw [transient_def]
    1.11 -     "[| project h C F : transient A;  \
    1.12 -\        ALL act: Acts F. project_act h (Restrict C act) ^^ A <= - A --> \
    1.13 -\                         Domain act <= C \
    1.14 -\             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
    1.15 -\     ==> F : transient (extend_set h A)";
    1.16 -by (auto_tac (claset() delrules [ballE],
    1.17 -	      simpset() addsimps [Domain_project_act]));
    1.18 -by (ball_tac 1);
    1.19 -by (rtac bexI 1);
    1.20 -by (assume_tac 2);
    1.21 -by Auto_tac;
    1.22 -by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1);
    1.23 -by (force_tac (claset(), simpset() addsimps [Int_absorb1]) 1);
    1.24 -(*The Domain requirement's proved; must prove the Image requirement*)
    1.25 -by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
    1.26 -by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
    1.27 -by Auto_tac;
    1.28 -by (thin_tac "A <= ?B" 1);
    1.29 -by (force_tac (claset() addSIs [ImageI, project_act_I], simpset()) 1);
    1.30 -qed "project_transient_imp_transient_extend_set";
    1.31 -
    1.32 -
    1.33  (** ensures **)
    1.34  
    1.35  (*For simplicity, the complicated condition on C is eliminated
    1.36 @@ -610,21 +584,16 @@
    1.37  by (Blast_tac 1);
    1.38  qed "ensures_extend_set_imp_project_ensures";
    1.39  
    1.40 -(*A strong condition: F can do anything that project G can.*)
    1.41 -Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
    1.42 +Goal "[| project h C G : transient (A-B) --> F : transient (A-B);  \
    1.43  \        extend h F Join G : stable C;  \
    1.44  \        F Join project h C G : A ensures B |] \
    1.45  \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
    1.46 -by (case_tac "A <= B" 1);
    1.47 -by (blast_tac (claset() addIs [subset_imp_ensures] addDs [extend_set_mono]) 1);
    1.48 -by (full_simp_tac (simpset() addsimps [ensures_def, Join_constrains,
    1.49 -				       Join_stable, Join_transient]) 1);
    1.50 -by (REPEAT_FIRST (rtac conjI));
    1.51 -by (blast_tac (claset() addDs [extend_transient RS iffD2] 
    1.52 -                        addIs [transient_strengthen]) 3);
    1.53 -by (REPEAT (force_tac (claset() addIs [project_unless RS unlessD, unlessI, 
    1.54 -				       project_extend_constrains_I], 
    1.55 -		       simpset()) 1));
    1.56 +by (auto_tac (claset() addDs [extend_transient RS iffD2] 
    1.57 +                       addIs [transient_strengthen, 
    1.58 +			      project_unless RS unlessD, unlessI, 
    1.59 +			      project_extend_constrains_I], 
    1.60 +	      simpset() addsimps [ensures_def, Join_constrains,
    1.61 +				  Join_stable, Join_transient]));
    1.62  qed_spec_mp "Join_project_ensures";
    1.63  
    1.64  (** Lemma useful for both STRONG and WEAK progress*)