src/HOL/UNITY/Project.thy
author paulson
Wed Jan 29 11:02:08 2003 +0100 (2003-01-29)
changeset 13790 8d7e9fce8c50
parent 10064 1a77667b21ef
child 13798 4c1a53627500
permissions -rw-r--r--
converting UNITY to new-style theories
     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 theory Project = Extend:
    12 
    13 constdefs
    14   projecting :: "['c program => 'c set, 'a*'b => 'c, 
    15 		  'a program, 'c program set, 'a program set] => bool"
    16     "projecting C h F X' X ==
    17        ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
    18 
    19   extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
    20 		 'c program set, 'a program set] => bool"
    21     "extending C h F Y' Y ==
    22        ALL G. extend h F  ok G --> F Join project h (C G) G : Y
    23 	      --> extend h F Join G : Y'"
    24 
    25   subset_closed :: "'a set set => bool"
    26     "subset_closed U == ALL A: U. Pow A <= U"  
    27 
    28 
    29 lemma (in Extend) project_extend_constrains_I:
    30      "F : A co B ==> project h C (extend h F) : A co B"
    31 apply (auto simp add: extend_act_def project_act_def constrains_def)
    32 done
    33 
    34 
    35 (** Safety **)
    36 
    37 (*used below to prove Join_project_ensures*)
    38 lemma (in Extend) project_unless [rule_format (no_asm)]:
    39      "[| G : stable C;  project h C G : A unless B |]  
    40       ==> G : (C Int 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 Join project h C G
    46   useful with guarantees reasoning*)
    47 lemma (in Extend) Join_project_constrains:
    48      "(F Join project h C G : A co B)  =   
    49         (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &   
    50          F : 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 : (C Int extend_set h A) co C*)
    58 lemma (in Extend) Join_project_stable: 
    59      "extend h F Join G : stable C  
    60       ==> (F Join project h C G : stable A)  =   
    61           (extend h F Join G : stable (C Int extend_set h A) &   
    62            F : 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 Join G : extend_set h A co extend_set h B  
    71       ==> F Join project h C G : 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 Join G : increasing (func o f)  
    78       ==> F Join project h C G : 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 Join project h UNIV G : increasing func)  =   
    86       (extend h F Join G : 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 Join project h UNIV G : A co B  
    97       ==> extend h F Join G : extend_set h A co extend_set h B"
    98 by (simp add: project_constrains extend_constrains)
    99 
   100 
   101 (*** "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' Int XB') (XA Int 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' Un XB') (XA Un XB)"
   111 by (unfold projecting_def, blast)
   112 
   113 lemma projecting_INT: 
   114      "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]  
   115       ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)"
   116 by (unfold projecting_def, blast)
   117 
   118 lemma projecting_UN: 
   119      "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]  
   120       ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)"
   121 by (unfold projecting_def, blast)
   122 
   123 lemma projecting_weaken: 
   124      "[| projecting C h F X' X;  U'<=X';  X<=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' Int YB') (YA Int 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' Un YB') (YA Un YB)"
   139 by (unfold extending_def, blast)
   140 
   141 lemma extending_INT: 
   142      "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]  
   143       ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)"
   144 by (unfold extending_def, blast)
   145 
   146 lemma extending_UN: 
   147      "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]  
   148       ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)"
   149 by (unfold extending_def, blast)
   150 
   151 lemma extending_weaken: 
   152      "[| extending C h F Y' Y;  Y'<=V';  V<=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 (** 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 Join G) <= C;   
   206          z : reachable (extend h F Join G) |]  
   207       ==> f z : reachable (F Join 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 Join project h (reachable (extend h F Join G)) G : A Co B   
   219       ==> extend h F Join G : (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 Join project h (reachable (extend h F Join G)) G : Stable A   
   229       ==> extend h F Join G : 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 Join project h (reachable (extend h F Join G)) G : Always A   
   236       ==> extend h F Join G : 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 Join project h (reachable (extend h F Join G)) G : Increasing func   
   243       ==> extend h F Join G : 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 (** 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 <= reachable(extend h F Join G);    
   255          x : reachable (F Join project h C G) |]  
   256       ==> EX y. h(x,y) : reachable (extend h F Join 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 Join G)) =  
   265       reachable (F Join project h (reachable (extend h F Join 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 Join G) <= C   
   272       ==> reachable (extend h F Join G) <=  
   273           extend_set h (reachable (F Join 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 Join G : (extend_set h A) Co (extend_set h B)   
   279       ==> F Join project h (reachable (extend h F Join G)) G : 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 Join G : Stable (extend_set h A)   
   293       ==> F Join project h (reachable (extend h F Join G)) G : 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 Join G : Always (extend_set h A)   
   300       ==> F Join project h (reachable (extend h F Join G)) G : 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 Join G : Increasing (func o f)   
   308      ==> F Join project h (reachable (extend h F Join G)) G : 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 Join project h (reachable (extend h F Join G)) G : A Co B)  =   
   315       (extend h F Join G : (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 Join project h (reachable (extend h F Join G)) G : Stable A)  =   
   321       (extend h F Join G : 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 Join project h (reachable (extend h F Join G)) G : Increasing func)  =  
   328     (extend h F Join G : Increasing (func o f))"
   329 apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
   330 done
   331 
   332 (** 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 Join 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 Join 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 Join 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 Join 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 Join 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 Join 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 Join 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 Join 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 (*** leadsETo in the precondition (??) ***)
   394 
   395 (** transient **)
   396 
   397 lemma (in Extend) transient_extend_set_imp_project_transient: 
   398      "[| G : transient (C Int extend_set h A);  G : stable C |]   
   399       ==> project h C G : transient (project_set h C Int A)"
   400 
   401 apply (unfold transient_def)
   402 apply (auto simp add: Domain_project_act)
   403 apply (subgoal_tac "act `` (C Int extend_set h A) <= - 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 <= -C Un ?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) : transient (project_set h C Int D)  
   415       ==> F : transient (project_set h C Int D)"
   416 apply (unfold transient_def)
   417 apply (auto simp add: Domain_project_act)
   418 apply (rule bexI)
   419 prefer 2 apply assumption
   420 apply auto
   421 apply (unfold extend_act_def, blast)
   422 done
   423 
   424 
   425 (** ensures -- a primitive combining progress with safety **)
   426 
   427 (*Used to prove project_leadsETo_I*)
   428 lemma (in Extend) ensures_extend_set_imp_project_ensures:
   429      "[| extend h F : stable C;  G : stable C;   
   430          extend h F Join G : A ensures B;  A-B = C Int extend_set h D |]   
   431       ==> F Join project h C G   
   432             : (project_set h C Int project_set h A) ensures (project_set h B)"
   433 apply (simp add: ensures_def project_constrains Join_transient extend_transient, clarify)
   434 apply (intro conjI) 
   435 (*first subgoal*)
   436 apply (blast intro: extend_stable_project_set 
   437                   [THEN stableD, THEN constrains_Int, THEN constrains_weaken] 
   438              dest!: extend_constrains_project_set equalityD1)
   439 (*2nd subgoal*)
   440 apply (erule stableD [THEN constrains_Int, THEN constrains_weaken])
   441     apply assumption
   442    apply (simp (no_asm_use) add: extend_set_def)
   443    apply blast
   444  apply (simp add: extend_set_Int_distrib extend_set_Un_distrib)
   445  apply (blast intro!: extend_set_project_set [THEN subsetD], blast)
   446 (*The transient part*)
   447 apply auto
   448  prefer 2
   449  apply (force dest!: equalityD1
   450               intro: transient_extend_set_imp_project_transient
   451                          [THEN transient_strengthen])
   452 apply (simp (no_asm_use) add: Int_Diff)
   453 apply (force dest!: equalityD1 
   454              intro: transient_extend_set_imp_project_transient 
   455                [THEN project_extend_transient_D, THEN transient_strengthen])
   456 done
   457 
   458 (*Used to prove project_leadsETo_D*)
   459 lemma (in Extend) Join_project_ensures [rule_format (no_asm)]:
   460      "[| project h C G ~: transient (A-B) | A<=B;   
   461          extend h F Join G : stable C;   
   462          F Join project h C G : A ensures B |]  
   463       ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
   464 apply (erule disjE)
   465 prefer 2 apply (blast intro: subset_imp_ensures)
   466 apply (auto dest: extend_transient [THEN iffD2]
   467             intro: transient_strengthen project_set_I
   468                    project_unless [THEN unlessD] unlessI 
   469                    project_extend_constrains_I 
   470             simp add: ensures_def Join_transient)
   471 done
   472 
   473 (** Lemma useful for both STRONG and WEAK progress, but the transient
   474     condition's very strong **)
   475 
   476 (*The strange induction formula allows induction over the leadsTo
   477   assumption's non-atomic precondition*)
   478 lemma (in Extend) PLD_lemma:
   479      "[| ALL D. project h C G : transient D --> D={};   
   480          extend h F Join G : stable C;   
   481          F Join project h C G : (project_set h C Int A) leadsTo B |]  
   482       ==> extend h F Join G :  
   483           C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)"
   484 apply (erule leadsTo_induct)
   485   apply (blast intro: leadsTo_Basis Join_project_ensures)
   486  apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans)
   487 apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union)
   488 done
   489 
   490 lemma (in Extend) project_leadsTo_D_lemma:
   491      "[| ALL D. project h C G : transient D --> D={};   
   492          extend h F Join G : stable C;   
   493          F Join project h C G : (project_set h C Int A) leadsTo B |]  
   494       ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"
   495 apply (rule PLD_lemma [THEN leadsTo_weaken])
   496 apply (auto simp add: split_extended_all)
   497 done
   498 
   499 lemma (in Extend) Join_project_LeadsTo:
   500      "[| C = (reachable (extend h F Join G));  
   501          ALL D. project h C G : transient D --> D={};   
   502          F Join project h C G : A LeadsTo B |]  
   503       ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
   504 by (simp del: Join_stable    add: LeadsTo_def project_leadsTo_D_lemma
   505                                   project_set_reachable_extend_eq)
   506 
   507 
   508 (*** Towards project_Ensures_D ***)
   509 
   510 
   511 lemma (in Extend) act_subset_imp_project_act_subset: 
   512      "act `` (C Int extend_set h A) <= B  
   513       ==> project_act h (Restrict C act) `` (project_set h C Int A)  
   514           <= project_set h B"
   515 apply (unfold project_set_def extend_set_def project_act_def, blast)
   516 done
   517 
   518 (*This trivial proof is the complementation part of transferring a transient
   519   property upwards.  The hard part would be to 
   520   show that G's action has a big enough domain.*)
   521 lemma (in Extend) 
   522      "[| act: Acts G;        
   523          (project_act h (Restrict C act))``  
   524               (project_set h C Int A - B) <= -(project_set h C Int A - B) |]  
   525       ==> act``(C Int extend_set h A - extend_set h B)  
   526             <= -(C Int extend_set h A - extend_set h B)"
   527 by (auto simp add: project_set_def extend_set_def project_act_def)
   528 
   529 lemma (in Extend) stable_project_transient:
   530      "[| G : stable ((C Int extend_set h A) - (extend_set h B));   
   531          project h C G : transient (project_set h C Int A - B) |]   
   532       ==> (C Int extend_set h A) - extend_set h B = {}"
   533 apply (auto simp add: transient_def subset_Compl_self_eq Domain_project_act split_extended_all, blast)
   534 apply (auto simp add: stable_def constrains_def)
   535 apply (drule bspec, assumption) 
   536 apply (auto simp add: Int_Diff extend_set_Diff_distrib [symmetric])
   537 apply (drule act_subset_imp_project_act_subset)
   538 apply (subgoal_tac "project_act h (Restrict C act) `` (project_set h C Int (A - B)) = {}")
   539 apply (erule_tac V = "?r``?A <= ?B" in thin_rl)+
   540 apply (unfold project_set_def extend_set_def project_act_def)
   541 prefer 2 apply blast
   542 apply (rule ccontr)
   543 apply (drule subsetD, blast)
   544 apply (force simp add: split_extended_all)
   545 done
   546 
   547 lemma (in Extend) project_unless2 [rule_format (no_asm)]:
   548      "[| G : stable C;  project h C G : (project_set h C Int A) unless B |]  
   549       ==> G : (C Int extend_set h A) unless (extend_set h B)"
   550 by (auto dest: stable_constrains_Int intro: constrains_weaken
   551          simp add: unless_def project_constrains Diff_eq Int_assoc 
   552                    Int_extend_set_lemma)
   553 
   554 lemma (in Extend) project_ensures_D_lemma:
   555      "[| G : stable ((C Int extend_set h A) - (extend_set h B));   
   556          F Join project h C G : (project_set h C Int A) ensures B;   
   557          extend h F Join G : stable C |]  
   558       ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
   559 (*unless*)
   560 apply (auto intro!: project_unless2 [unfolded unless_def] 
   561             intro: project_extend_constrains_I 
   562             simp add: ensures_def)
   563 (*transient*)
   564 (*A G-action cannot occur*)
   565  prefer 2
   566  apply (force dest: stable_project_transient 
   567               simp del: Diff_eq_empty_iff
   568               simp add: Diff_eq_empty_iff [symmetric])
   569 (*An F-action*)
   570 apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen]
   571              simp add: split_extended_all)
   572 done
   573 
   574 lemma (in Extend) project_ensures_D:
   575      "[| F Join project h UNIV G : A ensures B;   
   576          G : stable (extend_set h A - extend_set h B) |]  
   577       ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)"
   578 apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
   579 done
   580 
   581 lemma (in Extend) project_Ensures_D: 
   582      "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B;   
   583          G : stable (reachable (extend h F Join G) Int extend_set h A -  
   584                      extend_set h B) |]  
   585       ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)"
   586 apply (unfold Ensures_def)
   587 apply (rule project_ensures_D_lemma [THEN revcut_rl])
   588 apply (auto simp add: project_set_reachable_extend_eq [symmetric])
   589 done
   590 
   591 
   592 (*** Guarantees ***)
   593 
   594 lemma (in Extend) project_act_Restrict_subset_project_act:
   595      "project_act h (Restrict C act) <= project_act h act"
   596 apply (auto simp add: project_act_def)
   597 done
   598 					   
   599 							   
   600 lemma (in Extend) subset_closed_ok_extend_imp_ok_project:
   601      "[| extend h F ok G; subset_closed (AllowedActs F) |]  
   602       ==> F ok project h C G"
   603 apply (auto simp add: ok_def)
   604 apply (rename_tac act) 
   605 apply (drule subsetD, blast)
   606 apply (rule_tac x = "Restrict C  (extend_act h act)" in rev_image_eqI)
   607 apply simp +
   608 apply (cut_tac project_act_Restrict_subset_project_act)
   609 apply (auto simp add: subset_closed_def)
   610 done
   611 
   612 
   613 (*Weak precondition and postcondition
   614   Not clear that it has a converse [or that we want one!]*)
   615 
   616 (*The raw version; 3rd premise could be weakened by adding the
   617   precondition extend h F Join G : X' *)
   618 lemma (in Extend) project_guarantees_raw:
   619  assumes xguary:  "F : X guarantees Y"
   620      and closed:  "subset_closed (AllowedActs F)"
   621      and project: "!!G. extend h F Join G : X' 
   622                         ==> F Join project h (C G) G : X"
   623      and extend:  "!!G. [| F Join project h (C G) G : Y |]  
   624                         ==> extend h F Join G : Y'"
   625  shows "extend h F : X' guarantees Y'"
   626 apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
   627 apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
   628 apply (erule project)
   629 done
   630 
   631 lemma (in Extend) project_guarantees:
   632      "[| F : X guarantees Y;  subset_closed (AllowedActs F);  
   633          projecting C h F X' X;  extending C h F Y' Y |]  
   634       ==> extend h F : X' guarantees Y'"
   635 apply (rule guaranteesI)
   636 apply (auto simp add: guaranteesD projecting_def extending_def
   637                       subset_closed_ok_extend_imp_ok_project)
   638 done
   639 
   640 
   641 (*It seems that neither "guarantees" law can be proved from the other.*)
   642 
   643 
   644 (*** guarantees corollaries ***)
   645 
   646 (** Some could be deleted: the required versions are easy to prove **)
   647 
   648 lemma (in Extend) extend_guar_increasing:
   649      "[| F : UNIV guarantees increasing func;   
   650          subset_closed (AllowedActs F) |]  
   651       ==> extend h F : X' guarantees increasing (func o f)"
   652 apply (erule project_guarantees)
   653 apply (rule_tac [3] extending_increasing)
   654 apply (rule_tac [2] projecting_UNIV, auto)
   655 done
   656 
   657 lemma (in Extend) extend_guar_Increasing:
   658      "[| F : UNIV guarantees Increasing func;   
   659          subset_closed (AllowedActs F) |]  
   660       ==> extend h F : X' guarantees Increasing (func o f)"
   661 apply (erule project_guarantees)
   662 apply (rule_tac [3] extending_Increasing)
   663 apply (rule_tac [2] projecting_UNIV, auto)
   664 done
   665 
   666 lemma (in Extend) extend_guar_Always:
   667      "[| F : Always A guarantees Always B;   
   668          subset_closed (AllowedActs F) |]  
   669       ==> extend h F                    
   670             : Always(extend_set h A) guarantees Always(extend_set h B)"
   671 apply (erule project_guarantees)
   672 apply (rule_tac [3] extending_Always)
   673 apply (rule_tac [2] projecting_Always, auto)
   674 done
   675 
   676 lemma (in Extend) preserves_project_transient_empty:
   677      "[| G : preserves f;  project h C G : transient D |] ==> D={}"
   678 apply (rule stable_transient_empty)
   679  prefer 2 apply assumption
   680 apply (blast intro: project_preserves_id_I 
   681                     preserves_id_subset_stable [THEN subsetD])
   682 done
   683 
   684 
   685 (** Guarantees with a leadsTo postcondition 
   686     THESE ARE ALL TOO WEAK because G can't affect F's variables at all**)
   687 
   688 lemma (in Extend) project_leadsTo_D:
   689      "[| F Join project h UNIV G : A leadsTo B;     
   690          G : preserves f |]   
   691       ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"
   692 apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken])
   693 apply (auto dest: preserves_project_transient_empty)
   694 done
   695 
   696 lemma (in Extend) project_LeadsTo_D:
   697      "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B;
   698          G : preserves f |]   
   699        ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
   700 apply (rule refl [THEN Join_project_LeadsTo])
   701 apply (auto dest: preserves_project_transient_empty)
   702 done
   703 
   704 lemma (in Extend) extending_leadsTo: 
   705      "(ALL G. extend h F ok G --> G : preserves f)  
   706       ==> extending (%G. UNIV) h F  
   707                   (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
   708 apply (unfold extending_def)
   709 apply (blast intro: project_leadsTo_D)
   710 done
   711 
   712 lemma (in Extend) extending_LeadsTo: 
   713      "(ALL G. extend h F ok G --> G : preserves f)  
   714       ==> extending (%G. reachable (extend h F Join G)) h F  
   715                   (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
   716 apply (unfold extending_def)
   717 apply (blast intro: project_LeadsTo_D)
   718 done
   719 
   720 ML
   721 {*
   722 val projecting_Int = thm "projecting_Int";
   723 val projecting_Un = thm "projecting_Un";
   724 val projecting_INT = thm "projecting_INT";
   725 val projecting_UN = thm "projecting_UN";
   726 val projecting_weaken = thm "projecting_weaken";
   727 val projecting_weaken_L = thm "projecting_weaken_L";
   728 val extending_Int = thm "extending_Int";
   729 val extending_Un = thm "extending_Un";
   730 val extending_INT = thm "extending_INT";
   731 val extending_UN = thm "extending_UN";
   732 val extending_weaken = thm "extending_weaken";
   733 val extending_weaken_L = thm "extending_weaken_L";
   734 val projecting_UNIV = thm "projecting_UNIV";
   735 *}
   736 
   737 end