project_act no longer has a special case to allow identity actions

--- a/src/HOL/UNITY/Extend.ML	Tue Sep 21 10:39:33 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Tue Sep 21 11:09:24 1999 +0200
@@ -199,14 +199,15 @@
 qed "extend_act_Id";
 
 Goalw [project_act_def]
-     "[| (z, z') : act;  f z = f z' | z: C |] \
+     "[| (z, z') : act;  z: C |] \
 \     ==> (f z, f z') : project_act C h act";
 by (auto_tac (claset() addSIs [exI] addIs [h_f_g_eq RS ssubst], 
 	      simpset()));
 qed "project_act_I";
 
 Goalw [project_set_def, project_act_def]
-    "project_act C h Id = Id";
+    "UNIV <= project_set h C \
+\     ==> project_act C h Id = Id";
 by (Force_tac 1);
 qed "project_act_Id";
 
@@ -244,8 +245,8 @@
 	      simpset() addsimps [extend_def, image_iff]));
 qed "Acts_extend";
 
-Goal "Acts (project C h F) = (project_act C h `` Acts F)";
-by (auto_tac (claset() addSIs [project_act_Id RS sym], 
+Goal "Acts (project C h F) = insert Id (project_act C h `` Acts F)";
+by (auto_tac (claset(), 
 	      simpset() addsimps [project_def, image_iff]));
 qed "Acts_project";
 
@@ -256,12 +257,6 @@
 by Auto_tac;
 qed "extend_SKIP";
 
-Goalw [SKIP_def] "project C h SKIP = SKIP";
-by (rtac program_equalityI 1);
-by (auto_tac (claset() addIs  [h_f_g_eq RS sym], 
-	      simpset() addsimps [project_set_def]));
-qed "project_SKIP";
-
 Goalw [project_set_def] "UNIV <= project_set h UNIV";
 by Auto_tac;
 qed "project_set_UNIV";
@@ -336,11 +331,10 @@
 by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
 by (force_tac (claset() addIs [extend_act_D], simpset()) 1);
 by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
+by (force_tac (claset() addSDs [Id_in_Acts RSN (2,bspec)], simpset()) 1);
 (*the <== direction*)
 by (ball_tac 1);
 by (rewtac project_act_def);
-by Auto_tac;
-by (force_tac (claset() addSDs [Id_in_Acts RSN (2,bspec)], simpset()) 1);
 by (force_tac (claset() addSDs [subsetD], simpset()) 1);
 qed "Join_project_constrains";
 
@@ -361,7 +355,6 @@
 by (auto_tac (claset(),
 	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
 				  extend_stable RS iffD1]));
-
 qed "Join_project_increasing";
 
 Goal "(project C h F : A co B)  =  \
@@ -482,11 +475,14 @@
 \        z : reachable (extend h F Join G) |] \
 \     ==> f z : reachable (F Join project C h G)";
 by (etac reachable.induct 1);
-by (force_tac (claset() delrules [Id_in_Acts]
-		        addIs [reachable.Acts, project_act_I, extend_act_D],
-	       simpset()) 2);
 by (force_tac (claset() addIs [reachable.Init, project_set_I],
 	       simpset()) 1);
+by Auto_tac;
+by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)],
+	       simpset()) 2);
+by (res_inst_tac [("act","x")] reachable.Acts 1);
+by Auto_tac;
+by (etac extend_act_D 1);
 qed "reachable_imp_reachable_project";
 
 Goalw [Constrains_def]
@@ -717,12 +713,11 @@
 qed "extend_guarantees_eq";
 
 (*Weak precondition and postcondition; this is the good one!
-  Not clear that it has a converse [or that we want one!] 
-  Can generalize project (C G) to the function variable "proj"*)
+  Not clear that it has a converse [or that we want one!]*)
 val [xguary,project,extend] =
 Goal "[| F : X guarantees Y;  \
-\        !!G. extend h F Join G : X' ==> F Join project (C G) h G : X;  \
-\        !!G. F Join project (C G) h G : Y ==> extend h F Join G : Y' |] \
+\        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
+\        !!G. F Join proj G h G : Y ==> extend h F Join G : Y' |] \
 \     ==> extend h F : X' guarantees Y'";
 by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
 by (etac project 1);

--- a/src/HOL/UNITY/Extend.thy	Tue Sep 21 10:39:33 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy	Tue Sep 21 11:09:24 1999 +0200
@@ -25,10 +25,10 @@
   extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
     "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
 
+  (*Argument C allows weak safety laws to be projected*)
   project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"
     "project_act C h act ==
-         {(x,x'). EX y y'. (h(x,y), h(x',y')) : act &
-	                   (x = x' | h(x,y) : C)}"
+         {(x,x'). EX y y'. (h(x,y), h(x',y')) : act & (h(x,y) : C)}"
 
   extend :: "['a*'b => 'c, 'a program] => 'c program"
     "extend h F == mk_program (extend_set h (Init F),