# HG changeset patch
# User paulson
# Date 938183637 -7200
# Node ID 8a188ef6545e4e1065d02c57e48141ef979e2129
# Parent  6bc8fa8b4b24f97648ccc10dbff1a0de90cd5516
working version with  co-guarantees-leadsto  results

diff -r 6bc8fa8b4b24 -r 8a188ef6545e src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Fri Sep 24 15:28:12 1999 +0200
+++ b/src/HOL/UNITY/Client.ML	Fri Sep 24 16:33:57 1999 +0200
@@ -78,6 +78,7 @@
 by (rtac guaranteesI 1);
 by (rtac AlwaysI 1);
 by (Force_tac 1);
+by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
 by (blast_tac (claset() addIs [Increasing_localTo_Stable, 
 			       stable_rel_le_giv]) 1);
 qed "ok_guar_rel_prefix_giv";
@@ -109,6 +110,7 @@
 by (rtac AlwaysI 1);
 by (Force_tac 1);
 by (rtac Stable_Int 1);
+by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 2);
 by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
 	               addIs [Increasing_localTo_Stable, 
 			      stable_size_rel_le_giv]) 2);
diff -r 6bc8fa8b4b24 -r 8a188ef6545e src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Fri Sep 24 15:28:12 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Fri Sep 24 16:33:57 1999 +0200
@@ -77,3 +77,8 @@
 qed "component_constrains";
 
 bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
+
+Goal "Diff F (Acts G) <= F";
+by (auto_tac (claset() addSIs [program_equalityI],
+	      simpset() addsimps [Diff_def, component_eq_subset]));
+qed "Diff_component";
diff -r 6bc8fa8b4b24 -r 8a188ef6545e src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Fri Sep 24 15:28:12 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Fri Sep 24 16:33:57 1999 +0200
@@ -10,14 +10,6 @@
 
 (** These we prove OUTSIDE the locale. **)
 
-
-(****************UNITY.ML****************)
-Goalw [stable_def, constrains_def] "stable UNIV = UNIV";
-by Auto_tac;
-qed "stable_UNIV";
-Addsimps [stable_UNIV];
-
-
 (*Possibly easier than reasoning about "inv h"*)
 val [surj_h,prem] = 
 Goalw [good_map_def]
@@ -74,6 +66,10 @@
 
 (*** extend_set: basic properties ***)
 
+Goalw [extend_set_def] "A<=B ==> extend_set h A <= extend_set h B";
+by (Blast_tac 1);
+qed "extend_set_mono";
+
 Goalw [extend_set_def]
      "z : extend_set h A = (f z : A)";
 by (force_tac (claset() addIs  [h_f_g_eq RS sym], simpset()) 1);
@@ -84,6 +80,10 @@
 by Auto_tac;
 qed "Collect_eq_extend_set";
 
+Goal "extend_set h {x} = {s. f s = x}";
+by Auto_tac;
+qed "extend_set_sing";
+
 Goalw [extend_set_def, project_set_def]
      "project_set h (extend_set h F) = F";
 by Auto_tac;
@@ -211,10 +211,8 @@
 by (Force_tac 1);
 qed "project_act_Id";
 
-(*premise can be weakened*)
 Goalw [project_set_def, project_act_def]
-    "Domain act <= C \
-\    ==> Domain (project_act C h act) = project_set h (Domain act)";
+    "Domain (project_act C h act) = project_set h (Domain act Int C)";
 by Auto_tac;
 by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1);
 by Auto_tac;
@@ -325,17 +323,27 @@
 (** Safety and project **)
 
 Goalw [constrains_def]
-     "(F Join project C h G : A co B)  =  \
+     "(project C h F : A co B)  =  \
+\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
+by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
+by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
+(*the <== direction*)
+by (rewtac project_act_def);
+by (force_tac (claset() addSDs [subsetD], simpset()) 1);
+qed "project_constrains";
+
+Goalw [stable_def]
+     "(project UNIV h F : stable A) = (F : stable (extend_set h A))";
+by (simp_tac (simpset() addsimps [project_constrains]) 1);
+qed "project_stable";
+
+(*This form's useful with guarantees reasoning*)
+Goal "(F Join project C h G : A co B)  =  \
 \       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
 \        F : A co B)";
-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 (force_tac (claset() addSDs [subsetD], simpset()) 1);
+by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
+by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
+                        addDs [constrains_imp_subset]) 1);
 qed "Join_project_constrains";
 
 (*The condition is required to prove the left-to-right direction;
@@ -357,12 +365,6 @@
 				  extend_stable RS iffD1]));
 qed "Join_project_increasing";
 
-Goal "(project C h F : A co B)  =  \
-\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
-by (cut_inst_tac [("F", "SKIP")] Join_project_constrains 1);
-by (asm_full_simp_tac (simpset() addsimps [extend_SKIP]) 1);
-qed "project_constrains";
-
 
 (*** Diff, needed for localTo ***)
 
@@ -685,6 +687,104 @@
 qed "extend_LeadsTo";
 
 
+(** Progress includes safety in the definition of ensures **)
+
+(*** Progress for (project C h F) ***)
+
+(** 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 C h F : transient A";
+by (auto_tac (claset() delrules [ballE],
+              simpset() addsimps [Domain_project_act, Int_absorb2]));
+by (REPEAT (ball_tac 1));
+by (auto_tac (claset(),
+              simpset() addsimps [extend_set_def, project_set_def, 
+				  project_act_def]));
+by (ALLGOALS Blast_tac);
+qed "transient_extend_set_imp_project_transient";
+
+
+(*Converse of the above...it requires a strong assumption about actions
+  being enabled for all possible values of the new variables.*)
+Goalw [transient_def]
+     "[| project C h F : transient A;  \
+\        ALL act: Acts F. project_act C h act ^^ A <= - A --> \
+\                         Domain act <= C \
+\             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
+\     ==> F : transient (extend_set h A)";
+by (auto_tac (claset() delrules [ballE],
+	      simpset() addsimps [Domain_project_act]));
+by (ball_tac 1);
+by (rtac bexI 1);
+by (assume_tac 2);
+by Auto_tac;
+by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1);
+by (force_tac (claset(), simpset() addsimps [Int_absorb2]) 1);
+(*The Domain requirement's proved; must prove the Image requirement*)
+by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
+by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
+by Auto_tac;
+by (thin_tac "A <= ?B" 1);
+by (force_tac (claset() addSIs [ImageI, project_act_I], simpset()) 1);
+qed "project_transient_imp_transient_extend_set";
+
+
+(** ensures **)
+
+(*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 UNIV h F : A ensures 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);
+qed "ensures_extend_set_imp_project_ensures";
+
+(*A super-strong condition: G is not allowed to affect the
+  shared variables at all.*)
+Goal "[| ALL x. project UNIV h G ~: transient {x};  \
+\        F Join project UNIV h G : A ensures B |] \
+\     ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
+by (case_tac "A <= B" 1);
+by (etac (extend_set_mono RS subset_imp_ensures) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [ensures_def, extend_constrains, extend_transient, 
+			 extend_set_Un_distrib RS sym, 
+			 extend_set_Diff_distrib RS sym,
+			 Join_transient, Join_constrains,
+			 project_constrains, Int_absorb1]) 1);
+(*otherwise PROOF FAILED*)
+by Auto_tac;
+by (blast_tac (claset() addIs [transient_strengthen]) 1);
+qed_spec_mp "Join_project_ensures";
+
+Goal "[| ALL x. project UNIV h G ~: transient {x};  \
+\        F Join project UNIV h G : A leadsTo B |] \
+\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
+by (etac leadsTo_induct 1);
+by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
+by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
+qed "Join_project_leadsTo_I";
+
+
+
+Goal "F : stable{s} ==> F ~: transient {s}";
+by (auto_tac (claset(), 
+	      simpset() addsimps [FP_def, transient_def,
+				  stable_def, constrains_def]));
+qed "stable_sing_imp_not_transient";
+
+
 (** Strong precondition and postcondition; doesn't seem very useful. **)
 
 Goal "F : X guarantees Y ==> \
@@ -717,10 +817,14 @@
 val [xguary,project,extend] =
 Goal "[| F : X guarantees 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' |] \
+\        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
+\                Disjoint (extend h F) G |] \
+\             ==> 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);
+by (assume_tac 1);
+by (assume_tac 1);
 qed "project_guarantees";
 
 (** It seems that neither "guarantees" law can be proved from the other. **)
@@ -767,6 +871,37 @@
     (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
 qed "extend_localTo_guar_Increasing";
 
+
+(** Guarantees with a leadsTo postcondition **)
+
+Goal "[| G : f localTo extend h F; \
+\        Disjoint (extend h F) G |] ==> project UNIV h G : stable {x}";
+by (asm_full_simp_tac
+    (simpset() addsimps [localTo_imp_stable,
+			 extend_set_sing, project_stable]) 1);
+qed "localTo_imp_project_stable";
+
+
+Goal "F : (A co A') guarantees (B leadsTo B')  \
+\ ==> extend h F : ((extend_set h A) co (extend_set h A'))  \
+\                   Int (f localTo (extend h F)) \
+\                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
+by (etac project_guarantees 1);
+(*the safety precondition*)
+by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [project_constrains, Join_constrains, 
+			 extend_constrains]) 1);
+by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
+(*the liveness postcondition*)
+by (rtac Join_project_leadsTo_I 1);
+by Auto_tac;
+by (asm_full_simp_tac
+    (simpset() addsimps [Join_localTo, self_localTo,
+			 localTo_imp_project_stable, stable_sing_imp_not_transient]) 1);
+qed "extend_co_guar_leadsTo";
+
+
 Close_locale "Extend";
 
 (*Close_locale should do this!
diff -r 6bc8fa8b4b24 -r 8a188ef6545e src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Fri Sep 24 15:28:12 1999 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Fri Sep 24 16:33:57 1999 +0200
@@ -207,6 +207,11 @@
 by (assume_tac 1);
 qed "stableD";
 
+Goalw [stable_def, constrains_def] "stable UNIV = UNIV";
+by Auto_tac;
+qed "stable_UNIV";
+Addsimps [stable_UNIV];
+
 (** Union **)
 
 Goalw [stable_def]
diff -r 6bc8fa8b4b24 -r 8a188ef6545e src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Fri Sep 24 15:28:12 1999 +0200
+++ b/src/HOL/UNITY/Union.ML	Fri Sep 24 16:33:57 1999 +0200
@@ -203,11 +203,17 @@
 by (Blast_tac 1);
 bind_thm ("invariant_JN_I", ballI RS result());
 
-Goal "F Join G : stable A = \
+Goal "(F Join G : stable A) = \
 \     (F : stable A & G : stable A)";
 by (simp_tac (simpset() addsimps [stable_def, Join_constrains]) 1);
 qed "Join_stable";
 
+Goal "(F Join G : increasing f) = \
+\     (F : increasing f & G : increasing f)";
+by (simp_tac (simpset() addsimps [increasing_def, Join_stable]) 1);
+by (Blast_tac 1);
+qed "Join_increasing";
+
 Goal "[| F : invariant A; G : invariant A |]  \
 \     ==> F Join G : invariant A";
 by (full_simp_tac (simpset() addsimps [invariant_def, Join_stable]) 1);
@@ -283,17 +289,27 @@
 
 (** Diff and localTo **)
 
-Goalw [Join_def, Diff_def] "F Join (Diff G (Acts F)) = F Join G";
+Goalw [Diff_def] "F Join (Diff G (Acts F)) = F Join G";
 by (rtac program_equalityI 1);
 by Auto_tac;
 qed "Join_Diff2";
 
+Goalw [Diff_def]
+     "Diff (F Join G) (Acts H) = (Diff F (Acts H)) Join (Diff G (Acts H))";
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "Diff_Join_distrib";
+
+Goalw [Diff_def, constrains_def] "(Diff F (Acts F) : A co B) = (A <= B)";
+by Auto_tac;
+qed "Diff_self_constrains";
+
 Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
 by Auto_tac;
 qed "Diff_Disjoint";
 
-Goal "[| F Join G : v localTo F;  Disjoint F G |] \
-\     ==> G : (INT z. stable {s. v s = z})";
+Goal "[| G : v localTo F;  Disjoint F G |] \
+\     ==> G : stable {s. v s = z}";
 by (asm_full_simp_tac 
     (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
 			 stable_def, constrains_def]) 1);
@@ -314,6 +330,19 @@
 by (force_tac (claset() addSEs [allE, ballE], simpset()) 1);
 qed "localTo_imp_o_localTo";
 
+Goal "(F Join G : v localTo H) = (F : v localTo H  &  G : v localTo H)";
+by (asm_full_simp_tac 
+    (simpset() addsimps [localTo_def, Diff_Join_distrib,
+			 stable_def, Join_constrains]) 1);
+by (Blast_tac 1);
+qed "Join_localTo";
+
+Goal "F : v localTo F";
+by (simp_tac 
+    (simpset() addsimps [localTo_def, stable_def, Diff_self_constrains]) 1);
+qed "self_localTo";
+
+
 
 (*** Higher-level rules involving localTo and Join ***)
 
@@ -342,20 +371,20 @@
 qed "UN_eq_UNIV";
 
 Goal "[| F : stable {s. v s <= w s};   \
-\        F Join G : v localTo F;       \
+\        G : v localTo F;       \
 \        F Join G : Increasing w;      \
 \        Disjoint F G |]               \
 \     ==> F Join G : Stable {s. v s <= w s}";
-by (safe_tac (claset() addSDs [localTo_imp_stable]));
 by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]);
 by (subgoal_tac "ALL k: UNIV. ?H : ({s. v s = k} Int ?AA) Co ?AA" 1);
 by (dtac ball_Constrains_UN 1);
 by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1);
 by (rtac ballI 1);
 by (subgoal_tac "F Join G : ({s. v s = k} Int {s. v s <= w s}) co \
-\                                      ({s. v s = k} Un {s. v s <= w s})" 1);
+\                           ({s. v s = k} Un {s. v s <= w s})" 1);
 by (asm_simp_tac (simpset() addsimps [Join_constrains]) 2);
-by (blast_tac (claset() addIs [constrains_weaken]) 2);
+by (fast_tac (claset() addIs [constrains_weaken] 
+                addEs [localTo_imp_stable RS stableD RS constrains_weaken]) 2);
 by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
 by (etac Constrains_weaken 2);
 by Auto_tac;
diff -r 6bc8fa8b4b24 -r 8a188ef6545e src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Fri Sep 24 15:28:12 1999 +0200
+++ b/src/HOL/UNITY/WFair.ML	Fri Sep 24 16:33:57 1999 +0200
@@ -145,11 +145,12 @@
 qed "leadsTo_induct";
 
 
-Goal "A<=B ==> F : A leadsTo B";
-by (rtac leadsTo_Basis 1);
+Goal "A<=B ==> F : A ensures B";
 by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
 by (Blast_tac 1);
-qed "subset_imp_leadsTo";
+qed "subset_imp_ensures";
+
+bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis);
 
 bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
 Addsimps [empty_leadsTo];