1(* Title: ZF/UNITY/Union.thy 2 Author: Sidi O Ehmety, Computer Laboratory 3 Copyright 2001 University of Cambridge 4 5Unions of programs 6 7Partly from Misra's Chapter 5 \<in> Asynchronous Compositions of Programs 8 9Theory ported form HOL.. 10 11*) 12 13theory Union imports SubstAx FP 14begin 15 16definition 17 (*FIXME: conjoin Init(F) \<inter> Init(G) \<noteq> 0 *) 18 ok :: "[i, i] => o" (infixl "ok" 65) where 19 "F ok G == Acts(F) \<subseteq> AllowedActs(G) & 20 Acts(G) \<subseteq> AllowedActs(F)" 21 22definition 23 (*FIXME: conjoin (\<Inter>i \<in> I. Init(F(i))) \<noteq> 0 *) 24 OK :: "[i, i=>i] => o" where 25 "OK(I,F) == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts(F(i)) \<subseteq> AllowedActs(F(j)))" 26 27definition 28 JOIN :: "[i, i=>i] => i" where 29 "JOIN(I,F) == if I = 0 then SKIP else 30 mk_program(\<Inter>i \<in> I. Init(F(i)), \<Union>i \<in> I. Acts(F(i)), 31 \<Inter>i \<in> I. AllowedActs(F(i)))" 32 33definition 34 Join :: "[i, i] => i" (infixl "\<squnion>" 65) where 35 "F \<squnion> G == mk_program (Init(F) \<inter> Init(G), Acts(F) \<union> Acts(G), 36 AllowedActs(F) \<inter> AllowedActs(G))" 37definition 38 (*Characterizes safety properties. Used with specifying AllowedActs*) 39 safety_prop :: "i => o" where 40 "safety_prop(X) == X\<subseteq>program & 41 SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)" 42 43syntax 44 "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion>_./ _)" 10) 45 "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion>_ \<in> _./ _)" 10) 46 47translations 48 "\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))" 49 "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B" 50 "\<Squnion>x. B" == "CONST JOIN(CONST state, (\<lambda>x. B))" 51 52 53subsection\<open>SKIP\<close> 54 55lemma reachable_SKIP [simp]: "reachable(SKIP) = state" 56by (force elim: reachable.induct intro: reachable.intros) 57 58text\<open>Elimination programify from ok and \<squnion>\<close> 59 60lemma ok_programify_left [iff]: "programify(F) ok G \<longleftrightarrow> F ok G" 61by (simp add: ok_def) 62 63lemma ok_programify_right [iff]: "F ok programify(G) \<longleftrightarrow> F ok G" 64by (simp add: ok_def) 65 66lemma Join_programify_left [simp]: "programify(F) \<squnion> G = F \<squnion> G" 67by (simp add: Join_def) 68 69lemma Join_programify_right [simp]: "F \<squnion> programify(G) = F \<squnion> G" 70by (simp add: Join_def) 71 72subsection\<open>SKIP and safety properties\<close> 73 74lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) \<longleftrightarrow> (A\<subseteq>B & st_set(A))" 75by (unfold constrains_def st_set_def, auto) 76 77lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B)\<longleftrightarrow> (state \<inter> A\<subseteq>B)" 78by (unfold Constrains_def, auto) 79 80lemma SKIP_in_stable [iff]: "SKIP \<in> stable(A) \<longleftrightarrow> st_set(A)" 81by (auto simp add: stable_def) 82 83lemma SKIP_in_Stable [iff]: "SKIP \<in> Stable(A)" 84by (unfold Stable_def, auto) 85 86subsection\<open>Join and JOIN types\<close> 87 88lemma Join_in_program [iff,TC]: "F \<squnion> G \<in> program" 89by (unfold Join_def, auto) 90 91lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \<in> program" 92by (unfold JOIN_def, auto) 93 94subsection\<open>Init, Acts, and AllowedActs of Join and JOIN\<close> 95lemma Init_Join [simp]: "Init(F \<squnion> G) = Init(F) \<inter> Init(G)" 96by (simp add: Int_assoc Join_def) 97 98lemma Acts_Join [simp]: "Acts(F \<squnion> G) = Acts(F) \<union> Acts(G)" 99by (simp add: Int_Un_distrib2 cons_absorb Join_def) 100 101lemma AllowedActs_Join [simp]: "AllowedActs(F \<squnion> G) = 102 AllowedActs(F) \<inter> AllowedActs(G)" 103apply (simp add: Int_assoc cons_absorb Join_def) 104done 105 106subsection\<open>Join's algebraic laws\<close> 107 108lemma Join_commute: "F \<squnion> G = G \<squnion> F" 109by (simp add: Join_def Un_commute Int_commute) 110 111lemma Join_left_commute: "A \<squnion> (B \<squnion> C) = B \<squnion> (A \<squnion> C)" 112apply (simp add: Join_def Int_Un_distrib2 cons_absorb) 113apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb) 114done 115 116lemma Join_assoc: "(F \<squnion> G) \<squnion> H = F \<squnion> (G \<squnion> H)" 117by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2) 118 119subsection\<open>Needed below\<close> 120lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)" 121by auto 122 123lemma Join_SKIP_left [simp]: "SKIP \<squnion> F = programify(F)" 124apply (unfold Join_def SKIP_def) 125apply (auto simp add: Int_absorb cons_eq) 126done 127 128lemma Join_SKIP_right [simp]: "F \<squnion> SKIP = programify(F)" 129apply (subst Join_commute) 130apply (simp add: Join_SKIP_left) 131done 132 133lemma Join_absorb [simp]: "F \<squnion> F = programify(F)" 134by (rule program_equalityI, auto) 135 136lemma Join_left_absorb: "F \<squnion> (F \<squnion> G) = F \<squnion> G" 137by (simp add: Join_assoc [symmetric]) 138 139subsection\<open>Join is an AC-operator\<close> 140lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute 141 142subsection\<open>Eliminating programify form JOIN and OK expressions\<close> 143 144lemma OK_programify [iff]: "OK(I, %x. programify(F(x))) \<longleftrightarrow> OK(I, F)" 145by (simp add: OK_def) 146 147lemma JOIN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)" 148by (simp add: JOIN_def) 149 150 151subsection\<open>JOIN\<close> 152 153lemma JOIN_empty [simp]: "JOIN(0, F) = SKIP" 154by (unfold JOIN_def, auto) 155 156lemma Init_JOIN [simp]: 157 "Init(\<Squnion>i \<in> I. F(i)) = (if I=0 then state else (\<Inter>i \<in> I. Init(F(i))))" 158by (simp add: JOIN_def INT_extend_simps del: INT_simps) 159 160lemma Acts_JOIN [simp]: 161 "Acts(JOIN(I,F)) = cons(id(state), \<Union>i \<in> I. Acts(F(i)))" 162apply (unfold JOIN_def) 163apply (auto simp del: INT_simps UN_simps) 164apply (rule equalityI) 165apply (auto dest: Acts_type [THEN subsetD]) 166done 167 168lemma AllowedActs_JOIN [simp]: 169 "AllowedActs(\<Squnion>i \<in> I. F(i)) = 170 (if I=0 then Pow(state*state) else (\<Inter>i \<in> I. AllowedActs(F(i))))" 171apply (unfold JOIN_def, auto) 172apply (rule equalityI) 173apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD]) 174done 175 176lemma JOIN_cons [simp]: "(\<Squnion>i \<in> cons(a,I). F(i)) = F(a) \<squnion> (\<Squnion>i \<in> I. F(i))" 177by (rule program_equalityI, auto) 178 179lemma JOIN_cong [cong]: 180 "[| I=J; !!i. i \<in> J ==> F(i) = G(i) |] ==> 181 (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> J. G(i))" 182by (simp add: JOIN_def) 183 184 185 186subsection\<open>JOIN laws\<close> 187lemma JOIN_absorb: "k \<in> I ==>F(k) \<squnion> (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> I. F(i))" 188apply (subst JOIN_cons [symmetric]) 189apply (auto simp add: cons_absorb) 190done 191 192lemma JOIN_Un: "(\<Squnion>i \<in> I \<union> J. F(i)) = ((\<Squnion>i \<in> I. F(i)) \<squnion> (\<Squnion>i \<in> J. F(i)))" 193apply (rule program_equalityI) 194apply (simp_all add: UN_Un INT_Un) 195apply (simp_all del: INT_simps add: INT_extend_simps, blast) 196done 197 198lemma JOIN_constant: "(\<Squnion>i \<in> I. c) = (if I=0 then SKIP else programify(c))" 199by (rule program_equalityI, auto) 200 201lemma JOIN_Join_distrib: 202 "(\<Squnion>i \<in> I. F(i) \<squnion> G(i)) = (\<Squnion>i \<in> I. F(i)) \<squnion> (\<Squnion>i \<in> I. G(i))" 203apply (rule program_equalityI) 204apply (simp_all add: INT_Int_distrib, blast) 205done 206 207lemma JOIN_Join_miniscope: "(\<Squnion>i \<in> I. F(i) \<squnion> G) = ((\<Squnion>i \<in> I. F(i) \<squnion> G))" 208by (simp add: JOIN_Join_distrib JOIN_constant) 209 210text\<open>Used to prove guarantees_JOIN_I\<close> 211lemma JOIN_Join_diff: "i \<in> I==>F(i) \<squnion> JOIN(I - {i}, F) = JOIN(I, F)" 212apply (rule program_equalityI) 213apply (auto elim!: not_emptyE) 214done 215 216subsection\<open>Safety: co, stable, FP\<close> 217 218 219(*Fails if I=0 because it collapses to SKIP \<in> A co B, i.e. to A\<subseteq>B. So an 220 alternative precondition is A\<subseteq>B, but most proofs using this rule require 221 I to be nonempty for other reasons anyway.*) 222 223lemma JOIN_constrains: 224 "i \<in> I==>(\<Squnion>i \<in> I. F(i)) \<in> A co B \<longleftrightarrow> (\<forall>i \<in> I. programify(F(i)) \<in> A co B)" 225 226apply (unfold constrains_def JOIN_def st_set_def, auto) 227prefer 2 apply blast 228apply (rename_tac j act y z) 229apply (cut_tac F = "F (j) " in Acts_type) 230apply (drule_tac x = act in bspec, auto) 231done 232 233lemma Join_constrains [iff]: 234 "(F \<squnion> G \<in> A co B) \<longleftrightarrow> (programify(F) \<in> A co B & programify(G) \<in> A co B)" 235by (auto simp add: constrains_def) 236 237lemma Join_unless [iff]: 238 "(F \<squnion> G \<in> A unless B) \<longleftrightarrow> 239 (programify(F) \<in> A unless B & programify(G) \<in> A unless B)" 240by (simp add: Join_constrains unless_def) 241 242 243(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. 244 reachable (F \<squnion> G) could be much bigger than reachable F, reachable G 245*) 246 247lemma Join_constrains_weaken: 248 "[| F \<in> A co A'; G \<in> B co B' |] 249 ==> F \<squnion> G \<in> (A \<inter> B) co (A' \<union> B')" 250apply (subgoal_tac "st_set (A) & st_set (B) & F \<in> program & G \<in> program") 251prefer 2 apply (blast dest: constrainsD2, simp) 252apply (blast intro: constrains_weaken) 253done 254 255(*If I=0, it degenerates to SKIP \<in> state co 0, which is false.*) 256lemma JOIN_constrains_weaken: 257 assumes major: "(!!i. i \<in> I ==> F(i) \<in> A(i) co A'(i))" 258 and minor: "i \<in> I" 259 shows "(\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))" 260apply (cut_tac minor) 261apply (simp (no_asm_simp) add: JOIN_constrains) 262apply clarify 263apply (rename_tac "j") 264apply (frule_tac i = j in major) 265apply (frule constrainsD2, simp) 266apply (blast intro: constrains_weaken) 267done 268 269lemma JOIN_stable: 270 "(\<Squnion>i \<in> I. F(i)) \<in> stable(A) \<longleftrightarrow> ((\<forall>i \<in> I. programify(F(i)) \<in> stable(A)) & st_set(A))" 271apply (auto simp add: stable_def constrains_def JOIN_def) 272apply (cut_tac F = "F (i) " in Acts_type) 273apply (drule_tac x = act in bspec, auto) 274done 275 276lemma initially_JOIN_I: 277 assumes major: "(!!i. i \<in> I ==>F(i) \<in> initially(A))" 278 and minor: "i \<in> I" 279 shows "(\<Squnion>i \<in> I. F(i)) \<in> initially(A)" 280apply (cut_tac minor) 281apply (auto elim!: not_emptyE simp add: Inter_iff initially_def) 282apply (frule_tac i = x in major) 283apply (auto simp add: initially_def) 284done 285 286lemma invariant_JOIN_I: 287 assumes major: "(!!i. i \<in> I ==> F(i) \<in> invariant(A))" 288 and minor: "i \<in> I" 289 shows "(\<Squnion>i \<in> I. F(i)) \<in> invariant(A)" 290apply (cut_tac minor) 291apply (auto intro!: initially_JOIN_I dest: major simp add: invariant_def JOIN_stable) 292apply (erule_tac V = "i \<in> I" in thin_rl) 293apply (frule major) 294apply (drule_tac [2] major) 295apply (auto simp add: invariant_def) 296apply (frule stableD2, force)+ 297done 298 299lemma Join_stable [iff]: 300 " (F \<squnion> G \<in> stable(A)) \<longleftrightarrow> 301 (programify(F) \<in> stable(A) & programify(G) \<in> stable(A))" 302by (simp add: stable_def) 303 304lemma initially_JoinI [intro!]: 305 "[| F \<in> initially(A); G \<in> initially(A) |] ==> F \<squnion> G \<in> initially(A)" 306by (unfold initially_def, auto) 307 308lemma invariant_JoinI: 309 "[| F \<in> invariant(A); G \<in> invariant(A) |] 310 ==> F \<squnion> G \<in> invariant(A)" 311apply (subgoal_tac "F \<in> program&G \<in> program") 312prefer 2 apply (blast dest: invariantD2) 313apply (simp add: invariant_def) 314apply (auto intro: Join_in_program) 315done 316 317 318(* Fails if I=0 because \<Inter>i \<in> 0. A(i) = 0 *) 319lemma FP_JOIN: "i \<in> I ==> FP(\<Squnion>i \<in> I. F(i)) = (\<Inter>i \<in> I. FP (programify(F(i))))" 320by (auto simp add: FP_def Inter_def st_set_def JOIN_stable) 321 322subsection\<open>Progress: transient, ensures\<close> 323 324lemma JOIN_transient: 325 "i \<in> I ==> 326 (\<Squnion>i \<in> I. F(i)) \<in> transient(A) \<longleftrightarrow> (\<exists>i \<in> I. programify(F(i)) \<in> transient(A))" 327apply (auto simp add: transient_def JOIN_def) 328apply (unfold st_set_def) 329apply (drule_tac [2] x = act in bspec) 330apply (auto dest: Acts_type [THEN subsetD]) 331done 332 333lemma Join_transient [iff]: 334 "F \<squnion> G \<in> transient(A) \<longleftrightarrow> 335 (programify(F) \<in> transient(A) | programify(G) \<in> transient(A))" 336apply (auto simp add: transient_def Join_def Int_Un_distrib2) 337done 338 339lemma Join_transient_I1: "F \<in> transient(A) ==> F \<squnion> G \<in> transient(A)" 340by (simp add: Join_transient transientD2) 341 342 343lemma Join_transient_I2: "G \<in> transient(A) ==> F \<squnion> G \<in> transient(A)" 344by (simp add: Join_transient transientD2) 345 346(*If I=0 it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A\<subseteq>B) *) 347lemma JOIN_ensures: 348 "i \<in> I ==> 349 (\<Squnion>i \<in> I. F(i)) \<in> A ensures B \<longleftrightarrow> 350 ((\<forall>i \<in> I. programify(F(i)) \<in> (A-B) co (A \<union> B)) & 351 (\<exists>i \<in> I. programify(F(i)) \<in> A ensures B))" 352by (auto simp add: ensures_def JOIN_constrains JOIN_transient) 353 354 355lemma Join_ensures: 356 "F \<squnion> G \<in> A ensures B \<longleftrightarrow> 357 (programify(F) \<in> (A-B) co (A \<union> B) & programify(G) \<in> (A-B) co (A \<union> B) & 358 (programify(F) \<in> transient (A-B) | programify(G) \<in> transient (A-B)))" 359 360apply (unfold ensures_def) 361apply (auto simp add: Join_transient) 362done 363 364lemma stable_Join_constrains: 365 "[| F \<in> stable(A); G \<in> A co A' |] 366 ==> F \<squnion> G \<in> A co A'" 367apply (unfold stable_def constrains_def Join_def st_set_def) 368apply (cut_tac F = F in Acts_type) 369apply (cut_tac F = G in Acts_type, force) 370done 371 372(*Premise for G cannot use Always because F \<in> Stable A is 373 weaker than G \<in> stable A *) 374lemma stable_Join_Always1: 375 "[| F \<in> stable(A); G \<in> invariant(A) |] ==> F \<squnion> G \<in> Always(A)" 376apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ") 377prefer 2 apply (blast dest: invariantD2 stableD2) 378apply (simp add: Always_def invariant_def initially_def Stable_eq_stable) 379apply (force intro: stable_Int) 380done 381 382(*As above, but exchanging the roles of F and G*) 383lemma stable_Join_Always2: 384 "[| F \<in> invariant(A); G \<in> stable(A) |] ==> F \<squnion> G \<in> Always(A)" 385apply (subst Join_commute) 386apply (blast intro: stable_Join_Always1) 387done 388 389 390 391lemma stable_Join_ensures1: 392 "[| F \<in> stable(A); G \<in> A ensures B |] ==> F \<squnion> G \<in> A ensures B" 393apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ") 394prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD]) 395apply (simp (no_asm_simp) add: Join_ensures) 396apply (simp add: stable_def ensures_def) 397apply (erule constrains_weaken, auto) 398done 399 400 401(*As above, but exchanging the roles of F and G*) 402lemma stable_Join_ensures2: 403 "[| F \<in> A ensures B; G \<in> stable(A) |] ==> F \<squnion> G \<in> A ensures B" 404apply (subst Join_commute) 405apply (blast intro: stable_Join_ensures1) 406done 407 408subsection\<open>The ok and OK relations\<close> 409 410lemma ok_SKIP1 [iff]: "SKIP ok F" 411by (auto dest: Acts_type [THEN subsetD] simp add: ok_def) 412 413lemma ok_SKIP2 [iff]: "F ok SKIP" 414by (auto dest: Acts_type [THEN subsetD] simp add: ok_def) 415 416lemma ok_Join_commute: 417 "(F ok G & (F \<squnion> G) ok H) \<longleftrightarrow> (G ok H & F ok (G \<squnion> H))" 418by (auto simp add: ok_def) 419 420lemma ok_commute: "(F ok G) \<longleftrightarrow>(G ok F)" 421by (auto simp add: ok_def) 422 423lemmas ok_sym = ok_commute [THEN iffD1] 424 425lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) \<longleftrightarrow> (F ok G & (F \<squnion> G) ok H)" 426by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb 427 Int_Un_distrib2 Ball_def, safe, force+) 428 429lemma ok_Join_iff1 [iff]: "F ok (G \<squnion> H) \<longleftrightarrow> (F ok G & F ok H)" 430by (auto simp add: ok_def) 431 432lemma ok_Join_iff2 [iff]: "(G \<squnion> H) ok F \<longleftrightarrow> (G ok F & H ok F)" 433by (auto simp add: ok_def) 434 435(*useful? Not with the previous two around*) 436lemma ok_Join_commute_I: "[| F ok G; (F \<squnion> G) ok H |] ==> F ok (G \<squnion> H)" 437by (auto simp add: ok_def) 438 439lemma ok_JOIN_iff1 [iff]: "F ok JOIN(I,G) \<longleftrightarrow> (\<forall>i \<in> I. F ok G(i))" 440by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def) 441 442lemma ok_JOIN_iff2 [iff]: "JOIN(I,G) ok F \<longleftrightarrow> (\<forall>i \<in> I. G(i) ok F)" 443apply (auto elim!: not_emptyE simp add: ok_def) 444apply (blast dest: Acts_type [THEN subsetD]) 445done 446 447lemma OK_iff_ok: "OK(I,F) \<longleftrightarrow> (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F(i) ok (F(j)))" 448by (auto simp add: ok_def OK_def) 449 450lemma OK_imp_ok: "[| OK(I,F); i \<in> I; j \<in> I; i\<noteq>j|] ==> F(i) ok F(j)" 451by (auto simp add: OK_iff_ok) 452 453 454lemma OK_0 [iff]: "OK(0,F)" 455by (simp add: OK_def) 456 457lemma OK_cons_iff: 458 "OK(cons(i, I), F) \<longleftrightarrow> 459 (i \<in> I & OK(I, F)) | (i\<notin>I & OK(I, F) & F(i) ok JOIN(I,F))" 460apply (simp add: OK_iff_ok) 461apply (blast intro: ok_sym) 462done 463 464 465subsection\<open>Allowed\<close> 466 467lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program" 468by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def) 469 470lemma Allowed_Join [simp]: 471 "Allowed(F \<squnion> G) = 472 Allowed(programify(F)) \<inter> Allowed(programify(G))" 473apply (auto simp add: Allowed_def) 474done 475 476lemma Allowed_JOIN [simp]: 477 "i \<in> I ==> 478 Allowed(JOIN(I,F)) = (\<Inter>i \<in> I. Allowed(programify(F(i))))" 479apply (auto simp add: Allowed_def, blast) 480done 481 482lemma ok_iff_Allowed: 483 "F ok G \<longleftrightarrow> (programify(F) \<in> Allowed(programify(G)) & 484 programify(G) \<in> Allowed(programify(F)))" 485by (simp add: ok_def Allowed_def) 486 487 488lemma OK_iff_Allowed: 489 "OK(I,F) \<longleftrightarrow> 490 (\<forall>i \<in> I. \<forall>j \<in> I-{i}. programify(F(i)) \<in> Allowed(programify(F(j))))" 491apply (auto simp add: OK_iff_ok ok_iff_Allowed) 492done 493 494subsection\<open>safety_prop, for reasoning about given instances of "ok"\<close> 495 496lemma safety_prop_Acts_iff: 497 "safety_prop(X) ==> (Acts(G) \<subseteq> cons(id(state), (\<Union>F \<in> X. Acts(F)))) \<longleftrightarrow> (programify(G) \<in> X)" 498apply (simp (no_asm_use) add: safety_prop_def) 499apply clarify 500apply (case_tac "G \<in> program", simp_all, blast, safe) 501prefer 2 apply force 502apply (force simp add: programify_def) 503done 504 505lemma safety_prop_AllowedActs_iff_Allowed: 506 "safety_prop(X) ==> 507 (\<Union>G \<in> X. Acts(G)) \<subseteq> AllowedActs(F) \<longleftrightarrow> (X \<subseteq> Allowed(programify(F)))" 508apply (simp add: Allowed_def safety_prop_Acts_iff [THEN iff_sym] 509 safety_prop_def, blast) 510done 511 512 513lemma Allowed_eq: 514 "safety_prop(X) ==> Allowed(mk_program(init, acts, \<Union>F \<in> X. Acts(F))) = X" 515apply (subgoal_tac "cons (id (state), \<Union>(RepFun (X, Acts)) \<inter> Pow (state * state)) = \<Union>(RepFun (X, Acts))") 516apply (rule_tac [2] equalityI) 517 apply (simp del: UN_simps add: Allowed_def safety_prop_Acts_iff safety_prop_def, auto) 518apply (force dest: Acts_type [THEN subsetD] simp add: safety_prop_def)+ 519done 520 521lemma def_prg_Allowed: 522 "[| F == mk_program (init, acts, \<Union>F \<in> X. Acts(F)); safety_prop(X) |] 523 ==> Allowed(F) = X" 524by (simp add: Allowed_eq) 525 526(*For safety_prop to hold, the property must be satisfiable!*) 527lemma safety_prop_constrains [iff]: 528 "safety_prop(A co B) \<longleftrightarrow> (A \<subseteq> B & st_set(A))" 529by (simp add: safety_prop_def constrains_def st_set_def, blast) 530 531(* To be used with resolution *) 532lemma safety_prop_constrainsI [iff]: 533 "[| A\<subseteq>B; st_set(A) |] ==>safety_prop(A co B)" 534by auto 535 536lemma safety_prop_stable [iff]: "safety_prop(stable(A)) \<longleftrightarrow> st_set(A)" 537by (simp add: stable_def) 538 539lemma safety_prop_stableI: "st_set(A) ==> safety_prop(stable(A))" 540by auto 541 542lemma safety_prop_Int [simp]: 543 "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X \<inter> Y)" 544apply (simp add: safety_prop_def, safe, blast) 545apply (drule_tac [2] B = "\<Union>(RepFun (X \<inter> Y, Acts))" and C = "\<Union>(RepFun (Y, Acts))" in subset_trans) 546apply (drule_tac B = "\<Union>(RepFun (X \<inter> Y, Acts))" and C = "\<Union>(RepFun (X, Acts))" in subset_trans) 547apply blast+ 548done 549 550(* If I=0 the conclusion becomes safety_prop(0) which is false *) 551lemma safety_prop_Inter: 552 assumes major: "(!!i. i \<in> I ==>safety_prop(X(i)))" 553 and minor: "i \<in> I" 554 shows "safety_prop(\<Inter>i \<in> I. X(i))" 555apply (simp add: safety_prop_def) 556apply (cut_tac minor, safe) 557apply (simp (no_asm_use) add: Inter_iff) 558apply clarify 559apply (frule major) 560apply (drule_tac [2] i = xa in major) 561apply (frule_tac [4] i = xa in major) 562apply (auto simp add: safety_prop_def) 563apply (drule_tac B = "\<Union>(RepFun (\<Inter>(RepFun (I, X)), Acts))" and C = "\<Union>(RepFun (X (xa), Acts))" in subset_trans) 564apply blast+ 565done 566 567lemma def_UNION_ok_iff: 568"[| F == mk_program(init,acts, \<Union>G \<in> X. Acts(G)); safety_prop(X) |] 569 ==> F ok G \<longleftrightarrow> (programify(G) \<in> X & acts \<inter> Pow(state*state) \<subseteq> AllowedActs(G))" 570apply (unfold ok_def) 571apply (drule_tac G = G in safety_prop_Acts_iff) 572apply (cut_tac F = G in AllowedActs_type) 573apply (cut_tac F = G in Acts_type, auto) 574done 575 576end 577