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