src/HOL/UNITY/Project.thy
 author paulson Sat Feb 08 16:05:33 2003 +0100 (2003-02-08) changeset 13812 91713a1915ee parent 13798 4c1a53627500 child 13819 78f5885b76a9 permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
```     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 = Extend:
```
```    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 Join G \<in> X' --> F Join 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 Join project h (C G) G \<in> Y
```
```    25 	      --> extend h F Join 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 Join project h C G
```
```    48   useful with guarantees reasoning*)
```
```    49 lemma (in Extend) Join_project_constrains:
```
```    50      "(F Join project h C G \<in> A co B)  =
```
```    51         (extend h F Join 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 Join G \<in> stable C
```
```    62       ==> (F Join project h C G \<in> stable A)  =
```
```    63           (extend h F Join 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 Join G \<in> extend_set h A co extend_set h B
```
```    73       ==> F Join 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 Join G \<in> increasing (func o f)
```
```    80       ==> F Join 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 Join project h UNIV G \<in> increasing func)  =
```
```    88       (extend h F Join 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 Join project h UNIV G \<in> A co B
```
```    99       ==> extend h F Join 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 Join G) \<subseteq> C;
```
```   208          z \<in> reachable (extend h F Join G) |]
```
```   209       ==> f z \<in> reachable (F Join 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 Join project h (reachable (extend h F Join G)) G \<in> A Co B
```
```   221       ==> extend h F Join 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 Join project h (reachable (extend h F Join G)) G \<in> Stable A
```
```   231       ==> extend h F Join 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 Join project h (reachable (extend h F Join G)) G \<in> Always A
```
```   238       ==> extend h F Join 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 Join project h (reachable (extend h F Join G)) G \<in> Increasing func
```
```   245       ==> extend h F Join 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 Join G);
```
```   257          x \<in> reachable (F Join project h C G) |]
```
```   258       ==> \<exists>y. h(x,y) \<in> reachable (extend h F Join 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 Join G)) =
```
```   267       reachable (F Join project h (reachable (extend h F Join 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 Join G) \<subseteq> C
```
```   274       ==> reachable (extend h F Join G) \<subseteq>
```
```   275           extend_set h (reachable (F Join 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 Join G \<in> (extend_set h A) Co (extend_set h B)
```
```   281       ==> F Join project h (reachable (extend h F Join 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 Join G \<in> Stable (extend_set h A)
```
```   295       ==> F Join project h (reachable (extend h F Join 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 Join G \<in> Always (extend_set h A)
```
```   302       ==> F Join project h (reachable (extend h F Join 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 Join G \<in> Increasing (func o f)
```
```   310      ==> F Join project h (reachable (extend h F Join 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 Join project h (reachable (extend h F Join G)) G \<in> A Co B)  =
```
```   317       (extend h F Join 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 Join project h (reachable (extend h F Join G)) G \<in> Stable A)  =
```
```   323       (extend h F Join 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 Join project h (reachable (extend h F Join G)) G \<in> Increasing func)  =
```
```   330     (extend h F Join 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 Join 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 Join 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 Join 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 Join 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 Join 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 Join 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 Join 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 Join 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 Join G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]
```
```   427       ==> F Join 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 Join G \<in> stable C;
```
```   486          F Join project h C G \<in> A ensures B |]
```
```   487       ==> extend h F Join 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 Join G \<in> stable C;
```
```   500          F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
```
```   501       ==> extend h F Join 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 Join G \<in> stable C;
```
```   511          F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
```
```   512       ==> extend h F Join 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 Join G));
```
```   519          F Join project h C G \<in> A LeadsTo B |]
```
```   520       ==> extend h F Join 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 Join project h C G \<in> (project_set h C \<inter> A) ensures B;
```
```   530          extend h F Join G \<in> stable C |]
```
```   531       ==> extend h F Join 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 Join project h UNIV G \<in> A ensures B;
```
```   547          G \<in> stable (extend_set h A - extend_set h B) |]
```
```   548       ==> extend h F Join 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 Join project h (reachable (extend h F Join G)) G \<in> A Ensures B;
```
```   554          G \<in> stable (reachable (extend h F Join G) \<inter> extend_set h A -
```
```   555                      extend_set h B) |]
```
```   556       ==> extend h F Join 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 Join 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 Join G \<in> X'
```
```   593                         ==> F Join project h (C G) G \<in> X"
```
```   594      and extend:  "!!G. [| F Join project h (C G) G \<in> Y |]
```
```   595                         ==> extend h F Join 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 Join project h UNIV G \<in> A leadsTo B
```
```   652       ==> extend h F Join 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 Join project h (reachable (extend h F Join G)) G \<in> A LeadsTo B
```
```   658        ==> extend h F Join 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 Join 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
```