src/HOL/UNITY/ELT.ML

--- a/src/HOL/UNITY/ELT.ML	Thu Jan 06 16:00:18 2000 +0100
+++ b/src/HOL/UNITY/ELT.ML	Fri Jan 07 10:55:35 2000 +0100
@@ -183,7 +183,8 @@
 \     ==> F : B leadsTo[CC] B'";
 by (dtac (impOfSubs leadsETo_mono) 1);
 by (assume_tac 1);
-by (blast_tac (claset() addIs [leadsETo_weaken_R, leadsETo_weaken_L,
+by (blast_tac (claset() delrules [subsetCE]
+			addIs [leadsETo_weaken_R, leadsETo_weaken_L,
 			       leadsETo_Trans]) 1);
 qed "leadsETo_weaken";
 
@@ -534,7 +535,7 @@
 				project_preserves_I]) 1);
 result();
 
-(*Generalizes the version proved in Project.ML*)
+(*GENERALIZES the version proved in Project.ML*)
 Goal "[| G : preserves (v o f);  \
 \        project h C G : transient (C' Int D);  \
 \        project h C G : stable C';  D : givenBy v |]    \
@@ -570,7 +571,7 @@
 		  addsimps [Int_UN_distrib, leadsETo_UN, extend_set_Union]) 3);
 by (blast_tac (claset() addIs [e_psp_stable2 RS leadsETo_weaken_L, 
 			       leadsETo_Trans]) 2);
-auto();
+by Auto_tac;
 by (force_tac (claset() addIs [leadsETo_Basis, subset_imp_ensures],
 	       simpset()) 1);
 by (rtac leadsETo_Basis 1);
@@ -642,72 +643,6 @@
 
 (*** leadsETo in the precondition ***)
 
-Goalw [transient_def]
-     "[| G : transient (C Int extend_set h A);  G : stable C |]  \
-\     ==> project h C G : transient (project_set h C Int A)";
-by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
-by (subgoal_tac "act ^^ (C Int extend_set h A) <= - extend_set h A" 1);
-by (asm_full_simp_tac 
-    (simpset() addsimps [stable_def, constrains_def]) 2);
-by (Blast_tac 2);
-(*back to main goal*)
-by (thin_tac "?AA <= -C Un ?BB" 1);
-by (ball_tac 1);
-by (asm_full_simp_tac 
-    (simpset() addsimps [extend_set_def, project_act_def]) 1);
-by (Blast_tac 1);
-qed "transient_extend_set_imp_project_transient";
-
-(*converse might hold too?*)
-Goalw [transient_def]
-     "project h C (extend h F) : transient (project_set h C Int D) \
-\     ==> F : transient (project_set h C Int D)";
-by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
-by (rtac bexI 1);
-by (assume_tac 2);
-by Auto_tac;
-by (rewtac extend_act_def);
-by (Blast_tac 1);
-qed "project_extend_transient_D";
-
-
-Goal "[| extend h F : stable C;  G : stable C;  \
-\        extend h F Join G : A ensures B;  A-B = C Int extend_set h D |]  \
-\     ==> F Join project h C G  \
-\           : (project_set h C Int project_set h A) ensures (project_set h B)";
-by (asm_full_simp_tac
-    (simpset() addsimps [ensures_def, Join_constrains, project_constrains, 
-			 Join_transient, extend_transient]) 1);
-by (Clarify_tac 1);
-by (REPEAT_FIRST (rtac conjI));
-(*first subgoal*)
-by (blast_tac (claset() addIs [extend_stable_project_set RS stableD RS 
-			       constrains_Int RS constrains_weaken]
-	                addSDs [extend_constrains_project_set]
-			addSEs [equalityE]) 1);
-(*2nd subgoal*)
-by (etac (stableD RS constrains_Int RS constrains_weaken) 1);
-by (assume_tac 1);
-by (Blast_tac 3);
-by (full_simp_tac (simpset() addsimps [extend_set_Int_distrib,
-				       extend_set_Un_distrib]) 2);
-by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2);
-by (full_simp_tac (simpset() addsimps [extend_set_def]) 1);
-by (blast_tac (claset() addSEs [equalityE]) 1);
-(*The transient part*)
-by Auto_tac;
-by (force_tac (claset() addSEs [equalityE]
-	                addIs [transient_extend_set_imp_project_transient RS
-			       transient_strengthen], 
-              simpset()) 2);
-by (full_simp_tac (simpset() addsimps [Int_Diff]) 1);
-by (force_tac (claset() addSEs [equalityE]
-	                addIs [transient_extend_set_imp_project_transient RS 
-			 project_extend_transient_D RS transient_strengthen], 
-              simpset()) 1);
-qed "ensures_extend_set_imp_project_ensures";
-
-
 (*Lemma for the Trans case*)
 Goal "[| extend h F Join G : stable C;    \
 \        F Join project h C G    \