# HG changeset patch
# User paulson
# Date 935660164 -7200
# Node ID 477e1bdf230f37602d387e56db6d8765d3c65daf
# Parent  7d3136b9af080bc9e1f8c53f7179449b41871b6b
changed "guar" back to "guarantees" (sorry)

diff -r 7d3136b9af08 -r 477e1bdf230f src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/Alloc.thy	Thu Aug 26 11:36:04 1999 +0200
@@ -67,18 +67,18 @@
   (*spec (3) PROBABLY REQUIRES A LOCALTO PRECONDITION*)
   client_increasing :: clientState program set
     "client_increasing ==
-         UNIV guar Increasing ask Int Increasing rel"
+         UNIV guarantees Increasing ask Int Increasing rel"
 
   (*spec (4)*)
   client_bounded :: clientState program set
     "client_bounded ==
-         UNIV guar Always {s. ALL elt : set (ask s). elt <= NbT}"
+         UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
 
   (*spec (5)*)
   client_progress :: clientState program set
     "client_progress ==
 	 Increasing giv
-	 guar
+	 guarantees
 	 (INT h. {s. h <= giv s & h pfixGe ask s}
 		 LeadsTo
 		 {s. tokens h <= (tokens o rel) s})"
@@ -92,14 +92,14 @@
   alloc_increasing :: allocState program set
     "alloc_increasing ==
 	 UNIV
-         guar
+         guarantees
 	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk))"
 
   (*spec (7)*)
   alloc_safety :: allocState program set
     "alloc_safety ==
 	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
-         guar
+         guarantees
 	 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients
 	         <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
 
@@ -116,7 +116,7 @@
          (INT i : lessThan Nclients. 
 	  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
 		  LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})
-         guar
+         guarantees
 	     (INT i : lessThan Nclients.
 	      INT h. {s. h <= (sub i o allocAsk) s} LeadsTo
 	             {s. h pfixLe (sub i o allocGiv) s})"
@@ -130,21 +130,21 @@
   network_ask :: systemState program set
     "network_ask == INT i : lessThan Nclients.
                     Increasing (ask o sub i o client)
-                    guar
+                    guarantees
                     ((sub i o allocAsk) Fols (ask o sub i o client))"
 
   (*spec (9.2)*)
   network_giv :: systemState program set
     "network_giv == INT i : lessThan Nclients.
                     Increasing (sub i o allocGiv)
-                    guar
+                    guarantees
                     ((giv o sub i o client) Fols (sub i o allocGiv))"
 
   (*spec (9.3)*)
   network_rel :: systemState program set
     "network_rel == INT i : lessThan Nclients.
                     Increasing (rel o sub i o client)
-                    guar
+                    guarantees
                     ((sub i o allocRel) Fols (rel o sub i o client))"
 
   network_spec :: systemState program set
diff -r 7d3136b9af08 -r 477e1bdf230f src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/Client.ML	Thu Aug 26 11:36:04 1999 +0200
@@ -74,7 +74,7 @@
 
 (*Safety property 2: clients return the right number of tokens*)
 Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg))  \
-\               guar Always {s. rel s <= giv s}";
+\               guarantees Always {s. rel s <= giv s}";
 by (rtac guaranteesI 1);
 by (rtac AlwaysI 1);
 by (Force_tac 1);
@@ -101,7 +101,7 @@
 
 Goal "Cli_prg : \
 \      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
-\      guar Always ({s. size (ask s) <= Suc (size (rel s))} Int \
+\      guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
 \                            {s. size (rel s) <= size (giv s)})";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
@@ -121,7 +121,7 @@
 Goal "Cli_prg : \
 \      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
 \                 Int Always giv_meets_ask) \
-\      guar ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
+\      guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
 by (rtac Stable_transient_Always_LeadsTo 1);
diff -r 7d3136b9af08 -r 477e1bdf230f src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Thu Aug 26 11:36:04 1999 +0200
@@ -11,6 +11,14 @@
 (*** component ***)
 
 Goalw [component_def]
+     "H component F | H component G ==> H component (F Join G)";
+by Auto_tac;
+by (res_inst_tac [("x", "G Join Ga")] exI 1);
+by (res_inst_tac [("x", "G Join F")] exI 2);
+by (auto_tac (claset(), simpset() addsimps Join_ac));
+qed "componentI";
+
+Goalw [component_def]
      "(F component G) = (Init G <= Init F & Acts F <= Acts G)";
 by (force_tac (claset() addSIs [exI, program_equalityI], 
 	       simpset() addsimps [Acts_Join]) 1);
@@ -122,73 +130,81 @@
 
 val prems = Goal
      "(!!G. [| F Join G : X;  Disjoint F G |] ==> F Join G : Y) \
-\     ==> F : X guar Y";
-by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
+\     ==> F : X guarantees Y";
+by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "guaranteesI";
 
-Goalw [guarantees_def, component_def]
-     "[| F : X guar Y;  F Join G : X |] ==> F Join G : Y";
+Goalw [guar_def, component_def]
+     "[| F : X guarantees Y;  F Join G : X |] ==> F Join G : Y";
 by (Blast_tac 1);
 qed "guaranteesD";
 
+(*This version of guaranteesD matches more easily in the conclusion*)
+Goalw [guar_def]
+     "[| F : X guarantees Y;  H : X;  F component H |] ==> H : Y";
+by (Blast_tac 1);
+qed "component_guaranteesD";
+
 (*This equation is more intuitive than the official definition*)
-Goal "(F : X guar Y) = \
+Goal "(F : X guarantees Y) = \
 \     (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
-by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
+by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
 by (Blast_tac 1);
 qed "guarantees_eq";
 
-Goalw [guarantees_def] "[| F: X guar X'; Y <= X; X' <= Y' |] ==> F: Y guar Y'";
+Goalw [guar_def]
+     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
 by (Blast_tac 1);
 qed "guarantees_weaken";
 
-Goalw [guarantees_def] "[| F: X guar Y; F component F' |] ==> F': X guar Y";
+Goalw [guar_def]
+     "[| F: X guarantees Y; F component F' |] ==> F': X guarantees Y";
 by (blast_tac (claset() addIs [component_trans]) 1);
 qed "guarantees_weaken_prog";
 
-Goalw [guarantees_def] "X <= Y ==> X guar Y = UNIV";
+Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
 by (Blast_tac 1);
 qed "subset_imp_guarantees_UNIV";
 
 (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-Goalw [guarantees_def] "X <= Y ==> F : X guar Y";
+Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
 by (Blast_tac 1);
 qed "subset_imp_guarantees";
 
 (*Remark at end of section 4.1*)
-Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guar Y)";
+Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
 by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
 by (blast_tac (claset() addEs [equalityE]) 1);
 qed "ex_prop_equiv2";
 
 (** Distributive laws.  Re-orient to perform miniscoping **)
 
-Goalw [guarantees_def]
-     "(UN X:XX. X) guar Y = (INT X:XX. X guar Y)";
+Goalw [guar_def]
+     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
 by (Blast_tac 1);
 qed "guarantees_UN_left";
 
-Goalw [guarantees_def]
-    "(X Un Y) guar Z = (X guar Z) Int (Y guar Z)";
+Goalw [guar_def]
+    "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
 by (Blast_tac 1);
 qed "guarantees_Un_left";
 
-Goalw [guarantees_def]
-     "X guar (INT Y:YY. Y) = (INT Y:YY. X guar Y)";
+Goalw [guar_def]
+     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
 by (Blast_tac 1);
 qed "guarantees_INT_right";
 
-Goalw [guarantees_def]
-    "Z guar (X Int Y) = (Z guar X) Int (Z guar Y)";
+Goalw [guar_def]
+    "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
 by (Blast_tac 1);
 qed "guarantees_Int_right";
 
-Goalw [guarantees_def] "(X guar Y) = (UNIV guar (-X Un Y))";
+Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
 by (Blast_tac 1);
 qed "shunting";
 
-Goalw [guarantees_def] "(X guar Y) = -Y guar -X";
+Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
 by (Blast_tac 1);
 qed "contrapositive";
 
@@ -196,43 +212,45 @@
     is more faithful to the text but looks cryptic.
 **)
 
-Goalw [guarantees_def]
-    "[| F : V guar X;  F : (X Int Y) guar Z |]\
-\    ==> F : (V Int Y) guar Z";
+Goalw [guar_def]
+    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
+\    ==> F : (V Int Y) guarantees Z";
 by (Blast_tac 1);
 qed "combining1";
 
-Goalw [guarantees_def]
-    "[| F : V guar (X Un Y);  F : Y guar Z |]\
-\    ==> F : V guar (X Un Z)";
+Goalw [guar_def]
+    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
+\    ==> F : V guarantees (X Un Z)";
 by (Blast_tac 1);
 qed "combining2";
 
 (** The following two follow Chandy-Sanders, but the use of object-quantifiers
     does not suit Isabelle... **)
 
-(*Premise should be (!!i. i: I ==> F: X guar Y i) *)
-Goalw [guarantees_def]
-     "ALL i:I. F : X guar (Y i) ==> F : X guar (INT i:I. Y i)";
+(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
+Goalw [guar_def]
+     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
 by (Blast_tac 1);
 qed "all_guarantees";
 
-(*Premises should be [| F: X guar Y i; i: I |] *)
-Goalw [guarantees_def]
-     "EX i:I. F : X guar (Y i) ==> F : X guar (UN i:I. Y i)";
+(*Premises should be [| F: X guarantees Y i; i: I |] *)
+Goalw [guar_def]
+     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
 by (Blast_tac 1);
 qed "ex_guarantees";
 
 (*** Additional guarantees laws, by lcp ***)
 
-Goalw [guarantees_def]
-    "[| F: U guar V;  G: X guar Y |] ==> F Join G: (U Int X) guar (V Int Y)";
+Goalw [guar_def]
+    "[| F: U guarantees V;  G: X guarantees Y |] \
+\    ==> F Join G: (U Int X) guarantees (V Int Y)";
 by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
 by (Blast_tac 1);
 qed "guarantees_Join_Int";
 
-Goalw [guarantees_def]
-    "[| F: U guar V;  G: X guar Y |] ==> F Join G: (U Un X) guar (V Un Y)";
+Goalw [guar_def]
+    "[| F: U guarantees V;  G: X guarantees Y |]  \
+\    ==> F Join G: (U Un X) guarantees (V Un Y)";
 by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
 by (Blast_tac 1);
 qed "guarantees_Join_Un";
@@ -242,16 +260,16 @@
 by (Blast_tac 1);
 qed "JN_component_iff";
 
-Goalw [guarantees_def]
-    "[| ALL i:I. F i : X i guar Y i |] \
-\    ==> (JOIN I F) : (INTER I X) guar (INTER I Y)";
+Goalw [guar_def]
+    "[| ALL i:I. F i : X i guarantees Y i |] \
+\    ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
 by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
 by (Blast_tac 1);
 bind_thm ("guarantees_JN_INT", ballI RS result());
 
-Goalw [guarantees_def]
-    "[| ALL i:I. F i : X i guar Y i |] \
-\    ==> (JOIN I F) : (UNION I X) guar (UNION I Y)";
+Goalw [guar_def]
+    "[| ALL i:I. F i : X i guarantees Y i |] \
+\    ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
 by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
 by (Blast_tac 1);
 bind_thm ("guarantees_JN_UN", ballI RS result());
@@ -259,14 +277,14 @@
 
 (*** guarantees laws for breaking down the program, by lcp ***)
 
-Goalw [guarantees_def]
-    "F: X guar Y | G: X guar Y ==> F Join G: X guar Y";
+Goalw [guar_def]
+    "F: X guarantees Y | G: X guarantees Y ==> F Join G: X guarantees Y";
 by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
 by (Blast_tac 1);
 qed "guarantees_Join_I";
 
-Goalw [guarantees_def]
-     "[| i : I;  F i: X guar Y |] ==> (JN i:I. (F i)) : X guar Y";
+Goalw [guar_def]
+     "[| i : I;  F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y";
 by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
 by (Blast_tac 1);
 qed "guarantees_JN_I";
diff -r 7d3136b9af08 -r 477e1bdf230f src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Thu Aug 26 11:36:04 1999 +0200
@@ -346,13 +346,13 @@
 by (etac reachable_lift_prog_Join_D 1);
 qed "reachable_lift_prog_Join_subset";
 
-Goal "F Join drop_prog i G : Stable A    \
-\     ==> lift_prog i F Join G : Stable (lift_set i A)";
-by (full_simp_tac (simpset() addsimps [Stable_def, Constrains_def]) 1);
+Goalw [Constrains_def]
+     "F Join drop_prog i G : A Co B    \
+\     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
 by (subgoal_tac 
     "lift_prog i F Join G : lift_set i (reachable (F Join drop_prog i G)) Int \
 \                           lift_set i A \
-\    co lift_set i A" 1);
+\    co lift_set i B" 1);
 by (asm_full_simp_tac 
     (simpset() addsimps [lift_set_Int RS sym,
 			 lift_prog_constrains,
@@ -360,6 +360,12 @@
 			 drop_prog_lift_prog_Join]) 2);
 by (blast_tac (claset() addIs [constrains_weaken, 
 			       reachable_lift_prog_Join_D]) 1);
+qed "lift_prog_Join_Constrains";
+
+Goal "F Join drop_prog i G : Stable A    \
+\     ==> lift_prog i F Join G : Stable (lift_set i A)";
+by (asm_full_simp_tac (simpset() addsimps [Stable_def, 
+					   lift_prog_Join_Constrains]) 1);
 qed "lift_prog_Join_Stable";
 
 
@@ -369,8 +375,8 @@
 
 (*Strong precondition and postcondition; doesn't seem very useful.
   Probably can be strengthened to an equivalance.*)
-Goal "F : X guar Y \
-\     ==> lift_prog i F : (lift_prog i `` X) guar (lift_prog i `` Y)";
+Goal "F : X guarantees Y \
+\     ==> lift_prog i F : (lift_prog i `` X) guarantees (lift_prog i `` Y)";
 by (rtac guaranteesI 1);
 by Auto_tac;
 by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
@@ -378,10 +384,10 @@
 
 (*Weak precondition and postcondition; this is the good one!*)
 val [xguary,drop_prog,lift_prog] =
-Goal "[| F : X guar Y;  \
+Goal "[| F : X guarantees Y;  \
 \        !!H. H : XX ==> drop_prog i H : X;  \
 \        !!G. F Join drop_prog i G : Y ==> lift_prog i F Join G : YY |] \
-\     ==> lift_prog i F : XX guar YY";
+\     ==> lift_prog i F : XX guarantees YY";
 by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
 by (dtac drop_prog 1);
 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
@@ -421,8 +427,8 @@
 (*** guarantees corollaries ***)
 
 Goalw [increasing_def]
-     "F : UNIV guar increasing f \
-\     ==> lift_prog i F : UNIV guar increasing (f o sub i)";
+     "F : UNIV guarantees increasing f \
+\     ==> lift_prog i F : UNIV guarantees increasing (f o sub i)";
 by (etac drop_prog_guarantees 1);
 by Auto_tac;
 by (stac Collect_eq_lift_set 1); 
@@ -432,8 +438,8 @@
 qed "lift_prog_guar_increasing";
 
 Goalw [Increasing_def]
-     "F : UNIV guar Increasing f \
-\     ==> lift_prog i F : UNIV guar Increasing (f o sub i)";
+     "F : UNIV guarantees Increasing f \
+\     ==> lift_prog i F : UNIV guarantees Increasing (f o sub i)";
 by (etac drop_prog_guarantees 1);
 by Auto_tac;
 by (stac Collect_eq_lift_set 1); 
@@ -441,9 +447,9 @@
 qed "lift_prog_guar_Increasing";
 
 Goalw [localTo_def, increasing_def]
-     "F : (f localTo F) guar increasing f  \
+     "F : (f localTo F) guarantees increasing f  \
 \     ==> lift_prog i F : (f o sub i) localTo (lift_prog i F)  \
-\                         guar increasing (f o sub i)";
+\                         guarantees increasing (f o sub i)";
 by (etac drop_prog_guarantees 1);
 by Auto_tac;
 by (stac Collect_eq_lift_set 2); 
@@ -458,9 +464,9 @@
 qed "lift_prog_localTo_guar_increasing";
 
 Goalw [localTo_def, Increasing_def]
-     "F : (f localTo F) guar Increasing f  \
+     "F : (f localTo F) guarantees Increasing f  \
 \     ==> lift_prog i F : (f o sub i) localTo (lift_prog i F)  \
-\                         guar Increasing (f o sub i)";
+\                         guarantees Increasing (f o sub i)";
 by (etac drop_prog_guarantees 1);
 by Auto_tac;
 by (stac Collect_eq_lift_set 2); 
diff -r 7d3136b9af08 -r 477e1bdf230f src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Thu Aug 26 11:36:04 1999 +0200
@@ -263,20 +263,21 @@
 (*** guarantees properties ***)
 
 Goalw [PLam_def]
-     "[| i : I;  lift_prog i (F i): X guar Y |] ==> (PLam I F) : X guar Y";
+    "[| i : I;  lift_prog i (F i): X guarantees Y |]  \
+\    ==> (PLam I F) : X guarantees Y";
 by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
 qed "guarantees_PLam_I";
 
 Goalw [PLam_def]
-    "[| ALL i:I. F i : X guar Y |] \
+    "[| ALL i:I. F i : X guarantees Y |] \
 \    ==> (PLam I F) : (INT i: I. lift_prog i `` X) \
-\                 guar (INT i: I. lift_prog i `` Y)";
+\                 guarantees (INT i: I. lift_prog i `` Y)";
 by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1);
 bind_thm ("guarantees_PLam_INT", ballI RS result());
 
 Goalw [PLam_def]
-    "[| ALL i:I. F i : X guar Y |] \
+    "[| ALL i:I. F i : X guarantees Y |] \
 \    ==> (PLam I F) : (UN i: I. lift_prog i `` X) \
-\                 guar (UN i: I. lift_prog i `` Y)";
+\                 guarantees (UN i: I. lift_prog i `` Y)";
 by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1);
 bind_thm ("guarantees_PLam_UN", ballI RS result());