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