src/HOL/UNITY/ELT.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45605 a89b4bc311a5
child 46577 e5438c5797ae
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Title:      HOL/UNITY/ELT.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1999  University of Cambridge
     4 
     5 leadsTo strengthened with a specification of the allowable sets transient parts
     6 
     7 TRY 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 
    11 inductive "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 
    24 header{*Progress Under Allowable Sets*}
    25 
    26 theory ELT imports Project begin
    27 
    28 inductive_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 : A ensures B;  A-B : (insert {} CC) |] ==> (A,B) : elt CC F"
    35 
    36  | Trans:  "[| (A,B) : elt CC F;  (B,C) : elt CC F |] ==> (A,C) : elt CC F"
    37 
    38  | Union:  "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F"
    39 
    40 
    41 definition  
    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 
    46 definition
    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) : elt CC F}"
    51 
    52 definition
    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 : (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 [2] 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   using leadsETo_Union [of "{A, B}" F CC C] by auto
   190 
   191 lemma single_leadsETo_I:
   192      "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
   193 by (subst UN_singleton [symmetric], rule leadsETo_UN, blast)
   194 
   195 
   196 lemma subset_imp_leadsETo: "A<=B ==> F : A leadsTo[CC] B"
   197 by (simp add: subset_imp_ensures [THEN leadsETo_Basis] 
   198               Diff_eq_empty_iff [THEN iffD2])
   199 
   200 lemmas empty_leadsETo = empty_subsetI [THEN subset_imp_leadsETo, simp]
   201 
   202 
   203 
   204 (** Weakening laws **)
   205 
   206 lemma leadsETo_weaken_R:
   207      "[| F : A leadsTo[CC] A';  A'<=B' |] ==> F : A leadsTo[CC] B'"
   208 by (blast intro: subset_imp_leadsETo leadsETo_Trans)
   209 
   210 lemma leadsETo_weaken_L [rule_format]:
   211      "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
   212 by (blast intro: leadsETo_Trans subset_imp_leadsETo)
   213 
   214 (*Distributes over binary unions*)
   215 lemma leadsETo_Un_distrib:
   216      "F : (A Un B) leadsTo[CC] C  =   
   217       (F : A leadsTo[CC] C & F : B leadsTo[CC] C)"
   218 by (blast intro: leadsETo_Un leadsETo_weaken_L)
   219 
   220 lemma leadsETo_UN_distrib:
   221      "F : (UN i:I. A i) leadsTo[CC] B  =   
   222       (ALL i : I. F : (A i) leadsTo[CC] B)"
   223 by (blast intro: leadsETo_UN leadsETo_weaken_L)
   224 
   225 lemma leadsETo_Union_distrib:
   226      "F : (Union S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)"
   227 by (blast intro: leadsETo_Union leadsETo_weaken_L)
   228 
   229 lemma leadsETo_weaken:
   230      "[| F : A leadsTo[CC'] A'; B<=A; A'<=B';  CC' <= CC |]  
   231       ==> F : B leadsTo[CC] B'"
   232 apply (drule leadsETo_mono [THEN subsetD], assumption)
   233 apply (blast del: subsetCE 
   234              intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans)
   235 done
   236 
   237 lemma leadsETo_givenBy:
   238      "[| F : A leadsTo[CC] A';  CC <= givenBy v |]  
   239       ==> F : A leadsTo[givenBy v] A'"
   240 by (blast intro: empty_mem_givenBy leadsETo_weaken)
   241 
   242 
   243 (*Set difference*)
   244 lemma leadsETo_Diff:
   245      "[| F : (A-B) leadsTo[CC] C; F : B leadsTo[CC] C |]  
   246       ==> F : A leadsTo[CC] C"
   247 by (blast intro: leadsETo_Un leadsETo_weaken)
   248 
   249 
   250 (*Binary union version*)
   251 lemma leadsETo_Un_Un:
   252      "[| F : A leadsTo[CC] A';  F : B leadsTo[CC] B' |]  
   253       ==> F : (A Un B) leadsTo[CC] (A' Un B')"
   254 by (blast intro: leadsETo_Un leadsETo_weaken_R)
   255 
   256 
   257 (** The cancellation law **)
   258 
   259 lemma leadsETo_cancel2:
   260      "[| F : A leadsTo[CC] (A' Un B); F : B leadsTo[CC] B' |]  
   261       ==> F : A leadsTo[CC] (A' Un B')"
   262 by (blast intro: leadsETo_Un_Un subset_imp_leadsETo leadsETo_Trans)
   263 
   264 lemma leadsETo_cancel1:
   265      "[| F : A leadsTo[CC] (B Un A'); F : B leadsTo[CC] B' |]  
   266     ==> F : A leadsTo[CC] (B' Un A')"
   267 apply (simp add: Un_commute)
   268 apply (blast intro!: leadsETo_cancel2)
   269 done
   270 
   271 lemma leadsETo_cancel_Diff1:
   272      "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |]  
   273     ==> F : A leadsTo[CC] (B' Un A')"
   274 apply (rule leadsETo_cancel1)
   275  prefer 2 apply assumption
   276 apply simp_all
   277 done
   278 
   279 
   280 (** PSP: Progress-Safety-Progress **)
   281 
   282 (*Special case of PSP: Misra's "stable conjunction"*)
   283 lemma e_psp_stable: 
   284    "[| F : A leadsTo[CC] A';  F : stable B;  ALL C:CC. C Int B : CC |]  
   285     ==> F : (A Int B) leadsTo[CC] (A' Int B)"
   286 apply (unfold stable_def)
   287 apply (erule leadsETo_induct)
   288 prefer 3 apply (blast intro: leadsETo_Union_Int)
   289 prefer 2 apply (blast intro: leadsETo_Trans)
   290 apply (rule leadsETo_Basis)
   291 prefer 2 apply (force simp add: Diff_Int_distrib2 [symmetric])
   292 apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] 
   293                  Int_Un_distrib2 [symmetric])
   294 apply (blast intro: transient_strengthen constrains_Int)
   295 done
   296 
   297 lemma e_psp_stable2:
   298      "[| F : A leadsTo[CC] A'; F : stable B;  ALL C:CC. C Int B : CC |]  
   299       ==> F : (B Int A) leadsTo[CC] (B Int A')"
   300 by (simp (no_asm_simp) add: e_psp_stable Int_ac)
   301 
   302 lemma e_psp:
   303      "[| F : A leadsTo[CC] A'; F : B co B';   
   304          ALL C:CC. C Int B Int B' : CC |]  
   305       ==> F : (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))"
   306 apply (erule leadsETo_induct)
   307 prefer 3 apply (blast intro: leadsETo_Union_Int)
   308 (*Transitivity case has a delicate argument involving "cancellation"*)
   309 apply (rule_tac [2] leadsETo_Un_duplicate2)
   310 apply (erule_tac [2] leadsETo_cancel_Diff1)
   311 prefer 2
   312  apply (simp add: Int_Diff Diff_triv)
   313  apply (blast intro: leadsETo_weaken_L dest: constrains_imp_subset)
   314 (*Basis case*)
   315 apply (rule leadsETo_Basis)
   316 apply (blast intro: psp_ensures)
   317 apply (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'")
   318 apply auto
   319 done
   320 
   321 lemma e_psp2:
   322      "[| F : A leadsTo[CC] A'; F : B co B';   
   323          ALL C:CC. C Int B Int B' : CC |]  
   324       ==> F : (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))"
   325 by (simp add: e_psp Int_ac)
   326 
   327 
   328 (*** Special properties involving the parameter [CC] ***)
   329 
   330 (*??IS THIS NEEDED?? or is it just an example of what's provable??*)
   331 lemma gen_leadsETo_imp_Join_leadsETo:
   332      "[| F: (A leadsTo[givenBy v] B);  G : preserves v;   
   333          F\<squnion>G : stable C |]  
   334       ==> F\<squnion>G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
   335 apply (erule leadsETo_induct)
   336   prefer 3
   337   apply (subst Int_Union) 
   338   apply (blast intro: leadsETo_UN)
   339 prefer 2
   340  apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
   341 apply (rule leadsETo_Basis)
   342 apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] 
   343                       Int_Diff ensures_def givenBy_eq_Collect Join_transient)
   344 prefer 3 apply (blast intro: transient_strengthen)
   345 apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
   346 apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
   347 apply (unfold stable_def)
   348 apply (blast intro: constrains_Int [THEN constrains_weaken])+
   349 done
   350 
   351 (**** Relationship with traditional "leadsTo", strong & weak ****)
   352 
   353 (** strong **)
   354 
   355 lemma leadsETo_subset_leadsTo: "(A leadsTo[CC] B) <= (A leadsTo B)"
   356 apply safe
   357 apply (erule leadsETo_induct)
   358   prefer 3 apply (blast intro: leadsTo_Union)
   359  prefer 2 apply (blast intro: leadsTo_Trans, blast)
   360 done
   361 
   362 lemma leadsETo_UNIV_eq_leadsTo: "(A leadsTo[UNIV] B) = (A leadsTo B)"
   363 apply safe
   364 apply (erule leadsETo_subset_leadsTo [THEN subsetD])
   365 (*right-to-left case*)
   366 apply (erule leadsTo_induct)
   367   prefer 3 apply (blast intro: leadsETo_Union)
   368  prefer 2 apply (blast intro: leadsETo_Trans, blast)
   369 done
   370 
   371 (**** weak ****)
   372 
   373 lemma LeadsETo_eq_leadsETo: 
   374      "A LeadsTo[CC] B =  
   375         {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC]  
   376         (reachable F Int B)}"
   377 apply (unfold LeadsETo_def)
   378 apply (blast dest: e_psp_stable2 intro: leadsETo_weaken)
   379 done
   380 
   381 (*** Introduction rules: Basis, Trans, Union ***)
   382 
   383 lemma LeadsETo_Trans:
   384      "[| F : A LeadsTo[CC] B;  F : B LeadsTo[CC] C |]  
   385       ==> F : A LeadsTo[CC] C"
   386 apply (simp add: LeadsETo_eq_leadsETo)
   387 apply (blast intro: leadsETo_Trans)
   388 done
   389 
   390 lemma LeadsETo_Union:
   391      "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B"
   392 apply (simp add: LeadsETo_def)
   393 apply (subst Int_Union)
   394 apply (blast intro: leadsETo_UN)
   395 done
   396 
   397 lemma LeadsETo_UN:
   398      "(!!i. i : I ==> F : (A i) LeadsTo[CC] B)  
   399       ==> F : (UN i:I. A i) LeadsTo[CC] B"
   400 apply (simp only: Union_image_eq [symmetric])
   401 apply (blast intro: LeadsETo_Union)
   402 done
   403 
   404 (*Binary union introduction rule*)
   405 lemma LeadsETo_Un:
   406      "[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |]  
   407       ==> F : (A Un B) LeadsTo[CC] C"
   408   using LeadsETo_Union [of "{A, B}" F CC C] by auto
   409 
   410 (*Lets us look at the starting state*)
   411 lemma single_LeadsETo_I:
   412      "(!!s. s : A ==> F : {s} LeadsTo[CC] B) ==> F : A LeadsTo[CC] B"
   413 by (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)
   414 
   415 lemma subset_imp_LeadsETo:
   416      "A <= B ==> F : A LeadsTo[CC] B"
   417 apply (simp (no_asm) add: LeadsETo_def)
   418 apply (blast intro: subset_imp_leadsETo)
   419 done
   420 
   421 lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo]
   422 
   423 lemma LeadsETo_weaken_R [rule_format]:
   424      "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
   425 apply (simp (no_asm_use) add: LeadsETo_def)
   426 apply (blast intro: leadsETo_weaken_R)
   427 done
   428 
   429 lemma LeadsETo_weaken_L [rule_format]:
   430      "[| F : A LeadsTo[CC] A';  B <= A |] ==> F : B LeadsTo[CC] A'"
   431 apply (simp (no_asm_use) add: LeadsETo_def)
   432 apply (blast intro: leadsETo_weaken_L)
   433 done
   434 
   435 lemma LeadsETo_weaken:
   436      "[| F : A LeadsTo[CC'] A';    
   437          B <= A;  A' <= B';  CC' <= CC |]  
   438       ==> F : B LeadsTo[CC] B'"
   439 apply (simp (no_asm_use) add: LeadsETo_def)
   440 apply (blast intro: leadsETo_weaken)
   441 done
   442 
   443 lemma LeadsETo_subset_LeadsTo: "(A LeadsTo[CC] B) <= (A LeadsTo B)"
   444 apply (unfold LeadsETo_def LeadsTo_def)
   445 apply (blast intro: leadsETo_subset_leadsTo [THEN subsetD])
   446 done
   447 
   448 (*Postcondition can be strengthened to (reachable F Int B) *)
   449 lemma reachable_ensures:
   450      "F : A ensures B ==> F : (reachable F Int A) ensures B"
   451 apply (rule stable_ensures_Int [THEN ensures_weaken_R], auto)
   452 done
   453 
   454 lemma lel_lemma:
   455      "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B"
   456 apply (erule leadsTo_induct)
   457   apply (blast intro: reachable_ensures leadsETo_Basis)
   458  apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
   459 apply (subst Int_Union)
   460 apply (blast intro: leadsETo_UN)
   461 done
   462 
   463 lemma LeadsETo_UNIV_eq_LeadsTo: "(A LeadsTo[UNIV] B) = (A LeadsTo B)"
   464 apply safe
   465 apply (erule LeadsETo_subset_LeadsTo [THEN subsetD])
   466 (*right-to-left case*)
   467 apply (unfold LeadsETo_def LeadsTo_def)
   468 apply (blast intro: lel_lemma [THEN leadsETo_weaken])
   469 done
   470 
   471 
   472 (**** EXTEND/PROJECT PROPERTIES ****)
   473 
   474 lemma (in Extend) givenBy_o_eq_extend_set:
   475      "givenBy (v o f) = extend_set h ` (givenBy v)"
   476 apply (simp add: givenBy_eq_Collect)
   477 apply (rule equalityI, best)
   478 apply blast 
   479 done
   480 
   481 lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
   482 by (simp add: givenBy_eq_Collect, best)
   483 
   484 lemma (in Extend) extend_set_givenBy_I:
   485      "D : givenBy v ==> extend_set h D : givenBy (v o f)"
   486 apply (simp (no_asm_use) add: givenBy_eq_all, blast)
   487 done
   488 
   489 lemma (in Extend) leadsETo_imp_extend_leadsETo:
   490      "F : A leadsTo[CC] B  
   491       ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]  
   492                        (extend_set h B)"
   493 apply (erule leadsETo_induct)
   494   apply (force intro: leadsETo_Basis subset_imp_ensures 
   495                simp add: extend_ensures extend_set_Diff_distrib [symmetric])
   496  apply (blast intro: leadsETo_Trans)
   497 apply (simp add: leadsETo_UN extend_set_Union)
   498 done
   499 
   500 
   501 (*This version's stronger in the "ensures" precondition
   502   BUT there's no ensures_weaken_L*)
   503 lemma (in Extend) Join_project_ensures_strong:
   504      "[| project h C G ~: transient (project_set h C Int (A-B)) |  
   505            project_set h C Int (A - B) = {};   
   506          extend h F\<squnion>G : stable C;   
   507          F\<squnion>project h C G : (project_set h C Int A) ensures B |]  
   508       ==> extend h F\<squnion>G : (C Int extend_set h A) ensures (extend_set h B)"
   509 apply (subst Int_extend_set_lemma [symmetric])
   510 apply (rule Join_project_ensures)
   511 apply (auto simp add: Int_Diff)
   512 done
   513 
   514 (*NOT WORKING.  MODIFY AS IN Project.thy
   515 lemma (in Extend) pld_lemma:
   516      "[| extend h F\<squnion>G : stable C;   
   517          F\<squnion>project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
   518          G : preserves (v o f) |]  
   519       ==> extend h F\<squnion>G :  
   520             (C Int extend_set h (project_set h C Int A))  
   521             leadsTo[(%D. C Int extend_set h D)`givenBy v]  (extend_set h B)"
   522 apply (erule leadsETo_induct)
   523   prefer 3
   524   apply (simp del: UN_simps add: Int_UN_distrib leadsETo_UN extend_set_Union)
   525  prefer 2
   526  apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
   527 txt{*Base case is hard*}
   528 apply auto
   529 apply (force intro: leadsETo_Basis subset_imp_ensures)
   530 apply (rule leadsETo_Basis)
   531  prefer 2
   532  apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric])
   533 apply (rule Join_project_ensures_strong)
   534 apply (auto intro: project_stable_project_set simp add: Int_left_absorb)
   535 apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set)
   536 done
   537 
   538 lemma (in Extend) project_leadsETo_D_lemma:
   539      "[| extend h F\<squnion>G : stable C;   
   540          F\<squnion>project h C G :  
   541              (project_set h C Int A)  
   542              leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
   543          G : preserves (v o f) |]  
   544       ==> extend h F\<squnion>G : (C Int extend_set h A)  
   545             leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)"
   546 apply (rule pld_lemma [THEN leadsETo_weaken])
   547 apply (auto simp add: split_extended_all)
   548 done
   549 
   550 lemma (in Extend) project_leadsETo_D:
   551      "[| F\<squnion>project h UNIV G : A leadsTo[givenBy v] B;   
   552          G : preserves (v o f) |]   
   553       ==> extend h F\<squnion>G : (extend_set h A)  
   554             leadsTo[givenBy (v o f)] (extend_set h B)"
   555 apply (cut_tac project_leadsETo_D_lemma [of _ _ UNIV], auto) 
   556 apply (erule leadsETo_givenBy)
   557 apply (rule givenBy_o_eq_extend_set [THEN equalityD2])
   558 done
   559 
   560 lemma (in Extend) project_LeadsETo_D:
   561      "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G  
   562              : A LeadsTo[givenBy v] B;   
   563          G : preserves (v o f) |]  
   564       ==> extend h F\<squnion>G :  
   565             (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)"
   566 apply (cut_tac subset_refl [THEN stable_reachable, THEN project_leadsETo_D_lemma])
   567 apply (auto simp add: LeadsETo_def)
   568  apply (erule leadsETo_mono [THEN [2] rev_subsetD])
   569  apply (blast intro: extend_set_givenBy_I)
   570 apply (simp add: project_set_reachable_extend_eq [symmetric])
   571 done
   572 
   573 lemma (in Extend) extending_leadsETo: 
   574      "(ALL G. extend h F ok G --> G : preserves (v o f))  
   575       ==> extending (%G. UNIV) h F  
   576                 (extend_set h A leadsTo[givenBy (v o f)] extend_set h B)  
   577                 (A leadsTo[givenBy v] B)"
   578 apply (unfold extending_def)
   579 apply (auto simp add: project_leadsETo_D)
   580 done
   581 
   582 lemma (in Extend) extending_LeadsETo: 
   583      "(ALL G. extend h F ok G --> G : preserves (v o f))  
   584       ==> extending (%G. reachable (extend h F\<squnion>G)) h F  
   585                 (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B)  
   586                 (A LeadsTo[givenBy v]  B)"
   587 apply (unfold extending_def)
   588 apply (blast intro: project_LeadsETo_D)
   589 done
   590 *)
   591 
   592 
   593 (*** leadsETo in the precondition ***)
   594 
   595 (*Lemma for the Trans case*)
   596 lemma (in Extend) pli_lemma:
   597      "[| extend h F\<squnion>G : stable C;     
   598          F\<squnion>project h C G     
   599            : project_set h C Int project_set h A leadsTo project_set h B |]  
   600       ==> F\<squnion>project h C G     
   601             : project_set h C Int project_set h A leadsTo     
   602               project_set h C Int project_set h B"
   603 apply (rule psp_stable2 [THEN leadsTo_weaken_L])
   604 apply (auto simp add: project_stable_project_set extend_stable_project_set)
   605 done
   606 
   607 lemma (in Extend) project_leadsETo_I_lemma:
   608      "[| extend h F\<squnion>G : stable C;   
   609          extend h F\<squnion>G :  
   610            (C Int A) leadsTo[(%D. C Int D)`givenBy f]  B |]   
   611   ==> F\<squnion>project h C G   
   612     : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)"
   613 apply (erule leadsETo_induct)
   614   prefer 3
   615   apply (simp only: Int_UN_distrib project_set_Union)
   616   apply (blast intro: leadsTo_UN)
   617  prefer 2 apply (blast intro: leadsTo_Trans pli_lemma)
   618 apply (simp add: givenBy_eq_extend_set)
   619 apply (rule leadsTo_Basis)
   620 apply (blast intro: ensures_extend_set_imp_project_ensures)
   621 done
   622 
   623 lemma (in Extend) project_leadsETo_I:
   624      "extend h F\<squnion>G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
   625       ==> F\<squnion>project h UNIV G : A leadsTo B"
   626 apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto)
   627 done
   628 
   629 lemma (in Extend) project_LeadsETo_I:
   630      "extend h F\<squnion>G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B) 
   631       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G   
   632            : A LeadsTo B"
   633 apply (simp (no_asm_use) add: LeadsTo_def LeadsETo_def)
   634 apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken])
   635 apply (auto simp add: project_set_reachable_extend_eq [symmetric])
   636 done
   637 
   638 lemma (in Extend) projecting_leadsTo: 
   639      "projecting (%G. UNIV) h F  
   640                  (extend_set h A leadsTo[givenBy f] extend_set h B)  
   641                  (A leadsTo B)"
   642 apply (unfold projecting_def)
   643 apply (force dest: project_leadsETo_I)
   644 done
   645 
   646 lemma (in Extend) projecting_LeadsTo: 
   647      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
   648                  (extend_set h A LeadsTo[givenBy f] extend_set h B)  
   649                  (A LeadsTo B)"
   650 apply (unfold projecting_def)
   651 apply (force dest: project_LeadsETo_I)
   652 done
   653 
   654 end