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 [2] 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 [2] 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 [2] 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 [2] 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