# HG changeset patch
# User paulson
# Date 966414302 -7200
# Node ID 7dd6a1661bc94b400126857802be2278a482fdc2
# Parent  795baaf96201d83822661931fa4255f6a15522f7
major sharpening of stable_project_transient

diff -r 795baaf96201 -r 7dd6a1661bc9 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Wed Aug 16 10:23:25 2000 +0200
+++ b/src/HOL/UNITY/Project.ML	Wed Aug 16 10:25:02 2000 +0200
@@ -510,12 +510,21 @@
 by (Blast_tac 1);
 qed "act_subset_imp_project_act_subset";
 
+(*This trivial proof is the complementation part of transferring a transient
+  property upwards.  The hard part would be to 
+  show that G's action has a big enough domain.*)
+Goal "[| act: Acts G;       \
+\        (project_act h (Restrict C act))^^ \
+\             (project_set h C Int A - B) <= -(project_set h C Int A - B) |] \
+\     ==> act^^(C Int extend_set h A - extend_set h B) \
+\           <= -(C Int extend_set h A - extend_set h B)"; 
+by (auto_tac (claset(), 
+     simpset() addsimps [project_set_def, extend_set_def, project_act_def]));  
+result();
 
 Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B));  \
 \        project h C G : transient (project_set h C Int A - B) |]  \
-\     ==> G : transient (C Int extend_set h A - extend_set h B)";
-by (case_tac "C Int extend_set h A <= extend_set h B" 1);
-by (asm_simp_tac (simpset() addsimps [Diff_eq_empty_iff RS iffD2]) 1);
+\     ==> (C Int extend_set h A) - extend_set h B = {}";
 by (auto_tac (claset(), 
 	      simpset() addsimps [transient_def, subset_Compl_self_eq,
 				  Domain_project_act, split_extended_all]));
@@ -523,23 +532,21 @@
 by (auto_tac (claset(), 
 	      simpset() addsimps [stable_def, constrains_def]));
 by (ball_tac 1);
-by (thin_tac "ALL act: Acts G. ?P act" 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [Int_Diff,
 				  extend_set_Diff_distrib RS sym]));
 by (dtac act_subset_imp_project_act_subset 1);
 by (subgoal_tac
-    "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1);
+    "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) = {}" 1);
+by (REPEAT (thin_tac "?r^^?A <= ?B" 1));
 by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]);
-(*using Int_greatest actually slows the next step!*)
 by (Blast_tac 2);
 by (rtac ccontr 1);
 by (dtac subsetD 1);
-by (Blast_tac 1);  
+by (Blast_tac 1);
 by (force_tac (claset(), simpset() addsimps [split_extended_all]) 1);
 qed "stable_project_transient";
 
-
 Goal "[| G : stable C;  project h C G : (project_set h C Int A) unless B |] \
 \     ==> G : (C Int extend_set h A) unless (extend_set h B)";
 by (auto_tac
@@ -558,11 +565,14 @@
                        addIs [project_extend_constrains_I], 
 	      simpset() addsimps [ensures_def]));
 (*transient*)
-by (auto_tac (claset(), simpset() addsimps [Join_transient]));
-by (blast_tac (claset() addIs [stable_project_transient]) 2);
+(*A G-action cannot occur*)
+by (force_tac (claset() addDs [stable_project_transient], 
+                        simpset() delsimps [Diff_eq_empty_iff]
+				 addsimps [Diff_eq_empty_iff RS sym]) 2); 
+(*An F-action*)
 by (force_tac (claset() addSEs [extend_transient RS iffD2 RS 
 				transient_strengthen], 
-	       simpset() addsimps [Join_transient, split_extended_all]) 1);
+	       simpset() addsimps [split_extended_all]) 1);
 qed "project_ensures_D_lemma";
 
 Goal "[| F Join project h UNIV G : A ensures B;  \