src/HOL/UNITY/Project.ML
changeset 9337 58bd51302b21
parent 9190 b86ff604729f
child 9403 aad13b59b8d9
--- a/src/HOL/UNITY/Project.ML	Fri Jul 14 14:47:15 2000 +0200
+++ b/src/HOL/UNITY/Project.ML	Fri Jul 14 14:51:02 2000 +0200
@@ -27,7 +27,8 @@
 			addIs [constrains_weaken]) 1);
 qed_spec_mp "project_unless";
 
-(*This form's useful with guarantees reasoning*)
+(*Generalizes project_constrains to the program F Join project h C G;
+  useful with guarantees reasoning*)
 Goal "(F Join project h C G : A co B)  =  \
 \       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
 \        F : A co B)";
@@ -197,6 +198,7 @@
 
 (** Reachability and project **)
 
+(*In practice, C = reachable(...): the inclusion is equality*)
 Goal "[| reachable (extend h F Join G) <= C;  \
 \        z : reachable (extend h F Join G) |] \
 \     ==> f z : reachable (F Join project h C G)";
@@ -244,12 +246,12 @@
 
 (** Converse results for weak safety: benefits of the argument C *)
 
+(*In practice, C = reachable(...): the inclusion is equality*)
 Goal "[| C <= reachable(extend h F Join G);   \
 \        x : reachable (F Join project h C G) |] \
 \     ==> EX y. h(x,y) : reachable (extend h F Join G)";
 by (etac reachable.induct 1);
 by (ALLGOALS Asm_full_simp_tac);
-(*SLOW: 6.7s*)
 by (force_tac (claset() delrules [Id_in_Acts]
 		        addIs [reachable.Acts, extend_act_D],
 	       simpset() addsimps [project_act_def]) 2);
@@ -264,6 +266,7 @@
 	      simpset()));
 qed "project_set_reachable_extend_eq";
 
+(*UNUSED*)
 Goal "reachable (extend h F Join G) <= C  \
 \     ==> reachable (extend h F Join G) <= \
 \         extend_set h (reachable (F Join project h C G))";
@@ -591,12 +594,12 @@
 (*Weak precondition and postcondition
   Not clear that it has a converse [or that we want one!]*)
 
-(*The raw version*)
+(*The raw version; 3rd premise could be weakened by adding the
+  precondition extend h F Join G : X' *)
 val [xguary,project,extend] =
 Goal "[| F : X guarantees[v] Y;  \
 \        !!G. extend h F Join G : X' ==> F Join project h (C G) G : X;  \
-\        !!G. [| F Join project h (C G) G : Y; extend h F Join G : X'; \
-\                G : preserves (v o f) |] \
+\        !!G. [| F Join project h (C G) G : Y; G : preserves (v o f) |] \
 \             ==> extend h F Join G : Y' |] \
 \     ==> extend h F : X' guarantees[v o f] Y'";
 by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);