author | wenzelm |
Sun, 28 May 2006 19:54:20 +0200 | |
changeset 19741 | f65265d71426 |
parent 17233 | 41eee2e7b465 |
child 25135 | 4f8176c940cf |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
3071 | 4 |
*) |
5 |
||
17233 | 6 |
header {* Correctness of Refinement Mappings in HOLCF/IOA *} |
3071 | 7 |
|
17233 | 8 |
theory RefCorrectness |
9 |
imports RefMappings |
|
10 |
begin |
|
11 |
||
3071 | 12 |
consts |
13 |
||
17233 | 14 |
corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) => |
3071 | 15 |
('a,'s1)execution => ('a,'s2)execution" |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
16 |
corresp_exC ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
17 |
-> ('s1 => ('a,'s2)pairs)" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
18 |
is_fair_ref_map :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool" |
3071 | 19 |
|
20 |
defs |
|
21 |
||
17233 | 22 |
corresp_ex_def: |
10835 | 23 |
"corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))" |
3071 | 24 |
|
25 |
||
17233 | 26 |
corresp_exC_def: |
27 |
"corresp_exC A f == (fix$(LAM h ex. (%s. case ex of |
|
3071 | 28 |
nil => nil |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
29 |
| x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) |
10835 | 30 |
@@ ((h$xs) (snd pr))) |
31 |
$x) )))" |
|
17233 | 32 |
|
33 |
is_fair_ref_map_def: |
|
34 |
"is_fair_ref_map f C A == |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
35 |
is_ref_map f C A & |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
36 |
(! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
37 |
|
3071 | 38 |
|
39 |
||
17233 | 40 |
axioms |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
41 |
(* Axioms for fair trace inclusion proof support, not for the correctness proof |
17233 | 42 |
of refinement mappings! |
5976 | 43 |
Note: Everything is superseded by LiveIOA.thy! *) |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
44 |
|
17233 | 45 |
corresp_laststate: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
46 |
"Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
47 |
|
17233 | 48 |
corresp_Finite: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
49 |
"Finite (snd (corresp_ex A f (s,ex))) = Finite ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
50 |
|
17233 | 51 |
FromAtoC: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
52 |
"fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
53 |
|
17233 | 54 |
FromCtoA: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
55 |
"inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
56 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
57 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
58 |
(* Proof by case on inf W in ex: If so, ok. If not, only fin W in ex, ie there is |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
59 |
an index i from which on no W in ex. But W inf enabled, ie at least once after i |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
60 |
W is enabled. As W does not occur after i and W is enabling_persistent, W keeps |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
61 |
enabled until infinity, ie. indefinitely *) |
17233 | 62 |
persistent: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
63 |
"[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|] |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
64 |
==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
65 |
|
17233 | 66 |
infpostcond: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
67 |
"[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|] |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
68 |
==> inf_often (% x. set_was_enabled A W (snd x)) ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
69 |
|
19741 | 70 |
|
71 |
subsection "corresp_ex" |
|
72 |
||
73 |
lemma corresp_exC_unfold: "corresp_exC A f = (LAM ex. (%s. case ex of |
|
74 |
nil => nil |
|
75 |
| x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) |
|
76 |
@@ ((corresp_exC A f $xs) (snd pr))) |
|
77 |
$x) ))" |
|
78 |
apply (rule trans) |
|
79 |
apply (rule fix_eq2) |
|
80 |
apply (rule corresp_exC_def) |
|
81 |
apply (rule beta_cfun) |
|
82 |
apply (simp add: flift1_def) |
|
83 |
done |
|
84 |
||
85 |
lemma corresp_exC_UU: "(corresp_exC A f$UU) s=UU" |
|
86 |
apply (subst corresp_exC_unfold) |
|
87 |
apply simp |
|
88 |
done |
|
89 |
||
90 |
lemma corresp_exC_nil: "(corresp_exC A f$nil) s = nil" |
|
91 |
apply (subst corresp_exC_unfold) |
|
92 |
apply simp |
|
93 |
done |
|
94 |
||
95 |
lemma corresp_exC_cons: "(corresp_exC A f$(at>>xs)) s = |
|
96 |
(@cex. move A cex (f s) (fst at) (f (snd at))) |
|
97 |
@@ ((corresp_exC A f$xs) (snd at))" |
|
98 |
apply (rule trans) |
|
99 |
apply (subst corresp_exC_unfold) |
|
100 |
apply (simp add: Consq_def flift1_def) |
|
101 |
apply simp |
|
102 |
done |
|
103 |
||
104 |
||
105 |
declare corresp_exC_UU [simp] corresp_exC_nil [simp] corresp_exC_cons [simp] |
|
106 |
||
107 |
||
108 |
||
109 |
subsection "properties of move" |
|
110 |
||
111 |
lemma move_is_move: |
|
112 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
|
113 |
move A (@x. move A x (f s) a (f t)) (f s) a (f t)" |
|
114 |
apply (unfold is_ref_map_def) |
|
115 |
apply (subgoal_tac "? ex. move A ex (f s) a (f t) ") |
|
116 |
prefer 2 |
|
117 |
apply simp |
|
118 |
apply (erule exE) |
|
119 |
apply (rule someI) |
|
120 |
apply assumption |
|
121 |
done |
|
122 |
||
123 |
lemma move_subprop1: |
|
124 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
|
125 |
is_exec_frag A (f s,@x. move A x (f s) a (f t))" |
|
126 |
apply (cut_tac move_is_move) |
|
127 |
defer |
|
128 |
apply assumption+ |
|
129 |
apply (simp add: move_def) |
|
130 |
done |
|
131 |
||
132 |
lemma move_subprop2: |
|
133 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
|
134 |
Finite ((@x. move A x (f s) a (f t)))" |
|
135 |
apply (cut_tac move_is_move) |
|
136 |
defer |
|
137 |
apply assumption+ |
|
138 |
apply (simp add: move_def) |
|
139 |
done |
|
140 |
||
141 |
lemma move_subprop3: |
|
142 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
|
143 |
laststate (f s,@x. move A x (f s) a (f t)) = (f t)" |
|
144 |
apply (cut_tac move_is_move) |
|
145 |
defer |
|
146 |
apply assumption+ |
|
147 |
apply (simp add: move_def) |
|
148 |
done |
|
149 |
||
150 |
lemma move_subprop4: |
|
151 |
"[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> |
|
152 |
mk_trace A$((@x. move A x (f s) a (f t))) = |
|
153 |
(if a:ext A then a>>nil else nil)" |
|
154 |
apply (cut_tac move_is_move) |
|
155 |
defer |
|
156 |
apply assumption+ |
|
157 |
apply (simp add: move_def) |
|
158 |
done |
|
159 |
||
160 |
||
161 |
(* ------------------------------------------------------------------ *) |
|
162 |
(* The following lemmata contribute to *) |
|
163 |
(* TRACE INCLUSION Part 1: Traces coincide *) |
|
164 |
(* ------------------------------------------------------------------ *) |
|
165 |
||
166 |
section "Lemmata for <==" |
|
167 |
||
168 |
(* --------------------------------------------------- *) |
|
169 |
(* Lemma 1.1: Distribution of mk_trace and @@ *) |
|
170 |
(* --------------------------------------------------- *) |
|
171 |
||
172 |
lemma mk_traceConc: "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)" |
|
173 |
apply (simp add: mk_trace_def filter_act_def FilterConc MapConc) |
|
174 |
done |
|
175 |
||
176 |
||
177 |
||
178 |
(* ------------------------------------------------------ |
|
179 |
Lemma 1 :Traces coincide |
|
180 |
------------------------------------------------------- *) |
|
181 |
declare split_if [split del] |
|
182 |
||
183 |
lemma lemma_1: |
|
184 |
"[|is_ref_map f C A; ext C = ext A|] ==> |
|
185 |
!s. reachable C s & is_exec_frag C (s,xs) --> |
|
186 |
mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))" |
|
187 |
apply (unfold corresp_ex_def) |
|
188 |
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *}) |
|
189 |
(* cons case *) |
|
190 |
apply (tactic "safe_tac set_cs") |
|
191 |
apply (simp add: mk_traceConc) |
|
192 |
apply (frule reachable.reachable_n) |
|
193 |
apply assumption |
|
194 |
apply (erule_tac x = "y" in allE) |
|
195 |
apply simp |
|
196 |
apply (simp add: move_subprop4 split add: split_if) |
|
197 |
done |
|
198 |
||
199 |
declare split_if [split] |
|
200 |
||
201 |
(* ------------------------------------------------------------------ *) |
|
202 |
(* The following lemmata contribute to *) |
|
203 |
(* TRACE INCLUSION Part 2: corresp_ex is execution *) |
|
204 |
(* ------------------------------------------------------------------ *) |
|
205 |
||
206 |
section "Lemmata for ==>" |
|
207 |
||
208 |
(* -------------------------------------------------- *) |
|
209 |
(* Lemma 2.1 *) |
|
210 |
(* -------------------------------------------------- *) |
|
211 |
||
212 |
lemma lemma_2_1 [rule_format (no_asm)]: |
|
213 |
"Finite xs --> |
|
214 |
(!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) & |
|
215 |
t = laststate (s,xs) |
|
216 |
--> is_exec_frag A (s,xs @@ ys))" |
|
217 |
||
218 |
apply (rule impI) |
|
219 |
apply (tactic {* Seq_Finite_induct_tac 1 *}) |
|
220 |
(* main case *) |
|
221 |
apply (tactic "safe_tac set_cs") |
|
222 |
apply (tactic {* pair_tac "a" 1 *}) |
|
223 |
done |
|
224 |
||
225 |
||
226 |
(* ----------------------------------------------------------- *) |
|
227 |
(* Lemma 2 : corresp_ex is execution *) |
|
228 |
(* ----------------------------------------------------------- *) |
|
229 |
||
230 |
||
231 |
||
232 |
lemma lemma_2: |
|
233 |
"[| is_ref_map f C A |] ==> |
|
234 |
!s. reachable C s & is_exec_frag C (s,xs) |
|
235 |
--> is_exec_frag A (corresp_ex A f (s,xs))" |
|
236 |
||
237 |
apply (unfold corresp_ex_def) |
|
238 |
||
239 |
apply simp |
|
240 |
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *}) |
|
241 |
(* main case *) |
|
242 |
apply (tactic "safe_tac set_cs") |
|
243 |
apply (rule_tac t = "f y" in lemma_2_1) |
|
244 |
||
245 |
(* Finite *) |
|
246 |
apply (erule move_subprop2) |
|
247 |
apply assumption+ |
|
248 |
apply (rule conjI) |
|
249 |
||
250 |
(* is_exec_frag *) |
|
251 |
apply (erule move_subprop1) |
|
252 |
apply assumption+ |
|
253 |
apply (rule conjI) |
|
254 |
||
255 |
(* Induction hypothesis *) |
|
256 |
(* reachable_n looping, therefore apply it manually *) |
|
257 |
apply (erule_tac x = "y" in allE) |
|
258 |
apply simp |
|
259 |
apply (frule reachable.reachable_n) |
|
260 |
apply assumption |
|
261 |
apply simp |
|
262 |
(* laststate *) |
|
263 |
apply (erule move_subprop3 [symmetric]) |
|
264 |
apply assumption+ |
|
265 |
done |
|
266 |
||
267 |
||
268 |
subsection "Main Theorem: TRACE - INCLUSION" |
|
269 |
||
270 |
lemma trace_inclusion: |
|
271 |
"[| ext C = ext A; is_ref_map f C A |] |
|
272 |
==> traces C <= traces A" |
|
273 |
||
274 |
apply (unfold traces_def) |
|
275 |
||
276 |
apply (simp (no_asm) add: has_trace_def2) |
|
277 |
apply (tactic "safe_tac set_cs") |
|
278 |
||
279 |
(* give execution of abstract automata *) |
|
280 |
apply (rule_tac x = "corresp_ex A f ex" in bexI) |
|
281 |
||
282 |
(* Traces coincide, Lemma 1 *) |
|
283 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
284 |
apply (erule lemma_1 [THEN spec, THEN mp]) |
|
285 |
apply assumption+ |
|
286 |
apply (simp add: executions_def reachable.reachable_0) |
|
287 |
||
288 |
(* corresp_ex is execution, Lemma 2 *) |
|
289 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
290 |
apply (simp add: executions_def) |
|
291 |
(* start state *) |
|
292 |
apply (rule conjI) |
|
293 |
apply (simp add: is_ref_map_def corresp_ex_def) |
|
294 |
(* is-execution-fragment *) |
|
295 |
apply (erule lemma_2 [THEN spec, THEN mp]) |
|
296 |
apply (simp add: reachable.reachable_0) |
|
297 |
done |
|
298 |
||
299 |
||
300 |
subsection "Corollary: FAIR TRACE - INCLUSION" |
|
301 |
||
302 |
lemma fininf: "(~inf_often P s) = fin_often P s" |
|
303 |
apply (unfold fin_often_def) |
|
304 |
apply auto |
|
305 |
done |
|
306 |
||
307 |
||
308 |
lemma WF_alt: "is_wfair A W (s,ex) = |
|
309 |
(fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)" |
|
310 |
apply (simp add: is_wfair_def fin_often_def) |
|
311 |
apply auto |
|
312 |
done |
|
313 |
||
314 |
lemma WF_persistent: "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; |
|
315 |
en_persistent A W|] |
|
316 |
==> inf_often (%x. fst x :W) ex" |
|
317 |
apply (drule persistent) |
|
318 |
apply assumption |
|
319 |
apply (simp add: WF_alt) |
|
320 |
apply auto |
|
321 |
done |
|
322 |
||
323 |
||
324 |
lemma fair_trace_inclusion: "!! C A. |
|
325 |
[| is_ref_map f C A; ext C = ext A; |
|
326 |
!! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |] |
|
327 |
==> fairtraces C <= fairtraces A" |
|
328 |
apply (simp (no_asm) add: fairtraces_def fairexecutions_def) |
|
329 |
apply (tactic "safe_tac set_cs") |
|
330 |
apply (rule_tac x = "corresp_ex A f ex" in exI) |
|
331 |
apply (tactic "safe_tac set_cs") |
|
332 |
||
333 |
(* Traces coincide, Lemma 1 *) |
|
334 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
335 |
apply (erule lemma_1 [THEN spec, THEN mp]) |
|
336 |
apply assumption+ |
|
337 |
apply (simp add: executions_def reachable.reachable_0) |
|
338 |
||
339 |
(* corresp_ex is execution, Lemma 2 *) |
|
340 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
341 |
apply (simp add: executions_def) |
|
342 |
(* start state *) |
|
343 |
apply (rule conjI) |
|
344 |
apply (simp add: is_ref_map_def corresp_ex_def) |
|
345 |
(* is-execution-fragment *) |
|
346 |
apply (erule lemma_2 [THEN spec, THEN mp]) |
|
347 |
apply (simp add: reachable.reachable_0) |
|
348 |
||
349 |
(* Fairness *) |
|
350 |
apply auto |
|
351 |
done |
|
352 |
||
353 |
lemma fair_trace_inclusion2: "!! C A. |
|
354 |
[| inp(C) = inp(A); out(C)=out(A); |
|
355 |
is_fair_ref_map f C A |] |
|
356 |
==> fair_implements C A" |
|
357 |
apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def) |
|
358 |
apply (tactic "safe_tac set_cs") |
|
359 |
apply (rule_tac x = "corresp_ex A f ex" in exI) |
|
360 |
apply (tactic "safe_tac set_cs") |
|
361 |
(* Traces coincide, Lemma 1 *) |
|
362 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
363 |
apply (erule lemma_1 [THEN spec, THEN mp]) |
|
364 |
apply (simp (no_asm) add: externals_def) |
|
365 |
apply (auto)[1] |
|
366 |
apply (simp add: executions_def reachable.reachable_0) |
|
367 |
||
368 |
(* corresp_ex is execution, Lemma 2 *) |
|
369 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
370 |
apply (simp add: executions_def) |
|
371 |
(* start state *) |
|
372 |
apply (rule conjI) |
|
373 |
apply (simp add: is_ref_map_def corresp_ex_def) |
|
374 |
(* is-execution-fragment *) |
|
375 |
apply (erule lemma_2 [THEN spec, THEN mp]) |
|
376 |
apply (simp add: reachable.reachable_0) |
|
377 |
||
378 |
(* Fairness *) |
|
379 |
apply auto |
|
380 |
done |
|
381 |
||
17233 | 382 |
|
383 |
end |