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