*** empty log message ***
authorehmety
Fri Mar 02 13:18:56 2001 +0100 (2001-03-02)
changeset 1119044e157622cb2
parent 11189 1ea763a5d186
child 11191 a9d7b050b74a
*** empty log message ***
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/Guar.thy
     1.1 --- a/src/HOL/UNITY/Comp.ML	Fri Mar 02 13:18:31 2001 +0100
     1.2 +++ b/src/HOL/UNITY/Comp.ML	Fri Mar 02 13:18:56 2001 +0100
     1.3 @@ -4,12 +4,12 @@
     1.4      Copyright   1998  University of Cambridge
     1.5  
     1.6  Composition
     1.7 +From Chandy and Sanders, "Reasoning About Program Composition"
     1.8  
     1.9 -From Chandy and Sanders, "Reasoning About Program Composition"
    1.10 +Revised by Sidi Ehmety on January 2001
    1.11 +
    1.12  *)
    1.13 -
    1.14 -(*** component ***)
    1.15 -
    1.16 +(*** component <= ***)
    1.17  Goalw [component_def]
    1.18       "H <= F | H <= G ==> H <= (F Join G)";
    1.19  by Auto_tac;
    1.20 @@ -214,3 +214,50 @@
    1.21  by (Blast_tac 1);
    1.22  qed "Increasing_preserves_Stable";
    1.23  
    1.24 +(** component_of **)
    1.25 +
    1.26 +(*  component_of is stronger than <= *)
    1.27 +Goalw [component_def, component_of_def]
    1.28 +"F component_of H ==> F <= H";
    1.29 +by (Blast_tac 1);
    1.30 +qed "component_of_imp_component";
    1.31 +
    1.32 +
    1.33 +(* component_of satisfies many of the <='s properties *)
    1.34 +Goalw [component_of_def]
    1.35 +"F component_of F";
    1.36 +by (res_inst_tac [("x", "SKIP")] exI 1);
    1.37 +by Auto_tac;
    1.38 +qed "component_of_refl";
    1.39 +
    1.40 +Goalw [component_of_def]
    1.41 +"SKIP component_of F";
    1.42 +by Auto_tac;
    1.43 +qed "component_of_SKIP";
    1.44 +
    1.45 +Addsimps [component_of_refl, component_of_SKIP];
    1.46 +
    1.47 +Goalw [component_of_def]
    1.48 +"[| F component_of G; G component_of H |] ==> F component_of H";
    1.49 +by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
    1.50 +qed "component_of_trans";
    1.51 +
    1.52 +bind_thm ("strict_component_of_eq", strict_component_of_def RS meta_eq_to_obj_eq);
    1.53 +
    1.54 +(** localize **)
    1.55 +Goalw [localize_def]
    1.56 + "Init (localize v F) = Init F";
    1.57 +by (Simp_tac 1);
    1.58 +qed "localize_Init_eq";
    1.59 +
    1.60 +Goalw [localize_def]
    1.61 + "Acts (localize v F) = Acts F";
    1.62 +by (Simp_tac 1);
    1.63 +qed "localize_Acts_eq";
    1.64 +
    1.65 +Goalw [localize_def]
    1.66 + "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)";
    1.67 +by Auto_tac;
    1.68 +qed "localize_AllowedActs_eq";
    1.69 +
    1.70 +Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];
     2.1 --- a/src/HOL/UNITY/Comp.thy	Fri Mar 02 13:18:31 2001 +0100
     2.2 +++ b/src/HOL/UNITY/Comp.thy	Fri Mar 02 13:18:56 2001 +0100
     2.3 @@ -4,8 +4,13 @@
     2.4      Copyright   1998  University of Cambridge
     2.5  
     2.6  Composition
     2.7 +From Chandy and Sanders, "Reasoning About Program Composition",
     2.8 +Technical Report 2000-003, University of Florida, 2000.
     2.9  
    2.10 -From Chandy and Sanders, "Reasoning About Program Composition"
    2.11 +Revised by Sidi Ehmety on January  2001 
    2.12 +
    2.13 +Added: a strong form of the <= relation (component_of) and localize 
    2.14 +
    2.15  *)
    2.16  
    2.17  Comp = Union +
    2.18 @@ -14,16 +19,26 @@
    2.19    program :: (term)ord
    2.20  
    2.21  defs
    2.22 -
    2.23    component_def   "F <= H == EX G. F Join G = H"
    2.24 -
    2.25    strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
    2.26  
    2.27 +
    2.28  constdefs
    2.29 +  component_of :: "'a program=>'a program=> bool"
    2.30 +                                    (infixl "component'_of" 50)
    2.31 +  "F component_of H == EX G. F ok G & F Join G = H"
    2.32 +
    2.33 +  strict_component_of :: "'a program\\<Rightarrow>'a program=> bool"
    2.34 +                                    (infixl "strict'_component'_of" 50)
    2.35 +  "F strict_component_of H == F component_of H & F~=H"
    2.36 +  
    2.37    preserves :: "('a=>'b) => 'a program set"
    2.38      "preserves v == INT z. stable {s. v s = z}"
    2.39  
    2.40 +  localize  :: "('a=>'b) => 'a program => 'a program"
    2.41 +  "localize v F == mk_program(Init F, Acts F,
    2.42 +			      AllowedActs F Int (UN G:preserves v. Acts G))"
    2.43 +
    2.44    funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
    2.45 -    "funPair f g == %x. (f x, g x)"
    2.46 -
    2.47 +  "funPair f g == %x. (f x, g x)"
    2.48  end
     3.1 --- a/src/HOL/UNITY/Guar.ML	Fri Mar 02 13:18:31 2001 +0100
     3.2 +++ b/src/HOL/UNITY/Guar.ML	Fri Mar 02 13:18:56 2001 +0100
     3.3 @@ -6,62 +6,76 @@
     3.4  Guarantees, etc.
     3.5  
     3.6  From Chandy and Sanders, "Reasoning About Program Composition"
     3.7 +Revised by Sidi Ehmety on January 2001
     3.8  *)
     3.9  
    3.10 +Goal "(OK (insert i I) F) = (if i:I then OK I F else OK I F & (F i ok JOIN I F))";
    3.11 +by (auto_tac (claset() addIs [ok_sym], 
    3.12 +              simpset() addsimps [OK_iff_ok]));
    3.13 +qed "OK_insert_iff";
    3.14 +
    3.15 +
    3.16 +
    3.17  (*** existential properties ***)
    3.18 -
    3.19  Goalw [ex_prop_def]
    3.20 -     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
    3.21 + "[| ex_prop X; finite GG |] ==> \
    3.22 +\    GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X";
    3.23  by (etac finite_induct 1);
    3.24 -by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
    3.25 +by (auto_tac (claset(), simpset() addsimps [OK_insert_iff,Int_insert_left]));
    3.26  qed_spec_mp "ex1";
    3.27  
    3.28 +
    3.29  Goalw [ex_prop_def]
    3.30 -     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
    3.31 +     "ALL GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X ==> ex_prop X";
    3.32  by (Clarify_tac 1);
    3.33  by (dres_inst_tac [("x", "{F,G}")] spec 1);
    3.34 -by Auto_tac;
    3.35 +by (auto_tac (claset() addDs [ok_sym], 
    3.36 +              simpset() addsimps [OK_iff_ok]));
    3.37  qed "ex2";
    3.38  
    3.39 +
    3.40  (*Chandy & Sanders take this as a definition*)
    3.41 -Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
    3.42 +Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)";
    3.43  by (blast_tac (claset() addIs [ex1,ex2]) 1);
    3.44  qed "ex_prop_finite";
    3.45  
    3.46 +
    3.47  (*Their "equivalent definition" given at the end of section 3*)
    3.48 -Goal "ex_prop X = (ALL G. G:X = (ALL H. G <= H --> H: X))";
    3.49 +Goal
    3.50 + "ex_prop X = (ALL G. G:X = (ALL H. (G component_of H) --> H: X))";
    3.51  by Auto_tac;
    3.52 -by (rewrite_goals_tac [ex_prop_def, component_def]);
    3.53 -by (Blast_tac 1);
    3.54 +by (rewrite_goals_tac 
    3.55 +          [ex_prop_def, component_of_def]);
    3.56  by Safe_tac;
    3.57 -by (stac Join_commute 2);
    3.58 -by (ALLGOALS Blast_tac);
    3.59 +by (stac Join_commute 3);
    3.60 +by (dtac  ok_sym 3);
    3.61 +by (REPEAT(Blast_tac 1));
    3.62  qed "ex_prop_equiv";
    3.63  
    3.64  
    3.65  (*** universal properties ***)
    3.66 -
    3.67  Goalw [uv_prop_def]
    3.68 -     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
    3.69 +     "[| uv_prop X; finite GG |] ==>  \
    3.70 +\  GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X";
    3.71  by (etac finite_induct 1);
    3.72 -by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
    3.73 +by (auto_tac (claset(), simpset() addsimps 
    3.74 +           [Int_insert_left, OK_insert_iff]));
    3.75  qed_spec_mp "uv1";
    3.76  
    3.77  Goalw [uv_prop_def]
    3.78 -     "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X  ==> uv_prop X";
    3.79 +     "ALL GG. finite GG & GG <= X & OK GG (%G. G)-->(JN G:GG. G):X  ==> uv_prop X";
    3.80  by (rtac conjI 1);
    3.81  by (Clarify_tac 2);
    3.82  by (dres_inst_tac [("x", "{F,G}")] spec 2);
    3.83  by (dres_inst_tac [("x", "{}")] spec 1);
    3.84 -by Auto_tac;
    3.85 +by (auto_tac (claset() addDs [ok_sym], simpset() addsimps [OK_iff_ok]));
    3.86  qed "uv2";
    3.87  
    3.88  (*Chandy & Sanders take this as a definition*)
    3.89 -Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
    3.90 +Goal "uv_prop X = (ALL GG. finite GG & GG <= X & OK GG (%G. G)--> (JN G:GG. G): X)";
    3.91  by (blast_tac (claset() addIs [uv1,uv2]) 1);
    3.92  qed "uv_prop_finite";
    3.93  
    3.94 -
    3.95  (*** guarantees ***)
    3.96  
    3.97  val prems = Goal
    3.98 @@ -99,12 +113,35 @@
    3.99  by (Blast_tac 1);
   3.100  qed "subset_imp_guarantees";
   3.101  
   3.102 -(*Remark at end of section 4.1
   3.103 -Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
   3.104 +(*Remark at end of section 4.1 *)
   3.105 +
   3.106 +Goalw [guar_def] "ex_prop Y ==> (Y = UNIV guarantees Y)";
   3.107 +by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   3.108 +by Safe_tac;
   3.109 +by (dres_inst_tac [("x", "x")] spec 1);
   3.110 +by (dres_inst_tac [("x", "x")] spec 2);
   3.111 +by (dtac sym 2);
   3.112 +by (ALLGOALS(etac iffE));
   3.113 +by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
   3.114 +by (REPEAT(Blast_tac 1));
   3.115 +qed "ex_prop_imp";
   3.116 +
   3.117 +Goalw [guar_def] "(Y = UNIV guarantees Y) ==> ex_prop(Y)";
   3.118  by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   3.119 -by (blast_tac (claset() addEs [equalityE]) 1);
   3.120 +by Safe_tac;
   3.121 +by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
   3.122 +by (dtac sym 2);
   3.123 +by (ALLGOALS(etac equalityE));
   3.124 +by (REPEAT(Blast_tac 1));
   3.125 +qed "guarantees_imp";
   3.126 +
   3.127 +Goal "(ex_prop Y) = (Y = UNIV guarantees Y)";
   3.128 +by (rtac iffI 1);
   3.129 +by (rtac ex_prop_imp 1);
   3.130 +by (rtac guarantees_imp 2);
   3.131 +by (ALLGOALS(Asm_simp_tac));
   3.132  qed "ex_prop_equiv2";
   3.133 -*)
   3.134 +
   3.135  
   3.136  (** Distributive laws.  Re-orient to perform miniscoping **)
   3.137  
   3.138 @@ -177,6 +214,7 @@
   3.139  by (Blast_tac 1);
   3.140  qed "ex_guarantees";
   3.141  
   3.142 +
   3.143  (*** Additional guarantees laws, by lcp ***)
   3.144  
   3.145  Goalw [guar_def]
   3.146 @@ -279,20 +317,23 @@
   3.147  by (Blast_tac 1);
   3.148  qed "refines_refl";
   3.149  
   3.150 -Goalw [refines_def]
   3.151 -     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X";
   3.152 +(* Goalw [refines_def]
   3.153 +     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X"; 
   3.154  by Auto_tac;
   3.155 -qed "refines_trans";
   3.156 +qed "refines_trans"; *)
   3.157 +
   3.158 +
   3.159  
   3.160  Goalw [strict_ex_prop_def]
   3.161       "strict_ex_prop X \
   3.162 -\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   3.163 -by (Blast_tac 1);
   3.164 +\     ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) \
   3.165 +\             = (F:X --> G:X)";
   3.166 +by Auto_tac;
   3.167  qed "strict_ex_refine_lemma";
   3.168  
   3.169  Goalw [strict_ex_prop_def]
   3.170       "strict_ex_prop X \
   3.171 -\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
   3.172 +\     ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
   3.173  \         (F: welldef Int X --> G:X)";
   3.174  by Safe_tac;
   3.175  by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   3.176 @@ -300,7 +341,7 @@
   3.177  qed "strict_ex_refine_lemma_v";
   3.178  
   3.179  Goal "[| strict_ex_prop X;  \
   3.180 -\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
   3.181 +\        ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
   3.182  \     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   3.183  by (res_inst_tac [("x","SKIP")] allE 1
   3.184      THEN assume_tac 1);
   3.185 @@ -312,13 +353,13 @@
   3.186  
   3.187  Goalw [strict_uv_prop_def]
   3.188       "strict_uv_prop X \
   3.189 -\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   3.190 +\     ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)";
   3.191  by (Blast_tac 1);
   3.192  qed "strict_uv_refine_lemma";
   3.193  
   3.194  Goalw [strict_uv_prop_def]
   3.195       "strict_uv_prop X \
   3.196 -\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
   3.197 +\     ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
   3.198  \         (F: welldef Int X --> G:X)";
   3.199  by Safe_tac;
   3.200  by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   3.201 @@ -327,10 +368,165 @@
   3.202  qed "strict_uv_refine_lemma_v";
   3.203  
   3.204  Goal "[| strict_uv_prop X;  \
   3.205 -\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
   3.206 +\        ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
   3.207  \     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   3.208  by (res_inst_tac [("x","SKIP")] allE 1
   3.209      THEN assume_tac 1);
   3.210  by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
   3.211  					   strict_uv_refine_lemma_v]) 1);
   3.212  qed "uv_refinement_thm";
   3.213 +
   3.214 +(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
   3.215 +Goalw [guar_def, component_of_def]
   3.216 +"(F:X guarantees Y) = (ALL H. H:X \\<longrightarrow> (F component_of H \\<longrightarrow> H:Y))";
   3.217 +by Auto_tac;
   3.218 +qed "guarantees_equiv";
   3.219 +
   3.220 +Goalw [wg_def] "!!X. F:(X guarantees Y) ==> X <= (wg F Y)";
   3.221 +by Auto_tac;
   3.222 +qed "wg_weakest";
   3.223 +
   3.224 +Goalw [wg_def, guar_def] "F:((wg F Y) guarantees Y)";
   3.225 +by (Blast_tac 1);
   3.226 +qed "wg_guarantees";
   3.227 +
   3.228 +Goalw [wg_def]
   3.229 +  "(H: wg F X) = (F component_of H --> H:X)";
   3.230 +by (simp_tac (simpset() addsimps [guarantees_equiv]) 1);
   3.231 +by (rtac iffI 1);
   3.232 +by (res_inst_tac [("x", "{H}")] exI 2);
   3.233 +by (REPEAT(Blast_tac 1));
   3.234 +qed "wg_equiv";
   3.235 +
   3.236 +
   3.237 +Goal
   3.238 +"F component_of H ==> (H:wg F X) = (H:X)";
   3.239 +by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1);
   3.240 +qed "component_of_wg";
   3.241 +
   3.242 +
   3.243 +Goal
   3.244 +"ALL FF. finite FF & FF Int X ~= {} --> OK FF (%F. F) \
   3.245 +\  --> (ALL F:FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))";
   3.246 +by (Clarify_tac 1);
   3.247 +by (subgoal_tac "F component_of (JN F:FF. F)" 1);
   3.248 +by (dres_inst_tac [("X", "X")] component_of_wg 1);
   3.249 +by (Asm_full_simp_tac 1);
   3.250 +by (asm_full_simp_tac (simpset() addsimps [component_of_def]) 1);
   3.251 +by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1);
   3.252 +by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym], 
   3.253 +              simpset() addsimps [OK_iff_ok]));
   3.254 +qed "wg_finite";
   3.255 +
   3.256 +Goal "ex_prop X ==> (F:X) = (ALL H. H : wg F X)";
   3.257 +by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1);
   3.258 +by (Blast_tac 1);
   3.259 +qed "wg_ex_prop";
   3.260 +
   3.261 +(** From Charpentier and Chandy "Theorems About Composition" **)
   3.262 +(* Proposition 2 *)
   3.263 +Goalw [wx_def] "(wx X)<=X";
   3.264 +by Auto_tac;
   3.265 +qed "wx_subset";
   3.266 +
   3.267 +Goalw [wx_def]
   3.268 +"ex_prop (wx X)";
   3.269 +by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   3.270 +by Safe_tac;
   3.271 +by (Blast_tac 1);
   3.272 +by Auto_tac;
   3.273 +qed "wx_ex_prop";
   3.274 +
   3.275 +Goalw [wx_def]
   3.276 +"ALL Z. Z<= X --> ex_prop Z --> Z <= wx X";
   3.277 +by Auto_tac;
   3.278 +qed "wx_weakest";
   3.279 +
   3.280 +
   3.281 +(* Proposition 6 *)
   3.282 +Goalw [ex_prop_def]
   3.283 + "ex_prop({F. ALL G. F ok G --> F Join G:X})";
   3.284 +by Safe_tac;
   3.285 +by (dres_inst_tac [("x", "G Join Ga")] spec 1);
   3.286 +by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1);
   3.287 +by (dres_inst_tac [("x", "F Join Ga")] spec 1);
   3.288 +by (full_simp_tac (simpset() addsimps [ok_Join_iff1]) 1);
   3.289 +by Safe_tac;
   3.290 +by (asm_simp_tac (simpset() addsimps [ok_commute]) 1);
   3.291 +by (subgoal_tac "F Join G = G Join F" 1);
   3.292 +by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1);
   3.293 +by (simp_tac (simpset() addsimps [Join_commute]) 1);
   3.294 +qed "wx'_ex_prop";
   3.295 +
   3.296 +(* Equivalence with the other definition of wx *)
   3.297 +
   3.298 +Goalw [wx_def]
   3.299 + "wx X = {F. ALL G. F ok G --> (F Join G):X}";
   3.300 +by Safe_tac;
   3.301 +by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1);
   3.302 +by (dres_inst_tac [("x", "x")] spec 1);
   3.303 +by (dres_inst_tac [("x", "G")] spec 1);
   3.304 +by (forw_inst_tac [("c", "x Join G")] subsetD 1);
   3.305 +by Safe_tac;
   3.306 +by (Simp_tac 1);
   3.307 +by (res_inst_tac [("x", "{F. ALL G. F ok G --> F Join G:X}")] exI 1);
   3.308 +by Safe_tac;
   3.309 +by (rtac wx'_ex_prop 2);
   3.310 +by (rotate_tac 1 1);
   3.311 +by (dres_inst_tac [("x", "SKIP")] spec 1);
   3.312 +by Auto_tac;
   3.313 +qed "wx_equiv";
   3.314 +
   3.315 +
   3.316 +(* Propositions 7 to 11 are about this second definition of wx. And
   3.317 +   they are the same as the ones proved for the first definition of wx by equivalence *)
   3.318 +   
   3.319 +(* Proposition 12 *)
   3.320 +(* Main result of the paper *)
   3.321 +Goalw [guar_def] 
   3.322 +   "(X guarantees Y) = wx(-X Un Y)";
   3.323 +by (simp_tac (simpset() addsimps [wx_equiv]) 1);
   3.324 +qed "guarantees_wx_eq";
   3.325 +
   3.326 +(* {* Corollary, but this result has already been proved elsewhere *}
   3.327 + "ex_prop(X guarantees Y)";
   3.328 +  by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
   3.329 +  qed "guarantees_ex_prop";
   3.330 +*)
   3.331 +
   3.332 +(* Rules given in section 7 of Chandy and Sander's
   3.333 +    Reasoning About Program composition paper *)
   3.334 +
   3.335 +Goal "Init F <= A ==> F:(stable A) guarantees (Always A)";
   3.336 +by (rtac guaranteesI 1);
   3.337 +by (simp_tac (simpset() addsimps [Join_commute]) 1);
   3.338 +by (rtac stable_Join_Always1 1);
   3.339 +by (ALLGOALS(asm_full_simp_tac (simpset() 
   3.340 +     addsimps [invariant_def, Join_stable])));
   3.341 +qed "stable_guarantees_Always";
   3.342 +
   3.343 +(* To be moved to WFair.ML *)
   3.344 +Goal "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B";
   3.345 +by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1);
   3.346 +by (dres_inst_tac [("B", "A-B")] transient_strengthen 2);
   3.347 +by (rtac (ensuresI RS leadsTo_Basis) 3);
   3.348 +by (ALLGOALS(Blast_tac));
   3.349 +qed "leadsTo_Basis'";
   3.350 +
   3.351 +
   3.352 +
   3.353 +Goal "F:transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))";
   3.354 +by (rtac guaranteesI 1);
   3.355 +by (rtac leadsTo_Basis' 1);
   3.356 +by (dtac constrains_weaken_R 1);
   3.357 +by (assume_tac 2);
   3.358 +by (Blast_tac 1);
   3.359 +by (blast_tac (claset() addIs [Join_transient_I1]) 1);
   3.360 +qed "constrains_guarantees_leadsTo";
   3.361 +
   3.362 +
   3.363 +
   3.364 +
   3.365 +
   3.366 +
   3.367 +
     4.1 --- a/src/HOL/UNITY/Guar.thy	Fri Mar 02 13:18:31 2001 +0100
     4.2 +++ b/src/HOL/UNITY/Guar.thy	Fri Mar 02 13:18:56 2001 +0100
     4.3 @@ -5,7 +5,17 @@
     4.4  
     4.5  Guarantees, etc.
     4.6  
     4.7 -From Chandy and Sanders, "Reasoning About Program Composition"
     4.8 +From Chandy and Sanders, "Reasoning About Program Composition",
     4.9 +Technical Report 2000-003, University of Florida, 2000.
    4.10 +
    4.11 +Revised by Sidi Ehmety on January 2001
    4.12 +
    4.13 +Added: Compatibility, weakest guarantees, etc.
    4.14 +
    4.15 +and Weakest existential property,
    4.16 +from Charpentier and Chandy "Theorems about Composition",
    4.17 +Fifth International Conference on Mathematics of Program, 2000.
    4.18 +
    4.19  *)
    4.20  
    4.21  Guar = Comp +
    4.22 @@ -20,33 +30,42 @@
    4.23      case, proving equivalence with Chandy and Sanders's n-ary definitions*)
    4.24  
    4.25    ex_prop  :: 'a program set => bool
    4.26 -   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
    4.27 +   "ex_prop X == ALL F G. F ok G -->F:X | G: X --> (F Join G) : X"
    4.28  
    4.29    strict_ex_prop  :: 'a program set => bool
    4.30 -   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
    4.31 +   "strict_ex_prop X == ALL F G.  F ok G --> (F:X | G: X) = (F Join G : X)"
    4.32  
    4.33    uv_prop  :: 'a program set => bool
    4.34 -   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
    4.35 +   "uv_prop X == SKIP : X & (ALL F G. F ok G --> F:X & G: X --> (F Join G) : X)"
    4.36  
    4.37    strict_uv_prop  :: 'a program set => bool
    4.38 -   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
    4.39 -
    4.40 -  (*Ill-defined programs can arise through "Join"*)
    4.41 -  welldef :: 'a program set  
    4.42 -   "welldef == {F. Init F ~= {}}"
    4.43 +   "strict_uv_prop X == SKIP : X & (ALL F G. F ok G -->(F:X & G: X) = (F Join G : X))"
    4.44  
    4.45    guar :: ['a program set, 'a program set] => 'a program set
    4.46            (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
    4.47     "X guarantees Y == {F. ALL G. F ok G --> F Join G : X --> F Join G : Y}"
    4.48 +  
    4.49  
    4.50 +  (* Weakest guarantees *)
    4.51 +   wg :: ['a program, 'a program set] =>  'a program set
    4.52 +  "wg F Y == Union({X. F:X guarantees Y})"
    4.53 +
    4.54 +   (* Weakest existential property stronger than X *)
    4.55 +   wx :: "('a program) set => ('a program)set"
    4.56 +   "wx X == Union({Y. Y<=X & ex_prop Y})"
    4.57 +  
    4.58 +  (*Ill-defined programs can arise through "Join"*)
    4.59 +  welldef :: 'a program set  
    4.60 +  "welldef == {F. Init F ~= {}}"
    4.61 +  
    4.62    refines :: ['a program, 'a program, 'a program set] => bool
    4.63  			("(3_ refines _ wrt _)" [10,10,10] 10)
    4.64 -   "G refines F wrt X ==
    4.65 -      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
    4.66 +  "G refines F wrt X ==
    4.67 +   ALL H. (F ok H  & G ok H & F Join H:welldef Int X) --> (G Join H:welldef Int X)"
    4.68  
    4.69    iso_refines :: ['a program, 'a program, 'a program set] => bool
    4.70 -			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
    4.71 -   "G iso_refines F wrt X ==
    4.72 -      F : welldef Int X --> G : welldef Int X"
    4.73 +                              ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
    4.74 +  "G iso_refines F wrt X ==
    4.75 +   F : welldef Int X --> G : welldef Int X"
    4.76  
    4.77  end