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