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