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