src/HOL/UNITY/Project.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 59807 22bc39064290
child 63146 f1ecba0272f9
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/UNITY/Project.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1999  University of Cambridge
     4 
     5 Projections of state sets (also of actions and programs).
     6 
     7 Inheritance of GUARANTEES properties under extension.
     8 *)
     9 
    10 section{*Projections of State Sets*}
    11 
    12 theory Project imports Extend begin
    13 
    14 definition projecting :: "['c program => 'c set, 'a*'b => 'c, 
    15                   'a program, 'c program set, 'a program set] => bool" where
    16     "projecting C h F X' X ==
    17        \<forall>G. extend h F\<squnion>G \<in> X' --> F\<squnion>project h (C G) G \<in> X"
    18 
    19 definition extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
    20                  'c program set, 'a program set] => bool" where
    21     "extending C h F Y' Y ==
    22        \<forall>G. extend h F  ok G --> F\<squnion>project h (C G) G \<in> Y
    23               --> extend h F\<squnion>G \<in> Y'"
    24 
    25 definition subset_closed :: "'a set set => bool" where
    26     "subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U"  
    27 
    28 
    29 context Extend
    30 begin
    31 
    32 lemma project_extend_constrains_I:
    33      "F \<in> A co B ==> project h C (extend h F) \<in> A co B"
    34 apply (auto simp add: extend_act_def project_act_def constrains_def)
    35 done
    36 
    37 
    38 subsection{*Safety*}
    39 
    40 (*used below to prove Join_project_ensures*)
    41 lemma project_unless:
    42      "[| G \<in> stable C;  project h C G \<in> A unless B |]  
    43       ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
    44 apply (simp add: unless_def project_constrains)
    45 apply (blast dest: stable_constrains_Int intro: constrains_weaken)
    46 done
    47 
    48 (*Generalizes project_constrains to the program F\<squnion>project h C G
    49   useful with guarantees reasoning*)
    50 lemma Join_project_constrains:
    51      "(F\<squnion>project h C G \<in> A co B)  =   
    52         (extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) &   
    53          F \<in> A co B)"
    54 apply (simp (no_asm) add: project_constrains)
    55 apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] 
    56              dest: constrains_imp_subset)
    57 done
    58 
    59 (*The condition is required to prove the left-to-right direction
    60   could weaken it to G \<in> (C \<inter> extend_set h A) co C*)
    61 lemma Join_project_stable: 
    62      "extend h F\<squnion>G \<in> stable C  
    63       ==> (F\<squnion>project h C G \<in> stable A)  =   
    64           (extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) &   
    65            F \<in> stable A)"
    66 apply (unfold stable_def)
    67 apply (simp only: Join_project_constrains)
    68 apply (blast intro: constrains_weaken dest: constrains_Int)
    69 done
    70 
    71 (*For using project_guarantees in particular cases*)
    72 lemma project_constrains_I:
    73      "extend h F\<squnion>G \<in> extend_set h A co extend_set h B  
    74       ==> F\<squnion>project h C G \<in> A co B"
    75 apply (simp add: project_constrains extend_constrains)
    76 apply (blast intro: constrains_weaken dest: constrains_imp_subset)
    77 done
    78 
    79 lemma project_increasing_I: 
    80      "extend h F\<squnion>G \<in> increasing (func o f)  
    81       ==> F\<squnion>project h C G \<in> increasing func"
    82 apply (unfold increasing_def stable_def)
    83 apply (simp del: Join_constrains
    84             add: project_constrains_I extend_set_eq_Collect)
    85 done
    86 
    87 lemma Join_project_increasing:
    88      "(F\<squnion>project h UNIV G \<in> increasing func)  =   
    89       (extend h F\<squnion>G \<in> increasing (func o f))"
    90 apply (rule iffI)
    91 apply (erule_tac [2] project_increasing_I)
    92 apply (simp del: Join_stable
    93             add: increasing_def Join_project_stable)
    94 apply (auto simp add: extend_set_eq_Collect extend_stable [THEN iffD1])
    95 done
    96 
    97 (*The UNIV argument is essential*)
    98 lemma project_constrains_D:
    99      "F\<squnion>project h UNIV G \<in> A co B  
   100       ==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B"
   101 by (simp add: project_constrains extend_constrains)
   102 
   103 end
   104 
   105 
   106 subsection{*"projecting" and union/intersection (no converses)*}
   107 
   108 lemma projecting_Int: 
   109      "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
   110       ==> projecting C h F (XA' \<inter> XB') (XA \<inter> XB)"
   111 by (unfold projecting_def, blast)
   112 
   113 lemma projecting_Un: 
   114      "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
   115       ==> projecting C h F (XA' \<union> XB') (XA \<union> XB)"
   116 by (unfold projecting_def, blast)
   117 
   118 lemma projecting_INT: 
   119      "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]  
   120       ==> projecting C h F (\<Inter>i \<in> I. X' i) (\<Inter>i \<in> I. X i)"
   121 by (unfold projecting_def, blast)
   122 
   123 lemma projecting_UN: 
   124      "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]  
   125       ==> projecting C h F (\<Union>i \<in> I. X' i) (\<Union>i \<in> I. X i)"
   126 by (unfold projecting_def, blast)
   127 
   128 lemma projecting_weaken: 
   129      "[| projecting C h F X' X;  U'<=X';  X \<subseteq> U |] ==> projecting C h F U' U"
   130 by (unfold projecting_def, auto)
   131 
   132 lemma projecting_weaken_L: 
   133      "[| projecting C h F X' X;  U'<=X' |] ==> projecting C h F U' X"
   134 by (unfold projecting_def, auto)
   135 
   136 lemma extending_Int: 
   137      "[| extending C h F YA' YA;  extending C h F YB' YB |]  
   138       ==> extending C h F (YA' \<inter> YB') (YA \<inter> YB)"
   139 by (unfold extending_def, blast)
   140 
   141 lemma extending_Un: 
   142      "[| extending C h F YA' YA;  extending C h F YB' YB |]  
   143       ==> extending C h F (YA' \<union> YB') (YA \<union> YB)"
   144 by (unfold extending_def, blast)
   145 
   146 lemma extending_INT: 
   147      "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]  
   148       ==> extending C h F (\<Inter>i \<in> I. Y' i) (\<Inter>i \<in> I. Y i)"
   149 by (unfold extending_def, blast)
   150 
   151 lemma extending_UN: 
   152      "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]  
   153       ==> extending C h F (\<Union>i \<in> I. Y' i) (\<Union>i \<in> I. Y i)"
   154 by (unfold extending_def, blast)
   155 
   156 lemma extending_weaken: 
   157      "[| extending C h F Y' Y;  Y'<=V';  V \<subseteq> Y |] ==> extending C h F V' V"
   158 by (unfold extending_def, auto)
   159 
   160 lemma extending_weaken_L: 
   161      "[| extending C h F Y' Y;  Y'<=V' |] ==> extending C h F V' Y"
   162 by (unfold extending_def, auto)
   163 
   164 lemma projecting_UNIV: "projecting C h F X' UNIV"
   165 by (simp add: projecting_def)
   166 
   167 context Extend
   168 begin
   169 
   170 lemma projecting_constrains: 
   171      "projecting C h F (extend_set h A co extend_set h B) (A co B)"
   172 apply (unfold projecting_def)
   173 apply (blast intro: project_constrains_I)
   174 done
   175 
   176 lemma projecting_stable: 
   177      "projecting C h F (stable (extend_set h A)) (stable A)"
   178 apply (unfold stable_def)
   179 apply (rule projecting_constrains)
   180 done
   181 
   182 lemma projecting_increasing: 
   183      "projecting C h F (increasing (func o f)) (increasing func)"
   184 apply (unfold projecting_def)
   185 apply (blast intro: project_increasing_I)
   186 done
   187 
   188 lemma extending_UNIV: "extending C h F UNIV Y"
   189 apply (simp (no_asm) add: extending_def)
   190 done
   191 
   192 lemma extending_constrains: 
   193      "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)"
   194 apply (unfold extending_def)
   195 apply (blast intro: project_constrains_D)
   196 done
   197 
   198 lemma extending_stable: 
   199      "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)"
   200 apply (unfold stable_def)
   201 apply (rule extending_constrains)
   202 done
   203 
   204 lemma extending_increasing: 
   205      "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)"
   206 by (force simp only: extending_def Join_project_increasing)
   207 
   208 
   209 subsection{*Reachability and project*}
   210 
   211 (*In practice, C = reachable(...): the inclusion is equality*)
   212 lemma reachable_imp_reachable_project:
   213      "[| reachable (extend h F\<squnion>G) \<subseteq> C;   
   214          z \<in> reachable (extend h F\<squnion>G) |]  
   215       ==> f z \<in> reachable (F\<squnion>project h C G)"
   216 apply (erule reachable.induct)
   217 apply (force intro!: reachable.Init simp add: split_extended_all, auto)
   218  apply (rule_tac act = x in reachable.Acts)
   219  apply auto
   220  apply (erule extend_act_D)
   221 apply (rule_tac act1 = "Restrict C act"
   222        in project_act_I [THEN [3] reachable.Acts], auto) 
   223 done
   224 
   225 lemma project_Constrains_D: 
   226      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B   
   227       ==> extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)"
   228 apply (unfold Constrains_def)
   229 apply (simp del: Join_constrains
   230             add: Join_project_constrains, clarify)
   231 apply (erule constrains_weaken)
   232 apply (auto intro: reachable_imp_reachable_project)
   233 done
   234 
   235 lemma project_Stable_D: 
   236      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A   
   237       ==> extend h F\<squnion>G \<in> Stable (extend_set h A)"
   238 apply (unfold Stable_def)
   239 apply (simp (no_asm_simp) add: project_Constrains_D)
   240 done
   241 
   242 lemma project_Always_D: 
   243      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A   
   244       ==> extend h F\<squnion>G \<in> Always (extend_set h A)"
   245 apply (unfold Always_def)
   246 apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
   247 done
   248 
   249 lemma project_Increasing_D: 
   250      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func   
   251       ==> extend h F\<squnion>G \<in> Increasing (func o f)"
   252 apply (unfold Increasing_def, auto)
   253 apply (subst extend_set_eq_Collect [symmetric])
   254 apply (simp (no_asm_simp) add: project_Stable_D)
   255 done
   256 
   257 
   258 subsection{*Converse results for weak safety: benefits of the argument C *}
   259 
   260 (*In practice, C = reachable(...): the inclusion is equality*)
   261 lemma reachable_project_imp_reachable:
   262      "[| C \<subseteq> reachable(extend h F\<squnion>G);    
   263          x \<in> reachable (F\<squnion>project h C G) |]  
   264       ==> \<exists>y. h(x,y) \<in> reachable (extend h F\<squnion>G)"
   265 apply (erule reachable.induct)
   266 apply  (force intro: reachable.Init)
   267 apply (auto simp add: project_act_def)
   268 apply (force del: Id_in_Acts intro: reachable.Acts extend_act_D)+
   269 done
   270 
   271 lemma project_set_reachable_extend_eq:
   272      "project_set h (reachable (extend h F\<squnion>G)) =  
   273       reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)"
   274 by (auto dest: subset_refl [THEN reachable_imp_reachable_project] 
   275                subset_refl [THEN reachable_project_imp_reachable])
   276 
   277 (*UNUSED*)
   278 lemma reachable_extend_Join_subset:
   279      "reachable (extend h F\<squnion>G) \<subseteq> C   
   280       ==> reachable (extend h F\<squnion>G) \<subseteq>  
   281           extend_set h (reachable (F\<squnion>project h C G))"
   282 apply (auto dest: reachable_imp_reachable_project)
   283 done
   284 
   285 lemma project_Constrains_I: 
   286      "extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)   
   287       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B"
   288 apply (unfold Constrains_def)
   289 apply (simp del: Join_constrains
   290             add: Join_project_constrains extend_set_Int_distrib)
   291 apply (rule conjI)
   292  prefer 2 
   293  apply (force elim: constrains_weaken_L
   294               dest!: extend_constrains_project_set
   295                      subset_refl [THEN reachable_project_imp_reachable])
   296 apply (blast intro: constrains_weaken_L)
   297 done
   298 
   299 lemma project_Stable_I: 
   300      "extend h F\<squnion>G \<in> Stable (extend_set h A)   
   301       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A"
   302 apply (unfold Stable_def)
   303 apply (simp (no_asm_simp) add: project_Constrains_I)
   304 done
   305 
   306 lemma project_Always_I: 
   307      "extend h F\<squnion>G \<in> Always (extend_set h A)   
   308       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A"
   309 apply (unfold Always_def)
   310 apply (auto simp add: project_Stable_I)
   311 apply (unfold extend_set_def, blast)
   312 done
   313 
   314 lemma project_Increasing_I: 
   315     "extend h F\<squnion>G \<in> Increasing (func o f)   
   316      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func"
   317 apply (unfold Increasing_def, auto)
   318 apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
   319 done
   320 
   321 lemma project_Constrains:
   322      "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B)  =   
   323       (extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))"
   324 apply (blast intro: project_Constrains_I project_Constrains_D)
   325 done
   326 
   327 lemma project_Stable: 
   328      "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A)  =   
   329       (extend h F\<squnion>G \<in> Stable (extend_set h A))"
   330 apply (unfold Stable_def)
   331 apply (rule project_Constrains)
   332 done
   333 
   334 lemma project_Increasing: 
   335    "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func)  =  
   336     (extend h F\<squnion>G \<in> Increasing (func o f))"
   337 apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
   338 done
   339 
   340 subsection{*A lot of redundant theorems: all are proved to facilitate reasoning
   341     about guarantees.*}
   342 
   343 lemma projecting_Constrains: 
   344      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
   345                  (extend_set h A Co extend_set h B) (A Co B)"
   346 
   347 apply (unfold projecting_def)
   348 apply (blast intro: project_Constrains_I)
   349 done
   350 
   351 lemma projecting_Stable: 
   352      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
   353                  (Stable (extend_set h A)) (Stable A)"
   354 apply (unfold Stable_def)
   355 apply (rule projecting_Constrains)
   356 done
   357 
   358 lemma projecting_Always: 
   359      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
   360                  (Always (extend_set h A)) (Always A)"
   361 apply (unfold projecting_def)
   362 apply (blast intro: project_Always_I)
   363 done
   364 
   365 lemma projecting_Increasing: 
   366      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
   367                  (Increasing (func o f)) (Increasing func)"
   368 apply (unfold projecting_def)
   369 apply (blast intro: project_Increasing_I)
   370 done
   371 
   372 lemma extending_Constrains: 
   373      "extending (%G. reachable (extend h F\<squnion>G)) h F  
   374                   (extend_set h A Co extend_set h B) (A Co B)"
   375 apply (unfold extending_def)
   376 apply (blast intro: project_Constrains_D)
   377 done
   378 
   379 lemma extending_Stable: 
   380      "extending (%G. reachable (extend h F\<squnion>G)) h F  
   381                   (Stable (extend_set h A)) (Stable A)"
   382 apply (unfold extending_def)
   383 apply (blast intro: project_Stable_D)
   384 done
   385 
   386 lemma extending_Always: 
   387      "extending (%G. reachable (extend h F\<squnion>G)) h F  
   388                   (Always (extend_set h A)) (Always A)"
   389 apply (unfold extending_def)
   390 apply (blast intro: project_Always_D)
   391 done
   392 
   393 lemma extending_Increasing: 
   394      "extending (%G. reachable (extend h F\<squnion>G)) h F  
   395                   (Increasing (func o f)) (Increasing func)"
   396 apply (unfold extending_def)
   397 apply (blast intro: project_Increasing_D)
   398 done
   399 
   400 
   401 subsection{*leadsETo in the precondition (??)*}
   402 
   403 subsubsection{*transient*}
   404 
   405 lemma transient_extend_set_imp_project_transient: 
   406      "[| G \<in> transient (C \<inter> extend_set h A);  G \<in> stable C |]   
   407       ==> project h C G \<in> transient (project_set h C \<inter> A)"
   408 apply (auto simp add: transient_def Domain_project_act)
   409 apply (subgoal_tac "act `` (C \<inter> extend_set h A) \<subseteq> - extend_set h A")
   410  prefer 2
   411  apply (simp add: stable_def constrains_def, blast) 
   412 (*back to main goal*)
   413 apply (erule_tac V = "AA \<subseteq> -C \<union> BB" for AA BB in thin_rl)
   414 apply (drule bspec, assumption) 
   415 apply (simp add: extend_set_def project_act_def, blast)
   416 done
   417 
   418 (*converse might hold too?*)
   419 lemma project_extend_transient_D: 
   420      "project h C (extend h F) \<in> transient (project_set h C \<inter> D)  
   421       ==> F \<in> transient (project_set h C \<inter> D)"
   422 apply (simp add: transient_def Domain_project_act, safe)
   423 apply blast+
   424 done
   425 
   426 
   427 subsubsection{*ensures -- a primitive combining progress with safety*}
   428 
   429 (*Used to prove project_leadsETo_I*)
   430 lemma ensures_extend_set_imp_project_ensures:
   431      "[| extend h F \<in> stable C;  G \<in> stable C;   
   432          extend h F\<squnion>G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]   
   433       ==> F\<squnion>project h C G   
   434             \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
   435 apply (simp add: ensures_def project_constrains extend_transient,
   436        clarify)
   437 apply (intro conjI) 
   438 (*first subgoal*)
   439 apply (blast intro: extend_stable_project_set 
   440                   [THEN stableD, THEN constrains_Int, THEN constrains_weaken] 
   441              dest!: extend_constrains_project_set equalityD1)
   442 (*2nd subgoal*)
   443 apply (erule stableD [THEN constrains_Int, THEN constrains_weaken])
   444     apply assumption
   445    apply (simp (no_asm_use) add: extend_set_def)
   446    apply blast
   447  apply (simp add: extend_set_Int_distrib extend_set_Un_distrib)
   448  apply (blast intro!: extend_set_project_set [THEN subsetD], blast)
   449 (*The transient part*)
   450 apply auto
   451  prefer 2
   452  apply (force dest!: equalityD1
   453               intro: transient_extend_set_imp_project_transient
   454                          [THEN transient_strengthen])
   455 apply (simp (no_asm_use) add: Int_Diff)
   456 apply (force dest!: equalityD1 
   457              intro: transient_extend_set_imp_project_transient 
   458                [THEN project_extend_transient_D, THEN transient_strengthen])
   459 done
   460 
   461 text{*Transferring a transient property upwards*}
   462 lemma project_transient_extend_set:
   463      "project h C G \<in> transient (project_set h C \<inter> A - B)
   464       ==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)"
   465 apply (simp add: transient_def project_set_def extend_set_def project_act_def)
   466 apply (elim disjE bexE)
   467  apply (rule_tac x=Id in bexI)  
   468   apply (blast intro!: rev_bexI )+
   469 done
   470 
   471 lemma project_unless2:
   472      "[| G \<in> stable C;  project h C G \<in> (project_set h C \<inter> A) unless B |]  
   473       ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
   474 by (auto dest: stable_constrains_Int intro: constrains_weaken
   475          simp add: unless_def project_constrains Diff_eq Int_assoc 
   476                    Int_extend_set_lemma)
   477 
   478 
   479 lemma extend_unless:
   480    "[|extend h F \<in> stable C; F \<in> A unless B|]
   481     ==> extend h F \<in> C \<inter> extend_set h A unless extend_set h B"
   482 apply (simp add: unless_def stable_def)
   483 apply (drule constrains_Int) 
   484 apply (erule extend_constrains [THEN iffD2]) 
   485 apply (erule constrains_weaken, blast) 
   486 apply blast 
   487 done
   488 
   489 (*Used to prove project_leadsETo_D*)
   490 lemma Join_project_ensures:
   491      "[| extend h F\<squnion>G \<in> stable C;   
   492          F\<squnion>project h C G \<in> A ensures B |]  
   493       ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
   494 apply (auto simp add: ensures_eq extend_unless project_unless)
   495 apply (blast intro:  extend_transient [THEN iffD2] transient_strengthen)  
   496 apply (blast intro: project_transient_extend_set transient_strengthen)  
   497 done
   498 
   499 text{*Lemma useful for both STRONG and WEAK progress, but the transient
   500     condition's very strong*}
   501 
   502 (*The strange induction formula allows induction over the leadsTo
   503   assumption's non-atomic precondition*)
   504 lemma PLD_lemma:
   505      "[| extend h F\<squnion>G \<in> stable C;   
   506          F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
   507       ==> extend h F\<squnion>G \<in>  
   508           C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
   509 apply (erule leadsTo_induct)
   510   apply (blast intro: Join_project_ensures)
   511  apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans)
   512 apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union)
   513 done
   514 
   515 lemma project_leadsTo_D_lemma:
   516      "[| extend h F\<squnion>G \<in> stable C;   
   517          F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
   518       ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
   519 apply (rule PLD_lemma [THEN leadsTo_weaken])
   520 apply (auto simp add: split_extended_all)
   521 done
   522 
   523 lemma Join_project_LeadsTo:
   524      "[| C = (reachable (extend h F\<squnion>G));  
   525          F\<squnion>project h C G \<in> A LeadsTo B |]  
   526       ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
   527 by (simp del: Join_stable    add: LeadsTo_def project_leadsTo_D_lemma
   528                                   project_set_reachable_extend_eq)
   529 
   530 
   531 subsection{*Towards the theorem @{text project_Ensures_D}*}
   532 
   533 lemma project_ensures_D_lemma:
   534      "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));   
   535          F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B;   
   536          extend h F\<squnion>G \<in> stable C |]  
   537       ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
   538 (*unless*)
   539 apply (auto intro!: project_unless2 [unfolded unless_def] 
   540             intro: project_extend_constrains_I 
   541             simp add: ensures_def)
   542 (*transient*)
   543 (*A G-action cannot occur*)
   544  prefer 2
   545  apply (blast intro: project_transient_extend_set) 
   546 (*An F-action*)
   547 apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen]
   548              simp add: split_extended_all)
   549 done
   550 
   551 lemma project_ensures_D:
   552      "[| F\<squnion>project h UNIV G \<in> A ensures B;   
   553          G \<in> stable (extend_set h A - extend_set h B) |]  
   554       ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
   555 apply (rule project_ensures_D_lemma [of _ UNIV, elim_format], auto)
   556 done
   557 
   558 lemma project_Ensures_D: 
   559      "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Ensures B;   
   560          G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A -  
   561                      extend_set h B) |]  
   562       ==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
   563 apply (unfold Ensures_def)
   564 apply (rule project_ensures_D_lemma [elim_format])
   565 apply (auto simp add: project_set_reachable_extend_eq [symmetric])
   566 done
   567 
   568 
   569 subsection{*Guarantees*}
   570 
   571 lemma project_act_Restrict_subset_project_act:
   572      "project_act h (Restrict C act) \<subseteq> project_act h act"
   573 apply (auto simp add: project_act_def)
   574 done
   575                                            
   576                                                            
   577 lemma subset_closed_ok_extend_imp_ok_project:
   578      "[| extend h F ok G; subset_closed (AllowedActs F) |]  
   579       ==> F ok project h C G"
   580 apply (auto simp add: ok_def)
   581 apply (rename_tac act) 
   582 apply (drule subsetD, blast)
   583 apply (rule_tac x = "Restrict C  (extend_act h act)" in rev_image_eqI)
   584 apply simp +
   585 apply (cut_tac project_act_Restrict_subset_project_act)
   586 apply (auto simp add: subset_closed_def)
   587 done
   588 
   589 
   590 (*Weak precondition and postcondition
   591   Not clear that it has a converse [or that we want one!]*)
   592 
   593 (*The raw version; 3rd premise could be weakened by adding the
   594   precondition extend h F\<squnion>G \<in> X' *)
   595 lemma project_guarantees_raw:
   596  assumes xguary:  "F \<in> X guarantees Y"
   597      and closed:  "subset_closed (AllowedActs F)"
   598      and project: "!!G. extend h F\<squnion>G \<in> X' 
   599                         ==> F\<squnion>project h (C G) G \<in> X"
   600      and extend:  "!!G. [| F\<squnion>project h (C G) G \<in> Y |]  
   601                         ==> extend h F\<squnion>G \<in> Y'"
   602  shows "extend h F \<in> X' guarantees Y'"
   603 apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
   604 apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
   605 apply (erule project)
   606 done
   607 
   608 lemma project_guarantees:
   609      "[| F \<in> X guarantees Y;  subset_closed (AllowedActs F);  
   610          projecting C h F X' X;  extending C h F Y' Y |]  
   611       ==> extend h F \<in> X' guarantees Y'"
   612 apply (rule guaranteesI)
   613 apply (auto simp add: guaranteesD projecting_def extending_def
   614                       subset_closed_ok_extend_imp_ok_project)
   615 done
   616 
   617 
   618 (*It seems that neither "guarantees" law can be proved from the other.*)
   619 
   620 
   621 subsection{*guarantees corollaries*}
   622 
   623 subsubsection{*Some could be deleted: the required versions are easy to prove*}
   624 
   625 lemma extend_guar_increasing:
   626      "[| F \<in> UNIV guarantees increasing func;   
   627          subset_closed (AllowedActs F) |]  
   628       ==> extend h F \<in> X' guarantees increasing (func o f)"
   629 apply (erule project_guarantees)
   630 apply (rule_tac [3] extending_increasing)
   631 apply (rule_tac [2] projecting_UNIV, auto)
   632 done
   633 
   634 lemma extend_guar_Increasing:
   635      "[| F \<in> UNIV guarantees Increasing func;   
   636          subset_closed (AllowedActs F) |]  
   637       ==> extend h F \<in> X' guarantees Increasing (func o f)"
   638 apply (erule project_guarantees)
   639 apply (rule_tac [3] extending_Increasing)
   640 apply (rule_tac [2] projecting_UNIV, auto)
   641 done
   642 
   643 lemma extend_guar_Always:
   644      "[| F \<in> Always A guarantees Always B;   
   645          subset_closed (AllowedActs F) |]  
   646       ==> extend h F                    
   647             \<in> Always(extend_set h A) guarantees Always(extend_set h B)"
   648 apply (erule project_guarantees)
   649 apply (rule_tac [3] extending_Always)
   650 apply (rule_tac [2] projecting_Always, auto)
   651 done
   652 
   653 
   654 subsubsection{*Guarantees with a leadsTo postcondition*}
   655 
   656 lemma project_leadsTo_D:
   657      "F\<squnion>project h UNIV G \<in> A leadsTo B
   658       ==> extend h F\<squnion>G \<in> (extend_set h A) leadsTo (extend_set h B)"
   659 apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto)
   660 done
   661 
   662 lemma project_LeadsTo_D:
   663      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A LeadsTo B   
   664        ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
   665 apply (rule refl [THEN Join_project_LeadsTo], auto)
   666 done
   667 
   668 lemma extending_leadsTo: 
   669      "extending (%G. UNIV) h F  
   670                 (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
   671 apply (unfold extending_def)
   672 apply (blast intro: project_leadsTo_D)
   673 done
   674 
   675 lemma extending_LeadsTo: 
   676      "extending (%G. reachable (extend h F\<squnion>G)) h F  
   677                 (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
   678 apply (unfold extending_def)
   679 apply (blast intro: project_LeadsTo_D)
   680 done
   681 
   682 end
   683 
   684 end