1(* Title: HOL/UNITY/Guar.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Author: Sidi Ehmety 4 5From Chandy and Sanders, "Reasoning About Program Composition", 6Technical Report 2000-003, University of Florida, 2000. 7 8Compatibility, weakest guarantees, etc. and Weakest existential 9property, from Charpentier and Chandy "Theorems about Composition", 10Fifth International Conference on Mathematics of Program, 2000. 11*) 12 13section\<open>Guarantees Specifications\<close> 14 15theory Guar 16imports Comp 17begin 18 19instance program :: (type) order 20 by standard (auto simp add: program_less_le dest: component_antisym intro: component_trans) 21 22text\<open>Existential and Universal properties. I formalize the two-program 23 case, proving equivalence with Chandy and Sanders's n-ary definitions\<close> 24 25definition ex_prop :: "'a program set => bool" where 26 "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F\<squnion>G) \<in> X" 27 28definition strict_ex_prop :: "'a program set => bool" where 29 "strict_ex_prop X == \<forall>F G. F ok G --> (F \<in> X | G \<in> X) = (F\<squnion>G \<in> X)" 30 31definition uv_prop :: "'a program set => bool" where 32 "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F\<squnion>G) \<in> X)" 33 34definition strict_uv_prop :: "'a program set => bool" where 35 "strict_uv_prop X == 36 SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))" 37 38 39text\<open>Guarantees properties\<close> 40 41definition guar :: "['a program set, 'a program set] => 'a program set" (infixl "guarantees" 55) where 42 (*higher than membership, lower than Co*) 43 "X guarantees Y == {F. \<forall>G. F ok G --> F\<squnion>G \<in> X --> F\<squnion>G \<in> Y}" 44 45 46 (* Weakest guarantees *) 47definition wg :: "['a program, 'a program set] => 'a program set" where 48 "wg F Y == \<Union>({X. F \<in> X guarantees Y})" 49 50 (* Weakest existential property stronger than X *) 51definition wx :: "('a program) set => ('a program)set" where 52 "wx X == \<Union>({Y. Y \<subseteq> X & ex_prop Y})" 53 54 (*Ill-defined programs can arise through "Join"*) 55definition welldef :: "'a program set" where 56 "welldef == {F. Init F \<noteq> {}}" 57 58definition refines :: "['a program, 'a program, 'a program set] => bool" 59 ("(3_ refines _ wrt _)" [10,10,10] 10) where 60 "G refines F wrt X == 61 \<forall>H. (F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X) --> 62 (G\<squnion>H \<in> welldef \<inter> X)" 63 64definition iso_refines :: "['a program, 'a program, 'a program set] => bool" 65 ("(3_ iso'_refines _ wrt _)" [10,10,10] 10) where 66 "G iso_refines F wrt X == 67 F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X" 68 69 70lemma OK_insert_iff: 71 "(OK (insert i I) F) = 72 (if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))" 73by (auto intro: ok_sym simp add: OK_iff_ok) 74 75 76subsection\<open>Existential Properties\<close> 77 78lemma ex1: 79 assumes "ex_prop X" and "finite GG" 80 shows "GG \<inter> X \<noteq> {} \<Longrightarrow> OK GG (%G. G) \<Longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X" 81 apply (atomize (full)) 82 using assms(2) apply induct 83 using assms(1) apply (unfold ex_prop_def) 84 apply (auto simp add: OK_insert_iff Int_insert_left) 85 done 86 87lemma ex2: 88 "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} \<longrightarrow> OK GG (\<lambda>G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X 89 \<Longrightarrow> ex_prop X" 90apply (unfold ex_prop_def, clarify) 91apply (drule_tac x = "{F,G}" in spec) 92apply (auto dest: ok_sym simp add: OK_iff_ok) 93done 94 95 96(*Chandy & Sanders take this as a definition*) 97lemma ex_prop_finite: 98 "ex_prop X = 99 (\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)" 100by (blast intro: ex1 ex2) 101 102 103(*Their "equivalent definition" given at the end of section 3*) 104lemma ex_prop_equiv: 105 "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))" 106apply auto 107apply (unfold ex_prop_def component_of_def, safe, blast, blast) 108apply (subst Join_commute) 109apply (drule ok_sym, blast) 110done 111 112 113subsection\<open>Universal Properties\<close> 114 115lemma uv1: 116 assumes "uv_prop X" 117 and "finite GG" 118 and "GG \<subseteq> X" 119 and "OK GG (%G. G)" 120 shows "(\<Squnion>G \<in> GG. G) \<in> X" 121 using assms(2-) 122 apply induct 123 using assms(1) 124 apply (unfold uv_prop_def) 125 apply (auto simp add: Int_insert_left OK_insert_iff) 126 done 127 128lemma uv2: 129 "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X 130 ==> uv_prop X" 131apply (unfold uv_prop_def) 132apply (rule conjI) 133 apply (drule_tac x = "{}" in spec) 134 prefer 2 135 apply clarify 136 apply (drule_tac x = "{F,G}" in spec) 137apply (auto dest: ok_sym simp add: OK_iff_ok) 138done 139 140(*Chandy & Sanders take this as a definition*) 141lemma uv_prop_finite: 142 "uv_prop X = 143 (\<forall>GG. finite GG \<and> GG \<subseteq> X \<and> OK GG (\<lambda>G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)" 144by (blast intro: uv1 uv2) 145 146subsection\<open>Guarantees\<close> 147 148lemma guaranteesI: 149 "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y) ==> F \<in> X guarantees Y" 150by (simp add: guar_def component_def) 151 152lemma guaranteesD: 153 "[| F \<in> X guarantees Y; F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y" 154by (unfold guar_def component_def, blast) 155 156(*This version of guaranteesD matches more easily in the conclusion 157 The major premise can no longer be F \<subseteq> H since we need to reason about G*) 158lemma component_guaranteesD: 159 "[| F \<in> X guarantees Y; F\<squnion>G = H; H \<in> X; F ok G |] ==> H \<in> Y" 160by (unfold guar_def, blast) 161 162lemma guarantees_weaken: 163 "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'" 164by (unfold guar_def, blast) 165 166lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV" 167by (unfold guar_def, blast) 168 169(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) 170lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y" 171by (unfold guar_def, blast) 172 173(*Remark at end of section 4.1 *) 174 175lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)" 176apply (simp (no_asm_use) add: guar_def ex_prop_equiv) 177apply safe 178 apply (drule_tac x = x in spec) 179 apply (drule_tac [2] x = x in spec) 180 apply (drule_tac [2] sym) 181apply (auto simp add: component_of_def) 182done 183 184lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)" 185by (auto simp add: guar_def ex_prop_equiv component_of_def dest: sym) 186 187lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)" 188apply (rule iffI) 189apply (rule ex_prop_imp) 190apply (auto simp add: guarantees_imp) 191done 192 193 194subsection\<open>Distributive Laws. Re-Orient to Perform Miniscoping\<close> 195 196lemma guarantees_UN_left: 197 "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)" 198by (unfold guar_def, blast) 199 200lemma guarantees_Un_left: 201 "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)" 202by (unfold guar_def, blast) 203 204lemma guarantees_INT_right: 205 "X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)" 206by (unfold guar_def, blast) 207 208lemma guarantees_Int_right: 209 "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)" 210by (unfold guar_def, blast) 211 212lemma guarantees_Int_right_I: 213 "[| F \<in> Z guarantees X; F \<in> Z guarantees Y |] 214 ==> F \<in> Z guarantees (X \<inter> Y)" 215by (simp add: guarantees_Int_right) 216 217lemma guarantees_INT_right_iff: 218 "(F \<in> X guarantees (\<Inter>(Y ` I))) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))" 219by (simp add: guarantees_INT_right) 220 221lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))" 222by (unfold guar_def, blast) 223 224lemma contrapositive: "(X guarantees Y) = -Y guarantees -X" 225by (unfold guar_def, blast) 226 227(** The following two can be expressed using intersection and subset, which 228 is more faithful to the text but looks cryptic. 229**) 230 231lemma combining1: 232 "[| F \<in> V guarantees X; F \<in> (X \<inter> Y) guarantees Z |] 233 ==> F \<in> (V \<inter> Y) guarantees Z" 234by (unfold guar_def, blast) 235 236lemma combining2: 237 "[| F \<in> V guarantees (X \<union> Y); F \<in> Y guarantees Z |] 238 ==> F \<in> V guarantees (X \<union> Z)" 239by (unfold guar_def, blast) 240 241(** The following two follow Chandy-Sanders, but the use of object-quantifiers 242 does not suit Isabelle... **) 243 244(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *) 245lemma all_guarantees: 246 "\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)" 247by (unfold guar_def, blast) 248 249(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *) 250lemma ex_guarantees: 251 "\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)" 252by (unfold guar_def, blast) 253 254 255subsection\<open>Guarantees: Additional Laws (by lcp)\<close> 256 257lemma guarantees_Join_Int: 258 "[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |] 259 ==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)" 260apply (simp add: guar_def, safe) 261 apply (simp add: Join_assoc) 262apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ") 263 apply (simp add: ok_commute) 264apply (simp add: Join_ac) 265done 266 267lemma guarantees_Join_Un: 268 "[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |] 269 ==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)" 270apply (simp add: guar_def, safe) 271 apply (simp add: Join_assoc) 272apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ") 273 apply (simp add: ok_commute) 274apply (simp add: Join_ac) 275done 276 277lemma guarantees_JN_INT: 278 "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |] 279 ==> (JOIN I F) \<in> (\<Inter>(X ` I)) guarantees (\<Inter>(Y ` I))" 280apply (unfold guar_def, auto) 281apply (drule bspec, assumption) 282apply (rename_tac "i") 283apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec) 284apply (auto intro: OK_imp_ok 285 simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) 286done 287 288lemma guarantees_JN_UN: 289 "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |] 290 ==> (JOIN I F) \<in> (\<Union>(X ` I)) guarantees (\<Union>(Y ` I))" 291apply (unfold guar_def, auto) 292apply (drule bspec, assumption) 293apply (rename_tac "i") 294apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec) 295apply (auto intro: OK_imp_ok 296 simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) 297done 298 299 300subsection\<open>Guarantees Laws for Breaking Down the Program (by lcp)\<close> 301 302lemma guarantees_Join_I1: 303 "[| F \<in> X guarantees Y; F ok G |] ==> F\<squnion>G \<in> X guarantees Y" 304by (simp add: guar_def Join_assoc) 305 306lemma guarantees_Join_I2: 307 "[| G \<in> X guarantees Y; F ok G |] ==> F\<squnion>G \<in> X guarantees Y" 308apply (simp add: Join_commute [of _ G] ok_commute [of _ G]) 309apply (blast intro: guarantees_Join_I1) 310done 311 312lemma guarantees_JN_I: 313 "[| i \<in> I; F i \<in> X guarantees Y; OK I F |] 314 ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y" 315apply (unfold guar_def, clarify) 316apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec) 317apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric]) 318done 319 320 321(*** well-definedness ***) 322 323lemma Join_welldef_D1: "F\<squnion>G \<in> welldef ==> F \<in> welldef" 324by (unfold welldef_def, auto) 325 326lemma Join_welldef_D2: "F\<squnion>G \<in> welldef ==> G \<in> welldef" 327by (unfold welldef_def, auto) 328 329(*** refinement ***) 330 331lemma refines_refl: "F refines F wrt X" 332by (unfold refines_def, blast) 333 334(*We'd like transitivity, but how do we get it?*) 335lemma refines_trans: 336 "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X" 337apply (simp add: refines_def) 338oops 339 340 341lemma strict_ex_refine_lemma: 342 "strict_ex_prop X 343 ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) 344 = (F \<in> X --> G \<in> X)" 345by (unfold strict_ex_prop_def, auto) 346 347lemma strict_ex_refine_lemma_v: 348 "strict_ex_prop X 349 ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = 350 (F \<in> welldef \<inter> X --> G \<in> X)" 351apply (unfold strict_ex_prop_def, safe) 352apply (erule_tac x = SKIP and P = "%H. PP H --> RR H" for PP RR in allE) 353apply (auto dest: Join_welldef_D1 Join_welldef_D2) 354done 355 356lemma ex_refinement_thm: 357 "[| strict_ex_prop X; 358 \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> G\<squnion>H \<in> welldef |] 359 ==> (G refines F wrt X) = (G iso_refines F wrt X)" 360apply (rule_tac x = SKIP in allE, assumption) 361apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v) 362done 363 364 365lemma strict_uv_refine_lemma: 366 "strict_uv_prop X ==> 367 (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = (F \<in> X --> G \<in> X)" 368by (unfold strict_uv_prop_def, blast) 369 370lemma strict_uv_refine_lemma_v: 371 "strict_uv_prop X 372 ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = 373 (F \<in> welldef \<inter> X --> G \<in> X)" 374apply (unfold strict_uv_prop_def, safe) 375apply (erule_tac x = SKIP and P = "%H. PP H --> RR H" for PP RR in allE) 376apply (auto dest: Join_welldef_D1 Join_welldef_D2) 377done 378 379lemma uv_refinement_thm: 380 "[| strict_uv_prop X; 381 \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> 382 G\<squnion>H \<in> welldef |] 383 ==> (G refines F wrt X) = (G iso_refines F wrt X)" 384apply (rule_tac x = SKIP in allE, assumption) 385apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v) 386done 387 388(* Added by Sidi Ehmety from Chandy & Sander, section 6 *) 389lemma guarantees_equiv: 390 "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))" 391by (unfold guar_def component_of_def, auto) 392 393lemma wg_weakest: "!!X. F\<in> (X guarantees Y) ==> X \<subseteq> (wg F Y)" 394by (unfold wg_def, auto) 395 396lemma wg_guarantees: "F\<in> ((wg F Y) guarantees Y)" 397by (unfold wg_def guar_def, blast) 398 399lemma wg_equiv: "(H \<in> wg F X) = (F component_of H --> H \<in> X)" 400by (simp add: guarantees_equiv wg_def, blast) 401 402lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)" 403by (simp add: wg_equiv) 404 405lemma wg_finite: 406 "\<forall>FF. finite FF \<and> FF \<inter> X \<noteq> {} \<longrightarrow> OK FF (\<lambda>F. F) 407 \<longrightarrow> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F) \<in> wg F X) = ((\<Squnion>F \<in> FF. F) \<in> X))" 408apply clarify 409apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ") 410apply (drule_tac X = X in component_of_wg, simp) 411apply (simp add: component_of_def) 412apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI) 413apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok) 414done 415 416lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)" 417apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv) 418apply blast 419done 420 421(** From Charpentier and Chandy "Theorems About Composition" **) 422(* Proposition 2 *) 423lemma wx_subset: "(wx X)<=X" 424by (unfold wx_def, auto) 425 426lemma wx_ex_prop: "ex_prop (wx X)" 427apply (simp add: wx_def ex_prop_equiv cong: bex_cong, safe, blast) 428apply force 429done 430 431lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X" 432by (auto simp add: wx_def) 433 434(* Proposition 6 *) 435lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})" 436apply (unfold ex_prop_def, safe) 437 apply (drule_tac x = "G\<squnion>Ga" in spec) 438 apply (force simp add: Join_assoc) 439apply (drule_tac x = "F\<squnion>Ga" in spec) 440apply (simp add: ok_commute Join_ac) 441done 442 443text\<open>Equivalence with the other definition of wx\<close> 444 445lemma wx_equiv: "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G) \<in> X}" 446apply (unfold wx_def, safe) 447 apply (simp add: ex_prop_def, blast) 448apply (simp (no_asm)) 449apply (rule_tac x = "{F. \<forall>G. F ok G --> F\<squnion>G \<in> X}" in exI, safe) 450apply (rule_tac [2] wx'_ex_prop) 451apply (drule_tac x = SKIP in spec)+ 452apply auto 453done 454 455 456text\<open>Propositions 7 to 11 are about this second definition of wx. 457 They are the same as the ones proved for the first definition of wx, 458 by equivalence\<close> 459 460(* Proposition 12 *) 461(* Main result of the paper *) 462lemma guarantees_wx_eq: "(X guarantees Y) = wx(-X \<union> Y)" 463by (simp add: guar_def wx_equiv) 464 465 466(* Rules given in section 7 of Chandy and Sander's 467 Reasoning About Program composition paper *) 468lemma stable_guarantees_Always: 469 "Init F \<subseteq> A ==> F \<in> (stable A) guarantees (Always A)" 470apply (rule guaranteesI) 471apply (simp add: Join_commute) 472apply (rule stable_Join_Always1) 473 apply (simp_all add: invariant_def) 474done 475 476lemma constrains_guarantees_leadsTo: 477 "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))" 478apply (rule guaranteesI) 479apply (rule leadsTo_Basis') 480 apply (drule constrains_weaken_R) 481 prefer 2 apply assumption 482 apply blast 483apply (blast intro: Join_transient_I1) 484done 485 486end 487