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