author | wenzelm |
Thu, 22 Jul 2010 18:08:39 +0200 | |
changeset 37936 | 1e4c5015a72e |
parent 35416 | d8d7d1b785af |
child 40702 | cf26dd7395e4 |
permissions | -rw-r--r-- |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Rename.thy |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
3 |
Copyright 2000 University of Cambridge |
13798 | 4 |
*) |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
5 |
|
13798 | 6 |
header{*Renaming of State Sets*} |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
7 |
|
16417 | 8 |
theory Rename imports Extend begin |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
9 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
16417
diff
changeset
|
10 |
definition rename :: "['a => 'b, 'a program] => 'b program" where |
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
11 |
"rename h == extend (%(x,u::unit). h x)" |
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
12 |
|
13790 | 13 |
declare image_inv_f_f [simp] image_surj_f_inv_f [simp] |
14 |
||
15 |
declare Extend.intro [simp,intro] |
|
16 |
||
17 |
lemma good_map_bij [simp,intro]: "bij h ==> good_map (%(x,u). h x)" |
|
18 |
apply (rule good_mapI) |
|
19 |
apply (unfold bij_def inj_on_def surj_def, auto) |
|
20 |
done |
|
21 |
||
22 |
lemma fst_o_inv_eq_inv: "bij h ==> fst (inv (%(x,u). h x) s) = inv h s" |
|
23 |
apply (unfold bij_def split_def, clarify) |
|
24 |
apply (subgoal_tac "surj (%p. h (fst p))") |
|
25 |
prefer 2 apply (simp add: surj_def) |
|
26 |
apply (erule injD) |
|
27 |
apply (simp (no_asm_simp) add: surj_f_inv_f) |
|
28 |
apply (erule surj_f_inv_f) |
|
29 |
done |
|
30 |
||
13805 | 31 |
lemma mem_rename_set_iff: "bij h ==> z \<in> h`A = (inv h z \<in> A)" |
13790 | 32 |
by (force simp add: bij_is_inj bij_is_surj [THEN surj_f_inv_f]) |
33 |
||
34 |
||
35 |
lemma extend_set_eq_image [simp]: "extend_set (%(x,u). h x) A = h`A" |
|
36 |
by (force simp add: extend_set_def) |
|
37 |
||
38 |
lemma Init_rename [simp]: "Init (rename h F) = h`(Init F)" |
|
39 |
by (simp add: rename_def) |
|
40 |
||
41 |
||
13798 | 42 |
subsection{*inverse properties*} |
13790 | 43 |
|
44 |
lemma extend_set_inv: |
|
45 |
"bij h |
|
46 |
==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)" |
|
47 |
apply (unfold bij_def) |
|
48 |
apply (rule ext) |
|
49 |
apply (force simp add: extend_set_def project_set_def surj_f_inv_f) |
|
50 |
done |
|
51 |
||
52 |
(** for "rename" (programs) **) |
|
53 |
||
54 |
lemma bij_extend_act_eq_project_act: "bij h |
|
55 |
==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)" |
|
56 |
apply (rule ext) |
|
57 |
apply (force simp add: extend_act_def project_act_def bij_def surj_f_inv_f) |
|
58 |
done |
|
59 |
||
60 |
lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))" |
|
61 |
apply (rule bijI) |
|
62 |
apply (rule Extend.inj_extend_act) |
|
63 |
apply (auto simp add: bij_extend_act_eq_project_act) |
|
64 |
apply (rule surjI) |
|
65 |
apply (rule Extend.extend_act_inverse) |
|
66 |
apply (blast intro: bij_imp_bij_inv good_map_bij) |
|
67 |
done |
|
68 |
||
69 |
lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))" |
|
70 |
apply (frule bij_imp_bij_inv [THEN bij_extend_act]) |
|
71 |
apply (simp add: bij_extend_act_eq_project_act bij_imp_bij_inv inv_inv_eq) |
|
72 |
done |
|
73 |
||
74 |
lemma bij_inv_project_act_eq: "bij h ==> inv (project_act (%(x,u::'c). inv h x)) = |
|
75 |
project_act (%(x,u::'c). h x)" |
|
76 |
apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric]) |
|
77 |
apply (rule surj_imp_inv_eq) |
|
78 |
apply (blast intro: bij_extend_act bij_is_surj) |
|
79 |
apply (simp (no_asm_simp) add: Extend.extend_act_inverse) |
|
80 |
done |
|
81 |
||
82 |
lemma extend_inv: "bij h |
|
83 |
==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV" |
|
84 |
apply (frule bij_imp_bij_inv) |
|
85 |
apply (rule ext) |
|
86 |
apply (rule program_equalityI) |
|
87 |
apply (simp (no_asm_simp) add: extend_set_inv) |
|
88 |
apply (simp add: Extend.project_act_Id Extend.Acts_extend |
|
89 |
insert_Id_image_Acts bij_extend_act_eq_project_act inv_inv_eq) |
|
90 |
apply (simp add: Extend.AllowedActs_extend Extend.AllowedActs_project |
|
91 |
bij_project_act bij_vimage_eq_inv_image bij_inv_project_act_eq) |
|
92 |
done |
|
93 |
||
94 |
lemma rename_inv_rename [simp]: "bij h ==> rename (inv h) (rename h F) = F" |
|
95 |
by (simp add: rename_def extend_inv Extend.extend_inverse) |
|
96 |
||
97 |
lemma rename_rename_inv [simp]: "bij h ==> rename h (rename (inv h) F) = F" |
|
98 |
apply (frule bij_imp_bij_inv) |
|
99 |
apply (erule inv_inv_eq [THEN subst], erule rename_inv_rename) |
|
100 |
done |
|
101 |
||
102 |
lemma rename_inv_eq: "bij h ==> rename (inv h) = inv (rename h)" |
|
103 |
by (rule inv_equality [symmetric], auto) |
|
104 |
||
105 |
(** (rename h) is bijective <=> h is bijective **) |
|
106 |
||
107 |
lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))" |
|
108 |
apply (rule bijI) |
|
109 |
apply (blast intro: Extend.inj_extend) |
|
15976 | 110 |
apply (rule_tac f = "extend (% (x,u) . inv h x)" in surjI) |
111 |
apply (subst (1 2) inv_inv_eq [of h, symmetric], assumption+) |
|
112 |
apply (simp add: bij_imp_bij_inv extend_inv [of "inv h"]) |
|
113 |
apply (simp add: inv_inv_eq) |
|
13790 | 114 |
apply (rule Extend.extend_inverse) |
115 |
apply (simp add: bij_imp_bij_inv) |
|
116 |
done |
|
117 |
||
118 |
lemma bij_project: "bij h ==> bij (project (%(x,u::'c). h x) UNIV)" |
|
119 |
apply (subst extend_inv [symmetric]) |
|
120 |
apply (auto simp add: bij_imp_bij_inv bij_extend) |
|
121 |
done |
|
122 |
||
123 |
lemma inv_project_eq: |
|
124 |
"bij h |
|
125 |
==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)" |
|
126 |
apply (rule inj_imp_inv_eq) |
|
127 |
apply (erule bij_project [THEN bij_is_inj]) |
|
128 |
apply (simp (no_asm_simp) add: Extend.extend_inverse) |
|
129 |
done |
|
130 |
||
131 |
lemma Allowed_rename [simp]: |
|
132 |
"bij h ==> Allowed (rename h F) = rename h ` Allowed F" |
|
133 |
apply (simp (no_asm_simp) add: rename_def Extend.Allowed_extend) |
|
134 |
apply (subst bij_vimage_eq_inv_image) |
|
135 |
apply (rule bij_project, blast) |
|
136 |
apply (simp (no_asm_simp) add: inv_project_eq) |
|
137 |
done |
|
138 |
||
139 |
lemma bij_rename: "bij h ==> bij (rename h)" |
|
140 |
apply (simp (no_asm_simp) add: rename_def bij_extend) |
|
141 |
done |
|
142 |
lemmas surj_rename = bij_rename [THEN bij_is_surj, standard] |
|
143 |
||
144 |
lemma inj_rename_imp_inj: "inj (rename h) ==> inj h" |
|
145 |
apply (unfold inj_on_def, auto) |
|
15976 | 146 |
apply (drule_tac x = "mk_program ({x}, {}, {})" in spec) |
147 |
apply (drule_tac x = "mk_program ({y}, {}, {})" in spec) |
|
13790 | 148 |
apply (auto simp add: program_equality_iff rename_def extend_def) |
149 |
done |
|
150 |
||
151 |
lemma surj_rename_imp_surj: "surj (rename h) ==> surj h" |
|
152 |
apply (unfold surj_def, auto) |
|
15976 | 153 |
apply (drule_tac x = "mk_program ({y}, {}, {})" in spec) |
13790 | 154 |
apply (auto simp add: program_equality_iff rename_def extend_def) |
155 |
done |
|
156 |
||
157 |
lemma bij_rename_imp_bij: "bij (rename h) ==> bij h" |
|
158 |
apply (unfold bij_def) |
|
159 |
apply (simp (no_asm_simp) add: inj_rename_imp_inj surj_rename_imp_surj) |
|
160 |
done |
|
161 |
||
162 |
lemma bij_rename_iff [simp]: "bij (rename h) = bij h" |
|
163 |
by (blast intro: bij_rename bij_rename_imp_bij) |
|
164 |
||
165 |
||
13798 | 166 |
subsection{*the lattice operations*} |
13790 | 167 |
|
168 |
lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP" |
|
169 |
by (simp add: rename_def Extend.extend_SKIP) |
|
170 |
||
171 |
lemma rename_Join [simp]: |
|
172 |
"bij h ==> rename h (F Join G) = rename h F Join rename h G" |
|
173 |
by (simp add: rename_def Extend.extend_Join) |
|
174 |
||
175 |
lemma rename_JN [simp]: |
|
13805 | 176 |
"bij h ==> rename h (JOIN I F) = (\<Squnion>i \<in> I. rename h (F i))" |
13790 | 177 |
by (simp add: rename_def Extend.extend_JN) |
178 |
||
179 |
||
13798 | 180 |
subsection{*Strong Safety: co, stable*} |
13790 | 181 |
|
182 |
lemma rename_constrains: |
|
13805 | 183 |
"bij h ==> (rename h F \<in> (h`A) co (h`B)) = (F \<in> A co B)" |
13790 | 184 |
apply (unfold rename_def) |
185 |
apply (subst extend_set_eq_image [symmetric])+ |
|
186 |
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_constrains]) |
|
187 |
done |
|
188 |
||
189 |
lemma rename_stable: |
|
13805 | 190 |
"bij h ==> (rename h F \<in> stable (h`A)) = (F \<in> stable A)" |
13790 | 191 |
apply (simp add: stable_def rename_constrains) |
192 |
done |
|
193 |
||
194 |
lemma rename_invariant: |
|
13805 | 195 |
"bij h ==> (rename h F \<in> invariant (h`A)) = (F \<in> invariant A)" |
13790 | 196 |
apply (simp add: invariant_def rename_stable bij_is_inj [THEN inj_image_subset_iff]) |
197 |
done |
|
198 |
||
199 |
lemma rename_increasing: |
|
13805 | 200 |
"bij h ==> (rename h F \<in> increasing func) = (F \<in> increasing (func o h))" |
13790 | 201 |
apply (simp add: increasing_def rename_stable [symmetric] bij_image_Collect_eq bij_is_surj [THEN surj_f_inv_f]) |
202 |
done |
|
203 |
||
204 |
||
13798 | 205 |
subsection{*Weak Safety: Co, Stable*} |
13790 | 206 |
|
207 |
lemma reachable_rename_eq: |
|
208 |
"bij h ==> reachable (rename h F) = h ` (reachable F)" |
|
209 |
apply (simp add: rename_def Extend.reachable_extend_eq) |
|
210 |
done |
|
211 |
||
212 |
lemma rename_Constrains: |
|
13805 | 213 |
"bij h ==> (rename h F \<in> (h`A) Co (h`B)) = (F \<in> A Co B)" |
13790 | 214 |
by (simp add: Constrains_def reachable_rename_eq rename_constrains |
215 |
bij_is_inj image_Int [symmetric]) |
|
216 |
||
217 |
lemma rename_Stable: |
|
13805 | 218 |
"bij h ==> (rename h F \<in> Stable (h`A)) = (F \<in> Stable A)" |
13790 | 219 |
by (simp add: Stable_def rename_Constrains) |
220 |
||
13805 | 221 |
lemma rename_Always: "bij h ==> (rename h F \<in> Always (h`A)) = (F \<in> Always A)" |
13790 | 222 |
by (simp add: Always_def rename_Stable bij_is_inj [THEN inj_image_subset_iff]) |
223 |
||
224 |
lemma rename_Increasing: |
|
13805 | 225 |
"bij h ==> (rename h F \<in> Increasing func) = (F \<in> Increasing (func o h))" |
13790 | 226 |
by (simp add: Increasing_def rename_Stable [symmetric] bij_image_Collect_eq |
227 |
bij_is_surj [THEN surj_f_inv_f]) |
|
228 |
||
229 |
||
13798 | 230 |
subsection{*Progress: transient, ensures*} |
13790 | 231 |
|
232 |
lemma rename_transient: |
|
13805 | 233 |
"bij h ==> (rename h F \<in> transient (h`A)) = (F \<in> transient A)" |
13790 | 234 |
apply (unfold rename_def) |
235 |
apply (subst extend_set_eq_image [symmetric]) |
|
236 |
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_transient]) |
|
237 |
done |
|
238 |
||
239 |
lemma rename_ensures: |
|
13805 | 240 |
"bij h ==> (rename h F \<in> (h`A) ensures (h`B)) = (F \<in> A ensures B)" |
13790 | 241 |
apply (unfold rename_def) |
242 |
apply (subst extend_set_eq_image [symmetric])+ |
|
243 |
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_ensures]) |
|
244 |
done |
|
245 |
||
246 |
lemma rename_leadsTo: |
|
13805 | 247 |
"bij h ==> (rename h F \<in> (h`A) leadsTo (h`B)) = (F \<in> A leadsTo B)" |
13790 | 248 |
apply (unfold rename_def) |
249 |
apply (subst extend_set_eq_image [symmetric])+ |
|
250 |
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_leadsTo]) |
|
251 |
done |
|
252 |
||
253 |
lemma rename_LeadsTo: |
|
13805 | 254 |
"bij h ==> (rename h F \<in> (h`A) LeadsTo (h`B)) = (F \<in> A LeadsTo B)" |
13790 | 255 |
apply (unfold rename_def) |
256 |
apply (subst extend_set_eq_image [symmetric])+ |
|
257 |
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_LeadsTo]) |
|
258 |
done |
|
259 |
||
260 |
lemma rename_rename_guarantees_eq: |
|
13805 | 261 |
"bij h ==> (rename h F \<in> (rename h ` X) guarantees |
13790 | 262 |
(rename h ` Y)) = |
13805 | 263 |
(F \<in> X guarantees Y)" |
13790 | 264 |
apply (unfold rename_def) |
265 |
apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_guarantees_eq [symmetric]], assumption) |
|
266 |
apply (simp (no_asm_simp) add: fst_o_inv_eq_inv o_def) |
|
267 |
done |
|
268 |
||
269 |
lemma rename_guarantees_eq_rename_inv: |
|
13805 | 270 |
"bij h ==> (rename h F \<in> X guarantees Y) = |
271 |
(F \<in> (rename (inv h) ` X) guarantees |
|
13790 | 272 |
(rename (inv h) ` Y))" |
273 |
apply (subst rename_rename_guarantees_eq [symmetric], assumption) |
|
274 |
apply (simp add: image_eq_UN o_def bij_is_surj [THEN surj_f_inv_f]) |
|
275 |
done |
|
276 |
||
277 |
lemma rename_preserves: |
|
13805 | 278 |
"bij h ==> (rename h G \<in> preserves v) = (G \<in> preserves (v o h))" |
13790 | 279 |
apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_preserves [symmetric]], assumption) |
280 |
apply (simp add: o_def fst_o_inv_eq_inv rename_def bij_is_surj [THEN surj_f_inv_f]) |
|
281 |
done |
|
282 |
||
283 |
lemma ok_rename_iff [simp]: "bij h ==> (rename h F ok rename h G) = (F ok G)" |
|
284 |
by (simp add: Extend.ok_extend_iff rename_def) |
|
285 |
||
286 |
lemma OK_rename_iff [simp]: "bij h ==> OK I (%i. rename h (F i)) = (OK I F)" |
|
287 |
by (simp add: Extend.OK_extend_iff rename_def) |
|
288 |
||
289 |
||
13798 | 290 |
subsection{*"image" versions of the rules, for lifting "guarantees" properties*} |
13790 | 291 |
|
292 |
(*All the proofs are similar. Better would have been to prove one |
|
293 |
meta-theorem, but how can we handle the polymorphism? E.g. in |
|
294 |
rename_constrains the two appearances of "co" have different types!*) |
|
295 |
lemmas bij_eq_rename = surj_rename [THEN surj_f_inv_f, symmetric] |
|
296 |
||
297 |
lemma rename_image_constrains: |
|
298 |
"bij h ==> rename h ` (A co B) = (h ` A) co (h`B)" |
|
299 |
apply auto |
|
300 |
defer 1 |
|
301 |
apply (rename_tac F) |
|
302 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
303 |
apply (auto intro!: bij_eq_rename simp add: rename_constrains) |
|
304 |
done |
|
305 |
||
306 |
lemma rename_image_stable: "bij h ==> rename h ` stable A = stable (h ` A)" |
|
307 |
apply auto |
|
308 |
defer 1 |
|
309 |
apply (rename_tac F) |
|
310 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
311 |
apply (auto intro!: bij_eq_rename simp add: rename_stable) |
|
312 |
done |
|
313 |
||
314 |
lemma rename_image_increasing: |
|
315 |
"bij h ==> rename h ` increasing func = increasing (func o inv h)" |
|
316 |
apply auto |
|
317 |
defer 1 |
|
318 |
apply (rename_tac F) |
|
319 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
320 |
apply (auto intro!: bij_eq_rename simp add: rename_increasing o_def bij_is_inj) |
|
321 |
done |
|
322 |
||
323 |
lemma rename_image_invariant: |
|
324 |
"bij h ==> rename h ` invariant A = invariant (h ` A)" |
|
325 |
apply auto |
|
326 |
defer 1 |
|
327 |
apply (rename_tac F) |
|
328 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
329 |
apply (auto intro!: bij_eq_rename simp add: rename_invariant) |
|
330 |
done |
|
331 |
||
332 |
lemma rename_image_Constrains: |
|
333 |
"bij h ==> rename h ` (A Co B) = (h ` A) Co (h`B)" |
|
334 |
apply auto |
|
335 |
defer 1 |
|
336 |
apply (rename_tac F) |
|
337 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
338 |
apply (auto intro!: bij_eq_rename simp add: rename_Constrains) |
|
339 |
done |
|
340 |
||
341 |
lemma rename_image_preserves: |
|
342 |
"bij h ==> rename h ` preserves v = preserves (v o inv h)" |
|
343 |
by (simp add: o_def rename_image_stable preserves_def bij_image_INT |
|
344 |
bij_image_Collect_eq) |
|
345 |
||
346 |
lemma rename_image_Stable: |
|
347 |
"bij h ==> rename h ` Stable A = Stable (h ` A)" |
|
348 |
apply auto |
|
349 |
defer 1 |
|
350 |
apply (rename_tac F) |
|
351 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
352 |
apply (auto intro!: bij_eq_rename simp add: rename_Stable) |
|
353 |
done |
|
354 |
||
355 |
lemma rename_image_Increasing: |
|
356 |
"bij h ==> rename h ` Increasing func = Increasing (func o inv h)" |
|
357 |
apply auto |
|
358 |
defer 1 |
|
359 |
apply (rename_tac F) |
|
360 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
361 |
apply (auto intro!: bij_eq_rename simp add: rename_Increasing o_def bij_is_inj) |
|
362 |
done |
|
363 |
||
364 |
lemma rename_image_Always: "bij h ==> rename h ` Always A = Always (h ` A)" |
|
365 |
apply auto |
|
366 |
defer 1 |
|
367 |
apply (rename_tac F) |
|
368 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
369 |
apply (auto intro!: bij_eq_rename simp add: rename_Always) |
|
370 |
done |
|
371 |
||
372 |
lemma rename_image_leadsTo: |
|
373 |
"bij h ==> rename h ` (A leadsTo B) = (h ` A) leadsTo (h`B)" |
|
374 |
apply auto |
|
375 |
defer 1 |
|
376 |
apply (rename_tac F) |
|
377 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
378 |
apply (auto intro!: bij_eq_rename simp add: rename_leadsTo) |
|
379 |
done |
|
380 |
||
381 |
lemma rename_image_LeadsTo: |
|
382 |
"bij h ==> rename h ` (A LeadsTo B) = (h ` A) LeadsTo (h`B)" |
|
383 |
apply auto |
|
384 |
defer 1 |
|
385 |
apply (rename_tac F) |
|
386 |
apply (subgoal_tac "\<exists>G. F = rename h G") |
|
387 |
apply (auto intro!: bij_eq_rename simp add: rename_LeadsTo) |
|
388 |
done |
|
389 |
||
8256
6ba8fa2b0638
Rename: theory for applying a bijection over states to a UNITY program
paulson
parents:
diff
changeset
|
390 |
end |