guarantees -> guar
authorpaulson
Sun Jun 13 13:52:50 1999 +0200 (1999-06-13)
changeset 68228932f33259d4
parent 6821 350f27e2d649
child 6823 97babc436a41
guarantees -> guar
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Extend.ML
     1.1 --- a/src/HOL/UNITY/Comp.ML	Sun Jun 13 13:52:26 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.ML	Sun Jun 13 13:52:50 1999 +0200
     1.3 @@ -111,42 +111,54 @@
     1.4  (*** guarantees ***)
     1.5  
     1.6  (*This equation is more intuitive than the official definition*)
     1.7 -Goal "(F : X guarantees Y) = \
     1.8 +Goal "(F : X guar Y) = \
     1.9  \     (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
    1.10  by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
    1.11  by (Blast_tac 1);
    1.12  qed "guarantees_eq";
    1.13  
    1.14 -Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
    1.15 +Goalw [guarantees_def] "X <= Y ==> X guar Y = UNIV";
    1.16  by (Blast_tac 1);
    1.17  qed "subset_imp_guarantees_UNIV";
    1.18  
    1.19  (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
    1.20 -Goalw [guarantees_def] "X <= Y ==> F : X guarantees Y";
    1.21 +Goalw [guarantees_def] "X <= Y ==> F : X guar Y";
    1.22  by (Blast_tac 1);
    1.23  qed "subset_imp_guarantees";
    1.24  
    1.25  (*Remark at end of section 4.1*)
    1.26 -Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guarantees Y)";
    1.27 +Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guar Y)";
    1.28  by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
    1.29  by (blast_tac (claset() addEs [equalityE]) 1);
    1.30  qed "ex_prop_equiv2";
    1.31  
    1.32 +(** Distributive laws.  Re-orient to perform miniscoping **)
    1.33 +
    1.34  Goalw [guarantees_def]
    1.35 -     "(INT X:XX. X guarantees Y) = (UN X:XX. X) guarantees Y";
    1.36 +     "(UN X:XX. X) guar Y = (INT X:XX. X guar Y)";
    1.37  by (Blast_tac 1);
    1.38 -qed "INT_guarantees_left";
    1.39 +qed "guarantees_UN_left";
    1.40  
    1.41  Goalw [guarantees_def]
    1.42 -     "(INT Y:YY. X guarantees Y) = X guarantees (INT Y:YY. Y)";
    1.43 +    "(X Un Y) guar Z = (X guar Z) Int (Y guar Z)";
    1.44 +by (Blast_tac 1);
    1.45 +qed "guarantees_Un_left";
    1.46 +
    1.47 +Goalw [guarantees_def]
    1.48 +     "X guar (INT Y:YY. Y) = (INT Y:YY. X guar Y)";
    1.49  by (Blast_tac 1);
    1.50 -qed "INT_guarantees_right";
    1.51 +qed "guarantees_INT_right";
    1.52  
    1.53 -Goalw [guarantees_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
    1.54 +Goalw [guarantees_def]
    1.55 +    "Z guar (X Int Y) = (Z guar X) Int (Z guar Y)";
    1.56 +by (Blast_tac 1);
    1.57 +qed "guarantees_Int_right";
    1.58 +
    1.59 +Goalw [guarantees_def] "(X guar Y) = (UNIV guar (-X Un Y))";
    1.60  by (Blast_tac 1);
    1.61  qed "shunting";
    1.62  
    1.63 -Goalw [guarantees_def] "(X guarantees Y) = -Y guarantees -X";
    1.64 +Goalw [guarantees_def] "(X guar Y) = -Y guar -X";
    1.65  by (Blast_tac 1);
    1.66  qed "contrapositive";
    1.67  
    1.68 @@ -155,41 +167,41 @@
    1.69  **)
    1.70  
    1.71  Goalw [guarantees_def]
    1.72 -    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
    1.73 -\    ==> F : (V Int Y) guarantees Z";
    1.74 +    "[| F : V guar X;  F : (X Int Y) guar Z |]\
    1.75 +\    ==> F : (V Int Y) guar Z";
    1.76  by (Blast_tac 1);
    1.77  qed "combining1";
    1.78  
    1.79  Goalw [guarantees_def]
    1.80 -    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
    1.81 -\    ==> F : V guarantees (X Un Z)";
    1.82 +    "[| F : V guar (X Un Y);  F : Y guar Z |]\
    1.83 +\    ==> F : V guar (X Un Z)";
    1.84  by (Blast_tac 1);
    1.85  qed "combining2";
    1.86  
    1.87  (** The following two follow Chandy-Sanders, but the use of object-quantifiers
    1.88      does not suit Isabelle... **)
    1.89  
    1.90 -(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
    1.91 +(*Premise should be (!!i. i: I ==> F: X guar Y i) *)
    1.92  Goalw [guarantees_def]
    1.93 -     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
    1.94 +     "ALL i:I. F : X guar (Y i) ==> F : X guar (INT i:I. Y i)";
    1.95  by (Blast_tac 1);
    1.96  qed "all_guarantees";
    1.97  
    1.98 -(*Premises should be [| F: X guarantees Y i; i: I |] *)
    1.99 +(*Premises should be [| F: X guar Y i; i: I |] *)
   1.100  Goalw [guarantees_def]
   1.101 -     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
   1.102 +     "EX i:I. F : X guar (Y i) ==> F : X guar (UN i:I. Y i)";
   1.103  by (Blast_tac 1);
   1.104  qed "ex_guarantees";
   1.105  
   1.106  val prems = Goal
   1.107       "(!!G. [| F Join G : X;  Disjoint F G |] ==> F Join G : Y) \
   1.108 -\     ==> F : X guarantees Y";
   1.109 +\     ==> F : X guar Y";
   1.110  by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
   1.111  by (blast_tac (claset() addIs prems) 1);
   1.112  qed "guaranteesI";
   1.113  
   1.114  Goalw [guarantees_def, component_def]
   1.115 -     "[| F : X guarantees Y;  F Join G : X |] ==> F Join G : Y";
   1.116 +     "[| F : X guar Y;  F Join G : X |] ==> F Join G : Y";
   1.117  by (Blast_tac 1);
   1.118  qed "guaranteesD";
   1.119  
     2.1 --- a/src/HOL/UNITY/Comp.thy	Sun Jun 13 13:52:26 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Comp.thy	Sun Jun 13 13:52:50 1999 +0200
     2.3 @@ -34,8 +34,9 @@
     2.4    component :: ['a program, 'a program] => bool     (infixl 50)
     2.5     "F component H == EX G. F Join G = H"
     2.6  
     2.7 -  guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
     2.8 -   "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
     2.9 +  guarantees :: ['a program set, 'a program set] => 'a program set
    2.10 +                                                    (infixl "guar" 65)
    2.11 +   "X guar Y == {F. ALL H. F component H --> H:X --> H:Y}"
    2.12  
    2.13    refines :: ['a program, 'a program, 'a program set] => bool
    2.14  			("(3_ refines _ wrt _)" [10,10,10] 10)
     3.1 --- a/src/HOL/UNITY/Extend.ML	Sun Jun 13 13:52:26 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Extend.ML	Sun Jun 13 13:52:50 1999 +0200
     3.3 @@ -367,15 +367,13 @@
     3.4      (simpset() addsimps [Acts_Join, image_Un, image_compose RS sym, o_def]) 1);
     3.5  qed "extend_Join_eq_extend_D";
     3.6  
     3.7 -Goal "F : X guarantees Y \
     3.8 -\     ==> extend h F : (extend h `` X) guarantees (extend h `` Y)";
     3.9 +Goal "F : X guar Y ==> extend h F : (extend h `` X) guar (extend h `` Y)";
    3.10  by (rtac guaranteesI 1);
    3.11  by Auto_tac;
    3.12  by (blast_tac (claset() addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
    3.13  qed "guarantees_imp_extend_guarantees";
    3.14  
    3.15 -Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
    3.16 -\     ==> F : X guarantees Y";
    3.17 +Goal "extend h F : (extend h `` X) guar (extend h `` Y) ==> F : X guar Y";
    3.18  by (rtac guaranteesI 1);
    3.19  by (rewrite_goals_tac [guarantees_def, component_def]);
    3.20  by Auto_tac;
    3.21 @@ -386,8 +384,7 @@
    3.22  by Auto_tac;
    3.23  qed "extend_guarantees_imp_guarantees";
    3.24  
    3.25 -Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) \
    3.26 -\     = (F : X guarantees Y)";
    3.27 +Goal "(extend h F : (extend h `` X) guar (extend h `` Y)) = (F : X guar Y)";
    3.28  by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
    3.29  			       extend_guarantees_imp_guarantees]) 1);
    3.30  qed "extend_guarantees_eq";