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