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