1(* Title: HOL/UNITY/ProgressSets.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 2003 University of Cambridge 4 5Progress Sets. From 6 7 David Meier and Beverly Sanders, 8 Composing Leads-to Properties 9 Theoretical Computer Science 243:1-2 (2000), 339-361. 10 11 David Meier, 12 Progress Properties in Program Refinement and Parallel Composition 13 Swiss Federal Institute of Technology Zurich (1997) 14*) 15 16section\<open>Progress Sets\<close> 17 18theory ProgressSets imports Transformers begin 19 20subsection \<open>Complete Lattices and the Operator \<^term>\<open>cl\<close>\<close> 21 22definition lattice :: "'a set set => bool" where 23 \<comment> \<open>Meier calls them closure sets, but they are just complete lattices\<close> 24 "lattice L == 25 (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)" 26 27definition cl :: "['a set set, 'a set] => 'a set" where 28 \<comment> \<open>short for ``closure''\<close> 29 "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}" 30 31lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L" 32by (force simp add: lattice_def) 33 34lemma empty_in_lattice: "lattice L ==> {} \<in> L" 35by (force simp add: lattice_def) 36 37lemma Union_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Union>M \<in> L" 38by (simp add: lattice_def) 39 40lemma Inter_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Inter>M \<in> L" 41by (simp add: lattice_def) 42 43lemma UN_in_lattice: 44 "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L" 45apply (blast intro: Union_in_lattice) 46done 47 48lemma INT_in_lattice: 49 "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i) \<in> L" 50apply (blast intro: Inter_in_lattice) 51done 52 53lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L" 54 using Union_in_lattice [of "{x, y}" L] by simp 55 56lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L" 57 using Inter_in_lattice [of "{x, y}" L] by simp 58 59lemma lattice_stable: "lattice {X. F \<in> stable X}" 60by (simp add: lattice_def stable_def constrains_def, blast) 61 62text\<open>The next three results state that \<^term>\<open>cl L r\<close> is the minimal 63 element of \<^term>\<open>L\<close> that includes \<^term>\<open>r\<close>.\<close> 64lemma cl_in_lattice: "lattice L ==> cl L r \<in> L" 65 by (simp add: lattice_def cl_def) 66 67lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" 68by (force simp add: cl_def) 69 70text\<open>The next three lemmas constitute assertion (4.61)\<close> 71lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'" 72by (simp add: cl_def, blast) 73 74lemma subset_cl: "r \<subseteq> cl L r" 75by (simp add: cl_def le_Inf_iff) 76 77text\<open>A reformulation of @{thm subset_cl}\<close> 78lemma clI: "x \<in> r ==> x \<in> cl L r" 79by (simp add: cl_def, blast) 80 81text\<open>A reformulation of @{thm cl_least}\<close> 82lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B" 83by (force simp add: cl_def) 84 85lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)" 86by (simp add: cl_def, blast) 87 88lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s" 89apply (rule equalityI) 90 prefer 2 91 apply (simp add: cl_def, blast) 92apply (rule cl_least) 93 apply (blast intro: Un_in_lattice cl_in_lattice) 94apply (blast intro: subset_cl [THEN subsetD]) 95done 96 97lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))" 98apply (rule equalityI) 99 prefer 2 apply (simp add: cl_def, blast) 100apply (rule cl_least) 101 apply (blast intro: UN_in_lattice cl_in_lattice) 102apply (blast intro: subset_cl [THEN subsetD]) 103done 104 105lemma cl_Int_subset: "cl L (r\<inter>s) \<subseteq> cl L r \<inter> cl L s" 106by (simp add: cl_def, blast) 107 108lemma cl_idem [simp]: "cl L (cl L r) = cl L r" 109by (simp add: cl_def, blast) 110 111lemma cl_ident: "r\<in>L ==> cl L r = r" 112by (force simp add: cl_def) 113 114lemma cl_empty [simp]: "lattice L ==> cl L {} = {}" 115by (simp add: cl_ident empty_in_lattice) 116 117lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV" 118by (simp add: cl_ident UNIV_in_lattice) 119 120text\<open>Assertion (4.62)\<close> 121lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" 122apply (rule iffI) 123 apply (erule subst) 124 apply (erule cl_in_lattice) 125apply (erule cl_ident) 126done 127 128lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L" 129by (simp add: cl_ident_iff [symmetric] equalityI subset_cl) 130 131 132subsection \<open>Progress Sets and the Main Lemma\<close> 133text\<open>A progress set satisfies certain closure conditions and is a 134simple way of including the set \<^term>\<open>wens_set F B\<close>.\<close> 135 136definition closed :: "['a program, 'a set, 'a set, 'a set set] => bool" where 137 "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L --> 138 T \<inter> (B \<union> wp act M) \<in> L" 139 140definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where 141 "progress_set F T B == 142 {L. lattice L & B \<in> L & T \<in> L & closed F T B L}" 143 144lemma closedD: 145 "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] 146 ==> T \<inter> (B \<union> wp act M) \<in> L" 147by (simp add: closed_def) 148 149text\<open>Note: the formalization below replaces Meier's \<^term>\<open>q\<close> by \<^term>\<open>B\<close> 150and \<^term>\<open>m\<close> by \<^term>\<open>X\<close>.\<close> 151 152text\<open>Part of the proof of the claim at the bottom of page 97. It's 153proved separately because the argument requires a generalization over 154all \<^term>\<open>act \<in> Acts F\<close>.\<close> 155lemma lattice_awp_lemma: 156 assumes TXC: "T\<inter>X \<in> C" \<comment> \<open>induction hypothesis in theorem below\<close> 157 and BsubX: "B \<subseteq> X" \<comment> \<open>holds in inductive step\<close> 158 and latt: "lattice C" 159 and TC: "T \<in> C" 160 and BC: "B \<in> C" 161 and clos: "closed F T B C" 162 shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C" 163apply (simp del: INT_simps add: awp_def INT_extend_simps) 164apply (rule INT_in_lattice [OF latt]) 165apply (erule closedD [OF clos]) 166apply (simp add: subset_trans [OF BsubX Un_upper1]) 167apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)") 168 prefer 2 apply (blast intro: TC clD) 169apply (erule ssubst) 170apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 171done 172 173text\<open>Remainder of the proof of the claim at the bottom of page 97.\<close> 174lemma lattice_lemma: 175 assumes TXC: "T\<inter>X \<in> C" \<comment> \<open>induction hypothesis in theorem below\<close> 176 and BsubX: "B \<subseteq> X" \<comment> \<open>holds in inductive step\<close> 177 and act: "act \<in> Acts F" 178 and latt: "lattice C" 179 and TC: "T \<in> C" 180 and BC: "B \<in> C" 181 and clos: "closed F T B C" 182 shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C" 183apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C") 184 prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC) 185apply (drule Int_in_lattice 186 [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r] 187 latt]) 188apply (subgoal_tac 189 "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) = 190 T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") 191 prefer 2 apply blast 192apply simp 193apply (drule Un_in_lattice [OF _ TXC latt]) 194apply (subgoal_tac 195 "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X = 196 T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)") 197 apply simp 198apply (blast intro: BsubX [THEN subsetD]) 199done 200 201 202text\<open>Induction step for the main lemma\<close> 203lemma progress_induction_step: 204 assumes TXC: "T\<inter>X \<in> C" \<comment> \<open>induction hypothesis in theorem below\<close> 205 and act: "act \<in> Acts F" 206 and Xwens: "X \<in> wens_set F B" 207 and latt: "lattice C" 208 and TC: "T \<in> C" 209 and BC: "B \<in> C" 210 and clos: "closed F T B C" 211 and Fstable: "F \<in> stable T" 212 shows "T \<inter> wens F act X \<in> C" 213proof - 214 from Xwens have BsubX: "B \<subseteq> X" 215 by (rule wens_set_imp_subset) 216 let ?r = "wens F act X" 217 have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X" 218 by (simp add: wens_unfold [symmetric]) 219 then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)" 220 by blast 221 then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)" 222 by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 223 then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)" 224 by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD]) 225 then have "cl C (T\<inter>?r) \<subseteq> 226 cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))" 227 by (rule cl_mono) 228 then have "cl C (T\<inter>?r) \<subseteq> 229 T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)" 230 by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos]) 231 then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X" 232 by blast 233 then have "cl C (T\<inter>?r) \<subseteq> ?r" 234 by (blast intro!: subset_wens) 235 then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r" 236 by (simp add: cl_ident TC 237 subset_trans [OF cl_mono [OF Int_lower1]]) 238 show ?thesis 239 by (rule cl_subset_in_lattice [OF cl_subset latt]) 240qed 241 242text\<open>Proved on page 96 of Meier's thesis. The special case when 243 \<^term>\<open>T=UNIV\<close> states that every progress set for the program \<^term>\<open>F\<close> 244 and set \<^term>\<open>B\<close> includes the set \<^term>\<open>wens_set F B\<close>.\<close> 245lemma progress_set_lemma: 246 "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C" 247apply (simp add: progress_set_def, clarify) 248apply (erule wens_set.induct) 249 txt\<open>Base\<close> 250 apply (simp add: Int_in_lattice) 251 txt\<open>The difficult \<^term>\<open>wens\<close> case\<close> 252 apply (simp add: progress_induction_step) 253txt\<open>Disjunctive case\<close> 254apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 255 apply simp 256apply (blast intro: UN_in_lattice) 257done 258 259 260subsection \<open>The Progress Set Union Theorem\<close> 261 262lemma closed_mono: 263 assumes BB': "B \<subseteq> B'" 264 and TBwp: "T \<inter> (B \<union> wp act M) \<in> C" 265 and B'C: "B' \<in> C" 266 and TC: "T \<in> C" 267 and latt: "lattice C" 268 shows "T \<inter> (B' \<union> wp act M) \<in> C" 269proof - 270 from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C" 271 by (simp add: Int_Un_distrib) 272 then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C" 273 by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) 274 show ?thesis 275 by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], 276 blast intro: BB' [THEN subsetD]) 277qed 278 279 280lemma progress_set_mono: 281 assumes BB': "B \<subseteq> B'" 282 shows 283 "[| B' \<in> C; C \<in> progress_set F T B|] 284 ==> C \<in> progress_set F T B'" 285by (simp add: progress_set_def closed_def closed_mono [OF BB'] 286 subset_trans [OF BB']) 287 288theorem progress_set_Union: 289 assumes leadsTo: "F \<in> A leadsTo B'" 290 and prog: "C \<in> progress_set F T B" 291 and Fstable: "F \<in> stable T" 292 and BB': "B \<subseteq> B'" 293 and B'C: "B' \<in> C" 294 and Gco: "!!X. X\<in>C ==> G \<in> X-B co X" 295 shows "F\<squnion>G \<in> T\<inter>A leadsTo B'" 296apply (insert prog Fstable) 297apply (rule leadsTo_Join [OF leadsTo]) 298 apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 299apply (simp add: awp_iff_constrains) 300apply (drule progress_set_mono [OF BB' B'C]) 301apply (blast intro: progress_set_lemma Gco constrains_weaken_L 302 BB' [THEN subsetD]) 303done 304 305 306subsection \<open>Some Progress Sets\<close> 307 308lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B" 309by (simp add: progress_set_def lattice_def closed_def) 310 311 312 313subsubsection \<open>Lattices and Relations\<close> 314text\<open>From Meier's thesis, section 4.5.3\<close> 315 316definition relcl :: "'a set set => ('a * 'a) set" where 317 \<comment> \<open>Derived relation from a lattice\<close> 318 "relcl L == {(x,y). y \<in> cl L {x}}" 319 320definition latticeof :: "('a * 'a) set => 'a set set" where 321 \<comment> \<open>Derived lattice from a relation: the set of upwards-closed sets\<close> 322 "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}" 323 324 325lemma relcl_refl: "(a,a) \<in> relcl L" 326by (simp add: relcl_def subset_cl [THEN subsetD]) 327 328lemma relcl_trans: 329 "[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L" 330apply (simp add: relcl_def) 331apply (blast intro: clD cl_in_lattice) 332done 333 334lemma refl_relcl: "lattice L ==> refl (relcl L)" 335by (simp add: refl_onI relcl_def subset_cl [THEN subsetD]) 336 337lemma trans_relcl: "lattice L ==> trans (relcl L)" 338by (blast intro: relcl_trans transI) 339 340lemma lattice_latticeof: "lattice (latticeof r)" 341by (auto simp add: lattice_def latticeof_def) 342 343lemma lattice_singletonI: 344 "[|lattice L; !!s. s \<in> X ==> {s} \<in> L|] ==> X \<in> L" 345apply (cut_tac UN_singleton [of X]) 346apply (erule subst) 347apply (simp only: UN_in_lattice) 348done 349 350text\<open>Equation (4.71) of Meier's thesis. He gives no proof.\<close> 351lemma cl_latticeof: 352 "[|refl r; trans r|] 353 ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" 354apply (rule equalityI) 355 apply (rule cl_least) 356 apply (simp (no_asm_use) add: latticeof_def trans_def, blast) 357 apply (simp add: latticeof_def refl_on_def, blast) 358apply (simp add: latticeof_def, clarify) 359apply (unfold cl_def, blast) 360done 361 362text\<open>Related to (4.71).\<close> 363lemma cl_eq_Collect_relcl: 364 "lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}" 365apply (cut_tac UN_singleton [of X]) 366apply (erule subst) 367apply (force simp only: relcl_def cl_UN) 368done 369 370text\<open>Meier's theorem of section 4.5.3\<close> 371theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L" 372apply (rule equalityI) 373 prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify) 374apply (rename_tac X) 375apply (rule cl_subset_in_lattice) 376 prefer 2 apply assumption 377apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2]) 378apply (drule equalityD1) 379apply (rule subset_trans) 380 prefer 2 apply assumption 381apply (thin_tac "_ \<subseteq> X") 382apply (cut_tac A=X in UN_singleton) 383apply (erule subst) 384apply (simp only: cl_UN lattice_latticeof 385 cl_latticeof [OF refl_relcl trans_relcl]) 386apply (simp add: relcl_def) 387done 388 389theorem relcl_latticeof_eq: 390 "[|refl r; trans r|] ==> relcl (latticeof r) = r" 391by (simp add: relcl_def cl_latticeof) 392 393 394subsubsection \<open>Decoupling Theorems\<close> 395 396definition decoupled :: "['a program, 'a program] => bool" where 397 "decoupled F G == 398 \<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)" 399 400 401text\<open>Rao's Decoupling Theorem\<close> 402lemma stableco: "F \<in> stable A ==> F \<in> A-B co A" 403by (simp add: stable_def constrains_def, blast) 404 405theorem decoupling: 406 assumes leadsTo: "F \<in> A leadsTo B" 407 and Gstable: "G \<in> stable B" 408 and dec: "decoupled F G" 409 shows "F\<squnion>G \<in> A leadsTo B" 410proof - 411 have prog: "{X. G \<in> stable X} \<in> progress_set F UNIV B" 412 by (simp add: progress_set_def lattice_stable Gstable closed_def 413 stable_Un [OF Gstable] dec [unfolded decoupled_def]) 414 have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 415 by (rule progress_set_Union [OF leadsTo prog], 416 simp_all add: Gstable stableco) 417 thus ?thesis by simp 418qed 419 420 421text\<open>Rao's Weak Decoupling Theorem\<close> 422theorem weak_decoupling: 423 assumes leadsTo: "F \<in> A leadsTo B" 424 and stable: "F\<squnion>G \<in> stable B" 425 and dec: "decoupled F (F\<squnion>G)" 426 shows "F\<squnion>G \<in> A leadsTo B" 427proof - 428 have prog: "{X. F\<squnion>G \<in> stable X} \<in> progress_set F UNIV B" 429 by (simp del: Join_stable 430 add: progress_set_def lattice_stable stable closed_def 431 stable_Un [OF stable] dec [unfolded decoupled_def]) 432 have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 433 by (rule progress_set_Union [OF leadsTo prog], 434 simp_all del: Join_stable add: stable, 435 simp add: stableco) 436 thus ?thesis by simp 437qed 438 439text\<open>The ``Decoupling via \<^term>\<open>G'\<close> Union Theorem''\<close> 440theorem decoupling_via_aux: 441 assumes leadsTo: "F \<in> A leadsTo B" 442 and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B" 443 and GG': "G \<le> G'" 444 \<comment> \<open>Beware! This is the converse of the refinement relation!\<close> 445 shows "F\<squnion>G \<in> A leadsTo B" 446proof - 447 from prog have stable: "G' \<in> stable B" 448 by (simp add: progress_set_def) 449 have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 450 by (rule progress_set_Union [OF leadsTo prog], 451 simp_all add: stable stableco component_stable [OF GG']) 452 thus ?thesis by simp 453qed 454 455 456subsection\<open>Composition Theorems Based on Monotonicity and Commutativity\<close> 457 458subsubsection\<open>Commutativity of \<^term>\<open>cl L\<close> and assignment.\<close> 459definition commutes :: "['a program, 'a set, 'a set, 'a set set] => bool" where 460 "commutes F T B L == 461 \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> 462 cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))" 463 464 465text\<open>From Meier's thesis, section 4.5.6\<close> 466lemma commutativity1_lemma: 467 assumes commutes: "commutes F T B L" 468 and lattice: "lattice L" 469 and BL: "B \<in> L" 470 and TL: "T \<in> L" 471 shows "closed F T B L" 472apply (simp add: closed_def, clarify) 473apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice]) 474apply (simp add: Int_Un_distrib cl_Un [OF lattice] 475 cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1) 476apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 477 prefer 2 478 apply (cut_tac commutes, simp add: commutes_def) 479apply (erule subset_trans) 480apply (simp add: cl_ident) 481apply (blast intro: rev_subsetD [OF _ wp_mono]) 482done 483 484text\<open>Version packaged with @{thm progress_set_Union}\<close> 485lemma commutativity1: 486 assumes leadsTo: "F \<in> A leadsTo B" 487 and lattice: "lattice L" 488 and BL: "B \<in> L" 489 and TL: "T \<in> L" 490 and Fstable: "F \<in> stable T" 491 and Gco: "!!X. X\<in>L ==> G \<in> X-B co X" 492 and commutes: "commutes F T B L" 493 shows "F\<squnion>G \<in> T\<inter>A leadsTo B" 494by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco], 495 simp add: progress_set_def commutativity1_lemma commutes lattice BL TL) 496 497 498 499text\<open>Possibly move to Relation.thy, after \<^term>\<open>single_valued\<close>\<close> 500definition funof :: "[('a*'b)set, 'a] => 'b" where 501 "funof r == (\<lambda>x. THE y. (x,y) \<in> r)" 502 503lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y" 504by (simp add: funof_def single_valued_def, blast) 505 506lemma funof_Pair_in: 507 "[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r" 508by (force simp add: funof_eq) 509 510lemma funof_in: 511 "[|r``{x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A" 512by (force simp add: funof_eq) 513 514lemma funof_imp_wp: "[|funof act t \<in> A; single_valued act|] ==> t \<in> wp act A" 515by (force simp add: in_wp_iff funof_eq) 516 517 518subsubsection\<open>Commutativity of Functions and Relation\<close> 519text\<open>Thesis, page 109\<close> 520 521(*FIXME: this proof is still an ungodly mess*) 522text\<open>From Meier's thesis, section 4.5.6\<close> 523lemma commutativity2_lemma: 524 assumes dcommutes: 525 "\<And>act s t. act \<in> Acts F \<Longrightarrow> s \<in> T \<Longrightarrow> (s, t) \<in> relcl L \<Longrightarrow> 526 s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" 527 and determ: "!!act. act \<in> Acts F ==> single_valued act" 528 and total: "!!act. act \<in> Acts F ==> Domain act = UNIV" 529 and lattice: "lattice L" 530 and BL: "B \<in> L" 531 and TL: "T \<in> L" 532 and Fstable: "F \<in> stable T" 533 shows "commutes F T B L" 534proof - 535 { fix M and act and t 536 assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)" 537 then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M" 538 by (force simp add: cl_eq_Collect_relcl [OF lattice]) 539 then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M" 540 by blast 541 then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u" 542 apply (intro ballI impI) 543 apply (subst cl_ident [symmetric], assumption) 544 apply (simp add: relcl_def) 545 apply (blast intro: cl_mono [THEN [2] rev_subsetD]) 546 done 547 with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M" 548 by (force intro!: funof_in 549 simp add: wp_def stable_def constrains_def determ total) 550 with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" 551 by (intro dcommutes) assumption+ 552 with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)" 553 by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD]) 554 with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))" 555 by (blast intro: funof_imp_wp determ) 556 with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))" 557 by (blast intro: TL cl_mono [THEN [2] rev_subsetD]) 558 then have"t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))" 559 by simp 560 } 561 then show "commutes F T B L" unfolding commutes_def by clarify 562qed 563 564text\<open>Version packaged with @{thm progress_set_Union}\<close> 565lemma commutativity2: 566 assumes leadsTo: "F \<in> A leadsTo B" 567 and dcommutes: 568 "\<forall>act \<in> Acts F. 569 \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> 570 s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" 571 and determ: "!!act. act \<in> Acts F ==> single_valued act" 572 and total: "!!act. act \<in> Acts F ==> Domain act = UNIV" 573 and lattice: "lattice L" 574 and BL: "B \<in> L" 575 and TL: "T \<in> L" 576 and Fstable: "F \<in> stable T" 577 and Gco: "!!X. X\<in>L ==> G \<in> X-B co X" 578 shows "F\<squnion>G \<in> T\<inter>A leadsTo B" 579apply (rule commutativity1 [OF leadsTo lattice]) 580apply (simp_all add: Gco commutativity2_lemma dcommutes determ total 581 lattice BL TL Fstable) 582done 583 584 585subsection \<open>Monotonicity\<close> 586text\<open>From Meier's thesis, section 4.5.7, page 110\<close> 587(*to be continued?*) 588 589end 590