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