1(* Title: ZF/UNITY/WFair.thy 2 Author: Sidi Ehmety, Computer Laboratory 3 Copyright 1998 University of Cambridge 4*) 5 6section\<open>Progress under Weak Fairness\<close> 7 8theory WFair 9imports UNITY ZFC 10begin 11 12text\<open>This theory defines the operators transient, ensures and leadsTo, 13assuming weak fairness. From Misra, "A Logic for Concurrent Programming", 141994.\<close> 15 16definition 17 (* This definition specifies weak fairness. The rest of the theory 18 is generic to all forms of fairness.*) 19 transient :: "i=>i" where 20 "transient(A) =={F \<in> program. (\<exists>act\<in>Acts(F). A<=domain(act) & 21 act``A \<subseteq> state-A) & st_set(A)}" 22 23definition 24 ensures :: "[i,i] => i" (infixl "ensures" 60) where 25 "A ensures B == ((A-B) co (A \<union> B)) \<inter> transient(A-B)" 26 27consts 28 29 (*LEADS-TO constant for the inductive definition*) 30 leads :: "[i, i]=>i" 31 32inductive 33 domains 34 "leads(D, F)" \<subseteq> "Pow(D)*Pow(D)" 35 intros 36 Basis: "[| F \<in> A ensures B; A \<in> Pow(D); B \<in> Pow(D) |] ==> <A,B>:leads(D, F)" 37 Trans: "[| <A,B> \<in> leads(D, F); <B,C> \<in> leads(D, F) |] ==> <A,C>:leads(D, F)" 38 Union: "[| S \<in> Pow({A \<in> S. <A, B>:leads(D, F)}); B \<in> Pow(D); S \<in> Pow(Pow(D)) |] ==> 39 <\<Union>(S),B>:leads(D, F)" 40 41 monos Pow_mono 42 type_intros Union_Pow_iff [THEN iffD2] UnionI PowI 43 44definition 45 (* The Visible version of the LEADS-TO relation*) 46 leadsTo :: "[i, i] => i" (infixl "\<longmapsto>" 60) where 47 "A \<longmapsto> B == {F \<in> program. <A,B>:leads(state, F)}" 48 49definition 50 (* wlt(F, B) is the largest set that leads to B*) 51 wlt :: "[i, i] => i" where 52 "wlt(F, B) == \<Union>({A \<in> Pow(state). F \<in> A \<longmapsto> B})" 53 54(** Ad-hoc set-theory rules **) 55 56lemma Int_Union_Union: "\<Union>(B) \<inter> A = (\<Union>b \<in> B. b \<inter> A)" 57by auto 58 59lemma Int_Union_Union2: "A \<inter> \<Union>(B) = (\<Union>b \<in> B. A \<inter> b)" 60by auto 61 62(*** transient ***) 63 64lemma transient_type: "transient(A)<=program" 65by (unfold transient_def, auto) 66 67lemma transientD2: 68"F \<in> transient(A) ==> F \<in> program & st_set(A)" 69apply (unfold transient_def, auto) 70done 71 72lemma stable_transient_empty: "[| F \<in> stable(A); F \<in> transient(A) |] ==> A = 0" 73by (simp add: stable_def constrains_def transient_def, fast) 74 75lemma transient_strengthen: "[|F \<in> transient(A); B<=A|] ==> F \<in> transient(B)" 76apply (simp add: transient_def st_set_def, clarify) 77apply (blast intro!: rev_bexI) 78done 79 80lemma transientI: 81"[|act \<in> Acts(F); A \<subseteq> domain(act); act``A \<subseteq> state-A; 82 F \<in> program; st_set(A)|] ==> F \<in> transient(A)" 83by (simp add: transient_def, blast) 84 85lemma transientE: 86 "[| F \<in> transient(A); 87 !!act. [| act \<in> Acts(F); A \<subseteq> domain(act); act``A \<subseteq> state-A|]==>P|] 88 ==>P" 89by (simp add: transient_def, blast) 90 91lemma transient_state: "transient(state) = 0" 92apply (simp add: transient_def) 93apply (rule equalityI, auto) 94apply (cut_tac F = x in Acts_type) 95apply (simp add: Diff_cancel) 96apply (auto intro: st0_in_state) 97done 98 99lemma transient_state2: "state<=B ==> transient(B) = 0" 100apply (simp add: transient_def st_set_def) 101apply (rule equalityI, auto) 102apply (cut_tac F = x in Acts_type) 103apply (subgoal_tac "B=state") 104apply (auto intro: st0_in_state) 105done 106 107lemma transient_empty: "transient(0) = program" 108by (auto simp add: transient_def) 109 110declare transient_empty [simp] transient_state [simp] transient_state2 [simp] 111 112(*** ensures ***) 113 114lemma ensures_type: "A ensures B <=program" 115by (simp add: ensures_def constrains_def, auto) 116 117lemma ensuresI: 118"[|F:(A-B) co (A \<union> B); F \<in> transient(A-B)|]==>F \<in> A ensures B" 119apply (unfold ensures_def) 120apply (auto simp add: transient_type [THEN subsetD]) 121done 122 123(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *) 124lemma ensuresI2: "[| F \<in> A co A \<union> B; F \<in> transient(A) |] ==> F \<in> A ensures B" 125apply (drule_tac B = "A-B" in constrains_weaken_L) 126apply (drule_tac [2] B = "A-B" in transient_strengthen) 127apply (auto simp add: ensures_def transient_type [THEN subsetD]) 128done 129 130lemma ensuresD: "F \<in> A ensures B ==> F:(A-B) co (A \<union> B) & F \<in> transient (A-B)" 131by (unfold ensures_def, auto) 132 133lemma ensures_weaken_R: "[|F \<in> A ensures A'; A'<=B' |] ==> F \<in> A ensures B'" 134apply (unfold ensures_def) 135apply (blast intro: transient_strengthen constrains_weaken) 136done 137 138(*The L-version (precondition strengthening) fails, but we have this*) 139lemma stable_ensures_Int: 140 "[| F \<in> stable(C); F \<in> A ensures B |] ==> F:(C \<inter> A) ensures (C \<inter> B)" 141 142apply (unfold ensures_def) 143apply (simp (no_asm) add: Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric]) 144apply (blast intro: transient_strengthen stable_constrains_Int constrains_weaken) 145done 146 147lemma stable_transient_ensures: "[|F \<in> stable(A); F \<in> transient(C); A<=B \<union> C|] ==> F \<in> A ensures B" 148apply (frule stable_type [THEN subsetD]) 149apply (simp add: ensures_def stable_def) 150apply (blast intro: transient_strengthen constrains_weaken) 151done 152 153lemma ensures_eq: "(A ensures B) = (A unless B) \<inter> transient (A-B)" 154by (auto simp add: ensures_def unless_def) 155 156lemma subset_imp_ensures: "[| F \<in> program; A<=B |] ==> F \<in> A ensures B" 157by (auto simp add: ensures_def constrains_def transient_def st_set_def) 158 159(*** leadsTo ***) 160lemmas leads_left = leads.dom_subset [THEN subsetD, THEN SigmaD1] 161lemmas leads_right = leads.dom_subset [THEN subsetD, THEN SigmaD2] 162 163lemma leadsTo_type: "A \<longmapsto> B \<subseteq> program" 164by (unfold leadsTo_def, auto) 165 166lemma leadsToD2: 167"F \<in> A \<longmapsto> B ==> F \<in> program & st_set(A) & st_set(B)" 168apply (unfold leadsTo_def st_set_def) 169apply (blast dest: leads_left leads_right) 170done 171 172lemma leadsTo_Basis: 173 "[|F \<in> A ensures B; st_set(A); st_set(B)|] ==> F \<in> A \<longmapsto> B" 174apply (unfold leadsTo_def st_set_def) 175apply (cut_tac ensures_type) 176apply (auto intro: leads.Basis) 177done 178declare leadsTo_Basis [intro] 179 180(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *) 181(* [| F \<in> program; A<=B; st_set(A); st_set(B) |] ==> A \<longmapsto> B *) 182lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis] 183 184lemma leadsTo_Trans: "[|F \<in> A \<longmapsto> B; F \<in> B \<longmapsto> C |]==>F \<in> A \<longmapsto> C" 185apply (unfold leadsTo_def) 186apply (auto intro: leads.Trans) 187done 188 189(* Better when used in association with leadsTo_weaken_R *) 190lemma transient_imp_leadsTo: "F \<in> transient(A) ==> F \<in> A \<longmapsto> (state-A)" 191apply (unfold transient_def) 192apply (blast intro: ensuresI [THEN leadsTo_Basis] constrains_weaken transientI) 193done 194 195(*Useful with cancellation, disjunction*) 196lemma leadsTo_Un_duplicate: "F \<in> A \<longmapsto> (A' \<union> A') ==> F \<in> A \<longmapsto> A'" 197by simp 198 199lemma leadsTo_Un_duplicate2: 200 "F \<in> A \<longmapsto> (A' \<union> C \<union> C) ==> F \<in> A \<longmapsto> (A' \<union> C)" 201by (simp add: Un_ac) 202 203(*The Union introduction rule as we should have liked to state it*) 204lemma leadsTo_Union: 205 "[|!!A. A \<in> S ==> F \<in> A \<longmapsto> B; F \<in> program; st_set(B)|] 206 ==> F \<in> \<Union>(S) \<longmapsto> B" 207apply (unfold leadsTo_def st_set_def) 208apply (blast intro: leads.Union dest: leads_left) 209done 210 211lemma leadsTo_Union_Int: 212 "[|!!A. A \<in> S ==>F \<in> (A \<inter> C) \<longmapsto> B; F \<in> program; st_set(B)|] 213 ==> F \<in> (\<Union>(S)Int C)\<longmapsto> B" 214apply (unfold leadsTo_def st_set_def) 215apply (simp only: Int_Union_Union) 216apply (blast dest: leads_left intro: leads.Union) 217done 218 219lemma leadsTo_UN: 220 "[| !!i. i \<in> I ==> F \<in> A(i) \<longmapsto> B; F \<in> program; st_set(B)|] 221 ==> F:(\<Union>i \<in> I. A(i)) \<longmapsto> B" 222apply (simp add: Int_Union_Union leadsTo_def st_set_def) 223apply (blast dest: leads_left intro: leads.Union) 224done 225 226(* Binary union introduction rule *) 227lemma leadsTo_Un: 228 "[| F \<in> A \<longmapsto> C; F \<in> B \<longmapsto> C |] ==> F \<in> (A \<union> B) \<longmapsto> C" 229apply (subst Un_eq_Union) 230apply (blast intro: leadsTo_Union dest: leadsToD2) 231done 232 233lemma single_leadsTo_I: 234 "[|!!x. x \<in> A==> F:{x} \<longmapsto> B; F \<in> program; st_set(B) |] 235 ==> F \<in> A \<longmapsto> B" 236apply (rule_tac b = A in UN_singleton [THEN subst]) 237apply (rule leadsTo_UN, auto) 238done 239 240lemma leadsTo_refl: "[| F \<in> program; st_set(A) |] ==> F \<in> A \<longmapsto> A" 241by (blast intro: subset_imp_leadsTo) 242 243lemma leadsTo_refl_iff: "F \<in> A \<longmapsto> A \<longleftrightarrow> F \<in> program & st_set(A)" 244by (auto intro: leadsTo_refl dest: leadsToD2) 245 246lemma empty_leadsTo: "F \<in> 0 \<longmapsto> B \<longleftrightarrow> (F \<in> program & st_set(B))" 247by (auto intro: subset_imp_leadsTo dest: leadsToD2) 248declare empty_leadsTo [iff] 249 250lemma leadsTo_state: "F \<in> A \<longmapsto> state \<longleftrightarrow> (F \<in> program & st_set(A))" 251by (auto intro: subset_imp_leadsTo dest: leadsToD2 st_setD) 252declare leadsTo_state [iff] 253 254lemma leadsTo_weaken_R: "[| F \<in> A \<longmapsto> A'; A'<=B'; st_set(B') |] ==> F \<in> A \<longmapsto> B'" 255by (blast dest: leadsToD2 intro: subset_imp_leadsTo leadsTo_Trans) 256 257lemma leadsTo_weaken_L: "[| F \<in> A \<longmapsto> A'; B<=A |] ==> F \<in> B \<longmapsto> A'" 258apply (frule leadsToD2) 259apply (blast intro: leadsTo_Trans subset_imp_leadsTo st_set_subset) 260done 261 262lemma leadsTo_weaken: "[| F \<in> A \<longmapsto> A'; B<=A; A'<=B'; st_set(B')|]==> F \<in> B \<longmapsto> B'" 263apply (frule leadsToD2) 264apply (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans leadsTo_refl) 265done 266 267(* This rule has a nicer conclusion *) 268lemma transient_imp_leadsTo2: "[| F \<in> transient(A); state-A<=B; st_set(B)|] ==> F \<in> A \<longmapsto> B" 269apply (frule transientD2) 270apply (rule leadsTo_weaken_R) 271apply (auto simp add: transient_imp_leadsTo) 272done 273 274(*Distributes over binary unions*) 275lemma leadsTo_Un_distrib: "F:(A \<union> B) \<longmapsto> C \<longleftrightarrow> (F \<in> A \<longmapsto> C & F \<in> B \<longmapsto> C)" 276by (blast intro: leadsTo_Un leadsTo_weaken_L) 277 278lemma leadsTo_UN_distrib: 279"(F:(\<Union>i \<in> I. A(i)) \<longmapsto> B)\<longleftrightarrow> ((\<forall>i \<in> I. F \<in> A(i) \<longmapsto> B) & F \<in> program & st_set(B))" 280apply (blast dest: leadsToD2 intro: leadsTo_UN leadsTo_weaken_L) 281done 282 283lemma leadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto> B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A \<longmapsto> B) & F \<in> program & st_set(B)" 284by (blast dest: leadsToD2 intro: leadsTo_Union leadsTo_weaken_L) 285 286text\<open>Set difference: maybe combine with \<open>leadsTo_weaken_L\<close>??\<close> 287lemma leadsTo_Diff: 288 "[| F: (A-B) \<longmapsto> C; F \<in> B \<longmapsto> C; st_set(C) |] 289 ==> F \<in> A \<longmapsto> C" 290by (blast intro: leadsTo_Un leadsTo_weaken dest: leadsToD2) 291 292lemma leadsTo_UN_UN: 293 "[|!!i. i \<in> I ==> F \<in> A(i) \<longmapsto> A'(i); F \<in> program |] 294 ==> F: (\<Union>i \<in> I. A(i)) \<longmapsto> (\<Union>i \<in> I. A'(i))" 295apply (rule leadsTo_Union) 296apply (auto intro: leadsTo_weaken_R dest: leadsToD2) 297done 298 299(*Binary union version*) 300lemma leadsTo_Un_Un: "[| F \<in> A \<longmapsto> A'; F \<in> B \<longmapsto> B' |] ==> F \<in> (A \<union> B) \<longmapsto> (A' \<union> B')" 301apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') ") 302prefer 2 apply (blast dest: leadsToD2) 303apply (blast intro: leadsTo_Un leadsTo_weaken_R) 304done 305 306(** The cancellation law **) 307lemma leadsTo_cancel2: "[|F \<in> A \<longmapsto> (A' \<union> B); F \<in> B \<longmapsto> B'|] ==> F \<in> A \<longmapsto> (A' \<union> B')" 308apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') &F \<in> program") 309prefer 2 apply (blast dest: leadsToD2) 310apply (blast intro: leadsTo_Trans leadsTo_Un_Un leadsTo_refl) 311done 312 313lemma leadsTo_cancel_Diff2: "[|F \<in> A \<longmapsto> (A' \<union> B); F \<in> (B-A') \<longmapsto> B'|]==> F \<in> A \<longmapsto> (A' \<union> B')" 314apply (rule leadsTo_cancel2) 315prefer 2 apply assumption 316apply (blast dest: leadsToD2 intro: leadsTo_weaken_R) 317done 318 319 320lemma leadsTo_cancel1: "[| F \<in> A \<longmapsto> (B \<union> A'); F \<in> B \<longmapsto> B' |] ==> F \<in> A \<longmapsto> (B' \<union> A')" 321apply (simp add: Un_commute) 322apply (blast intro!: leadsTo_cancel2) 323done 324 325lemma leadsTo_cancel_Diff1: 326 "[|F \<in> A \<longmapsto> (B \<union> A'); F: (B-A') \<longmapsto> B'|]==> F \<in> A \<longmapsto> (B' \<union> A')" 327apply (rule leadsTo_cancel1) 328prefer 2 apply assumption 329apply (blast intro: leadsTo_weaken_R dest: leadsToD2) 330done 331 332(*The INDUCTION rule as we should have liked to state it*) 333lemma leadsTo_induct: 334 assumes major: "F \<in> za \<longmapsto> zb" 335 and basis: "!!A B. [|F \<in> A ensures B; st_set(A); st_set(B)|] ==> P(A,B)" 336 and trans: "!!A B C. [| F \<in> A \<longmapsto> B; P(A, B); 337 F \<in> B \<longmapsto> C; P(B, C) |] ==> P(A,C)" 338 and union: "!!B S. [| \<forall>A \<in> S. F \<in> A \<longmapsto> B; \<forall>A \<in> S. P(A,B); 339 st_set(B); \<forall>A \<in> S. st_set(A)|] ==> P(\<Union>(S), B)" 340 shows "P(za, zb)" 341apply (cut_tac major) 342apply (unfold leadsTo_def, clarify) 343apply (erule leads.induct) 344 apply (blast intro: basis [unfolded st_set_def]) 345 apply (blast intro: trans [unfolded leadsTo_def]) 346apply (force intro: union [unfolded st_set_def leadsTo_def]) 347done 348 349 350(* Added by Sidi, an induction rule without ensures *) 351lemma leadsTo_induct2: 352 assumes major: "F \<in> za \<longmapsto> zb" 353 and basis1: "!!A B. [| A<=B; st_set(B) |] ==> P(A, B)" 354 and basis2: "!!A B. [| F \<in> A co A \<union> B; F \<in> transient(A); st_set(B) |] 355 ==> P(A, B)" 356 and trans: "!!A B C. [| F \<in> A \<longmapsto> B; P(A, B); 357 F \<in> B \<longmapsto> C; P(B, C) |] ==> P(A,C)" 358 and union: "!!B S. [| \<forall>A \<in> S. F \<in> A \<longmapsto> B; \<forall>A \<in> S. P(A,B); 359 st_set(B); \<forall>A \<in> S. st_set(A)|] ==> P(\<Union>(S), B)" 360 shows "P(za, zb)" 361apply (cut_tac major) 362apply (erule leadsTo_induct) 363apply (auto intro: trans union) 364apply (simp add: ensures_def, clarify) 365apply (frule constrainsD2) 366apply (drule_tac B' = " (A-B) \<union> B" in constrains_weaken_R) 367apply blast 368apply (frule ensuresI2 [THEN leadsTo_Basis]) 369apply (drule_tac [4] basis2, simp_all) 370apply (frule_tac A1 = A and B = B in Int_lower2 [THEN basis1]) 371apply (subgoal_tac "A=\<Union>({A - B, A \<inter> B}) ") 372prefer 2 apply blast 373apply (erule ssubst) 374apply (rule union) 375apply (auto intro: subset_imp_leadsTo) 376done 377 378 379(** Variant induction rule: on the preconditions for B **) 380(*Lemma is the weak version: can't see how to do it in one step*) 381lemma leadsTo_induct_pre_aux: 382 "[| F \<in> za \<longmapsto> zb; 383 P(zb); 384 !!A B. [| F \<in> A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A); 385 !!S. [| \<forall>A \<in> S. P(A); \<forall>A \<in> S. st_set(A) |] ==> P(\<Union>(S)) 386 |] ==> P(za)" 387txt\<open>by induction on this formula\<close> 388apply (subgoal_tac "P (zb) \<longrightarrow> P (za) ") 389txt\<open>now solve first subgoal: this formula is sufficient\<close> 390apply (blast intro: leadsTo_refl) 391apply (erule leadsTo_induct) 392apply (blast+) 393done 394 395 396lemma leadsTo_induct_pre: 397 "[| F \<in> za \<longmapsto> zb; 398 P(zb); 399 !!A B. [| F \<in> A ensures B; F \<in> B \<longmapsto> zb; P(B); st_set(A) |] ==> P(A); 400 !!S. \<forall>A \<in> S. F \<in> A \<longmapsto> zb & P(A) & st_set(A) ==> P(\<Union>(S)) 401 |] ==> P(za)" 402apply (subgoal_tac " (F \<in> za \<longmapsto> zb) & P (za) ") 403apply (erule conjunct2) 404apply (frule leadsToD2) 405apply (erule leadsTo_induct_pre_aux) 406prefer 3 apply (blast dest: leadsToD2 intro: leadsTo_Union) 407prefer 2 apply (blast intro: leadsTo_Trans leadsTo_Basis) 408apply (blast intro: leadsTo_refl) 409done 410 411(** The impossibility law **) 412lemma leadsTo_empty: 413 "F \<in> A \<longmapsto> 0 ==> A=0" 414apply (erule leadsTo_induct_pre) 415apply (auto simp add: ensures_def constrains_def transient_def st_set_def) 416apply (drule bspec, assumption)+ 417apply blast 418done 419declare leadsTo_empty [simp] 420 421subsection\<open>PSP: Progress-Safety-Progress\<close> 422 423text\<open>Special case of PSP: Misra's "stable conjunction"\<close> 424 425lemma psp_stable: 426 "[| F \<in> A \<longmapsto> A'; F \<in> stable(B) |] ==> F:(A \<inter> B) \<longmapsto> (A' \<inter> B)" 427apply (unfold stable_def) 428apply (frule leadsToD2) 429apply (erule leadsTo_induct) 430prefer 3 apply (blast intro: leadsTo_Union_Int) 431prefer 2 apply (blast intro: leadsTo_Trans) 432apply (rule leadsTo_Basis) 433apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric]) 434apply (auto intro: transient_strengthen constrains_Int) 435done 436 437 438lemma psp_stable2: "[|F \<in> A \<longmapsto> A'; F \<in> stable(B) |]==>F: (B \<inter> A) \<longmapsto> (B \<inter> A')" 439apply (simp (no_asm_simp) add: psp_stable Int_ac) 440done 441 442lemma psp_ensures: 443"[| F \<in> A ensures A'; F \<in> B co B' |]==> F: (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))" 444apply (unfold ensures_def constrains_def st_set_def) 445(*speeds up the proof*) 446apply clarify 447apply (blast intro: transient_strengthen) 448done 449 450lemma psp: 451"[|F \<in> A \<longmapsto> A'; F \<in> B co B'; st_set(B')|]==> F:(A \<inter> B') \<longmapsto> ((A' \<inter> B) \<union> (B' - B))" 452apply (subgoal_tac "F \<in> program & st_set (A) & st_set (A') & st_set (B) ") 453prefer 2 apply (blast dest!: constrainsD2 leadsToD2) 454apply (erule leadsTo_induct) 455prefer 3 apply (blast intro: leadsTo_Union_Int) 456 txt\<open>Basis case\<close> 457 apply (blast intro: psp_ensures leadsTo_Basis) 458txt\<open>Transitivity case has a delicate argument involving "cancellation"\<close> 459apply (rule leadsTo_Un_duplicate2) 460apply (erule leadsTo_cancel_Diff1) 461apply (simp add: Int_Diff Diff_triv) 462apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset) 463done 464 465 466lemma psp2: "[| F \<in> A \<longmapsto> A'; F \<in> B co B'; st_set(B') |] 467 ==> F \<in> (B' \<inter> A) \<longmapsto> ((B \<inter> A') \<union> (B' - B))" 468by (simp (no_asm_simp) add: psp Int_ac) 469 470lemma psp_unless: 471 "[| F \<in> A \<longmapsto> A'; F \<in> B unless B'; st_set(B); st_set(B') |] 472 ==> F \<in> (A \<inter> B) \<longmapsto> ((A' \<inter> B) \<union> B')" 473apply (unfold unless_def) 474apply (subgoal_tac "st_set (A) &st_set (A') ") 475prefer 2 apply (blast dest: leadsToD2) 476apply (drule psp, assumption, blast) 477apply (blast intro: leadsTo_weaken) 478done 479 480 481subsection\<open>Proving the induction rules\<close> 482 483(** The most general rule \<in> r is any wf relation; f is any variant function **) 484lemma leadsTo_wf_induct_aux: "[| wf(r); 485 m \<in> I; 486 field(r)<=I; 487 F \<in> program; st_set(B); 488 \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) \<longmapsto> 489 ((A \<inter> f-``(converse(r)``{m})) \<union> B) |] 490 ==> F \<in> (A \<inter> f-``{m}) \<longmapsto> B" 491apply (erule_tac a = m in wf_induct2, simp_all) 492apply (subgoal_tac "F \<in> (A \<inter> (f-`` (converse (r) ``{x}))) \<longmapsto> B") 493 apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate) 494apply (subst vimage_eq_UN) 495apply (simp del: UN_simps add: Int_UN_distrib) 496apply (auto intro: leadsTo_UN simp del: UN_simps simp add: Int_UN_distrib) 497done 498 499(** Meta or object quantifier ? **) 500lemma leadsTo_wf_induct: "[| wf(r); 501 field(r)<=I; 502 A<=f-``I; 503 F \<in> program; st_set(A); st_set(B); 504 \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) \<longmapsto> 505 ((A \<inter> f-``(converse(r)``{m})) \<union> B) |] 506 ==> F \<in> A \<longmapsto> B" 507apply (rule_tac b = A in subst) 508 defer 1 509 apply (rule_tac I = I in leadsTo_UN) 510 apply (erule_tac I = I in leadsTo_wf_induct_aux, assumption+, best) 511done 512 513lemma nat_measure_field: "field(measure(nat, %x. x)) = nat" 514apply (unfold field_def) 515apply (simp add: measure_def) 516apply (rule equalityI, force, clarify) 517apply (erule_tac V = "x\<notin>range (y)" for y in thin_rl) 518apply (erule nat_induct) 519apply (rule_tac [2] b = "succ (succ (xa))" in domainI) 520apply (rule_tac b = "succ (0) " in domainI) 521apply simp_all 522done 523 524 525lemma Image_inverse_lessThan: "k<A ==> measure(A, %x. x) -`` {k} = k" 526apply (rule equalityI) 527apply (auto simp add: measure_def) 528apply (blast intro: ltD) 529apply (rule vimageI) 530prefer 2 apply blast 531apply (simp add: lt_Ord lt_Ord2 Ord_mem_iff_lt) 532apply (blast intro: lt_trans) 533done 534 535(*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) \<longmapsto> B*) 536lemma lessThan_induct: 537 "[| A<=f-``nat; 538 F \<in> program; st_set(A); st_set(B); 539 \<forall>m \<in> nat. F:(A \<inter> f-``{m}) \<longmapsto> ((A \<inter> f -`` m) \<union> B) |] 540 ==> F \<in> A \<longmapsto> B" 541apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN leadsTo_wf_induct]) 542apply (simp_all add: nat_measure_field) 543apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric]) 544done 545 546 547(*** wlt ****) 548 549(*Misra's property W3*) 550lemma wlt_type: "wlt(F,B) <=state" 551by (unfold wlt_def, auto) 552 553lemma wlt_st_set: "st_set(wlt(F, B))" 554apply (unfold st_set_def) 555apply (rule wlt_type) 556done 557declare wlt_st_set [iff] 558 559lemma wlt_leadsTo_iff: "F \<in> wlt(F, B) \<longmapsto> B \<longleftrightarrow> (F \<in> program & st_set(B))" 560apply (unfold wlt_def) 561apply (blast dest: leadsToD2 intro!: leadsTo_Union) 562done 563 564(* [| F \<in> program; st_set(B) |] ==> F \<in> wlt(F, B) \<longmapsto> B *) 565lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]] 566 567lemma leadsTo_subset: "F \<in> A \<longmapsto> B ==> A \<subseteq> wlt(F, B)" 568apply (unfold wlt_def) 569apply (frule leadsToD2) 570apply (auto simp add: st_set_def) 571done 572 573(*Misra's property W2*) 574lemma leadsTo_eq_subset_wlt: "F \<in> A \<longmapsto> B \<longleftrightarrow> (A \<subseteq> wlt(F,B) & F \<in> program & st_set(B))" 575apply auto 576apply (blast dest: leadsToD2 leadsTo_subset intro: leadsTo_weaken_L wlt_leadsTo)+ 577done 578 579(*Misra's property W4*) 580lemma wlt_increasing: "[| F \<in> program; st_set(B) |] ==> B \<subseteq> wlt(F,B)" 581apply (rule leadsTo_subset) 582apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [THEN iff_sym] subset_imp_leadsTo) 583done 584 585(*Used in the Trans case below*) 586lemma leadsTo_123_aux: 587 "[| B \<subseteq> A2; 588 F \<in> (A1 - B) co (A1 \<union> B); 589 F \<in> (A2 - C) co (A2 \<union> C) |] 590 ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)" 591apply (unfold constrains_def st_set_def, blast) 592done 593 594(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) 595(* slightly different from the HOL one \<in> B here is bounded *) 596lemma leadsTo_123: "F \<in> A \<longmapsto> A' 597 ==> \<exists>B \<in> Pow(state). A<=B & F \<in> B \<longmapsto> A' & F \<in> (B-A') co (B \<union> A')" 598apply (frule leadsToD2) 599apply (erule leadsTo_induct) 600 txt\<open>Basis\<close> 601 apply (blast dest: ensuresD constrainsD2 st_setD) 602 txt\<open>Trans\<close> 603 apply clarify 604 apply (rule_tac x = "Ba \<union> Bb" in bexI) 605 apply (blast intro: leadsTo_123_aux leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate, blast) 606txt\<open>Union\<close> 607apply (clarify dest!: ball_conj_distrib [THEN iffD1]) 608apply (subgoal_tac "\<exists>y. y \<in> Pi (S, %A. {Ba \<in> Pow (state) . A<=Ba & F \<in> Ba \<longmapsto> B & F \<in> Ba - B co Ba \<union> B}) ") 609defer 1 610apply (rule AC_ball_Pi, safe) 611apply (rotate_tac 1) 612apply (drule_tac x = x in bspec, blast, blast) 613apply (rule_tac x = "\<Union>A \<in> S. y`A" in bexI, safe) 614apply (rule_tac [3] I1 = S in constrains_UN [THEN constrains_weaken]) 615apply (rule_tac [2] leadsTo_Union) 616prefer 5 apply (blast dest!: apply_type, simp_all) 617apply (force dest!: apply_type)+ 618done 619 620 621(*Misra's property W5*) 622lemma wlt_constrains_wlt: "[| F \<in> program; st_set(B) |] ==>F \<in> (wlt(F, B) - B) co (wlt(F,B))" 623apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], assumption, blast) 624apply clarify 625apply (subgoal_tac "Ba = wlt (F,B) ") 626prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify) 627apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]]) 628done 629 630 631subsection\<open>Completion: Binary and General Finite versions\<close> 632 633lemma completion_aux: "[| W = wlt(F, (B' \<union> C)); 634 F \<in> A \<longmapsto> (A' \<union> C); F \<in> A' co (A' \<union> C); 635 F \<in> B \<longmapsto> (B' \<union> C); F \<in> B' co (B' \<union> C) |] 636 ==> F \<in> (A \<inter> B) \<longmapsto> ((A' \<inter> B') \<union> C)" 637apply (subgoal_tac "st_set (C) &st_set (W) &st_set (W-C) &st_set (A') &st_set (A) & st_set (B) & st_set (B') & F \<in> program") 638 prefer 2 639 apply simp 640 apply (blast dest!: leadsToD2) 641apply (subgoal_tac "F \<in> (W-C) co (W \<union> B' \<union> C) ") 642 prefer 2 643 apply (blast intro!: constrains_weaken [OF constrains_Un [OF _ wlt_constrains_wlt]]) 644apply (subgoal_tac "F \<in> (W-C) co W") 645 prefer 2 646 apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]] Un_assoc) 647apply (subgoal_tac "F \<in> (A \<inter> W - C) \<longmapsto> (A' \<inter> W \<union> C) ") 648 prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken]) 649(** step 13 **) 650apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) \<longmapsto> (A' \<inter> B' \<union> C) ") 651apply (drule leadsTo_Diff) 652apply (blast intro: subset_imp_leadsTo dest: leadsToD2 constrainsD2) 653apply (force simp add: st_set_def) 654apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W") 655prefer 2 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono]) 656apply (blast intro: leadsTo_Trans subset_imp_leadsTo) 657txt\<open>last subgoal\<close> 658apply (rule_tac leadsTo_Un_duplicate2) 659apply (rule_tac leadsTo_Un_Un) 660 prefer 2 apply (blast intro: leadsTo_refl) 661apply (rule_tac A'1 = "B' \<union> C" in wlt_leadsTo[THEN psp2, THEN leadsTo_weaken]) 662apply blast+ 663done 664 665lemmas completion = refl [THEN completion_aux] 666 667lemma finite_completion_aux: 668 "[| I \<in> Fin(X); F \<in> program; st_set(C) |] ==> 669 (\<forall>i \<in> I. F \<in> (A(i)) \<longmapsto> (A'(i) \<union> C)) \<longrightarrow> 670 (\<forall>i \<in> I. F \<in> (A'(i)) co (A'(i) \<union> C)) \<longrightarrow> 671 F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto> ((\<Inter>i \<in> I. A'(i)) \<union> C)" 672apply (erule Fin_induct) 673apply (auto simp add: Inter_0) 674apply (rule completion) 675apply (auto simp del: INT_simps simp add: INT_extend_simps) 676apply (blast intro: constrains_INT) 677done 678 679lemma finite_completion: 680 "[| I \<in> Fin(X); 681 !!i. i \<in> I ==> F \<in> A(i) \<longmapsto> (A'(i) \<union> C); 682 !!i. i \<in> I ==> F \<in> A'(i) co (A'(i) \<union> C); F \<in> program; st_set(C)|] 683 ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto> ((\<Inter>i \<in> I. A'(i)) \<union> C)" 684by (blast intro: finite_completion_aux [THEN mp, THEN mp]) 685 686lemma stable_completion: 687 "[| F \<in> A \<longmapsto> A'; F \<in> stable(A'); 688 F \<in> B \<longmapsto> B'; F \<in> stable(B') |] 689 ==> F \<in> (A \<inter> B) \<longmapsto> (A' \<inter> B')" 690apply (unfold stable_def) 691apply (rule_tac C1 = 0 in completion [THEN leadsTo_weaken_R], simp+) 692apply (blast dest: leadsToD2) 693done 694 695 696lemma finite_stable_completion: 697 "[| I \<in> Fin(X); 698 (!!i. i \<in> I ==> F \<in> A(i) \<longmapsto> A'(i)); 699 (!!i. i \<in> I ==> F \<in> stable(A'(i))); F \<in> program |] 700 ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto> (\<Inter>i \<in> I. A'(i))" 701apply (unfold stable_def) 702apply (subgoal_tac "st_set (\<Inter>i \<in> I. A' (i))") 703prefer 2 apply (blast dest: leadsToD2) 704apply (rule_tac C1 = 0 in finite_completion [THEN leadsTo_weaken_R], auto) 705done 706 707end 708