# HG changeset patch
# User paulson
# Date 963579062 -7200
# Node ID 58bd51302b2123b6e8ef69f515eccc62708f861c
# Parent  9ae89b9ce20687d52f9b726446fe1bdeb6e8438d
used bounded quantification in definition of guarantees and other minor
adjustments

diff -r 9ae89b9ce206 -r 58bd51302b21 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Fri Jul 14 14:47:15 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML	Fri Jul 14 14:51:02 2000 +0200
@@ -283,7 +283,7 @@
 Goalw [extend_act_def, project_act_def]
      "project_act h (extend_act h act) = act";
 by (Blast_tac 1);
-qed "project_act_extend_act";
+qed "extend_act_inverse";
 
 Goalw [extend_act_def, project_act_def]
      "project_act h (Restrict C (extend_act h act)) = \
@@ -292,13 +292,6 @@
 qed "project_act_extend_act_restrict";
 Addsimps [project_act_extend_act_restrict];
 
-(*Premise is still undesirably strong, since Domain act can include
-  non-reachable states, but it seems necessary for this result.*)
-Goal "Domain act <= project_set h C \
-\     ==> project_act h (Restrict C (extend_act h act)) = act";
-by (asm_simp_tac (simpset() addsimps [Restrict_triv]) 1);
-qed "extend_act_inverse";
-
 Goalw [extend_act_def, project_act_def]
      "act' <= extend_act h act ==> project_act h act' <= act";
 by (Force_tac 1);
@@ -307,7 +300,6 @@
 Goal "inj (extend_act h)";
 by (rtac inj_on_inverseI 1);
 by (rtac extend_act_inverse 1);
-by (Force_tac 1);
 qed "inj_extend_act";
 
 Goalw [extend_set_def, extend_act_def]
@@ -454,7 +446,8 @@
 by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);
 qed "extend_invariant";
 
-(*Converse fails: A and B may differ in their extra variables*)
+(*Projects the state predicates in the property satisfied by  extend h F.
+  Converse fails: A and B may differ in their extra variables*)
 Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)";
 by (auto_tac (claset(), simpset() addsimps [constrains_def]));
 by (Force_tac 1);
@@ -527,6 +520,7 @@
     (simpset() addsimps [stable_def, project_constrains_mono]) 1);
 qed "project_stable_mono";
 
+(*Key lemma used in several proofs about project and co*)
 Goalw [constrains_def]
      "(project h C F : A co B)  =  \
 \     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
@@ -551,6 +545,7 @@
 by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
 qed "Int_extend_set_lemma";
 
+(*Strange (look at occurrences of C) but used in leadsETo proofs*)
 Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
 by (full_simp_tac (simpset() addsimps [constrains_def, project_def, 
 				       project_act_def]) 1);
@@ -688,7 +683,7 @@
 Goal "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)";
 by (rtac program_equalityI 1);
 by (asm_simp_tac
-    (simpset() addsimps [image_eq_UN, UN_Un, project_act_extend_act]) 2);
+    (simpset() addsimps [image_eq_UN, UN_Un, extend_act_inverse]) 2);
 by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
 qed "project_extend_Join";
 
@@ -711,11 +706,11 @@
 Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
 \     ==> F : X guarantees[v] Y";
 by (auto_tac (claset(), simpset() addsimps [guar_def]));
-by (dres_inst_tac [("x", "extend h G")] spec 1);
+by (dres_inst_tac [("x", "extend h G")] bspec 1);
 by (asm_full_simp_tac 
     (simpset() delsimps [extend_Join] 
-           addsimps [extend_Join RS sym, extend_preserves,
-		     inj_extend RS inj_image_mem_iff]) 1);
+           addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 2);
+by (asm_simp_tac (simpset() addsimps [extend_preserves]) 1);
 qed "extend_guarantees_imp_guarantees";
 
 Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
@@ -728,7 +723,6 @@
 Close_locale "Extend";
 
 (*Close_locale should do this!
-Delsimps [f_h_eq, extend_set_inverse, f_image_extend_set, extend_act_inverse,
-	  extend_act_Image];
+Delsimps [f_h_eq, extend_set_inverse, f_image_extend_set, extend_act_Image];
 Delrules [make_elim h_inject1];
 *)
diff -r 9ae89b9ce206 -r 58bd51302b21 src/HOL/UNITY/Guar.ML
--- a/src/HOL/UNITY/Guar.ML	Fri Jul 14 14:47:15 2000 +0200
+++ b/src/HOL/UNITY/Guar.ML	Fri Jul 14 14:51:02 2000 +0200
@@ -210,13 +210,27 @@
 qed "guarantees_Join_Un";
 
 Goalw [guar_def]
+     "[| ALL i:I. F i : X i guarantees[v] Y i;  \
+\        ALL i:I. F i : preserves v |] \
+\     ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)";
+by Auto_tac;
+by (ball_tac 1);
+by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
+by (auto_tac
+    (claset(),
+     simpset() addsimps [Join_assoc RS sym, JN_absorb]));
+qed "guarantees_JN_INT";
+
+Goalw [guar_def]
     "[| ALL i:I. F i : X i guarantees[v] Y i;  \
 \       ALL i:I. F i : preserves v |] \
 \    ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)";
 by Auto_tac;
 by (ball_tac 1);
-by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [Join_assoc RS sym, JN_absorb]) 1);
+by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
+by (auto_tac
+    (claset(),
+     simpset() addsimps [Join_assoc RS sym, JN_absorb]));
 qed "guarantees_JN_INT";
 
 Goalw [guar_def]
@@ -225,7 +239,7 @@
 \    ==> (JOIN I F) : (UNION I X) guarantees[v] (UNION I Y)";
 by Auto_tac;
 by (ball_tac 1);
-by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1);
+by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
 by (auto_tac
     (claset(),
      simpset() addsimps [Join_assoc RS sym, JN_absorb]));
@@ -253,7 +267,7 @@
 \        ALL j:I. i~=j --> F j : preserves v |] \
 \     ==> (JN i:I. (F i)) : X guarantees[v] Y";
 by (Clarify_tac 1);
-by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] bspec 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [JN_Join_diff, Join_assoc RS sym]));
 qed "guarantees_JN_I";
diff -r 9ae89b9ce206 -r 58bd51302b21 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Fri Jul 14 14:47:15 2000 +0200
+++ b/src/HOL/UNITY/Guar.thy	Fri Jul 14 14:51:02 2000 +0200
@@ -38,8 +38,8 @@
   guar :: ['a program set, 'a=>'b, 'a program set] => 'a program set
    ("(_/ guarantees[_]/ _)" [55,0,55] 55)
                               (*higher than membership, lower than Co*)
-   "X guarantees[v] Y == {F. ALL G. G : preserves v --> F Join G : X -->
-		       F Join G : Y}"
+   "X guarantees[v] Y == {F. ALL G : preserves v. 
+                               F Join G : X --> F Join G : Y}"
 
   refines :: ['a program, 'a program, 'a program set] => bool
 			("(3_ refines _ wrt _)" [10,10,10] 10)
diff -r 9ae89b9ce206 -r 58bd51302b21 src/HOL/UNITY/Project.ML
--- 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);