# HG changeset patch
# User paulson
# Date 929274770 -7200
# Node ID 8932f33259d41a75fda17c750e7a7d2a2ffca926
# Parent  350f27e2d649a29cb341ee7dd3074582363f390b
guarantees -> guar

diff -r 350f27e2d649 -r 8932f33259d4 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Sun Jun 13 13:52:26 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Sun Jun 13 13:52:50 1999 +0200
@@ -111,42 +111,54 @@
 (*** guarantees ***)
 
 (*This equation is more intuitive than the official definition*)
-Goal "(F : X guarantees Y) = \
+Goal "(F : X guar 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 (Blast_tac 1);
 qed "guarantees_eq";
 
-Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
+Goalw [guarantees_def] "X <= Y ==> X guar 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 guarantees Y";
+Goalw [guarantees_def] "X <= Y ==> F : X guar Y";
 by (Blast_tac 1);
 qed "subset_imp_guarantees";
 
 (*Remark at end of section 4.1*)
-Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guarantees Y)";
+Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guar 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]
-     "(INT X:XX. X guarantees Y) = (UN X:XX. X) guarantees Y";
+     "(UN X:XX. X) guar Y = (INT X:XX. X guar Y)";
 by (Blast_tac 1);
-qed "INT_guarantees_left";
+qed "guarantees_UN_left";
 
 Goalw [guarantees_def]
-     "(INT Y:YY. X guarantees Y) = X guarantees (INT Y:YY. Y)";
+    "(X Un Y) guar Z = (X guar Z) Int (Y guar Z)";
+by (Blast_tac 1);
+qed "guarantees_Un_left";
+
+Goalw [guarantees_def]
+     "X guar (INT Y:YY. Y) = (INT Y:YY. X guar Y)";
 by (Blast_tac 1);
-qed "INT_guarantees_right";
+qed "guarantees_INT_right";
 
-Goalw [guarantees_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
+Goalw [guarantees_def]
+    "Z guar (X Int Y) = (Z guar X) Int (Z guar Y)";
+by (Blast_tac 1);
+qed "guarantees_Int_right";
+
+Goalw [guarantees_def] "(X guar Y) = (UNIV guar (-X Un Y))";
 by (Blast_tac 1);
 qed "shunting";
 
-Goalw [guarantees_def] "(X guarantees Y) = -Y guarantees -X";
+Goalw [guarantees_def] "(X guar Y) = -Y guar -X";
 by (Blast_tac 1);
 qed "contrapositive";
 
@@ -155,41 +167,41 @@
 **)
 
 Goalw [guarantees_def]
-    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
-\    ==> F : (V Int Y) guarantees Z";
+    "[| F : V guar X;  F : (X Int Y) guar Z |]\
+\    ==> F : (V Int Y) guar Z";
 by (Blast_tac 1);
 qed "combining1";
 
 Goalw [guarantees_def]
-    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
-\    ==> F : V guarantees (X Un Z)";
+    "[| F : V guar (X Un Y);  F : Y guar Z |]\
+\    ==> F : V guar (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 guarantees Y i) *)
+(*Premise should be (!!i. i: I ==> F: X guar Y i) *)
 Goalw [guarantees_def]
-     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
+     "ALL i:I. F : X guar (Y i) ==> F : X guar (INT i:I. Y i)";
 by (Blast_tac 1);
 qed "all_guarantees";
 
-(*Premises should be [| F: X guarantees Y i; i: I |] *)
+(*Premises should be [| F: X guar Y i; i: I |] *)
 Goalw [guarantees_def]
-     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
+     "EX i:I. F : X guar (Y i) ==> F : X guar (UN i:I. Y i)";
 by (Blast_tac 1);
 qed "ex_guarantees";
 
 val prems = Goal
      "(!!G. [| F Join G : X;  Disjoint F G |] ==> F Join G : Y) \
-\     ==> F : X guarantees Y";
+\     ==> F : X guar Y";
 by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "guaranteesI";
 
 Goalw [guarantees_def, component_def]
-     "[| F : X guarantees Y;  F Join G : X |] ==> F Join G : Y";
+     "[| F : X guar Y;  F Join G : X |] ==> F Join G : Y";
 by (Blast_tac 1);
 qed "guaranteesD";
 
diff -r 350f27e2d649 -r 8932f33259d4 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Sun Jun 13 13:52:26 1999 +0200
+++ b/src/HOL/UNITY/Comp.thy	Sun Jun 13 13:52:50 1999 +0200
@@ -34,8 +34,9 @@
   component :: ['a program, 'a program] => bool     (infixl 50)
    "F component H == EX G. F Join G = H"
 
-  guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
-   "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
+  guarantees :: ['a program set, 'a program set] => 'a program set
+                                                    (infixl "guar" 65)
+   "X guar Y == {F. ALL H. F component H --> H:X --> H:Y}"
 
   refines :: ['a program, 'a program, 'a program set] => bool
 			("(3_ refines _ wrt _)" [10,10,10] 10)
diff -r 350f27e2d649 -r 8932f33259d4 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Sun Jun 13 13:52:26 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Sun Jun 13 13:52:50 1999 +0200
@@ -367,15 +367,13 @@
     (simpset() addsimps [Acts_Join, image_Un, image_compose RS sym, o_def]) 1);
 qed "extend_Join_eq_extend_D";
 
-Goal "F : X guarantees Y \
-\     ==> extend h F : (extend h `` X) guarantees (extend h `` Y)";
+Goal "F : X guar Y ==> extend h F : (extend h `` X) guar (extend h `` Y)";
 by (rtac guaranteesI 1);
 by Auto_tac;
 by (blast_tac (claset() addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
 qed "guarantees_imp_extend_guarantees";
 
-Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
-\     ==> F : X guarantees Y";
+Goal "extend h F : (extend h `` X) guar (extend h `` Y) ==> F : X guar Y";
 by (rtac guaranteesI 1);
 by (rewrite_goals_tac [guarantees_def, component_def]);
 by Auto_tac;
@@ -386,8 +384,7 @@
 by Auto_tac;
 qed "extend_guarantees_imp_guarantees";
 
-Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) \
-\     = (F : X guarantees Y)";
+Goal "(extend h F : (extend h `` X) guar (extend h `` Y)) = (F : X guar Y)";
 by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
 			       extend_guarantees_imp_guarantees]) 1);
 qed "extend_guarantees_eq";