1(* Title: HOL/UNITY/Extend.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5Extending of state setsExtending of state sets 6 function f (forget) maps the extended state to the original state 7 function g (forgotten) maps the extended state to the "extending part" 8*) 9 10section\<open>Extending State Sets\<close> 11 12theory Extend imports Guar begin 13 14definition 15 (*MOVE to Relation.thy?*) 16 Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set" 17 where "Restrict A r = r \<inter> (A \<times> UNIV)" 18 19definition 20 good_map :: "['a*'b => 'c] => bool" 21 where "good_map h \<longleftrightarrow> surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)" 22 (*Using the locale constant "f", this is f (h (x,y))) = x*) 23 24definition 25 extend_set :: "['a*'b => 'c, 'a set] => 'c set" 26 where "extend_set h A = h ` (A \<times> UNIV)" 27 28definition 29 project_set :: "['a*'b => 'c, 'c set] => 'a set" 30 where "project_set h C = {x. \<exists>y. h(x,y) \<in> C}" 31 32definition 33 extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set" 34 where "extend_act h = (%act. \<Union>(s,s') \<in> act. \<Union>y. {(h(s,y), h(s',y))})" 35 36definition 37 project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set" 38 where "project_act h act = {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}" 39 40definition 41 extend :: "['a*'b => 'c, 'a program] => 'c program" 42 where "extend h F = mk_program (extend_set h (Init F), 43 extend_act h ` Acts F, 44 project_act h -` AllowedActs F)" 45 46definition 47 (*Argument C allows weak safety laws to be projected*) 48 project :: "['a*'b => 'c, 'c set, 'c program] => 'a program" 49 where "project h C F = 50 mk_program (project_set h (Init F), 51 project_act h ` Restrict C ` Acts F, 52 {act. Restrict (project_set h C) act \<in> 53 project_act h ` Restrict C ` AllowedActs F})" 54 55locale Extend = 56 fixes f :: "'c => 'a" 57 and g :: "'c => 'b" 58 and h :: "'a*'b => 'c" (*isomorphism between 'a * 'b and 'c *) 59 and slice :: "['c set, 'b] => 'a set" 60 assumes 61 good_h: "good_map h" 62 defines f_def: "f z == fst (inv h z)" 63 and g_def: "g z == snd (inv h z)" 64 and slice_def: "slice Z y == {x. h(x,y) \<in> Z}" 65 66 67(** These we prove OUTSIDE the locale. **) 68 69 70subsection\<open>Restrict\<close> 71(*MOVE to Relation.thy?*) 72 73lemma Restrict_iff [iff]: "((x,y) \<in> Restrict A r) = ((x,y) \<in> r & x \<in> A)" 74by (unfold Restrict_def, blast) 75 76lemma Restrict_UNIV [simp]: "Restrict UNIV = id" 77apply (rule ext) 78apply (auto simp add: Restrict_def) 79done 80 81lemma Restrict_empty [simp]: "Restrict {} r = {}" 82by (auto simp add: Restrict_def) 83 84lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A \<inter> B) r" 85by (unfold Restrict_def, blast) 86 87lemma Restrict_triv: "Domain r \<subseteq> A ==> Restrict A r = r" 88by (unfold Restrict_def, auto) 89 90lemma Restrict_subset: "Restrict A r \<subseteq> r" 91by (unfold Restrict_def, auto) 92 93lemma Restrict_eq_mono: 94 "[| A \<subseteq> B; Restrict B r = Restrict B s |] 95 ==> Restrict A r = Restrict A s" 96by (unfold Restrict_def, blast) 97 98lemma Restrict_imageI: 99 "[| s \<in> RR; Restrict A r = Restrict A s |] 100 ==> Restrict A r \<in> Restrict A ` RR" 101by (unfold Restrict_def image_def, auto) 102 103lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A \<inter> Domain r" 104by blast 105 106lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \<inter> B)" 107by blast 108 109(*Possibly easier than reasoning about "inv h"*) 110lemma good_mapI: 111 assumes surj_h: "surj h" 112 and prem: "!! x x' y y'. h(x,y) = h(x',y') ==> x=x'" 113 shows "good_map h" 114apply (simp add: good_map_def) 115apply (safe intro!: surj_h) 116apply (rule prem) 117apply (subst surjective_pairing [symmetric]) 118apply (subst surj_h [THEN surj_f_inv_f]) 119apply (rule refl) 120done 121 122lemma good_map_is_surj: "good_map h ==> surj h" 123by (unfold good_map_def, auto) 124 125(*A convenient way of finding a closed form for inv h*) 126lemma fst_inv_equalityI: 127 assumes surj_h: "surj h" 128 and prem: "!! x y. g (h(x,y)) = x" 129 shows "fst (inv h z) = g z" 130by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h) 131 132 133subsection\<open>Trivial properties of f, g, h\<close> 134 135context Extend 136begin 137 138lemma f_h_eq [simp]: "f(h(x,y)) = x" 139by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2]) 140 141lemma h_inject1 [dest]: "h(x,y) = h(x',y') ==> x=x'" 142apply (drule_tac f = f in arg_cong) 143apply (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2]) 144done 145 146lemma h_f_g_equiv: "h(f z, g z) == z" 147by (simp add: f_def g_def 148 good_h [unfolded good_map_def, THEN conjunct1, THEN surj_f_inv_f]) 149 150lemma h_f_g_eq: "h(f z, g z) = z" 151by (simp add: h_f_g_equiv) 152 153 154lemma split_extended_all: 155 "(!!z. PROP P z) == (!!u y. PROP P (h (u, y)))" 156proof 157 assume allP: "\<And>z. PROP P z" 158 fix u y 159 show "PROP P (h (u, y))" by (rule allP) 160 next 161 assume allPh: "\<And>u y. PROP P (h(u,y))" 162 fix z 163 have Phfgz: "PROP P (h (f z, g z))" by (rule allPh) 164 show "PROP P z" by (rule Phfgz [unfolded h_f_g_equiv]) 165qed 166 167end 168 169 170subsection\<open>@{term extend_set}: basic properties\<close> 171 172lemma project_set_iff [iff]: 173 "(x \<in> project_set h C) = (\<exists>y. h(x,y) \<in> C)" 174by (simp add: project_set_def) 175 176lemma extend_set_mono: "A \<subseteq> B ==> extend_set h A \<subseteq> extend_set h B" 177by (unfold extend_set_def, blast) 178 179context Extend 180begin 181 182lemma mem_extend_set_iff [iff]: "z \<in> extend_set h A = (f z \<in> A)" 183apply (unfold extend_set_def) 184apply (force intro: h_f_g_eq [symmetric]) 185done 186 187lemma extend_set_strict_mono [iff]: 188 "(extend_set h A \<subseteq> extend_set h B) = (A \<subseteq> B)" 189by (unfold extend_set_def, force) 190 191lemma (in -) extend_set_empty [simp]: "extend_set h {} = {}" 192by (unfold extend_set_def, auto) 193 194lemma extend_set_eq_Collect: "extend_set h {s. P s} = {s. P(f s)}" 195by auto 196 197lemma extend_set_sing: "extend_set h {x} = {s. f s = x}" 198by auto 199 200lemma extend_set_inverse [simp]: "project_set h (extend_set h C) = C" 201by (unfold extend_set_def, auto) 202 203lemma extend_set_project_set: "C \<subseteq> extend_set h (project_set h C)" 204apply (unfold extend_set_def) 205apply (auto simp add: split_extended_all, blast) 206done 207 208lemma inj_extend_set: "inj (extend_set h)" 209apply (rule inj_on_inverseI) 210apply (rule extend_set_inverse) 211done 212 213lemma extend_set_UNIV_eq [simp]: "extend_set h UNIV = UNIV" 214apply (unfold extend_set_def) 215apply (auto simp add: split_extended_all) 216done 217 218subsection\<open>@{term project_set}: basic properties\<close> 219 220(*project_set is simply image!*) 221lemma project_set_eq: "project_set h C = f ` C" 222by (auto intro: f_h_eq [symmetric] simp add: split_extended_all) 223 224(*Converse appears to fail*) 225lemma project_set_I: "!!z. z \<in> C ==> f z \<in> project_set h C" 226by (auto simp add: split_extended_all) 227 228 229subsection\<open>More laws\<close> 230 231(*Because A and B could differ on the "other" part of the state, 232 cannot generalize to 233 project_set h (A \<inter> B) = project_set h A \<inter> project_set h B 234*) 235lemma project_set_extend_set_Int: "project_set h ((extend_set h A) \<inter> B) = A \<inter> (project_set h B)" 236 by auto 237 238(*Unused, but interesting?*) 239lemma project_set_extend_set_Un: "project_set h ((extend_set h A) \<union> B) = A \<union> (project_set h B)" 240 by auto 241 242lemma (in -) project_set_Int_subset: 243 "project_set h (A \<inter> B) \<subseteq> (project_set h A) \<inter> (project_set h B)" 244 by auto 245 246lemma extend_set_Un_distrib: "extend_set h (A \<union> B) = extend_set h A \<union> extend_set h B" 247 by auto 248 249lemma extend_set_Int_distrib: "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B" 250 by auto 251 252lemma extend_set_INT_distrib: "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))" 253 by auto 254 255lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B" 256 by auto 257 258lemma extend_set_Union: "extend_set h (\<Union>A) = (\<Union>X \<in> A. extend_set h X)" 259 by blast 260 261lemma extend_set_subset_Compl_eq: "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)" 262 by (auto simp: extend_set_def) 263 264 265subsection\<open>@{term extend_act}\<close> 266 267(*Can't strengthen it to 268 ((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y') 269 because h doesn't have to be injective in the 2nd argument*) 270lemma mem_extend_act_iff [iff]: "((h(s,y), h(s',y)) \<in> extend_act h act) = ((s, s') \<in> act)" 271 by (auto simp: extend_act_def) 272 273(*Converse fails: (z,z') would include actions that changed the g-part*) 274lemma extend_act_D: "(z, z') \<in> extend_act h act ==> (f z, f z') \<in> act" 275 by (auto simp: extend_act_def) 276 277lemma extend_act_inverse [simp]: "project_act h (extend_act h act) = act" 278 unfolding extend_act_def project_act_def by blast 279 280lemma project_act_extend_act_restrict [simp]: 281 "project_act h (Restrict C (extend_act h act)) = 282 Restrict (project_set h C) act" 283 unfolding extend_act_def project_act_def by blast 284 285lemma subset_extend_act_D: "act' \<subseteq> extend_act h act ==> project_act h act' \<subseteq> act" 286 unfolding extend_act_def project_act_def by force 287 288lemma inj_extend_act: "inj (extend_act h)" 289apply (rule inj_on_inverseI) 290apply (rule extend_act_inverse) 291done 292 293lemma extend_act_Image [simp]: 294 "extend_act h act `` (extend_set h A) = extend_set h (act `` A)" 295 unfolding extend_set_def extend_act_def by force 296 297lemma extend_act_strict_mono [iff]: 298 "(extend_act h act' \<subseteq> extend_act h act) = (act'<=act)" 299 by (auto simp: extend_act_def) 300 301lemma [iff]: "(extend_act h act = extend_act h act') = (act = act')" 302 by (rule inj_extend_act [THEN inj_eq]) 303 304lemma (in -) Domain_extend_act: 305 "Domain (extend_act h act) = extend_set h (Domain act)" 306 unfolding extend_set_def extend_act_def by force 307 308lemma extend_act_Id [simp]: "extend_act h Id = Id" 309 unfolding extend_act_def by (force intro: h_f_g_eq [symmetric]) 310 311lemma project_act_I: "!!z z'. (z, z') \<in> act ==> (f z, f z') \<in> project_act h act" 312 unfolding project_act_def by (force simp add: split_extended_all) 313 314lemma project_act_Id [simp]: "project_act h Id = Id" 315 unfolding project_act_def by force 316 317lemma Domain_project_act: "Domain (project_act h act) = project_set h (Domain act)" 318 unfolding project_act_def by (force simp add: split_extended_all) 319 320 321subsection\<open>extend\<close> 322 323text\<open>Basic properties\<close> 324 325lemma (in -) Init_extend [simp]: 326 "Init (extend h F) = extend_set h (Init F)" 327 by (auto simp: extend_def) 328 329lemma (in -) Init_project [simp]: 330 "Init (project h C F) = project_set h (Init F)" 331 by (auto simp: project_def) 332 333lemma Acts_extend [simp]: "Acts (extend h F) = (extend_act h ` Acts F)" 334 by (simp add: extend_def insert_Id_image_Acts) 335 336lemma AllowedActs_extend [simp]: 337 "AllowedActs (extend h F) = project_act h -` AllowedActs F" 338 by (simp add: extend_def insert_absorb) 339 340lemma (in -) Acts_project [simp]: 341 "Acts(project h C F) = insert Id (project_act h ` Restrict C ` Acts F)" 342 by (auto simp add: project_def image_iff) 343 344lemma AllowedActs_project [simp]: 345 "AllowedActs(project h C F) = 346 {act. Restrict (project_set h C) act 347 \<in> project_act h ` Restrict C ` AllowedActs F}" 348apply (simp (no_asm) add: project_def image_iff) 349apply (subst insert_absorb) 350apply (auto intro!: bexI [of _ Id] simp add: project_act_def) 351done 352 353lemma Allowed_extend: "Allowed (extend h F) = project h UNIV -` Allowed F" 354 by (auto simp add: Allowed_def) 355 356lemma extend_SKIP [simp]: "extend h SKIP = SKIP" 357apply (unfold SKIP_def) 358apply (rule program_equalityI, auto) 359done 360 361lemma (in -) project_set_UNIV [simp]: "project_set h UNIV = UNIV" 362 by auto 363 364lemma (in -) project_set_Union: "project_set h (\<Union>A) = (\<Union>X \<in> A. project_set h X)" 365 by blast 366 367 368(*Converse FAILS: the extended state contributing to project_set h C 369 may not coincide with the one contributing to project_act h act*) 370lemma (in -) project_act_Restrict_subset: 371 "project_act h (Restrict C act) \<subseteq> Restrict (project_set h C) (project_act h act)" 372 by (auto simp add: project_act_def) 373 374lemma project_act_Restrict_Id_eq: "project_act h (Restrict C Id) = Restrict (project_set h C) Id" 375 by (auto simp add: project_act_def) 376 377lemma project_extend_eq: 378 "project h C (extend h F) = 379 mk_program (Init F, Restrict (project_set h C) ` Acts F, 380 {act. Restrict (project_set h C) act 381 \<in> project_act h ` Restrict C ` 382 (project_act h -` AllowedActs F)})" 383apply (rule program_equalityI) 384 apply simp 385 apply (simp add: image_image) 386apply (simp add: project_def) 387done 388 389lemma extend_inverse [simp]: 390 "project h UNIV (extend h F) = F" 391apply (simp (no_asm_simp) add: project_extend_eq 392 subset_UNIV [THEN subset_trans, THEN Restrict_triv]) 393apply (rule program_equalityI) 394apply (simp_all (no_asm)) 395apply (subst insert_absorb) 396apply (simp (no_asm) add: bexI [of _ Id]) 397apply auto 398apply (simp add: image_def) 399using project_act_Id apply blast 400apply (simp add: image_def) 401apply (rename_tac "act") 402apply (rule_tac x = "extend_act h act" in exI) 403apply simp 404done 405 406lemma inj_extend: "inj (extend h)" 407apply (rule inj_on_inverseI) 408apply (rule extend_inverse) 409done 410 411lemma extend_Join [simp]: "extend h (F\<squnion>G) = extend h F\<squnion>extend h G" 412apply (rule program_equalityI) 413apply (simp (no_asm) add: extend_set_Int_distrib) 414apply (simp add: image_Un, auto) 415done 416 417lemma extend_JN [simp]: "extend h (JOIN I F) = (\<Squnion>i \<in> I. extend h (F i))" 418apply (rule program_equalityI) 419 apply (simp (no_asm) add: extend_set_INT_distrib) 420 apply (simp add: image_UN, auto) 421done 422 423(** These monotonicity results look natural but are UNUSED **) 424 425lemma extend_mono: "F \<le> G ==> extend h F \<le> extend h G" 426 by (force simp add: component_eq_subset) 427 428lemma project_mono: "F \<le> G ==> project h C F \<le> project h C G" 429 by (simp add: component_eq_subset, blast) 430 431lemma all_total_extend: "all_total F ==> all_total (extend h F)" 432 by (simp add: all_total_def Domain_extend_act) 433 434subsection\<open>Safety: co, stable\<close> 435 436lemma extend_constrains: 437 "(extend h F \<in> (extend_set h A) co (extend_set h B)) = 438 (F \<in> A co B)" 439 by (simp add: constrains_def) 440 441lemma extend_stable: 442 "(extend h F \<in> stable (extend_set h A)) = (F \<in> stable A)" 443 by (simp add: stable_def extend_constrains) 444 445lemma extend_invariant: 446 "(extend h F \<in> invariant (extend_set h A)) = (F \<in> invariant A)" 447 by (simp add: invariant_def extend_stable) 448 449(*Projects the state predicates in the property satisfied by extend h F. 450 Converse fails: A and B may differ in their extra variables*) 451lemma extend_constrains_project_set: 452 "extend h F \<in> A co B ==> F \<in> (project_set h A) co (project_set h B)" 453 by (auto simp add: constrains_def, force) 454 455lemma extend_stable_project_set: 456 "extend h F \<in> stable A ==> F \<in> stable (project_set h A)" 457 by (simp add: stable_def extend_constrains_project_set) 458 459 460subsection\<open>Weak safety primitives: Co, Stable\<close> 461 462lemma reachable_extend_f: "p \<in> reachable (extend h F) ==> f p \<in> reachable F" 463 by (induct set: reachable) (auto intro: reachable.intros simp add: extend_act_def image_iff) 464 465lemma h_reachable_extend: "h(s,y) \<in> reachable (extend h F) ==> s \<in> reachable F" 466 by (force dest!: reachable_extend_f) 467 468lemma reachable_extend_eq: "reachable (extend h F) = extend_set h (reachable F)" 469apply (unfold extend_set_def) 470apply (rule equalityI) 471apply (force intro: h_f_g_eq [symmetric] dest!: reachable_extend_f, clarify) 472apply (erule reachable.induct) 473apply (force intro: reachable.intros)+ 474done 475 476lemma extend_Constrains: 477 "(extend h F \<in> (extend_set h A) Co (extend_set h B)) = 478 (F \<in> A Co B)" 479 by (simp add: Constrains_def reachable_extend_eq extend_constrains 480 extend_set_Int_distrib [symmetric]) 481 482lemma extend_Stable: "(extend h F \<in> Stable (extend_set h A)) = (F \<in> Stable A)" 483 by (simp add: Stable_def extend_Constrains) 484 485lemma extend_Always: "(extend h F \<in> Always (extend_set h A)) = (F \<in> Always A)" 486 by (simp add: Always_def extend_Stable) 487 488 489(** Safety and "project" **) 490 491(** projection: monotonicity for safety **) 492 493lemma (in -) project_act_mono: 494 "D \<subseteq> C ==> 495 project_act h (Restrict D act) \<subseteq> project_act h (Restrict C act)" 496 by (auto simp add: project_act_def) 497 498lemma project_constrains_mono: 499 "[| D \<subseteq> C; project h C F \<in> A co B |] ==> project h D F \<in> A co B" 500apply (auto simp add: constrains_def) 501apply (drule project_act_mono, blast) 502done 503 504lemma project_stable_mono: 505 "[| D \<subseteq> C; project h C F \<in> stable A |] ==> project h D F \<in> stable A" 506 by (simp add: stable_def project_constrains_mono) 507 508(*Key lemma used in several proofs about project and co*) 509lemma project_constrains: 510 "(project h C F \<in> A co B) = 511 (F \<in> (C \<inter> extend_set h A) co (extend_set h B) & A \<subseteq> B)" 512apply (unfold constrains_def) 513apply (auto intro!: project_act_I simp add: ball_Un) 514apply (force intro!: project_act_I dest!: subsetD) 515(*the <== direction*) 516apply (unfold project_act_def) 517apply (force dest!: subsetD) 518done 519 520lemma project_stable: "(project h UNIV F \<in> stable A) = (F \<in> stable (extend_set h A))" 521 by (simp add: stable_def project_constrains) 522 523lemma project_stable_I: "F \<in> stable (extend_set h A) ==> project h C F \<in> stable A" 524apply (drule project_stable [THEN iffD2]) 525apply (blast intro: project_stable_mono) 526done 527 528lemma Int_extend_set_lemma: 529 "A \<inter> extend_set h ((project_set h A) \<inter> B) = A \<inter> extend_set h B" 530 by (auto simp add: split_extended_all) 531 532(*Strange (look at occurrences of C) but used in leadsETo proofs*) 533lemma project_constrains_project_set: 534 "G \<in> C co B ==> project h C G \<in> project_set h C co project_set h B" 535 by (simp add: constrains_def project_def project_act_def, blast) 536 537lemma project_stable_project_set: 538 "G \<in> stable C ==> project h C G \<in> stable (project_set h C)" 539 by (simp add: stable_def project_constrains_project_set) 540 541 542subsection\<open>Progress: transient, ensures\<close> 543 544lemma extend_transient: 545 "(extend h F \<in> transient (extend_set h A)) = (F \<in> transient A)" 546 by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act) 547 548lemma extend_ensures: 549 "(extend h F \<in> (extend_set h A) ensures (extend_set h B)) = 550 (F \<in> A ensures B)" 551 by (simp add: ensures_def extend_constrains extend_transient 552 extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric]) 553 554lemma leadsTo_imp_extend_leadsTo: 555 "F \<in> A leadsTo B 556 ==> extend h F \<in> (extend_set h A) leadsTo (extend_set h B)" 557apply (erule leadsTo_induct) 558 apply (simp add: leadsTo_Basis extend_ensures) 559 apply (blast intro: leadsTo_Trans) 560apply (simp add: leadsTo_UN extend_set_Union) 561done 562 563subsection\<open>Proving the converse takes some doing!\<close> 564 565lemma slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)" 566 by (simp add: slice_def) 567 568lemma slice_Union: "slice (\<Union>S) y = (\<Union>x \<in> S. slice x y)" 569 by auto 570 571lemma slice_extend_set: "slice (extend_set h A) y = A" 572 by auto 573 574lemma project_set_is_UN_slice: "project_set h A = (\<Union>y. slice A y)" 575 by auto 576 577lemma extend_transient_slice: 578 "extend h F \<in> transient A ==> F \<in> transient (slice A y)" 579 by (auto simp: transient_def) 580 581(*Converse?*) 582lemma extend_constrains_slice: 583 "extend h F \<in> A co B ==> F \<in> (slice A y) co (slice B y)" 584 by (auto simp add: constrains_def) 585 586lemma extend_ensures_slice: 587 "extend h F \<in> A ensures B ==> F \<in> (slice A y) ensures (project_set h B)" 588apply (auto simp add: ensures_def extend_constrains extend_transient) 589apply (erule_tac [2] extend_transient_slice [THEN transient_strengthen]) 590apply (erule extend_constrains_slice [THEN constrains_weaken], auto) 591done 592 593lemma leadsTo_slice_project_set: 594 "\<forall>y. F \<in> (slice B y) leadsTo CU ==> F \<in> (project_set h B) leadsTo CU" 595apply (simp add: project_set_is_UN_slice) 596apply (blast intro: leadsTo_UN) 597done 598 599lemma extend_leadsTo_slice [rule_format]: 600 "extend h F \<in> AU leadsTo BU 601 ==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)" 602apply (erule leadsTo_induct) 603 apply (blast intro: extend_ensures_slice) 604 apply (blast intro: leadsTo_slice_project_set leadsTo_Trans) 605apply (simp add: leadsTo_UN slice_Union) 606done 607 608lemma extend_leadsTo: 609 "(extend h F \<in> (extend_set h A) leadsTo (extend_set h B)) = 610 (F \<in> A leadsTo B)" 611apply safe 612apply (erule_tac [2] leadsTo_imp_extend_leadsTo) 613apply (drule extend_leadsTo_slice) 614apply (simp add: slice_extend_set) 615done 616 617lemma extend_LeadsTo: 618 "(extend h F \<in> (extend_set h A) LeadsTo (extend_set h B)) = 619 (F \<in> A LeadsTo B)" 620 by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo 621 extend_set_Int_distrib [symmetric]) 622 623 624subsection\<open>preserves\<close> 625 626lemma project_preserves_I: 627 "G \<in> preserves (v o f) ==> project h C G \<in> preserves v" 628 by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect) 629 630(*to preserve f is to preserve the whole original state*) 631lemma project_preserves_id_I: 632 "G \<in> preserves f ==> project h C G \<in> preserves id" 633 by (simp add: project_preserves_I) 634 635lemma extend_preserves: 636 "(extend h G \<in> preserves (v o f)) = (G \<in> preserves v)" 637 by (auto simp add: preserves_def extend_stable [symmetric] 638 extend_set_eq_Collect) 639 640lemma inj_extend_preserves: "inj h ==> (extend h G \<in> preserves g)" 641 by (auto simp add: preserves_def extend_def extend_act_def stable_def 642 constrains_def g_def) 643 644 645subsection\<open>Guarantees\<close> 646 647lemma project_extend_Join: "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)" 648 apply (rule program_equalityI) 649 apply (auto simp add: project_set_extend_set_Int image_iff) 650 apply (metis Un_iff extend_act_inverse image_iff) 651 apply (metis Un_iff extend_act_inverse image_iff) 652 done 653 654lemma extend_Join_eq_extend_D: 655 "(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)" 656apply (drule_tac f = "project h UNIV" in arg_cong) 657apply (simp add: project_extend_Join) 658done 659 660(** Strong precondition and postcondition; only useful when 661 the old and new state sets are in bijection **) 662 663 664lemma ok_extend_imp_ok_project: "extend h F ok G ==> F ok project h UNIV G" 665apply (auto simp add: ok_def) 666apply (drule subsetD) 667apply (auto intro!: rev_image_eqI) 668done 669 670lemma ok_extend_iff: "(extend h F ok extend h G) = (F ok G)" 671apply (simp add: ok_def, safe) 672apply force+ 673done 674 675lemma OK_extend_iff: "OK I (%i. extend h (F i)) = (OK I F)" 676apply (unfold OK_def, safe) 677apply (drule_tac x = i in bspec) 678apply (drule_tac [2] x = j in bspec) 679apply force+ 680done 681 682lemma guarantees_imp_extend_guarantees: 683 "F \<in> X guarantees Y ==> 684 extend h F \<in> (extend h ` X) guarantees (extend h ` Y)" 685apply (rule guaranteesI, clarify) 686apply (blast dest: ok_extend_imp_ok_project extend_Join_eq_extend_D 687 guaranteesD) 688done 689 690lemma extend_guarantees_imp_guarantees: 691 "extend h F \<in> (extend h ` X) guarantees (extend h ` Y) 692 ==> F \<in> X guarantees Y" 693apply (auto simp add: guar_def) 694apply (drule_tac x = "extend h G" in spec) 695apply (simp del: extend_Join 696 add: extend_Join [symmetric] ok_extend_iff 697 inj_extend [THEN inj_image_mem_iff]) 698done 699 700lemma extend_guarantees_eq: 701 "(extend h F \<in> (extend h ` X) guarantees (extend h ` Y)) = 702 (F \<in> X guarantees Y)" 703 by (blast intro: guarantees_imp_extend_guarantees 704 extend_guarantees_imp_guarantees) 705 706end 707 708end 709