1(* Title: HOL/UNITY/ELT.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1999 University of Cambridge 4 5leadsTo strengthened with a specification of the allowable sets transient parts 6 7TRY INSTEAD (to get rid of the {} and to gain strong induction) 8 9 elt :: "['a set set, 'a program, 'a set] => ('a set) set" 10 11inductive "elt CC F B" 12 intros 13 14 Weaken: "A <= B ==> A : elt CC F B" 15 16 ETrans: "[| F : A ensures A'; A-A' : CC; A' : elt CC F B |] 17 ==> A : elt CC F B" 18 19 Union: "{A. A: S} : Pow (elt CC F B) ==> (Union S) : elt CC F B" 20 21 monos Pow_mono 22*) 23 24section\<open>Progress Under Allowable Sets\<close> 25 26theory ELT imports Project begin 27 28inductive_set 29 (*LEADS-TO constant for the inductive definition*) 30 elt :: "['a set set, 'a program] => ('a set * 'a set) set" 31 for CC :: "'a set set" and F :: "'a program" 32 where 33 34 Basis: "[| F \<in> A ensures B; A-B \<in> (insert {} CC) |] ==> (A,B) \<in> elt CC F" 35 36 | Trans: "[| (A,B) \<in> elt CC F; (B,C) \<in> elt CC F |] ==> (A,C) \<in> elt CC F" 37 38 | Union: "\<forall>A\<in>S. (A,B) \<in> elt CC F ==> (Union S, B) \<in> elt CC F" 39 40 41definition 42 (*the set of all sets determined by f alone*) 43 givenBy :: "['a => 'b] => 'a set set" 44 where "givenBy f = range (%B. f-` B)" 45 46definition 47 (*visible version of the LEADS-TO relation*) 48 leadsETo :: "['a set, 'a set set, 'a set] => 'a program set" 49 ("(3_/ leadsTo[_]/ _)" [80,0,80] 80) 50 where "leadsETo A CC B = {F. (A,B) \<in> elt CC F}" 51 52definition 53 LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set" 54 ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80) 55 where "LeadsETo A CC B = 56 {F. F \<in> (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}" 57 58 59(*** givenBy ***) 60 61lemma givenBy_id [simp]: "givenBy id = UNIV" 62by (unfold givenBy_def, auto) 63 64lemma givenBy_eq_all: "(givenBy v) = {A. \<forall>x\<in>A. \<forall>y. v x = v y \<longrightarrow> y \<in> A}" 65apply (unfold givenBy_def, safe) 66apply (rule_tac [2] x = "v ` _" in image_eqI, auto) 67done 68 69lemma givenByI: "(\<And>x y. [| x \<in> A; v x = v y |] ==> y \<in> A) ==> A \<in> givenBy v" 70by (subst givenBy_eq_all, blast) 71 72lemma givenByD: "[| A \<in> givenBy v; x \<in> A; v x = v y |] ==> y \<in> A" 73by (unfold givenBy_def, auto) 74 75lemma empty_mem_givenBy [iff]: "{} \<in> givenBy v" 76by (blast intro!: givenByI) 77 78lemma givenBy_imp_eq_Collect: "A \<in> givenBy v ==> \<exists>P. A = {s. P(v s)}" 79apply (rule_tac x = "\<lambda>n. \<exists>s. v s = n \<and> s \<in> A" in exI) 80apply (simp (no_asm_use) add: givenBy_eq_all) 81apply blast 82done 83 84lemma Collect_mem_givenBy: "{s. P(v s)} \<in> givenBy v" 85by (unfold givenBy_def, best) 86 87lemma givenBy_eq_Collect: "givenBy v = {A. \<exists>P. A = {s. P(v s)}}" 88by (blast intro: Collect_mem_givenBy givenBy_imp_eq_Collect) 89 90(*preserving v preserves properties given by v*) 91lemma preserves_givenBy_imp_stable: 92 "[| F \<in> preserves v; D \<in> givenBy v |] ==> F \<in> stable D" 93by (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect) 94 95lemma givenBy_o_subset: "givenBy (w o v) <= givenBy v" 96apply (simp (no_asm) add: givenBy_eq_Collect) 97apply best 98done 99 100lemma givenBy_DiffI: 101 "[| A \<in> givenBy v; B \<in> givenBy v |] ==> A-B \<in> givenBy v" 102apply (simp (no_asm_use) add: givenBy_eq_Collect) 103apply safe 104apply (rule_tac x = "%z. R z & ~ Q z" for R Q in exI) 105unfolding set_diff_eq 106apply auto 107done 108 109 110(** Standard leadsTo rules **) 111 112lemma leadsETo_Basis [intro]: 113 "[| F \<in> A ensures B; A-B \<in> insert {} CC |] ==> F \<in> A leadsTo[CC] B" 114apply (unfold leadsETo_def) 115apply (blast intro: elt.Basis) 116done 117 118lemma leadsETo_Trans: 119 "[| F \<in> A leadsTo[CC] B; F \<in> B leadsTo[CC] C |] ==> F \<in> A leadsTo[CC] C" 120apply (unfold leadsETo_def) 121apply (blast intro: elt.Trans) 122done 123 124 125(*Useful with cancellation, disjunction*) 126lemma leadsETo_Un_duplicate: 127 "F \<in> A leadsTo[CC] (A' \<union> A') \<Longrightarrow> F \<in> A leadsTo[CC] A'" 128by (simp add: Un_ac) 129 130lemma leadsETo_Un_duplicate2: 131 "F \<in> A leadsTo[CC] (A' \<union> C \<union> C) ==> F \<in> A leadsTo[CC] (A' Un C)" 132by (simp add: Un_ac) 133 134(*The Union introduction rule as we should have liked to state it*) 135lemma leadsETo_Union: 136 "(\<And>A. A \<in> S \<Longrightarrow> F \<in> A leadsTo[CC] B) \<Longrightarrow> F \<in> (\<Union>S) leadsTo[CC] B" 137apply (unfold leadsETo_def) 138apply (blast intro: elt.Union) 139done 140 141lemma leadsETo_UN: 142 "(\<And>i. i \<in> I \<Longrightarrow> F \<in> (A i) leadsTo[CC] B) 143 ==> F \<in> (UN i:I. A i) leadsTo[CC] B" 144apply (blast intro: leadsETo_Union) 145done 146 147(*The INDUCTION rule as we should have liked to state it*) 148lemma leadsETo_induct: 149 "[| F \<in> za leadsTo[CC] zb; 150 !!A B. [| F \<in> A ensures B; A-B \<in> insert {} CC |] ==> P A B; 151 !!A B C. [| F \<in> A leadsTo[CC] B; P A B; F \<in> B leadsTo[CC] C; P B C |] 152 ==> P A C; 153 !!B S. \<forall>A\<in>S. F \<in> A leadsTo[CC] B & P A B ==> P (\<Union>S) B 154 |] ==> P za zb" 155apply (unfold leadsETo_def) 156apply (drule CollectD) 157apply (erule elt.induct, blast+) 158done 159 160 161(** New facts involving leadsETo **) 162 163lemma leadsETo_mono: "CC' <= CC ==> (A leadsTo[CC'] B) <= (A leadsTo[CC] B)" 164apply safe 165apply (erule leadsETo_induct) 166prefer 3 apply (blast intro: leadsETo_Union) 167prefer 2 apply (blast intro: leadsETo_Trans) 168apply blast 169done 170 171lemma leadsETo_Trans_Un: 172 "[| F \<in> A leadsTo[CC] B; F \<in> B leadsTo[DD] C |] 173 ==> F \<in> A leadsTo[CC Un DD] C" 174by (blast intro: leadsETo_mono [THEN subsetD] leadsETo_Trans) 175 176lemma leadsETo_Union_Int: 177 "(!!A. A \<in> S ==> F \<in> (A Int C) leadsTo[CC] B) 178 ==> F \<in> (\<Union>S Int C) leadsTo[CC] B" 179apply (unfold leadsETo_def) 180apply (simp only: Int_Union_Union) 181apply (blast intro: elt.Union) 182done 183 184(*Binary union introduction rule*) 185lemma leadsETo_Un: 186 "[| F \<in> A leadsTo[CC] C; F \<in> B leadsTo[CC] C |] 187 ==> F \<in> (A Un B) leadsTo[CC] C" 188 using leadsETo_Union [of "{A, B}" F CC C] by auto 189 190lemma single_leadsETo_I: 191 "(\<And>x. x \<in> A ==> F \<in> {x} leadsTo[CC] B) \<Longrightarrow> F \<in> A leadsTo[CC] B" 192by (subst UN_singleton [symmetric], rule leadsETo_UN, blast) 193 194 195lemma subset_imp_leadsETo: "A<=B \<Longrightarrow> F \<in> A leadsTo[CC] B" 196by (simp add: subset_imp_ensures [THEN leadsETo_Basis] 197 Diff_eq_empty_iff [THEN iffD2]) 198 199lemmas empty_leadsETo = empty_subsetI [THEN subset_imp_leadsETo, simp] 200 201 202 203(** Weakening laws **) 204 205lemma leadsETo_weaken_R: 206 "[| F \<in> A leadsTo[CC] A'; A'<=B' |] ==> F \<in> A leadsTo[CC] B'" 207by (blast intro: subset_imp_leadsETo leadsETo_Trans) 208 209lemma leadsETo_weaken_L: 210 "[| F \<in> A leadsTo[CC] A'; B<=A |] ==> F \<in> B leadsTo[CC] A'" 211by (blast intro: leadsETo_Trans subset_imp_leadsETo) 212 213(*Distributes over binary unions*) 214lemma leadsETo_Un_distrib: 215 "F \<in> (A Un B) leadsTo[CC] C = 216 (F \<in> A leadsTo[CC] C \<and> F \<in> B leadsTo[CC] C)" 217by (blast intro: leadsETo_Un leadsETo_weaken_L) 218 219lemma leadsETo_UN_distrib: 220 "F \<in> (UN i:I. A i) leadsTo[CC] B = 221 (\<forall>i\<in>I. F \<in> (A i) leadsTo[CC] B)" 222by (blast intro: leadsETo_UN leadsETo_weaken_L) 223 224lemma leadsETo_Union_distrib: 225 "F \<in> (\<Union>S) leadsTo[CC] B = (\<forall>A\<in>S. F \<in> A leadsTo[CC] B)" 226by (blast intro: leadsETo_Union leadsETo_weaken_L) 227 228lemma leadsETo_weaken: 229 "[| F \<in> A leadsTo[CC'] A'; B<=A; A'<=B'; CC' <= CC |] 230 ==> F \<in> B leadsTo[CC] B'" 231apply (drule leadsETo_mono [THEN subsetD], assumption) 232apply (blast del: subsetCE 233 intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans) 234done 235 236lemma leadsETo_givenBy: 237 "[| F \<in> A leadsTo[CC] A'; CC <= givenBy v |] 238 ==> F \<in> A leadsTo[givenBy v] A'" 239by (blast intro: leadsETo_weaken) 240 241 242(*Set difference*) 243lemma leadsETo_Diff: 244 "[| F \<in> (A-B) leadsTo[CC] C; F \<in> B leadsTo[CC] C |] 245 ==> F \<in> A leadsTo[CC] C" 246by (blast intro: leadsETo_Un leadsETo_weaken) 247 248 249(*Binary union version*) 250lemma leadsETo_Un_Un: 251 "[| F \<in> A leadsTo[CC] A'; F \<in> B leadsTo[CC] B' |] 252 ==> F \<in> (A Un B) leadsTo[CC] (A' Un B')" 253by (blast intro: leadsETo_Un leadsETo_weaken_R) 254 255 256(** The cancellation law **) 257 258lemma leadsETo_cancel2: 259 "[| F \<in> A leadsTo[CC] (A' Un B); F \<in> B leadsTo[CC] B' |] 260 ==> F \<in> A leadsTo[CC] (A' Un B')" 261by (blast intro: leadsETo_Un_Un subset_imp_leadsETo leadsETo_Trans) 262 263lemma leadsETo_cancel1: 264 "[| F \<in> A leadsTo[CC] (B Un A'); F \<in> B leadsTo[CC] B' |] 265 ==> F \<in> A leadsTo[CC] (B' Un A')" 266apply (simp add: Un_commute) 267apply (blast intro!: leadsETo_cancel2) 268done 269 270lemma leadsETo_cancel_Diff1: 271 "[| F \<in> A leadsTo[CC] (B Un A'); F \<in> (B-A') leadsTo[CC] B' |] 272 ==> F \<in> A leadsTo[CC] (B' Un A')" 273apply (rule leadsETo_cancel1) 274 prefer 2 apply assumption 275apply simp_all 276done 277 278 279(** PSP: Progress-Safety-Progress **) 280 281(*Special case of PSP: Misra's "stable conjunction"*) 282lemma e_psp_stable: 283 "[| F \<in> A leadsTo[CC] A'; F \<in> stable B; \<forall>C\<in>CC. C Int B \<in> CC |] 284 ==> F \<in> (A Int B) leadsTo[CC] (A' Int B)" 285apply (unfold stable_def) 286apply (erule leadsETo_induct) 287prefer 3 apply (blast intro: leadsETo_Union_Int) 288prefer 2 apply (blast intro: leadsETo_Trans) 289apply (rule leadsETo_Basis) 290prefer 2 apply (force simp add: Diff_Int_distrib2 [symmetric]) 291apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] 292 Int_Un_distrib2 [symmetric]) 293apply (blast intro: transient_strengthen constrains_Int) 294done 295 296lemma e_psp_stable2: 297 "[| F \<in> A leadsTo[CC] A'; F \<in> stable B; \<forall>C\<in>CC. C Int B \<in> CC |] 298 ==> F \<in> (B Int A) leadsTo[CC] (B Int A')" 299by (simp (no_asm_simp) add: e_psp_stable Int_ac) 300 301lemma e_psp: 302 "[| F \<in> A leadsTo[CC] A'; F \<in> B co B'; 303 \<forall>C\<in>CC. C Int B Int B' \<in> CC |] 304 ==> F \<in> (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))" 305apply (erule leadsETo_induct) 306prefer 3 apply (blast intro: leadsETo_Union_Int) 307(*Transitivity case has a delicate argument involving "cancellation"*) 308apply (rule_tac [2] leadsETo_Un_duplicate2) 309apply (erule_tac [2] leadsETo_cancel_Diff1) 310prefer 2 311 apply (simp add: Int_Diff Diff_triv) 312 apply (blast intro: leadsETo_weaken_L dest: constrains_imp_subset) 313(*Basis case*) 314apply (rule leadsETo_Basis) 315apply (blast intro: psp_ensures) 316apply (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'") 317apply auto 318done 319 320lemma e_psp2: 321 "[| F \<in> A leadsTo[CC] A'; F \<in> B co B'; 322 \<forall>C\<in>CC. C Int B Int B' \<in> CC |] 323 ==> F \<in> (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))" 324by (simp add: e_psp Int_ac) 325 326 327(*** Special properties involving the parameter [CC] ***) 328 329(*??IS THIS NEEDED?? or is it just an example of what's provable??*) 330lemma gen_leadsETo_imp_Join_leadsETo: 331 "[| F \<in> (A leadsTo[givenBy v] B); G \<in> preserves v; 332 F\<squnion>G \<in> stable C |] 333 ==> F\<squnion>G \<in> ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)" 334apply (erule leadsETo_induct) 335 prefer 3 336 apply (subst Int_Union) 337 apply (blast intro: leadsETo_UN) 338prefer 2 339 apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans) 340apply (rule leadsETo_Basis) 341apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] 342 Int_Diff ensures_def givenBy_eq_Collect) 343prefer 3 apply (blast intro: transient_strengthen) 344apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD]) 345apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD]) 346apply (unfold stable_def) 347apply (blast intro: constrains_Int [THEN constrains_weaken])+ 348done 349 350(**** Relationship with traditional "leadsTo", strong & weak ****) 351 352(** strong **) 353 354lemma leadsETo_subset_leadsTo: "(A leadsTo[CC] B) <= (A leadsTo B)" 355apply safe 356apply (erule leadsETo_induct) 357 prefer 3 apply (blast intro: leadsTo_Union) 358 prefer 2 apply (blast intro: leadsTo_Trans, blast) 359done 360 361lemma leadsETo_UNIV_eq_leadsTo: "(A leadsTo[UNIV] B) = (A leadsTo B)" 362apply safe 363apply (erule leadsETo_subset_leadsTo [THEN subsetD]) 364(*right-to-left case*) 365apply (erule leadsTo_induct) 366 prefer 3 apply (blast intro: leadsETo_Union) 367 prefer 2 apply (blast intro: leadsETo_Trans, blast) 368done 369 370(**** weak ****) 371 372lemma LeadsETo_eq_leadsETo: 373 "A LeadsTo[CC] B = 374 {F. F \<in> (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] 375 (reachable F Int B)}" 376apply (unfold LeadsETo_def) 377apply (blast dest: e_psp_stable2 intro: leadsETo_weaken) 378done 379 380(*** Introduction rules: Basis, Trans, Union ***) 381 382lemma LeadsETo_Trans: 383 "[| F \<in> A LeadsTo[CC] B; F \<in> B LeadsTo[CC] C |] 384 ==> F \<in> A LeadsTo[CC] C" 385apply (simp add: LeadsETo_eq_leadsETo) 386apply (blast intro: leadsETo_Trans) 387done 388 389lemma LeadsETo_Union: 390 "(\<And>A. A \<in> S \<Longrightarrow> F \<in> A LeadsTo[CC] B) \<Longrightarrow> F \<in> (\<Union>S) LeadsTo[CC] B" 391apply (simp add: LeadsETo_def) 392apply (subst Int_Union) 393apply (blast intro: leadsETo_UN) 394done 395 396lemma LeadsETo_UN: 397 "(\<And>i. i \<in> I \<Longrightarrow> F \<in> (A i) LeadsTo[CC] B) 398 \<Longrightarrow> F \<in> (UN i:I. A i) LeadsTo[CC] B" 399apply (blast intro: LeadsETo_Union) 400done 401 402(*Binary union introduction rule*) 403lemma LeadsETo_Un: 404 "[| F \<in> A LeadsTo[CC] C; F \<in> B LeadsTo[CC] C |] 405 ==> F \<in> (A Un B) LeadsTo[CC] C" 406 using LeadsETo_Union [of "{A, B}" F CC C] by auto 407 408(*Lets us look at the starting state*) 409lemma single_LeadsETo_I: 410 "(\<And>s. s \<in> A ==> F \<in> {s} LeadsTo[CC] B) \<Longrightarrow> F \<in> A LeadsTo[CC] B" 411by (subst UN_singleton [symmetric], rule LeadsETo_UN, blast) 412 413lemma subset_imp_LeadsETo: 414 "A <= B \<Longrightarrow> F \<in> A LeadsTo[CC] B" 415apply (simp (no_asm) add: LeadsETo_def) 416apply (blast intro: subset_imp_leadsETo) 417done 418 419lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo] 420 421lemma LeadsETo_weaken_R: 422 "[| F \<in> A LeadsTo[CC] A'; A' <= B' |] ==> F \<in> A LeadsTo[CC] B'" 423apply (simp add: LeadsETo_def) 424apply (blast intro: leadsETo_weaken_R) 425done 426 427lemma LeadsETo_weaken_L: 428 "[| F \<in> A LeadsTo[CC] A'; B <= A |] ==> F \<in> B LeadsTo[CC] A'" 429apply (simp add: LeadsETo_def) 430apply (blast intro: leadsETo_weaken_L) 431done 432 433lemma LeadsETo_weaken: 434 "[| F \<in> A LeadsTo[CC'] A'; 435 B <= A; A' <= B'; CC' <= CC |] 436 ==> F \<in> B LeadsTo[CC] B'" 437apply (simp (no_asm_use) add: LeadsETo_def) 438apply (blast intro: leadsETo_weaken) 439done 440 441lemma LeadsETo_subset_LeadsTo: "(A LeadsTo[CC] B) <= (A LeadsTo B)" 442apply (unfold LeadsETo_def LeadsTo_def) 443apply (blast intro: leadsETo_subset_leadsTo [THEN subsetD]) 444done 445 446(*Postcondition can be strengthened to (reachable F Int B) *) 447lemma reachable_ensures: 448 "F \<in> A ensures B \<Longrightarrow> F \<in> (reachable F Int A) ensures B" 449apply (rule stable_ensures_Int [THEN ensures_weaken_R], auto) 450done 451 452lemma lel_lemma: 453 "F \<in> A leadsTo B \<Longrightarrow> F \<in> (reachable F Int A) leadsTo[Pow(reachable F)] B" 454apply (erule leadsTo_induct) 455 apply (blast intro: reachable_ensures) 456 apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L) 457apply (subst Int_Union) 458apply (blast intro: leadsETo_UN) 459done 460 461lemma LeadsETo_UNIV_eq_LeadsTo: "(A LeadsTo[UNIV] B) = (A LeadsTo B)" 462apply safe 463apply (erule LeadsETo_subset_LeadsTo [THEN subsetD]) 464(*right-to-left case*) 465apply (unfold LeadsETo_def LeadsTo_def) 466apply (blast intro: lel_lemma [THEN leadsETo_weaken]) 467done 468 469 470(**** EXTEND/PROJECT PROPERTIES ****) 471 472context Extend 473begin 474 475lemma givenBy_o_eq_extend_set: 476 "givenBy (v o f) = extend_set h ` (givenBy v)" 477apply (simp add: givenBy_eq_Collect) 478apply (rule equalityI, best) 479apply blast 480done 481 482lemma givenBy_eq_extend_set: "givenBy f = range (extend_set h)" 483by (simp add: givenBy_eq_Collect, best) 484 485lemma extend_set_givenBy_I: 486 "D \<in> givenBy v ==> extend_set h D \<in> givenBy (v o f)" 487apply (simp (no_asm_use) add: givenBy_eq_all, blast) 488done 489 490lemma leadsETo_imp_extend_leadsETo: 491 "F \<in> A leadsTo[CC] B 492 ==> extend h F \<in> (extend_set h A) leadsTo[extend_set h ` CC] 493 (extend_set h B)" 494apply (erule leadsETo_induct) 495 apply (force intro: subset_imp_ensures 496 simp add: extend_ensures extend_set_Diff_distrib [symmetric]) 497 apply (blast intro: leadsETo_Trans) 498apply (simp add: leadsETo_UN extend_set_Union) 499done 500 501 502(*This version's stronger in the "ensures" precondition 503 BUT there's no ensures_weaken_L*) 504lemma Join_project_ensures_strong: 505 "[| project h C G \<notin> transient (project_set h C Int (A-B)) | 506 project_set h C Int (A - B) = {}; 507 extend h F\<squnion>G \<in> stable C; 508 F\<squnion>project h C G \<in> (project_set h C Int A) ensures B |] 509 ==> extend h F\<squnion>G \<in> (C Int extend_set h A) ensures (extend_set h B)" 510apply (subst Int_extend_set_lemma [symmetric]) 511apply (rule Join_project_ensures) 512apply (auto simp add: Int_Diff) 513done 514 515(*NOT WORKING. MODIFY AS IN Project.thy 516lemma pld_lemma: 517 "[| extend h F\<squnion>G : stable C; 518 F\<squnion>project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B; 519 G : preserves (v o f) |] 520 ==> extend h F\<squnion>G : 521 (C Int extend_set h (project_set h C Int A)) 522 leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)" 523apply (erule leadsETo_induct) 524 prefer 3 525 apply (simp del: UN_simps add: Int_UN_distrib leadsETo_UN extend_set_Union) 526 prefer 2 527 apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans) 528txt{*Base case is hard*} 529apply auto 530apply (force intro: leadsETo_Basis subset_imp_ensures) 531apply (rule leadsETo_Basis) 532 prefer 2 533 apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric]) 534apply (rule Join_project_ensures_strong) 535apply (auto intro: project_stable_project_set simp add: Int_left_absorb) 536apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set) 537done 538 539lemma project_leadsETo_D_lemma: 540 "[| extend h F\<squnion>G : stable C; 541 F\<squnion>project h C G : 542 (project_set h C Int A) 543 leadsTo[(%D. project_set h C Int D)`givenBy v] B; 544 G : preserves (v o f) |] 545 ==> extend h F\<squnion>G : (C Int extend_set h A) 546 leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)" 547apply (rule pld_lemma [THEN leadsETo_weaken]) 548apply (auto simp add: split_extended_all) 549done 550 551lemma project_leadsETo_D: 552 "[| F\<squnion>project h UNIV G : A leadsTo[givenBy v] B; 553 G : preserves (v o f) |] 554 ==> extend h F\<squnion>G : (extend_set h A) 555 leadsTo[givenBy (v o f)] (extend_set h B)" 556apply (cut_tac project_leadsETo_D_lemma [of _ _ UNIV], auto) 557apply (erule leadsETo_givenBy) 558apply (rule givenBy_o_eq_extend_set [THEN equalityD2]) 559done 560 561lemma project_LeadsETo_D: 562 "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G 563 : A LeadsTo[givenBy v] B; 564 G : preserves (v o f) |] 565 ==> extend h F\<squnion>G : 566 (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)" 567apply (cut_tac subset_refl [THEN stable_reachable, THEN project_leadsETo_D_lemma]) 568apply (auto simp add: LeadsETo_def) 569 apply (erule leadsETo_mono [THEN [2] rev_subsetD]) 570 apply (blast intro: extend_set_givenBy_I) 571apply (simp add: project_set_reachable_extend_eq [symmetric]) 572done 573 574lemma extending_leadsETo: 575 "(ALL G. extend h F ok G --> G : preserves (v o f)) 576 ==> extending (%G. UNIV) h F 577 (extend_set h A leadsTo[givenBy (v o f)] extend_set h B) 578 (A leadsTo[givenBy v] B)" 579apply (unfold extending_def) 580apply (auto simp add: project_leadsETo_D) 581done 582 583lemma extending_LeadsETo: 584 "(ALL G. extend h F ok G --> G : preserves (v o f)) 585 ==> extending (%G. reachable (extend h F\<squnion>G)) h F 586 (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B) 587 (A LeadsTo[givenBy v] B)" 588apply (unfold extending_def) 589apply (blast intro: project_LeadsETo_D) 590done 591*) 592 593 594(*** leadsETo in the precondition ***) 595 596(*Lemma for the Trans case*) 597lemma pli_lemma: 598 "[| extend h F\<squnion>G \<in> stable C; 599 F\<squnion>project h C G 600 \<in> project_set h C Int project_set h A leadsTo project_set h B |] 601 ==> F\<squnion>project h C G 602 \<in> project_set h C Int project_set h A leadsTo 603 project_set h C Int project_set h B" 604apply (rule psp_stable2 [THEN leadsTo_weaken_L]) 605apply (auto simp add: project_stable_project_set extend_stable_project_set) 606done 607 608lemma project_leadsETo_I_lemma: 609 "[| extend h F\<squnion>G \<in> stable C; 610 extend h F\<squnion>G \<in> 611 (C Int A) leadsTo[(%D. C Int D)`givenBy f] B |] 612 ==> F\<squnion>project h C G 613 \<in> (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)" 614apply (erule leadsETo_induct) 615 prefer 3 616 apply (simp only: Int_UN_distrib project_set_Union) 617 apply (blast intro: leadsTo_UN) 618 prefer 2 apply (blast intro: leadsTo_Trans pli_lemma) 619apply (simp add: givenBy_eq_extend_set) 620apply (rule leadsTo_Basis) 621apply (blast intro: ensures_extend_set_imp_project_ensures) 622done 623 624lemma project_leadsETo_I: 625 "extend h F\<squnion>G \<in> (extend_set h A) leadsTo[givenBy f] (extend_set h B) 626 \<Longrightarrow> F\<squnion>project h UNIV G \<in> A leadsTo B" 627apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto) 628done 629 630lemma project_LeadsETo_I: 631 "extend h F\<squnion>G \<in> (extend_set h A) LeadsTo[givenBy f] (extend_set h B) 632 \<Longrightarrow> F\<squnion>project h (reachable (extend h F\<squnion>G)) G 633 \<in> A LeadsTo B" 634apply (simp (no_asm_use) add: LeadsTo_def LeadsETo_def) 635apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken]) 636apply (auto simp add: project_set_reachable_extend_eq [symmetric]) 637done 638 639lemma projecting_leadsTo: 640 "projecting (\<lambda>G. UNIV) h F 641 (extend_set h A leadsTo[givenBy f] extend_set h B) 642 (A leadsTo B)" 643apply (unfold projecting_def) 644apply (force dest: project_leadsETo_I) 645done 646 647lemma projecting_LeadsTo: 648 "projecting (\<lambda>G. reachable (extend h F\<squnion>G)) h F 649 (extend_set h A LeadsTo[givenBy f] extend_set h B) 650 (A LeadsTo B)" 651apply (unfold projecting_def) 652apply (force dest: project_LeadsETo_I) 653done 654 655end 656 657end 658