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 +Goalw [ex_prop_def]
3.19 + "[| ex_prop X; finite GG |] ==> \
3.20 +\ GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X";
3.21 +by (etac finite_induct 1);
3.22 +by (auto_tac (claset(), simpset() addsimps [OK_insert_iff,Int_insert_left]));
3.23 +qed_spec_mp "ex1";
3.24 +
3.25
3.26 Goalw [ex_prop_def]
3.27 - "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
3.28 -by (etac finite_induct 1);
3.29 -by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
3.30 -qed_spec_mp "ex1";
3.31 -
3.32 -Goalw [ex_prop_def]
3.33 - "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
3.34 + "ALL GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X ==> ex_prop X";
3.35 by (Clarify_tac 1);
3.36 by (dres_inst_tac [("x", "{F,G}")] spec 1);
3.37 -by Auto_tac;
3.38 +by (auto_tac (claset() addDs [ok_sym],
3.39 + simpset() addsimps [OK_iff_ok]));
3.40 qed "ex2";
3.41
3.42 +
3.43 (*Chandy & Sanders take this as a definition*)
3.44 -Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
3.45 +Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)";
3.46 by (blast_tac (claset() addIs [ex1,ex2]) 1);
3.47 qed "ex_prop_finite";
3.48
3.49 +
3.50 (*Their "equivalent definition" given at the end of section 3*)
3.51 -Goal "ex_prop X = (ALL G. G:X = (ALL H. G <= H --> H: X))";
3.52 +Goal
3.53 + "ex_prop X = (ALL G. G:X = (ALL H. (G component_of H) --> H: X))";
3.54 by Auto_tac;
3.55 -by (rewrite_goals_tac [ex_prop_def, component_def]);
3.56 -by (Blast_tac 1);
3.57 +by (rewrite_goals_tac
3.58 + [ex_prop_def, component_of_def]);
3.59 by Safe_tac;
3.60 -by (stac Join_commute 2);
3.61 -by (ALLGOALS Blast_tac);
3.62 +by (stac Join_commute 3);
3.63 +by (dtac ok_sym 3);
3.64 +by (REPEAT(Blast_tac 1));
3.65 qed "ex_prop_equiv";
3.66
3.67
3.68 (*** universal properties ***)
3.69 -
3.70 Goalw [uv_prop_def]
3.71 - "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
3.72 + "[| uv_prop X; finite GG |] ==> \
3.73 +\ GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X";
3.74 by (etac finite_induct 1);
3.75 -by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
3.76 +by (auto_tac (claset(), simpset() addsimps
3.77 + [Int_insert_left, OK_insert_iff]));
3.78 qed_spec_mp "uv1";
3.79
3.80 Goalw [uv_prop_def]
3.81 - "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X ==> uv_prop X";
3.82 + "ALL GG. finite GG & GG <= X & OK GG (%G. G)-->(JN G:GG. G):X ==> uv_prop X";
3.83 by (rtac conjI 1);
3.84 by (Clarify_tac 2);
3.85 by (dres_inst_tac [("x", "{F,G}")] spec 2);
3.86 by (dres_inst_tac [("x", "{}")] spec 1);
3.87 -by Auto_tac;
3.88 +by (auto_tac (claset() addDs [ok_sym], simpset() addsimps [OK_iff_ok]));
3.89 qed "uv2";
3.90
3.91 (*Chandy & Sanders take this as a definition*)
3.92 -Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
3.93 +Goal "uv_prop X = (ALL GG. finite GG & GG <= X & OK GG (%G. G)--> (JN G:GG. G): X)";
3.94 by (blast_tac (claset() addIs [uv1,uv2]) 1);
3.95 qed "uv_prop_finite";
3.96
3.97 -
3.98 (*** guarantees ***)
3.99
3.100 val prems = Goal
3.101 @@ -99,12 +113,35 @@
3.102 by (Blast_tac 1);
3.103 qed "subset_imp_guarantees";
3.104
3.105 -(*Remark at end of section 4.1
3.106 -Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
3.107 +(*Remark at end of section 4.1 *)
3.108 +
3.109 +Goalw [guar_def] "ex_prop Y ==> (Y = UNIV guarantees Y)";
3.110 +by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
3.111 +by Safe_tac;
3.112 +by (dres_inst_tac [("x", "x")] spec 1);
3.113 +by (dres_inst_tac [("x", "x")] spec 2);
3.114 +by (dtac sym 2);
3.115 +by (ALLGOALS(etac iffE));
3.116 +by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
3.117 +by (REPEAT(Blast_tac 1));
3.118 +qed "ex_prop_imp";
3.119 +
3.120 +Goalw [guar_def] "(Y = UNIV guarantees Y) ==> ex_prop(Y)";
3.121 by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
3.122 -by (blast_tac (claset() addEs [equalityE]) 1);
3.123 +by Safe_tac;
3.124 +by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
3.125 +by (dtac sym 2);
3.126 +by (ALLGOALS(etac equalityE));
3.127 +by (REPEAT(Blast_tac 1));
3.128 +qed "guarantees_imp";
3.129 +
3.130 +Goal "(ex_prop Y) = (Y = UNIV guarantees Y)";
3.131 +by (rtac iffI 1);
3.132 +by (rtac ex_prop_imp 1);
3.133 +by (rtac guarantees_imp 2);
3.134 +by (ALLGOALS(Asm_simp_tac));
3.135 qed "ex_prop_equiv2";
3.136 -*)
3.137 +
3.138
3.139 (** Distributive laws. Re-orient to perform miniscoping **)
3.140
3.141 @@ -177,6 +214,7 @@
3.142 by (Blast_tac 1);
3.143 qed "ex_guarantees";
3.144
3.145 +
3.146 (*** Additional guarantees laws, by lcp ***)
3.147
3.148 Goalw [guar_def]
3.149 @@ -279,20 +317,23 @@
3.150 by (Blast_tac 1);
3.151 qed "refines_refl";
3.152
3.153 -Goalw [refines_def]
3.154 - "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X";
3.155 +(* Goalw [refines_def]
3.156 + "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X";
3.157 by Auto_tac;
3.158 -qed "refines_trans";
3.159 +qed "refines_trans"; *)
3.160 +
3.161 +
3.162
3.163 Goalw [strict_ex_prop_def]
3.164 "strict_ex_prop X \
3.165 -\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
3.166 -by (Blast_tac 1);
3.167 +\ ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) \
3.168 +\ = (F:X --> G:X)";
3.169 +by Auto_tac;
3.170 qed "strict_ex_refine_lemma";
3.171
3.172 Goalw [strict_ex_prop_def]
3.173 "strict_ex_prop X \
3.174 -\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
3.175 +\ ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
3.176 \ (F: welldef Int X --> G:X)";
3.177 by Safe_tac;
3.178 by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
3.179 @@ -300,7 +341,7 @@
3.180 qed "strict_ex_refine_lemma_v";
3.181
3.182 Goal "[| strict_ex_prop X; \
3.183 -\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
3.184 +\ ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
3.185 \ ==> (G refines F wrt X) = (G iso_refines F wrt X)";
3.186 by (res_inst_tac [("x","SKIP")] allE 1
3.187 THEN assume_tac 1);
3.188 @@ -312,13 +353,13 @@
3.189
3.190 Goalw [strict_uv_prop_def]
3.191 "strict_uv_prop X \
3.192 -\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
3.193 +\ ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)";
3.194 by (Blast_tac 1);
3.195 qed "strict_uv_refine_lemma";
3.196
3.197 Goalw [strict_uv_prop_def]
3.198 "strict_uv_prop X \
3.199 -\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
3.200 +\ ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
3.201 \ (F: welldef Int X --> G:X)";
3.202 by Safe_tac;
3.203 by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
3.204 @@ -327,10 +368,165 @@
3.205 qed "strict_uv_refine_lemma_v";
3.206
3.207 Goal "[| strict_uv_prop X; \
3.208 -\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
3.209 +\ ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
3.210 \ ==> (G refines F wrt X) = (G iso_refines F wrt X)";
3.211 by (res_inst_tac [("x","SKIP")] allE 1
3.212 THEN assume_tac 1);
3.213 by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
3.214 strict_uv_refine_lemma_v]) 1);
3.215 qed "uv_refinement_thm";
3.216 +
3.217 +(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
3.218 +Goalw [guar_def, component_of_def]
3.219 +"(F:X guarantees Y) = (ALL H. H:X \\<longrightarrow> (F component_of H \\<longrightarrow> H:Y))";
3.220 +by Auto_tac;
3.221 +qed "guarantees_equiv";
3.222 +
3.223 +Goalw [wg_def] "!!X. F:(X guarantees Y) ==> X <= (wg F Y)";
3.224 +by Auto_tac;
3.225 +qed "wg_weakest";
3.226 +
3.227 +Goalw [wg_def, guar_def] "F:((wg F Y) guarantees Y)";
3.228 +by (Blast_tac 1);
3.229 +qed "wg_guarantees";
3.230 +
3.231 +Goalw [wg_def]
3.232 + "(H: wg F X) = (F component_of H --> H:X)";
3.233 +by (simp_tac (simpset() addsimps [guarantees_equiv]) 1);
3.234 +by (rtac iffI 1);
3.235 +by (res_inst_tac [("x", "{H}")] exI 2);
3.236 +by (REPEAT(Blast_tac 1));
3.237 +qed "wg_equiv";
3.238 +
3.239 +
3.240 +Goal
3.241 +"F component_of H ==> (H:wg F X) = (H:X)";
3.242 +by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1);
3.243 +qed "component_of_wg";
3.244 +
3.245 +
3.246 +Goal
3.247 +"ALL FF. finite FF & FF Int X ~= {} --> OK FF (%F. F) \
3.248 +\ --> (ALL F:FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))";
3.249 +by (Clarify_tac 1);
3.250 +by (subgoal_tac "F component_of (JN F:FF. F)" 1);
3.251 +by (dres_inst_tac [("X", "X")] component_of_wg 1);
3.252 +by (Asm_full_simp_tac 1);
3.253 +by (asm_full_simp_tac (simpset() addsimps [component_of_def]) 1);
3.254 +by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1);
3.255 +by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym],
3.256 + simpset() addsimps [OK_iff_ok]));
3.257 +qed "wg_finite";
3.258 +
3.259 +Goal "ex_prop X ==> (F:X) = (ALL H. H : wg F X)";
3.260 +by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1);
3.261 +by (Blast_tac 1);
3.262 +qed "wg_ex_prop";
3.263 +
3.264 +(** From Charpentier and Chandy "Theorems About Composition" **)
3.265 +(* Proposition 2 *)
3.266 +Goalw [wx_def] "(wx X)<=X";
3.267 +by Auto_tac;
3.268 +qed "wx_subset";
3.269 +
3.270 +Goalw [wx_def]
3.271 +"ex_prop (wx X)";
3.272 +by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
3.273 +by Safe_tac;
3.274 +by (Blast_tac 1);
3.275 +by Auto_tac;
3.276 +qed "wx_ex_prop";
3.277 +
3.278 +Goalw [wx_def]
3.279 +"ALL Z. Z<= X --> ex_prop Z --> Z <= wx X";
3.280 +by Auto_tac;
3.281 +qed "wx_weakest";
3.282 +
3.283 +
3.284 +(* Proposition 6 *)
3.285 +Goalw [ex_prop_def]
3.286 + "ex_prop({F. ALL G. F ok G --> F Join G:X})";
3.287 +by Safe_tac;
3.288 +by (dres_inst_tac [("x", "G Join Ga")] spec 1);
3.289 +by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1);
3.290 +by (dres_inst_tac [("x", "F Join Ga")] spec 1);
3.291 +by (full_simp_tac (simpset() addsimps [ok_Join_iff1]) 1);
3.292 +by Safe_tac;
3.293 +by (asm_simp_tac (simpset() addsimps [ok_commute]) 1);
3.294 +by (subgoal_tac "F Join G = G Join F" 1);
3.295 +by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1);
3.296 +by (simp_tac (simpset() addsimps [Join_commute]) 1);
3.297 +qed "wx'_ex_prop";
3.298 +
3.299 +(* Equivalence with the other definition of wx *)
3.300 +
3.301 +Goalw [wx_def]
3.302 + "wx X = {F. ALL G. F ok G --> (F Join G):X}";
3.303 +by Safe_tac;
3.304 +by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1);
3.305 +by (dres_inst_tac [("x", "x")] spec 1);
3.306 +by (dres_inst_tac [("x", "G")] spec 1);
3.307 +by (forw_inst_tac [("c", "x Join G")] subsetD 1);
3.308 +by Safe_tac;
3.309 +by (Simp_tac 1);
3.310 +by (res_inst_tac [("x", "{F. ALL G. F ok G --> F Join G:X}")] exI 1);
3.311 +by Safe_tac;
3.312 +by (rtac wx'_ex_prop 2);
3.313 +by (rotate_tac 1 1);
3.314 +by (dres_inst_tac [("x", "SKIP")] spec 1);
3.315 +by Auto_tac;
3.316 +qed "wx_equiv";
3.317 +
3.318 +
3.319 +(* Propositions 7 to 11 are about this second definition of wx. And
3.320 + they are the same as the ones proved for the first definition of wx by equivalence *)
3.321 +
3.322 +(* Proposition 12 *)
3.323 +(* Main result of the paper *)
3.324 +Goalw [guar_def]
3.325 + "(X guarantees Y) = wx(-X Un Y)";
3.326 +by (simp_tac (simpset() addsimps [wx_equiv]) 1);
3.327 +qed "guarantees_wx_eq";
3.328 +
3.329 +(* {* Corollary, but this result has already been proved elsewhere *}
3.330 + "ex_prop(X guarantees Y)";
3.331 + by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
3.332 + qed "guarantees_ex_prop";
3.333 +*)
3.334 +
3.335 +(* Rules given in section 7 of Chandy and Sander's
3.336 + Reasoning About Program composition paper *)
3.337 +
3.338 +Goal "Init F <= A ==> F:(stable A) guarantees (Always A)";
3.339 +by (rtac guaranteesI 1);
3.340 +by (simp_tac (simpset() addsimps [Join_commute]) 1);
3.341 +by (rtac stable_Join_Always1 1);
3.342 +by (ALLGOALS(asm_full_simp_tac (simpset()
3.343 + addsimps [invariant_def, Join_stable])));
3.344 +qed "stable_guarantees_Always";
3.345 +
3.346 +(* To be moved to WFair.ML *)
3.347 +Goal "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B";
3.348 +by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1);
3.349 +by (dres_inst_tac [("B", "A-B")] transient_strengthen 2);
3.350 +by (rtac (ensuresI RS leadsTo_Basis) 3);
3.351 +by (ALLGOALS(Blast_tac));
3.352 +qed "leadsTo_Basis'";
3.353 +
3.354 +
3.355 +
3.356 +Goal "F:transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))";
3.357 +by (rtac guaranteesI 1);
3.358 +by (rtac leadsTo_Basis' 1);
3.359 +by (dtac constrains_weaken_R 1);
3.360 +by (assume_tac 2);
3.361 +by (Blast_tac 1);
3.362 +by (blast_tac (claset() addIs [Join_transient_I1]) 1);
3.363 +qed "constrains_guarantees_leadsTo";
3.364 +
3.365 +
3.366 +
3.367 +
3.368 +
3.369 +
3.370 +
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