# HG changeset patch
# User paulson
# Date 947238935 -3600
# Node ID f7651ede12b764a9a50cbbc2203f500e2f783dd9
# Parent  aca11f954993a82566f478a33f438a3025f60d2c
moved some proofs from UNITY/ELT to UNITY/Project

diff -r aca11f954993 -r f7651ede12b7 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    \
diff -r aca11f954993 -r f7651ede12b7 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Thu Jan 06 16:00:18 2000 +0100
+++ b/src/HOL/UNITY/Project.ML	Fri Jan 07 10:55:35 2000 +0100
@@ -446,42 +446,79 @@
 qed "extending_Increasing";
 
 
-(** Progress includes safety in the definition of ensures **)
-
-(*** Progress for (project h C F) ***)
+(*** leadsETo in the precondition ***)
 
 (** transient **)
 
-(*Premise is that C includes the domains of all actions that could be the
-  transient one.  Could have C=UNIV of course*)
 Goalw [transient_def]
-     "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \
-\                      Domain act <= C;    \
-\        F : transient (extend_set h A) |] \
-\     ==> project h C F : transient A";
-by (auto_tac (claset() delrules [ballE],
-              simpset() addsimps [Domain_project_act, Int_absorb1]));
-by (REPEAT (ball_tac 1));
-by (auto_tac (claset(),
-              simpset() addsimps [extend_set_def, project_act_def]));
-by (ALLGOALS Blast_tac);
+     "[| 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";
 
-(** ensures **)
+
+(** ensures -- a primitive combining progress with safety **)
 
-(*For simplicity, the complicated condition on C is eliminated
-  NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*)
-Goal "F : (extend_set h A) ensures (extend_set h B) \
-\     ==> project h UNIV F : A ensures B";
+(*Used to prove project_leadsETo_I*)
+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, project_constrains, 
-			 transient_extend_set_imp_project_transient,
-			 extend_set_Un_distrib RS sym, 
-			 extend_set_Diff_distrib RS sym]) 1);
-by (Blast_tac 1);
+    (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]
+			addSDs [equalityD1]) 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() addSDs [equalityD1]
+	                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() addSDs [equalityD1]
+	                addIs [transient_extend_set_imp_project_transient RS 
+			 project_extend_transient_D RS transient_strengthen], 
+              simpset()) 1);
 qed "ensures_extend_set_imp_project_ensures";
 
+(*Used to prove project_leadsETo_D*)
 Goal "[| project h C G ~: transient (A-B) | A<=B;  \
 \        extend h F Join G : stable C;  \
 \        F Join project h C G : A ensures B |] \
@@ -519,14 +556,14 @@
 \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
 by (rtac (lemma RS leadsTo_weaken) 1);
 by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
-qed "project_leadsTo_lemma";
+qed "project_leadsTo_D_lemma";
 
 Goal "[| C = (reachable (extend h F Join G)); \
 \        ALL D. project h C G : transient D --> D={};  \
 \        F Join project h C G : A LeadsTo B |] \
 \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (asm_full_simp_tac 
-    (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma, 
+    (simpset() addsimps [LeadsTo_def, project_leadsTo_D_lemma, 
 			 project_set_reachable_extend_eq]) 1);
 qed "Join_project_LeadsTo";
 
@@ -660,7 +697,8 @@
 Goal "[| F Join project h UNIV G : A leadsTo B;    \
 \        G : preserves f |]  \
 \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
-by (res_inst_tac [("C1", "UNIV")] (project_leadsTo_lemma RS leadsTo_weaken) 1);
+by (res_inst_tac [("C1", "UNIV")] 
+    (project_leadsTo_D_lemma RS leadsTo_weaken) 1);
 by (auto_tac (claset() addDs [preserves_project_transient_empty], 
 	      simpset()));
 qed "project_leadsTo_D";