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