1(* Title: HOL/UNITY/Union.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5Partly from Misra's Chapter 5: Asynchronous Compositions of Programs. 6*) 7 8section\<open>Unions of Programs\<close> 9 10theory Union imports SubstAx FP begin 11 12 (*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) 13definition 14 ok :: "['a program, 'a program] => bool" (infixl "ok" 65) 15 where "F ok G == Acts F \<subseteq> AllowedActs G & 16 Acts G \<subseteq> AllowedActs F" 17 18 (*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *) 19definition 20 OK :: "['a set, 'a => 'b program] => bool" 21 where "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))" 22 23definition 24 JOIN :: "['a set, 'a => 'b program] => 'b program" 25 where "JOIN I F = mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i), 26 \<Inter>i \<in> I. AllowedActs (F i))" 27 28definition 29 Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65) 30 where "F \<squnion> G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G, 31 AllowedActs F \<inter> AllowedActs G)" 32 33definition SKIP :: "'a program" ("\<bottom>") 34 where "\<bottom> = mk_program (UNIV, {}, UNIV)" 35 36 (*Characterizes safety properties. Used with specifying Allowed*) 37definition 38 safety_prop :: "'a program set => bool" 39 where "safety_prop X \<longleftrightarrow> SKIP \<in> X \<and> (\<forall>G. Acts G \<subseteq> \<Union>(Acts ` X) \<longrightarrow> G \<in> X)" 40 41syntax 42 "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion>_./ _)" 10) 43 "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion>_\<in>_./ _)" 10) 44translations 45 "\<Squnion>x \<in> A. B" == "CONST JOIN A (\<lambda>x. B)" 46 "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B" 47 "\<Squnion>x. B" == "CONST JOIN (CONST UNIV) (\<lambda>x. B)" 48 49 50subsection\<open>SKIP\<close> 51 52lemma Init_SKIP [simp]: "Init SKIP = UNIV" 53by (simp add: SKIP_def) 54 55lemma Acts_SKIP [simp]: "Acts SKIP = {Id}" 56by (simp add: SKIP_def) 57 58lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV" 59by (auto simp add: SKIP_def) 60 61lemma reachable_SKIP [simp]: "reachable SKIP = UNIV" 62by (force elim: reachable.induct intro: reachable.intros) 63 64subsection\<open>SKIP and safety properties\<close> 65 66lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) = (A \<subseteq> B)" 67by (unfold constrains_def, auto) 68 69lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B) = (A \<subseteq> B)" 70by (unfold Constrains_def, auto) 71 72lemma SKIP_in_stable [iff]: "SKIP \<in> stable A" 73by (unfold stable_def, auto) 74 75declare SKIP_in_stable [THEN stable_imp_Stable, iff] 76 77 78subsection\<open>Join\<close> 79 80lemma Init_Join [simp]: "Init (F\<squnion>G) = Init F \<inter> Init G" 81by (simp add: Join_def) 82 83lemma Acts_Join [simp]: "Acts (F\<squnion>G) = Acts F \<union> Acts G" 84by (auto simp add: Join_def) 85 86lemma AllowedActs_Join [simp]: 87 "AllowedActs (F\<squnion>G) = AllowedActs F \<inter> AllowedActs G" 88by (auto simp add: Join_def) 89 90 91subsection\<open>JN\<close> 92 93lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP" 94by (unfold JOIN_def SKIP_def, auto) 95 96lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a)\<squnion>(\<Squnion>i \<in> I. F i)" 97apply (rule program_equalityI) 98apply (auto simp add: JOIN_def Join_def) 99done 100 101lemma Init_JN [simp]: "Init (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. Init (F i))" 102by (simp add: JOIN_def) 103 104lemma Acts_JN [simp]: "Acts (\<Squnion>i \<in> I. F i) = insert Id (\<Union>i \<in> I. Acts (F i))" 105by (auto simp add: JOIN_def) 106 107lemma AllowedActs_JN [simp]: 108 "AllowedActs (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. AllowedActs (F i))" 109by (auto simp add: JOIN_def) 110 111 112lemma JN_cong [cong]: 113 "[| I=J; !!i. i \<in> J ==> F i = G i |] ==> (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> J. G i)" 114by (simp add: JOIN_def) 115 116 117subsection\<open>Algebraic laws\<close> 118 119lemma Join_commute: "F\<squnion>G = G\<squnion>F" 120by (simp add: Join_def Un_commute Int_commute) 121 122lemma Join_assoc: "(F\<squnion>G)\<squnion>H = F\<squnion>(G\<squnion>H)" 123by (simp add: Un_ac Join_def Int_assoc insert_absorb) 124 125lemma Join_left_commute: "A\<squnion>(B\<squnion>C) = B\<squnion>(A\<squnion>C)" 126by (simp add: Un_ac Int_ac Join_def insert_absorb) 127 128lemma Join_SKIP_left [simp]: "SKIP\<squnion>F = F" 129apply (unfold Join_def SKIP_def) 130apply (rule program_equalityI) 131apply (simp_all (no_asm) add: insert_absorb) 132done 133 134lemma Join_SKIP_right [simp]: "F\<squnion>SKIP = F" 135apply (unfold Join_def SKIP_def) 136apply (rule program_equalityI) 137apply (simp_all (no_asm) add: insert_absorb) 138done 139 140lemma Join_absorb [simp]: "F\<squnion>F = F" 141apply (unfold Join_def) 142apply (rule program_equalityI, auto) 143done 144 145lemma Join_left_absorb: "F\<squnion>(F\<squnion>G) = F\<squnion>G" 146apply (unfold Join_def) 147apply (rule program_equalityI, auto) 148done 149 150(*Join is an AC-operator*) 151lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute 152 153 154subsection\<open>Laws Governing \<open>\<Squnion>\<close>\<close> 155 156(*Also follows by JN_insert and insert_absorb, but the proof is longer*) 157lemma JN_absorb: "k \<in> I ==> F k\<squnion>(\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)" 158by (auto intro!: program_equalityI) 159 160lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i)\<squnion>(\<Squnion>i \<in> J. F i))" 161by (auto intro!: program_equalityI) 162 163lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I={} then SKIP else c)" 164by (rule program_equalityI, auto) 165 166lemma JN_Join_distrib: 167 "(\<Squnion>i \<in> I. F i\<squnion>G i) = (\<Squnion>i \<in> I. F i) \<squnion> (\<Squnion>i \<in> I. G i)" 168by (auto intro!: program_equalityI) 169 170lemma JN_Join_miniscope: 171 "i \<in> I ==> (\<Squnion>i \<in> I. F i\<squnion>G) = ((\<Squnion>i \<in> I. F i)\<squnion>G)" 172by (auto simp add: JN_Join_distrib JN_constant) 173 174(*Used to prove guarantees_JN_I*) 175lemma JN_Join_diff: "i \<in> I ==> F i\<squnion>JOIN (I - {i}) F = JOIN I F" 176apply (unfold JOIN_def Join_def) 177apply (rule program_equalityI, auto) 178done 179 180 181subsection\<open>Safety: co, stable, FP\<close> 182 183(*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B. So an 184 alternative precondition is A \<subseteq> B, but most proofs using this rule require 185 I to be nonempty for other reasons anyway.*) 186lemma JN_constrains: 187 "i \<in> I ==> (\<Squnion>i \<in> I. F i) \<in> A co B = (\<forall>i \<in> I. F i \<in> A co B)" 188by (simp add: constrains_def JOIN_def, blast) 189 190lemma Join_constrains [simp]: 191 "(F\<squnion>G \<in> A co B) = (F \<in> A co B & G \<in> A co B)" 192by (auto simp add: constrains_def Join_def) 193 194lemma Join_unless [simp]: 195 "(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)" 196by (simp add: unless_def) 197 198(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. 199 reachable (F\<squnion>G) could be much bigger than reachable F, reachable G 200*) 201 202 203lemma Join_constrains_weaken: 204 "[| F \<in> A co A'; G \<in> B co B' |] 205 ==> F\<squnion>G \<in> (A \<inter> B) co (A' \<union> B')" 206by (simp, blast intro: constrains_weaken) 207 208(*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*) 209lemma JN_constrains_weaken: 210 "[| \<forall>i \<in> I. F i \<in> A i co A' i; i \<in> I |] 211 ==> (\<Squnion>i \<in> I. F i) \<in> (\<Inter>i \<in> I. A i) co (\<Union>i \<in> I. A' i)" 212apply (simp (no_asm_simp) add: JN_constrains) 213apply (blast intro: constrains_weaken) 214done 215 216lemma JN_stable: "(\<Squnion>i \<in> I. F i) \<in> stable A = (\<forall>i \<in> I. F i \<in> stable A)" 217by (simp add: stable_def constrains_def JOIN_def) 218 219lemma invariant_JN_I: 220 "[| !!i. i \<in> I ==> F i \<in> invariant A; i \<in> I |] 221 ==> (\<Squnion>i \<in> I. F i) \<in> invariant A" 222by (simp add: invariant_def JN_stable, blast) 223 224lemma Join_stable [simp]: 225 "(F\<squnion>G \<in> stable A) = 226 (F \<in> stable A & G \<in> stable A)" 227by (simp add: stable_def) 228 229lemma Join_increasing [simp]: 230 "(F\<squnion>G \<in> increasing f) = 231 (F \<in> increasing f & G \<in> increasing f)" 232by (auto simp add: increasing_def) 233 234lemma invariant_JoinI: 235 "[| F \<in> invariant A; G \<in> invariant A |] 236 ==> F\<squnion>G \<in> invariant A" 237by (auto simp add: invariant_def) 238 239lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))" 240by (simp add: FP_def JN_stable INTER_eq) 241 242 243subsection\<open>Progress: transient, ensures\<close> 244 245lemma JN_transient: 246 "i \<in> I ==> 247 (\<Squnion>i \<in> I. F i) \<in> transient A = (\<exists>i \<in> I. F i \<in> transient A)" 248by (auto simp add: transient_def JOIN_def) 249 250lemma Join_transient [simp]: 251 "F\<squnion>G \<in> transient A = 252 (F \<in> transient A | G \<in> transient A)" 253by (auto simp add: bex_Un transient_def Join_def) 254 255lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A" 256by simp 257 258lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A" 259by simp 260 261(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *) 262lemma JN_ensures: 263 "i \<in> I ==> 264 (\<Squnion>i \<in> I. F i) \<in> A ensures B = 265 ((\<forall>i \<in> I. F i \<in> (A-B) co (A \<union> B)) & (\<exists>i \<in> I. F i \<in> A ensures B))" 266by (auto simp add: ensures_def JN_constrains JN_transient) 267 268lemma Join_ensures: 269 "F\<squnion>G \<in> A ensures B = 270 (F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) & 271 (F \<in> transient (A-B) | G \<in> transient (A-B)))" 272by (auto simp add: ensures_def) 273 274lemma stable_Join_constrains: 275 "[| F \<in> stable A; G \<in> A co A' |] 276 ==> F\<squnion>G \<in> A co A'" 277apply (unfold stable_def constrains_def Join_def) 278apply (simp add: ball_Un, blast) 279done 280 281(*Premise for G cannot use Always because F \<in> Stable A is weaker than 282 G \<in> stable A *) 283lemma stable_Join_Always1: 284 "[| F \<in> stable A; G \<in> invariant A |] ==> F\<squnion>G \<in> Always A" 285apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable) 286apply (force intro: stable_Int) 287done 288 289(*As above, but exchanging the roles of F and G*) 290lemma stable_Join_Always2: 291 "[| F \<in> invariant A; G \<in> stable A |] ==> F\<squnion>G \<in> Always A" 292apply (subst Join_commute) 293apply (blast intro: stable_Join_Always1) 294done 295 296lemma stable_Join_ensures1: 297 "[| F \<in> stable A; G \<in> A ensures B |] ==> F\<squnion>G \<in> A ensures B" 298apply (simp (no_asm_simp) add: Join_ensures) 299apply (simp add: stable_def ensures_def) 300apply (erule constrains_weaken, auto) 301done 302 303(*As above, but exchanging the roles of F and G*) 304lemma stable_Join_ensures2: 305 "[| F \<in> A ensures B; G \<in> stable A |] ==> F\<squnion>G \<in> A ensures B" 306apply (subst Join_commute) 307apply (blast intro: stable_Join_ensures1) 308done 309 310 311subsection\<open>the ok and OK relations\<close> 312 313lemma ok_SKIP1 [iff]: "SKIP ok F" 314by (simp add: ok_def) 315 316lemma ok_SKIP2 [iff]: "F ok SKIP" 317by (simp add: ok_def) 318 319lemma ok_Join_commute: 320 "(F ok G & (F\<squnion>G) ok H) = (G ok H & F ok (G\<squnion>H))" 321by (auto simp add: ok_def) 322 323lemma ok_commute: "(F ok G) = (G ok F)" 324by (auto simp add: ok_def) 325 326lemmas ok_sym = ok_commute [THEN iffD1] 327 328lemma ok_iff_OK: 329 "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)" 330apply (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb 331 all_conj_distrib) 332apply blast 333done 334 335lemma ok_Join_iff1 [iff]: "F ok (G\<squnion>H) = (F ok G & F ok H)" 336by (auto simp add: ok_def) 337 338lemma ok_Join_iff2 [iff]: "(G\<squnion>H) ok F = (G ok F & H ok F)" 339by (auto simp add: ok_def) 340 341(*useful? Not with the previous two around*) 342lemma ok_Join_commute_I: "[| F ok G; (F\<squnion>G) ok H |] ==> F ok (G\<squnion>H)" 343by (auto simp add: ok_def) 344 345lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\<forall>i \<in> I. F ok G i)" 346by (auto simp add: ok_def) 347 348lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (\<forall>i \<in> I. G i ok F)" 349by (auto simp add: ok_def) 350 351lemma OK_iff_ok: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. (F i) ok (F j))" 352by (auto simp add: ok_def OK_def) 353 354lemma OK_imp_ok: "[| OK I F; i \<in> I; j \<in> I; i \<noteq> j|] ==> (F i) ok (F j)" 355by (auto simp add: OK_iff_ok) 356 357 358subsection\<open>Allowed\<close> 359 360lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV" 361by (auto simp add: Allowed_def) 362 363lemma Allowed_Join [simp]: "Allowed (F\<squnion>G) = Allowed F \<inter> Allowed G" 364by (auto simp add: Allowed_def) 365 366lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i \<in> I. Allowed (F i))" 367by (auto simp add: Allowed_def) 368 369lemma ok_iff_Allowed: "F ok G = (F \<in> Allowed G & G \<in> Allowed F)" 370by (simp add: ok_def Allowed_def) 371 372lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))" 373by (auto simp add: OK_iff_ok ok_iff_Allowed) 374 375subsection\<open>\<^term>\<open>safety_prop\<close>, for reasoning about 376 given instances of "ok"\<close> 377 378lemma safety_prop_Acts_iff: 379 "safety_prop X ==> (Acts G \<subseteq> insert Id (\<Union>(Acts ` X))) = (G \<in> X)" 380by (auto simp add: safety_prop_def) 381 382lemma safety_prop_AllowedActs_iff_Allowed: 383 "safety_prop X ==> (\<Union>(Acts ` X) \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)" 384by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric]) 385 386lemma Allowed_eq: 387 "safety_prop X ==> Allowed (mk_program (init, acts, \<Union>(Acts ` X))) = X" 388by (simp add: Allowed_def safety_prop_Acts_iff) 389 390(*For safety_prop to hold, the property must be satisfiable!*) 391lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \<subseteq> B)" 392by (simp add: safety_prop_def constrains_def, blast) 393 394lemma safety_prop_stable [iff]: "safety_prop (stable A)" 395by (simp add: stable_def) 396 397lemma safety_prop_Int [simp]: 398 "safety_prop X \<Longrightarrow> safety_prop Y \<Longrightarrow> safety_prop (X \<inter> Y)" 399proof (clarsimp simp add: safety_prop_def) 400 fix G 401 assume "\<forall>G. Acts G \<subseteq> (\<Union>x\<in>X. Acts x) \<longrightarrow> G \<in> X" 402 then have X: "Acts G \<subseteq> (\<Union>x\<in>X. Acts x) \<Longrightarrow> G \<in> X" by blast 403 assume "\<forall>G. Acts G \<subseteq> (\<Union>x\<in>Y. Acts x) \<longrightarrow> G \<in> Y" 404 then have Y: "Acts G \<subseteq> (\<Union>x\<in>Y. Acts x) \<Longrightarrow> G \<in> Y" by blast 405 assume Acts: "Acts G \<subseteq> (\<Union>x\<in>X \<inter> Y. Acts x)" 406 with X and Y show "G \<in> X \<and> G \<in> Y" by auto 407qed 408 409lemma safety_prop_INTER [simp]: 410 "(\<And>i. i \<in> I \<Longrightarrow> safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i\<in>I. X i)" 411proof (clarsimp simp add: safety_prop_def) 412 fix G and i 413 assume "\<And>i. i \<in> I \<Longrightarrow> \<bottom> \<in> X i \<and> 414 (\<forall>G. Acts G \<subseteq> (\<Union>x\<in>X i. Acts x) \<longrightarrow> G \<in> X i)" 415 then have *: "i \<in> I \<Longrightarrow> Acts G \<subseteq> (\<Union>x\<in>X i. Acts x) \<Longrightarrow> G \<in> X i" 416 by blast 417 assume "i \<in> I" 418 moreover assume "Acts G \<subseteq> (\<Union>j\<in>\<Inter>i\<in>I. X i. Acts j)" 419 ultimately have "Acts G \<subseteq> (\<Union>i\<in>X i. Acts i)" 420 by auto 421 with * \<open>i \<in> I\<close> show "G \<in> X i" by blast 422qed 423 424lemma safety_prop_INTER1 [simp]: 425 "(\<And>i. safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i. X i)" 426 by (rule safety_prop_INTER) simp 427 428lemma def_prg_Allowed: 429 "[| F == mk_program (init, acts, \<Union>(Acts ` X)) ; safety_prop X |] 430 ==> Allowed F = X" 431by (simp add: Allowed_eq) 432 433lemma Allowed_totalize [simp]: "Allowed (totalize F) = Allowed F" 434by (simp add: Allowed_def) 435 436lemma def_total_prg_Allowed: 437 "[| F = mk_total_program (init, acts, \<Union>(Acts ` X)) ; safety_prop X |] 438 ==> Allowed F = X" 439by (simp add: mk_total_program_def def_prg_Allowed) 440 441lemma def_UNION_ok_iff: 442 "[| F = mk_program(init,acts,\<Union>(Acts ` X)); safety_prop X |] 443 ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)" 444by (auto simp add: ok_def safety_prop_Acts_iff) 445 446text\<open>The union of two total programs is total.\<close> 447lemma totalize_Join: "totalize F\<squnion>totalize G = totalize (F\<squnion>G)" 448by (simp add: program_equalityI totalize_def Join_def image_Un) 449 450lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F\<squnion>G)" 451by (simp add: all_total_def, blast) 452 453lemma totalize_JN: "(\<Squnion>i \<in> I. totalize (F i)) = totalize(\<Squnion>i \<in> I. F i)" 454by (simp add: program_equalityI totalize_def JOIN_def image_UN) 455 456lemma all_total_JN: "(!!i. i\<in>I ==> all_total (F i)) ==> all_total(\<Squnion>i\<in>I. F i)" 457by (simp add: all_total_iff_totalize totalize_JN [symmetric]) 458 459end 460