src/HOL/UNITY/Extend.thy
 author wenzelm Mon Mar 16 18:24:30 2009 +0100 (2009-03-16) changeset 30549 d2d7874648bd parent 16417 9bc16273c2d4 child 32960 69916a850301 child 32988 d1d4d7a08a66 permissions -rw-r--r--
simplified method setup;
```     1 (*  Title:      HOL/UNITY/Extend.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1998  University of Cambridge
```
```     5
```
```     6 Extending of state setsExtending of state sets
```
```     7   function f (forget)    maps the extended state to the original state
```
```     8   function g (forgotten) maps the extended state to the "extending part"
```
```     9 *)
```
```    10
```
```    11 header{*Extending State Sets*}
```
```    12
```
```    13 theory Extend imports Guar begin
```
```    14
```
```    15 constdefs
```
```    16
```
```    17   (*MOVE to Relation.thy?*)
```
```    18   Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
```
```    19     "Restrict A r == r \<inter> (A <*> UNIV)"
```
```    20
```
```    21   good_map :: "['a*'b => 'c] => bool"
```
```    22     "good_map h == surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
```
```    23      (*Using the locale constant "f", this is  f (h (x,y))) = x*)
```
```    24
```
```    25   extend_set :: "['a*'b => 'c, 'a set] => 'c set"
```
```    26     "extend_set h A == h ` (A <*> UNIV)"
```
```    27
```
```    28   project_set :: "['a*'b => 'c, 'c set] => 'a set"
```
```    29     "project_set h C == {x. \<exists>y. h(x,y) \<in> C}"
```
```    30
```
```    31   extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
```
```    32     "extend_act h == %act. \<Union>(s,s') \<in> act. \<Union>y. {(h(s,y), h(s',y))}"
```
```    33
```
```    34   project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
```
```    35     "project_act h act == {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}"
```
```    36
```
```    37   extend :: "['a*'b => 'c, 'a program] => 'c program"
```
```    38     "extend h F == mk_program (extend_set h (Init F),
```
```    39 			       extend_act h ` Acts F,
```
```    40 			       project_act h -` AllowedActs F)"
```
```    41
```
```    42   (*Argument C allows weak safety laws to be projected*)
```
```    43   project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
```
```    44     "project h C F ==
```
```    45        mk_program (project_set h (Init F),
```
```    46 		   project_act h ` Restrict C ` Acts F,
```
```    47 		   {act. Restrict (project_set h C) act :
```
```    48 		         project_act h ` Restrict C ` AllowedActs F})"
```
```    49
```
```    50 locale Extend =
```
```    51   fixes f     :: "'c => 'a"
```
```    52     and g     :: "'c => 'b"
```
```    53     and h     :: "'a*'b => 'c"    (*isomorphism between 'a * 'b and 'c *)
```
```    54     and slice :: "['c set, 'b] => 'a set"
```
```    55   assumes
```
```    56     good_h:  "good_map h"
```
```    57   defines f_def: "f z == fst (inv h z)"
```
```    58       and g_def: "g z == snd (inv h z)"
```
```    59       and slice_def: "slice Z y == {x. h(x,y) \<in> Z}"
```
```    60
```
```    61
```
```    62 (** These we prove OUTSIDE the locale. **)
```
```    63
```
```    64
```
```    65 subsection{*Restrict*}
```
```    66 (*MOVE to Relation.thy?*)
```
```    67
```
```    68 lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x \<in> A)"
```
```    69 by (unfold Restrict_def, blast)
```
```    70
```
```    71 lemma Restrict_UNIV [simp]: "Restrict UNIV = id"
```
```    72 apply (rule ext)
```
```    73 apply (auto simp add: Restrict_def)
```
```    74 done
```
```    75
```
```    76 lemma Restrict_empty [simp]: "Restrict {} r = {}"
```
```    77 by (auto simp add: Restrict_def)
```
```    78
```
```    79 lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A \<inter> B) r"
```
```    80 by (unfold Restrict_def, blast)
```
```    81
```
```    82 lemma Restrict_triv: "Domain r \<subseteq> A ==> Restrict A r = r"
```
```    83 by (unfold Restrict_def, auto)
```
```    84
```
```    85 lemma Restrict_subset: "Restrict A r \<subseteq> r"
```
```    86 by (unfold Restrict_def, auto)
```
```    87
```
```    88 lemma Restrict_eq_mono:
```
```    89      "[| A \<subseteq> B;  Restrict B r = Restrict B s |]
```
```    90       ==> Restrict A r = Restrict A s"
```
```    91 by (unfold Restrict_def, blast)
```
```    92
```
```    93 lemma Restrict_imageI:
```
```    94      "[| s \<in> RR;  Restrict A r = Restrict A s |]
```
```    95       ==> Restrict A r \<in> Restrict A ` RR"
```
```    96 by (unfold Restrict_def image_def, auto)
```
```    97
```
```    98 lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A \<inter> Domain r"
```
```    99 by blast
```
```   100
```
```   101 lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \<inter> B)"
```
```   102 by blast
```
```   103
```
```   104 (*Possibly easier than reasoning about "inv h"*)
```
```   105 lemma good_mapI:
```
```   106      assumes surj_h: "surj h"
```
```   107 	 and prem:   "!! x x' y y'. h(x,y) = h(x',y') ==> x=x'"
```
```   108      shows "good_map h"
```
```   109 apply (simp add: good_map_def)
```
```   110 apply (safe intro!: surj_h)
```
```   111 apply (rule prem)
```
```   112 apply (subst surjective_pairing [symmetric])
```
```   113 apply (subst surj_h [THEN surj_f_inv_f])
```
```   114 apply (rule refl)
```
```   115 done
```
```   116
```
```   117 lemma good_map_is_surj: "good_map h ==> surj h"
```
```   118 by (unfold good_map_def, auto)
```
```   119
```
```   120 (*A convenient way of finding a closed form for inv h*)
```
```   121 lemma fst_inv_equalityI:
```
```   122      assumes surj_h: "surj h"
```
```   123 	 and prem:   "!! x y. g (h(x,y)) = x"
```
```   124      shows "fst (inv h z) = g z"
```
```   125 apply (unfold inv_def)
```
```   126 apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE])
```
```   127 apply (rule someI2)
```
```   128 apply (drule_tac  f = g in arg_cong)
```
```   129 apply (auto simp add: prem)
```
```   130 done
```
```   131
```
```   132
```
```   133 subsection{*Trivial properties of f, g, h*}
```
```   134
```
```   135 lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x"
```
```   136 by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
```
```   137
```
```   138 lemma (in Extend) h_inject1 [dest]: "h(x,y) = h(x',y') ==> x=x'"
```
```   139 apply (drule_tac f = f in arg_cong)
```
```   140 apply (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
```
```   141 done
```
```   142
```
```   143 lemma (in Extend) h_f_g_equiv: "h(f z, g z) == z"
```
```   144 by (simp add: f_def g_def
```
```   145             good_h [unfolded good_map_def, THEN conjunct1, THEN surj_f_inv_f])
```
```   146
```
```   147 lemma (in Extend) h_f_g_eq: "h(f z, g z) = z"
```
```   148 by (simp add: h_f_g_equiv)
```
```   149
```
```   150
```
```   151 lemma (in Extend) split_extended_all:
```
```   152      "(!!z. PROP P z) == (!!u y. PROP P (h (u, y)))"
```
```   153 proof
```
```   154    assume allP: "\<And>z. PROP P z"
```
```   155    fix u y
```
```   156    show "PROP P (h (u, y))" by (rule allP)
```
```   157  next
```
```   158    assume allPh: "\<And>u y. PROP P (h(u,y))"
```
```   159    fix z
```
```   160    have Phfgz: "PROP P (h (f z, g z))" by (rule allPh)
```
```   161    show "PROP P z" by (rule Phfgz [unfolded h_f_g_equiv])
```
```   162 qed
```
```   163
```
```   164
```
```   165
```
```   166 subsection{*@{term extend_set}: basic properties*}
```
```   167
```
```   168 lemma project_set_iff [iff]:
```
```   169      "(x \<in> project_set h C) = (\<exists>y. h(x,y) \<in> C)"
```
```   170 by (simp add: project_set_def)
```
```   171
```
```   172 lemma extend_set_mono: "A \<subseteq> B ==> extend_set h A \<subseteq> extend_set h B"
```
```   173 by (unfold extend_set_def, blast)
```
```   174
```
```   175 lemma (in Extend) mem_extend_set_iff [iff]: "z \<in> extend_set h A = (f z \<in> A)"
```
```   176 apply (unfold extend_set_def)
```
```   177 apply (force intro: h_f_g_eq [symmetric])
```
```   178 done
```
```   179
```
```   180 lemma (in Extend) extend_set_strict_mono [iff]:
```
```   181      "(extend_set h A \<subseteq> extend_set h B) = (A \<subseteq> B)"
```
```   182 by (unfold extend_set_def, force)
```
```   183
```
```   184 lemma extend_set_empty [simp]: "extend_set h {} = {}"
```
```   185 by (unfold extend_set_def, auto)
```
```   186
```
```   187 lemma (in Extend) extend_set_eq_Collect: "extend_set h {s. P s} = {s. P(f s)}"
```
```   188 by auto
```
```   189
```
```   190 lemma (in Extend) extend_set_sing: "extend_set h {x} = {s. f s = x}"
```
```   191 by auto
```
```   192
```
```   193 lemma (in Extend) extend_set_inverse [simp]:
```
```   194      "project_set h (extend_set h C) = C"
```
```   195 by (unfold extend_set_def, auto)
```
```   196
```
```   197 lemma (in Extend) extend_set_project_set:
```
```   198      "C \<subseteq> extend_set h (project_set h C)"
```
```   199 apply (unfold extend_set_def)
```
```   200 apply (auto simp add: split_extended_all, blast)
```
```   201 done
```
```   202
```
```   203 lemma (in Extend) inj_extend_set: "inj (extend_set h)"
```
```   204 apply (rule inj_on_inverseI)
```
```   205 apply (rule extend_set_inverse)
```
```   206 done
```
```   207
```
```   208 lemma (in Extend) extend_set_UNIV_eq [simp]: "extend_set h UNIV = UNIV"
```
```   209 apply (unfold extend_set_def)
```
```   210 apply (auto simp add: split_extended_all)
```
```   211 done
```
```   212
```
```   213 subsection{*@{term project_set}: basic properties*}
```
```   214
```
```   215 (*project_set is simply image!*)
```
```   216 lemma (in Extend) project_set_eq: "project_set h C = f ` C"
```
```   217 by (auto intro: f_h_eq [symmetric] simp add: split_extended_all)
```
```   218
```
```   219 (*Converse appears to fail*)
```
```   220 lemma (in Extend) project_set_I: "!!z. z \<in> C ==> f z \<in> project_set h C"
```
```   221 by (auto simp add: split_extended_all)
```
```   222
```
```   223
```
```   224 subsection{*More laws*}
```
```   225
```
```   226 (*Because A and B could differ on the "other" part of the state,
```
```   227    cannot generalize to
```
```   228       project_set h (A \<inter> B) = project_set h A \<inter> project_set h B
```
```   229 *)
```
```   230 lemma (in Extend) project_set_extend_set_Int:
```
```   231      "project_set h ((extend_set h A) \<inter> B) = A \<inter> (project_set h B)"
```
```   232 by auto
```
```   233
```
```   234 (*Unused, but interesting?*)
```
```   235 lemma (in Extend) project_set_extend_set_Un:
```
```   236      "project_set h ((extend_set h A) \<union> B) = A \<union> (project_set h B)"
```
```   237 by auto
```
```   238
```
```   239 lemma project_set_Int_subset:
```
```   240      "project_set h (A \<inter> B) \<subseteq> (project_set h A) \<inter> (project_set h B)"
```
```   241 by auto
```
```   242
```
```   243 lemma (in Extend) extend_set_Un_distrib:
```
```   244      "extend_set h (A \<union> B) = extend_set h A \<union> extend_set h B"
```
```   245 by auto
```
```   246
```
```   247 lemma (in Extend) extend_set_Int_distrib:
```
```   248      "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
```
```   249 by auto
```
```   250
```
```   251 lemma (in Extend) extend_set_INT_distrib:
```
```   252      "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
```
```   253 by auto
```
```   254
```
```   255 lemma (in Extend) extend_set_Diff_distrib:
```
```   256      "extend_set h (A - B) = extend_set h A - extend_set h B"
```
```   257 by auto
```
```   258
```
```   259 lemma (in Extend) extend_set_Union:
```
```   260      "extend_set h (Union A) = (\<Union>X \<in> A. extend_set h X)"
```
```   261 by blast
```
```   262
```
```   263 lemma (in Extend) extend_set_subset_Compl_eq:
```
```   264      "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
```
```   265 by (unfold extend_set_def, auto)
```
```   266
```
```   267
```
```   268 subsection{*@{term extend_act}*}
```
```   269
```
```   270 (*Can't strengthen it to
```
```   271   ((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y')
```
```   272   because h doesn't have to be injective in the 2nd argument*)
```
```   273 lemma (in Extend) mem_extend_act_iff [iff]:
```
```   274      "((h(s,y), h(s',y)) \<in> extend_act h act) = ((s, s') \<in> act)"
```
```   275 by (unfold extend_act_def, auto)
```
```   276
```
```   277 (*Converse fails: (z,z') would include actions that changed the g-part*)
```
```   278 lemma (in Extend) extend_act_D:
```
```   279      "(z, z') \<in> extend_act h act ==> (f z, f z') \<in> act"
```
```   280 by (unfold extend_act_def, auto)
```
```   281
```
```   282 lemma (in Extend) extend_act_inverse [simp]:
```
```   283      "project_act h (extend_act h act) = act"
```
```   284 by (unfold extend_act_def project_act_def, blast)
```
```   285
```
```   286 lemma (in Extend) project_act_extend_act_restrict [simp]:
```
```   287      "project_act h (Restrict C (extend_act h act)) =
```
```   288       Restrict (project_set h C) act"
```
```   289 by (unfold extend_act_def project_act_def, blast)
```
```   290
```
```   291 lemma (in Extend) subset_extend_act_D:
```
```   292      "act' \<subseteq> extend_act h act ==> project_act h act' \<subseteq> act"
```
```   293 by (unfold extend_act_def project_act_def, force)
```
```   294
```
```   295 lemma (in Extend) inj_extend_act: "inj (extend_act h)"
```
```   296 apply (rule inj_on_inverseI)
```
```   297 apply (rule extend_act_inverse)
```
```   298 done
```
```   299
```
```   300 lemma (in Extend) extend_act_Image [simp]:
```
```   301      "extend_act h act `` (extend_set h A) = extend_set h (act `` A)"
```
```   302 by (unfold extend_set_def extend_act_def, force)
```
```   303
```
```   304 lemma (in Extend) extend_act_strict_mono [iff]:
```
```   305      "(extend_act h act' \<subseteq> extend_act h act) = (act'<=act)"
```
```   306 by (unfold extend_act_def, auto)
```
```   307
```
```   308 declare (in Extend) inj_extend_act [THEN inj_eq, iff]
```
```   309 (*This theorem is  (extend_act h act' = extend_act h act) = (act'=act) *)
```
```   310
```
```   311 lemma Domain_extend_act:
```
```   312     "Domain (extend_act h act) = extend_set h (Domain act)"
```
```   313 by (unfold extend_set_def extend_act_def, force)
```
```   314
```
```   315 lemma (in Extend) extend_act_Id [simp]:
```
```   316     "extend_act h Id = Id"
```
```   317 apply (unfold extend_act_def)
```
```   318 apply (force intro: h_f_g_eq [symmetric])
```
```   319 done
```
```   320
```
```   321 lemma (in Extend) project_act_I:
```
```   322      "!!z z'. (z, z') \<in> act ==> (f z, f z') \<in> project_act h act"
```
```   323 apply (unfold project_act_def)
```
```   324 apply (force simp add: split_extended_all)
```
```   325 done
```
```   326
```
```   327 lemma (in Extend) project_act_Id [simp]: "project_act h Id = Id"
```
```   328 by (unfold project_act_def, force)
```
```   329
```
```   330 lemma (in Extend) Domain_project_act:
```
```   331   "Domain (project_act h act) = project_set h (Domain act)"
```
```   332 apply (unfold project_act_def)
```
```   333 apply (force simp add: split_extended_all)
```
```   334 done
```
```   335
```
```   336
```
```   337
```
```   338 subsection{*extend*}
```
```   339
```
```   340 text{*Basic properties*}
```
```   341
```
```   342 lemma Init_extend [simp]:
```
```   343      "Init (extend h F) = extend_set h (Init F)"
```
```   344 by (unfold extend_def, auto)
```
```   345
```
```   346 lemma Init_project [simp]:
```
```   347      "Init (project h C F) = project_set h (Init F)"
```
```   348 by (unfold project_def, auto)
```
```   349
```
```   350 lemma (in Extend) Acts_extend [simp]:
```
```   351      "Acts (extend h F) = (extend_act h ` Acts F)"
```
```   352 by (simp add: extend_def insert_Id_image_Acts)
```
```   353
```
```   354 lemma (in Extend) AllowedActs_extend [simp]:
```
```   355      "AllowedActs (extend h F) = project_act h -` AllowedActs F"
```
```   356 by (simp add: extend_def insert_absorb)
```
```   357
```
```   358 lemma Acts_project [simp]:
```
```   359      "Acts(project h C F) = insert Id (project_act h ` Restrict C ` Acts F)"
```
```   360 by (auto simp add: project_def image_iff)
```
```   361
```
```   362 lemma (in Extend) AllowedActs_project [simp]:
```
```   363      "AllowedActs(project h C F) =
```
```   364         {act. Restrict (project_set h C) act
```
```   365                \<in> project_act h ` Restrict C ` AllowedActs F}"
```
```   366 apply (simp (no_asm) add: project_def image_iff)
```
```   367 apply (subst insert_absorb)
```
```   368 apply (auto intro!: bexI [of _ Id] simp add: project_act_def)
```
```   369 done
```
```   370
```
```   371 lemma (in Extend) Allowed_extend:
```
```   372      "Allowed (extend h F) = project h UNIV -` Allowed F"
```
```   373 apply (simp (no_asm) add: AllowedActs_extend Allowed_def)
```
```   374 apply blast
```
```   375 done
```
```   376
```
```   377 lemma (in Extend) extend_SKIP [simp]: "extend h SKIP = SKIP"
```
```   378 apply (unfold SKIP_def)
```
```   379 apply (rule program_equalityI, auto)
```
```   380 done
```
```   381
```
```   382 lemma project_set_UNIV [simp]: "project_set h UNIV = UNIV"
```
```   383 by auto
```
```   384
```
```   385 lemma project_set_Union:
```
```   386      "project_set h (Union A) = (\<Union>X \<in> A. project_set h X)"
```
```   387 by blast
```
```   388
```
```   389
```
```   390 (*Converse FAILS: the extended state contributing to project_set h C
```
```   391   may not coincide with the one contributing to project_act h act*)
```
```   392 lemma (in Extend) project_act_Restrict_subset:
```
```   393      "project_act h (Restrict C act) \<subseteq>
```
```   394       Restrict (project_set h C) (project_act h act)"
```
```   395 by (auto simp add: project_act_def)
```
```   396
```
```   397 lemma (in Extend) project_act_Restrict_Id_eq:
```
```   398      "project_act h (Restrict C Id) = Restrict (project_set h C) Id"
```
```   399 by (auto simp add: project_act_def)
```
```   400
```
```   401 lemma (in Extend) project_extend_eq:
```
```   402      "project h C (extend h F) =
```
```   403       mk_program (Init F, Restrict (project_set h C) ` Acts F,
```
```   404                   {act. Restrict (project_set h C) act
```
```   405                           \<in> project_act h ` Restrict C `
```
```   406                                      (project_act h -` AllowedActs F)})"
```
```   407 apply (rule program_equalityI)
```
```   408   apply simp
```
```   409  apply (simp add: image_eq_UN)
```
```   410 apply (simp add: project_def)
```
```   411 done
```
```   412
```
```   413 lemma (in Extend) extend_inverse [simp]:
```
```   414      "project h UNIV (extend h F) = F"
```
```   415 apply (simp (no_asm_simp) add: project_extend_eq image_eq_UN
```
```   416           subset_UNIV [THEN subset_trans, THEN Restrict_triv])
```
```   417 apply (rule program_equalityI)
```
```   418 apply (simp_all (no_asm))
```
```   419 apply (subst insert_absorb)
```
```   420 apply (simp (no_asm) add: bexI [of _ Id])
```
```   421 apply auto
```
```   422 apply (rename_tac "act")
```
```   423 apply (rule_tac x = "extend_act h act" in bexI, auto)
```
```   424 done
```
```   425
```
```   426 lemma (in Extend) inj_extend: "inj (extend h)"
```
```   427 apply (rule inj_on_inverseI)
```
```   428 apply (rule extend_inverse)
```
```   429 done
```
```   430
```
```   431 lemma (in Extend) extend_Join [simp]:
```
```   432      "extend h (F\<squnion>G) = extend h F\<squnion>extend h G"
```
```   433 apply (rule program_equalityI)
```
```   434 apply (simp (no_asm) add: extend_set_Int_distrib)
```
```   435 apply (simp add: image_Un, auto)
```
```   436 done
```
```   437
```
```   438 lemma (in Extend) extend_JN [simp]:
```
```   439      "extend h (JOIN I F) = (\<Squnion>i \<in> I. extend h (F i))"
```
```   440 apply (rule program_equalityI)
```
```   441   apply (simp (no_asm) add: extend_set_INT_distrib)
```
```   442  apply (simp add: image_UN, auto)
```
```   443 done
```
```   444
```
```   445 (** These monotonicity results look natural but are UNUSED **)
```
```   446
```
```   447 lemma (in Extend) extend_mono: "F \<le> G ==> extend h F \<le> extend h G"
```
```   448 by (force simp add: component_eq_subset)
```
```   449
```
```   450 lemma (in Extend) project_mono: "F \<le> G ==> project h C F \<le> project h C G"
```
```   451 by (simp add: component_eq_subset, blast)
```
```   452
```
```   453 lemma (in Extend) all_total_extend: "all_total F ==> all_total (extend h F)"
```
```   454 by (simp add: all_total_def Domain_extend_act)
```
```   455
```
```   456 subsection{*Safety: co, stable*}
```
```   457
```
```   458 lemma (in Extend) extend_constrains:
```
```   459      "(extend h F \<in> (extend_set h A) co (extend_set h B)) =
```
```   460       (F \<in> A co B)"
```
```   461 by (simp add: constrains_def)
```
```   462
```
```   463 lemma (in Extend) extend_stable:
```
```   464      "(extend h F \<in> stable (extend_set h A)) = (F \<in> stable A)"
```
```   465 by (simp add: stable_def extend_constrains)
```
```   466
```
```   467 lemma (in Extend) extend_invariant:
```
```   468      "(extend h F \<in> invariant (extend_set h A)) = (F \<in> invariant A)"
```
```   469 by (simp add: invariant_def extend_stable)
```
```   470
```
```   471 (*Projects the state predicates in the property satisfied by  extend h F.
```
```   472   Converse fails: A and B may differ in their extra variables*)
```
```   473 lemma (in Extend) extend_constrains_project_set:
```
```   474      "extend h F \<in> A co B ==> F \<in> (project_set h A) co (project_set h B)"
```
```   475 by (auto simp add: constrains_def, force)
```
```   476
```
```   477 lemma (in Extend) extend_stable_project_set:
```
```   478      "extend h F \<in> stable A ==> F \<in> stable (project_set h A)"
```
```   479 by (simp add: stable_def extend_constrains_project_set)
```
```   480
```
```   481
```
```   482 subsection{*Weak safety primitives: Co, Stable*}
```
```   483
```
```   484 lemma (in Extend) reachable_extend_f:
```
```   485      "p \<in> reachable (extend h F) ==> f p \<in> reachable F"
```
```   486 apply (erule reachable.induct)
```
```   487 apply (auto intro: reachable.intros simp add: extend_act_def image_iff)
```
```   488 done
```
```   489
```
```   490 lemma (in Extend) h_reachable_extend:
```
```   491      "h(s,y) \<in> reachable (extend h F) ==> s \<in> reachable F"
```
```   492 by (force dest!: reachable_extend_f)
```
```   493
```
```   494 lemma (in Extend) reachable_extend_eq:
```
```   495      "reachable (extend h F) = extend_set h (reachable F)"
```
```   496 apply (unfold extend_set_def)
```
```   497 apply (rule equalityI)
```
```   498 apply (force intro: h_f_g_eq [symmetric] dest!: reachable_extend_f, clarify)
```
```   499 apply (erule reachable.induct)
```
```   500 apply (force intro: reachable.intros)+
```
```   501 done
```
```   502
```
```   503 lemma (in Extend) extend_Constrains:
```
```   504      "(extend h F \<in> (extend_set h A) Co (extend_set h B)) =
```
```   505       (F \<in> A Co B)"
```
```   506 by (simp add: Constrains_def reachable_extend_eq extend_constrains
```
```   507               extend_set_Int_distrib [symmetric])
```
```   508
```
```   509 lemma (in Extend) extend_Stable:
```
```   510      "(extend h F \<in> Stable (extend_set h A)) = (F \<in> Stable A)"
```
```   511 by (simp add: Stable_def extend_Constrains)
```
```   512
```
```   513 lemma (in Extend) extend_Always:
```
```   514      "(extend h F \<in> Always (extend_set h A)) = (F \<in> Always A)"
```
```   515 by (simp (no_asm_simp) add: Always_def extend_Stable)
```
```   516
```
```   517
```
```   518 (** Safety and "project" **)
```
```   519
```
```   520 (** projection: monotonicity for safety **)
```
```   521
```
```   522 lemma project_act_mono:
```
```   523      "D \<subseteq> C ==>
```
```   524       project_act h (Restrict D act) \<subseteq> project_act h (Restrict C act)"
```
```   525 by (auto simp add: project_act_def)
```
```   526
```
```   527 lemma (in Extend) project_constrains_mono:
```
```   528      "[| D \<subseteq> C; project h C F \<in> A co B |] ==> project h D F \<in> A co B"
```
```   529 apply (auto simp add: constrains_def)
```
```   530 apply (drule project_act_mono, blast)
```
```   531 done
```
```   532
```
```   533 lemma (in Extend) project_stable_mono:
```
```   534      "[| D \<subseteq> C;  project h C F \<in> stable A |] ==> project h D F \<in> stable A"
```
```   535 by (simp add: stable_def project_constrains_mono)
```
```   536
```
```   537 (*Key lemma used in several proofs about project and co*)
```
```   538 lemma (in Extend) project_constrains:
```
```   539      "(project h C F \<in> A co B)  =
```
```   540       (F \<in> (C \<inter> extend_set h A) co (extend_set h B) & A \<subseteq> B)"
```
```   541 apply (unfold constrains_def)
```
```   542 apply (auto intro!: project_act_I simp add: ball_Un)
```
```   543 apply (force intro!: project_act_I dest!: subsetD)
```
```   544 (*the <== direction*)
```
```   545 apply (unfold project_act_def)
```
```   546 apply (force dest!: subsetD)
```
```   547 done
```
```   548
```
```   549 lemma (in Extend) project_stable:
```
```   550      "(project h UNIV F \<in> stable A) = (F \<in> stable (extend_set h A))"
```
```   551 apply (unfold stable_def)
```
```   552 apply (simp (no_asm) add: project_constrains)
```
```   553 done
```
```   554
```
```   555 lemma (in Extend) project_stable_I:
```
```   556      "F \<in> stable (extend_set h A) ==> project h C F \<in> stable A"
```
```   557 apply (drule project_stable [THEN iffD2])
```
```   558 apply (blast intro: project_stable_mono)
```
```   559 done
```
```   560
```
```   561 lemma (in Extend) Int_extend_set_lemma:
```
```   562      "A \<inter> extend_set h ((project_set h A) \<inter> B) = A \<inter> extend_set h B"
```
```   563 by (auto simp add: split_extended_all)
```
```   564
```
```   565 (*Strange (look at occurrences of C) but used in leadsETo proofs*)
```
```   566 lemma project_constrains_project_set:
```
```   567      "G \<in> C co B ==> project h C G \<in> project_set h C co project_set h B"
```
```   568 by (simp add: constrains_def project_def project_act_def, blast)
```
```   569
```
```   570 lemma project_stable_project_set:
```
```   571      "G \<in> stable C ==> project h C G \<in> stable (project_set h C)"
```
```   572 by (simp add: stable_def project_constrains_project_set)
```
```   573
```
```   574
```
```   575 subsection{*Progress: transient, ensures*}
```
```   576
```
```   577 lemma (in Extend) extend_transient:
```
```   578      "(extend h F \<in> transient (extend_set h A)) = (F \<in> transient A)"
```
```   579 by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act)
```
```   580
```
```   581 lemma (in Extend) extend_ensures:
```
```   582      "(extend h F \<in> (extend_set h A) ensures (extend_set h B)) =
```
```   583       (F \<in> A ensures B)"
```
```   584 by (simp add: ensures_def extend_constrains extend_transient
```
```   585         extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric])
```
```   586
```
```   587 lemma (in Extend) leadsTo_imp_extend_leadsTo:
```
```   588      "F \<in> A leadsTo B
```
```   589       ==> extend h F \<in> (extend_set h A) leadsTo (extend_set h B)"
```
```   590 apply (erule leadsTo_induct)
```
```   591   apply (simp add: leadsTo_Basis extend_ensures)
```
```   592  apply (blast intro: leadsTo_Trans)
```
```   593 apply (simp add: leadsTo_UN extend_set_Union)
```
```   594 done
```
```   595
```
```   596 subsection{*Proving the converse takes some doing!*}
```
```   597
```
```   598 lemma (in Extend) slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
```
```   599 by (simp (no_asm) add: slice_def)
```
```   600
```
```   601 lemma (in Extend) slice_Union: "slice (Union S) y = (\<Union>x \<in> S. slice x y)"
```
```   602 by auto
```
```   603
```
```   604 lemma (in Extend) slice_extend_set: "slice (extend_set h A) y = A"
```
```   605 by auto
```
```   606
```
```   607 lemma (in Extend) project_set_is_UN_slice:
```
```   608      "project_set h A = (\<Union>y. slice A y)"
```
```   609 by auto
```
```   610
```
```   611 lemma (in Extend) extend_transient_slice:
```
```   612      "extend h F \<in> transient A ==> F \<in> transient (slice A y)"
```
```   613 by (unfold transient_def, auto)
```
```   614
```
```   615 (*Converse?*)
```
```   616 lemma (in Extend) extend_constrains_slice:
```
```   617      "extend h F \<in> A co B ==> F \<in> (slice A y) co (slice B y)"
```
```   618 by (auto simp add: constrains_def)
```
```   619
```
```   620 lemma (in Extend) extend_ensures_slice:
```
```   621      "extend h F \<in> A ensures B ==> F \<in> (slice A y) ensures (project_set h B)"
```
```   622 apply (auto simp add: ensures_def extend_constrains extend_transient)
```
```   623 apply (erule_tac  extend_transient_slice [THEN transient_strengthen])
```
```   624 apply (erule extend_constrains_slice [THEN constrains_weaken], auto)
```
```   625 done
```
```   626
```
```   627 lemma (in Extend) leadsTo_slice_project_set:
```
```   628      "\<forall>y. F \<in> (slice B y) leadsTo CU ==> F \<in> (project_set h B) leadsTo CU"
```
```   629 apply (simp (no_asm) add: project_set_is_UN_slice)
```
```   630 apply (blast intro: leadsTo_UN)
```
```   631 done
```
```   632
```
```   633 lemma (in Extend) extend_leadsTo_slice [rule_format]:
```
```   634      "extend h F \<in> AU leadsTo BU
```
```   635       ==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
```
```   636 apply (erule leadsTo_induct)
```
```   637   apply (blast intro: extend_ensures_slice leadsTo_Basis)
```
```   638  apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
```
```   639 apply (simp add: leadsTo_UN slice_Union)
```
```   640 done
```
```   641
```
```   642 lemma (in Extend) extend_leadsTo:
```
```   643      "(extend h F \<in> (extend_set h A) leadsTo (extend_set h B)) =
```
```   644       (F \<in> A leadsTo B)"
```
```   645 apply safe
```
```   646 apply (erule_tac  leadsTo_imp_extend_leadsTo)
```
```   647 apply (drule extend_leadsTo_slice)
```
```   648 apply (simp add: slice_extend_set)
```
```   649 done
```
```   650
```
```   651 lemma (in Extend) extend_LeadsTo:
```
```   652      "(extend h F \<in> (extend_set h A) LeadsTo (extend_set h B)) =
```
```   653       (F \<in> A LeadsTo B)"
```
```   654 by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo
```
```   655               extend_set_Int_distrib [symmetric])
```
```   656
```
```   657
```
```   658 subsection{*preserves*}
```
```   659
```
```   660 lemma (in Extend) project_preserves_I:
```
```   661      "G \<in> preserves (v o f) ==> project h C G \<in> preserves v"
```
```   662 by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect)
```
```   663
```
```   664 (*to preserve f is to preserve the whole original state*)
```
```   665 lemma (in Extend) project_preserves_id_I:
```
```   666      "G \<in> preserves f ==> project h C G \<in> preserves id"
```
```   667 by (simp add: project_preserves_I)
```
```   668
```
```   669 lemma (in Extend) extend_preserves:
```
```   670      "(extend h G \<in> preserves (v o f)) = (G \<in> preserves v)"
```
```   671 by (auto simp add: preserves_def extend_stable [symmetric]
```
```   672                    extend_set_eq_Collect)
```
```   673
```
```   674 lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G \<in> preserves g)"
```
```   675 by (auto simp add: preserves_def extend_def extend_act_def stable_def
```
```   676                    constrains_def g_def)
```
```   677
```
```   678
```
```   679 subsection{*Guarantees*}
```
```   680
```
```   681 lemma (in Extend) project_extend_Join:
```
```   682      "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
```
```   683 apply (rule program_equalityI)
```
```   684   apply (simp add: project_set_extend_set_Int)
```
```   685  apply (simp add: image_eq_UN UN_Un, auto)
```
```   686 done
```
```   687
```
```   688 lemma (in Extend) extend_Join_eq_extend_D:
```
```   689      "(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)"
```
```   690 apply (drule_tac f = "project h UNIV" in arg_cong)
```
```   691 apply (simp add: project_extend_Join)
```
```   692 done
```
```   693
```
```   694 (** Strong precondition and postcondition; only useful when
```
```   695     the old and new state sets are in bijection **)
```
```   696
```
```   697
```
```   698 lemma (in Extend) ok_extend_imp_ok_project:
```
```   699      "extend h F ok G ==> F ok project h UNIV G"
```
```   700 apply (auto simp add: ok_def)
```
```   701 apply (drule subsetD)
```
```   702 apply (auto intro!: rev_image_eqI)
```
```   703 done
```
```   704
```
```   705 lemma (in Extend) ok_extend_iff: "(extend h F ok extend h G) = (F ok G)"
```
```   706 apply (simp add: ok_def, safe)
```
```   707 apply (force+)
```
```   708 done
```
```   709
```
```   710 lemma (in Extend) OK_extend_iff: "OK I (%i. extend h (F i)) = (OK I F)"
```
```   711 apply (unfold OK_def, safe)
```
```   712 apply (drule_tac x = i in bspec)
```
```   713 apply (drule_tac  x = j in bspec)
```
```   714 apply (force+)
```
```   715 done
```
```   716
```
```   717 lemma (in Extend) guarantees_imp_extend_guarantees:
```
```   718      "F \<in> X guarantees Y ==>
```
```   719       extend h F \<in> (extend h ` X) guarantees (extend h ` Y)"
```
```   720 apply (rule guaranteesI, clarify)
```
```   721 apply (blast dest: ok_extend_imp_ok_project extend_Join_eq_extend_D
```
```   722                    guaranteesD)
```
```   723 done
```
```   724
```
```   725 lemma (in Extend) extend_guarantees_imp_guarantees:
```
```   726      "extend h F \<in> (extend h ` X) guarantees (extend h ` Y)
```
```   727       ==> F \<in> X guarantees Y"
```
```   728 apply (auto simp add: guar_def)
```
```   729 apply (drule_tac x = "extend h G" in spec)
```
```   730 apply (simp del: extend_Join
```
```   731             add: extend_Join [symmetric] ok_extend_iff
```
```   732                  inj_extend [THEN inj_image_mem_iff])
```
```   733 done
```
```   734
```
```   735 lemma (in Extend) extend_guarantees_eq:
```
```   736      "(extend h F \<in> (extend h ` X) guarantees (extend h ` Y)) =
```
```   737       (F \<in> X guarantees Y)"
```
```   738 by (blast intro: guarantees_imp_extend_guarantees
```
```   739                  extend_guarantees_imp_guarantees)
```
```   740
```
```   741 end
```