1 (* Title: HOLCF/IOA/meta_theory/Traces.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 header {* Executions and Traces of I/O automata in HOLCF *} |
|
6 |
|
7 theory Traces |
|
8 imports Sequence Automata |
|
9 begin |
|
10 |
|
11 default_sort type |
|
12 |
|
13 types |
|
14 ('a,'s)pairs = "('a * 's) Seq" |
|
15 ('a,'s)execution = "'s * ('a,'s)pairs" |
|
16 'a trace = "'a Seq" |
|
17 |
|
18 ('a,'s)execution_module = "('a,'s)execution set * 'a signature" |
|
19 'a schedule_module = "'a trace set * 'a signature" |
|
20 'a trace_module = "'a trace set * 'a signature" |
|
21 |
|
22 consts |
|
23 |
|
24 (* Executions *) |
|
25 |
|
26 is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr" |
|
27 is_exec_frag ::"[('a,'s)ioa, ('a,'s)execution] => bool" |
|
28 has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool" |
|
29 executions :: "('a,'s)ioa => ('a,'s)execution set" |
|
30 |
|
31 (* Schedules and traces *) |
|
32 filter_act ::"('a,'s)pairs -> 'a trace" |
|
33 has_schedule :: "[('a,'s)ioa, 'a trace] => bool" |
|
34 has_trace :: "[('a,'s)ioa, 'a trace] => bool" |
|
35 schedules :: "('a,'s)ioa => 'a trace set" |
|
36 traces :: "('a,'s)ioa => 'a trace set" |
|
37 mk_trace :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace" |
|
38 |
|
39 laststate ::"('a,'s)execution => 's" |
|
40 |
|
41 (* A predicate holds infinitely (finitely) often in a sequence *) |
|
42 |
|
43 inf_often ::"('a => bool) => 'a Seq => bool" |
|
44 fin_often ::"('a => bool) => 'a Seq => bool" |
|
45 |
|
46 (* fairness of executions *) |
|
47 |
|
48 wfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" |
|
49 sfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" |
|
50 is_wfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool" |
|
51 is_sfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool" |
|
52 fair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" |
|
53 |
|
54 (* fair behavior sets *) |
|
55 |
|
56 fairexecutions ::"('a,'s)ioa => ('a,'s)execution set" |
|
57 fairtraces ::"('a,'s)ioa => 'a trace set" |
|
58 |
|
59 (* Notions of implementation *) |
|
60 ioa_implements :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "=<|" 12) |
|
61 fair_implements :: "('a,'s1)ioa => ('a,'s2)ioa => bool" |
|
62 |
|
63 (* Execution, schedule and trace modules *) |
|
64 Execs :: "('a,'s)ioa => ('a,'s)execution_module" |
|
65 Scheds :: "('a,'s)ioa => 'a schedule_module" |
|
66 Traces :: "('a,'s)ioa => 'a trace_module" |
|
67 |
|
68 |
|
69 defs |
|
70 |
|
71 |
|
72 (* ------------------- Executions ------------------------------ *) |
|
73 |
|
74 |
|
75 is_exec_frag_def: |
|
76 "is_exec_frag A ex == ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)" |
|
77 |
|
78 |
|
79 is_exec_fragC_def: |
|
80 "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of |
|
81 nil => TT |
|
82 | x##xs => (flift1 |
|
83 (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) |
|
84 $x) |
|
85 )))" |
|
86 |
|
87 |
|
88 |
|
89 executions_def: |
|
90 "executions ioa == {e. ((fst e) : starts_of(ioa)) & |
|
91 is_exec_frag ioa e}" |
|
92 |
|
93 |
|
94 (* ------------------- Schedules ------------------------------ *) |
|
95 |
|
96 |
|
97 filter_act_def: |
|
98 "filter_act == Map fst" |
|
99 |
|
100 has_schedule_def: |
|
101 "has_schedule ioa sch == |
|
102 (? ex:executions ioa. sch = filter_act$(snd ex))" |
|
103 |
|
104 schedules_def: |
|
105 "schedules ioa == {sch. has_schedule ioa sch}" |
|
106 |
|
107 |
|
108 (* ------------------- Traces ------------------------------ *) |
|
109 |
|
110 has_trace_def: |
|
111 "has_trace ioa tr == |
|
112 (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)" |
|
113 |
|
114 traces_def: |
|
115 "traces ioa == {tr. has_trace ioa tr}" |
|
116 |
|
117 |
|
118 mk_trace_def: |
|
119 "mk_trace ioa == LAM tr. |
|
120 Filter (%a. a:ext(ioa))$(filter_act$tr)" |
|
121 |
|
122 |
|
123 (* ------------------- Fair Traces ------------------------------ *) |
|
124 |
|
125 laststate_def: |
|
126 "laststate ex == case Last$(snd ex) of |
|
127 UU => fst ex |
|
128 | Def at => snd at" |
|
129 |
|
130 inf_often_def: |
|
131 "inf_often P s == Infinite (Filter P$s)" |
|
132 |
|
133 (* filtering P yields a finite or partial sequence *) |
|
134 fin_often_def: |
|
135 "fin_often P s == ~inf_often P s" |
|
136 |
|
137 (* Note that partial execs cannot be wfair as the inf_often predicate in the |
|
138 else branch prohibits it. However they can be sfair in the case when all W |
|
139 are only finitely often enabled: Is this the right model? |
|
140 See LiveIOA for solution conforming with the literature and superseding this one *) |
|
141 wfair_ex_def: |
|
142 "wfair_ex A ex == ! W : wfair_of A. |
|
143 if Finite (snd ex) |
|
144 then ~Enabled A W (laststate ex) |
|
145 else is_wfair A W ex" |
|
146 |
|
147 is_wfair_def: |
|
148 "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex) |
|
149 | inf_often (%x.~Enabled A W (snd x)) (snd ex))" |
|
150 |
|
151 sfair_ex_def: |
|
152 "sfair_ex A ex == ! W : sfair_of A. |
|
153 if Finite (snd ex) |
|
154 then ~Enabled A W (laststate ex) |
|
155 else is_sfair A W ex" |
|
156 |
|
157 is_sfair_def: |
|
158 "is_sfair A W ex == (inf_often (%x. fst x:W) (snd ex) |
|
159 | fin_often (%x. Enabled A W (snd x)) (snd ex))" |
|
160 |
|
161 fair_ex_def: |
|
162 "fair_ex A ex == wfair_ex A ex & sfair_ex A ex" |
|
163 |
|
164 fairexecutions_def: |
|
165 "fairexecutions A == {ex. ex:executions A & fair_ex A ex}" |
|
166 |
|
167 fairtraces_def: |
|
168 "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}" |
|
169 |
|
170 |
|
171 (* ------------------- Implementation ------------------------------ *) |
|
172 |
|
173 ioa_implements_def: |
|
174 "ioa1 =<| ioa2 == |
|
175 (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & |
|
176 (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) & |
|
177 traces(ioa1) <= traces(ioa2))" |
|
178 |
|
179 fair_implements_def: |
|
180 "fair_implements C A == inp(C) = inp(A) & out(C)=out(A) & |
|
181 fairtraces(C) <= fairtraces(A)" |
|
182 |
|
183 (* ------------------- Modules ------------------------------ *) |
|
184 |
|
185 Execs_def: |
|
186 "Execs A == (executions A, asig_of A)" |
|
187 |
|
188 Scheds_def: |
|
189 "Scheds A == (schedules A, asig_of A)" |
|
190 |
|
191 Traces_def: |
|
192 "Traces A == (traces A,asig_of A)" |
|
193 |
|
194 |
|
195 lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex |
|
196 declare Let_def [simp] |
|
197 declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *} |
|
198 |
|
199 lemmas exec_rws = executions_def is_exec_frag_def |
|
200 |
|
201 |
|
202 |
|
203 subsection "recursive equations of operators" |
|
204 |
|
205 (* ---------------------------------------------------------------- *) |
|
206 (* filter_act *) |
|
207 (* ---------------------------------------------------------------- *) |
|
208 |
|
209 |
|
210 lemma filter_act_UU: "filter_act$UU = UU" |
|
211 apply (simp add: filter_act_def) |
|
212 done |
|
213 |
|
214 lemma filter_act_nil: "filter_act$nil = nil" |
|
215 apply (simp add: filter_act_def) |
|
216 done |
|
217 |
|
218 lemma filter_act_cons: "filter_act$(x>>xs) = (fst x) >> filter_act$xs" |
|
219 apply (simp add: filter_act_def) |
|
220 done |
|
221 |
|
222 declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp] |
|
223 |
|
224 |
|
225 (* ---------------------------------------------------------------- *) |
|
226 (* mk_trace *) |
|
227 (* ---------------------------------------------------------------- *) |
|
228 |
|
229 lemma mk_trace_UU: "mk_trace A$UU=UU" |
|
230 apply (simp add: mk_trace_def) |
|
231 done |
|
232 |
|
233 lemma mk_trace_nil: "mk_trace A$nil=nil" |
|
234 apply (simp add: mk_trace_def) |
|
235 done |
|
236 |
|
237 lemma mk_trace_cons: "mk_trace A$(at >> xs) = |
|
238 (if ((fst at):ext A) |
|
239 then (fst at) >> (mk_trace A$xs) |
|
240 else mk_trace A$xs)" |
|
241 |
|
242 apply (simp add: mk_trace_def) |
|
243 done |
|
244 |
|
245 declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp] |
|
246 |
|
247 (* ---------------------------------------------------------------- *) |
|
248 (* is_exec_fragC *) |
|
249 (* ---------------------------------------------------------------- *) |
|
250 |
|
251 |
|
252 lemma is_exec_fragC_unfold: "is_exec_fragC A = (LAM ex. (%s. case ex of |
|
253 nil => TT |
|
254 | x##xs => (flift1 |
|
255 (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p)) |
|
256 $x) |
|
257 ))" |
|
258 apply (rule trans) |
|
259 apply (rule fix_eq2) |
|
260 apply (rule is_exec_fragC_def) |
|
261 apply (rule beta_cfun) |
|
262 apply (simp add: flift1_def) |
|
263 done |
|
264 |
|
265 lemma is_exec_fragC_UU: "(is_exec_fragC A$UU) s=UU" |
|
266 apply (subst is_exec_fragC_unfold) |
|
267 apply simp |
|
268 done |
|
269 |
|
270 lemma is_exec_fragC_nil: "(is_exec_fragC A$nil) s = TT" |
|
271 apply (subst is_exec_fragC_unfold) |
|
272 apply simp |
|
273 done |
|
274 |
|
275 lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr>>xs)) s = |
|
276 (Def ((s,pr):trans_of A) |
|
277 andalso (is_exec_fragC A$xs)(snd pr))" |
|
278 apply (rule trans) |
|
279 apply (subst is_exec_fragC_unfold) |
|
280 apply (simp add: Consq_def flift1_def) |
|
281 apply simp |
|
282 done |
|
283 |
|
284 |
|
285 declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp] |
|
286 |
|
287 |
|
288 (* ---------------------------------------------------------------- *) |
|
289 (* is_exec_frag *) |
|
290 (* ---------------------------------------------------------------- *) |
|
291 |
|
292 lemma is_exec_frag_UU: "is_exec_frag A (s, UU)" |
|
293 apply (simp add: is_exec_frag_def) |
|
294 done |
|
295 |
|
296 lemma is_exec_frag_nil: "is_exec_frag A (s, nil)" |
|
297 apply (simp add: is_exec_frag_def) |
|
298 done |
|
299 |
|
300 lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)>>ex) = |
|
301 (((s,a,t):trans_of A) & |
|
302 is_exec_frag A (t, ex))" |
|
303 apply (simp add: is_exec_frag_def) |
|
304 done |
|
305 |
|
306 |
|
307 (* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *) |
|
308 declare is_exec_frag_UU [simp] is_exec_frag_nil [simp] is_exec_frag_cons [simp] |
|
309 |
|
310 (* ---------------------------------------------------------------------------- *) |
|
311 section "laststate" |
|
312 (* ---------------------------------------------------------------------------- *) |
|
313 |
|
314 lemma laststate_UU: "laststate (s,UU) = s" |
|
315 apply (simp add: laststate_def) |
|
316 done |
|
317 |
|
318 lemma laststate_nil: "laststate (s,nil) = s" |
|
319 apply (simp add: laststate_def) |
|
320 done |
|
321 |
|
322 lemma laststate_cons: "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)" |
|
323 apply (simp (no_asm) add: laststate_def) |
|
324 apply (case_tac "ex=nil") |
|
325 apply (simp (no_asm_simp)) |
|
326 apply (simp (no_asm_simp)) |
|
327 apply (drule Finite_Last1 [THEN mp]) |
|
328 apply assumption |
|
329 apply defined |
|
330 done |
|
331 |
|
332 declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp] |
|
333 |
|
334 lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)" |
|
335 apply (tactic "Seq_Finite_induct_tac @{context} 1") |
|
336 done |
|
337 |
|
338 |
|
339 subsection "has_trace, mk_trace" |
|
340 |
|
341 (* alternative definition of has_trace tailored for the refinement proof, as it does not |
|
342 take the detour of schedules *) |
|
343 |
|
344 lemma has_trace_def2: |
|
345 "has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))" |
|
346 apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def) |
|
347 apply auto |
|
348 done |
|
349 |
|
350 |
|
351 subsection "signatures and executions, schedules" |
|
352 |
|
353 (* All executions of A have only actions of A. This is only true because of the |
|
354 predicate state_trans (part of the predicate IOA): We have no dependent types. |
|
355 For executions of parallel automata this assumption is not needed, as in par_def |
|
356 this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *) |
|
357 |
|
358 lemma execfrag_in_sig: |
|
359 "!! A. is_trans_of A ==> |
|
360 ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)" |
|
361 apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, |
|
362 @{thm Forall_def}, @{thm sforall_def}] 1 *}) |
|
363 (* main case *) |
|
364 apply (auto simp add: is_trans_of_def) |
|
365 done |
|
366 |
|
367 lemma exec_in_sig: |
|
368 "!! A.[| is_trans_of A; x:executions A |] ==> |
|
369 Forall (%a. a:act A) (filter_act$(snd x))" |
|
370 apply (simp add: executions_def) |
|
371 apply (tactic {* pair_tac @{context} "x" 1 *}) |
|
372 apply (rule execfrag_in_sig [THEN spec, THEN mp]) |
|
373 apply auto |
|
374 done |
|
375 |
|
376 lemma scheds_in_sig: |
|
377 "!! A.[| is_trans_of A; x:schedules A |] ==> |
|
378 Forall (%a. a:act A) x" |
|
379 apply (unfold schedules_def has_schedule_def) |
|
380 apply (fast intro!: exec_in_sig) |
|
381 done |
|
382 |
|
383 |
|
384 subsection "executions are prefix closed" |
|
385 |
|
386 (* only admissible in y, not if done in x !! *) |
|
387 lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x --> is_exec_frag A (s,y)" |
|
388 apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *}) |
|
389 apply (intro strip) |
|
390 apply (tactic {* Seq_case_simp_tac @{context} "xa" 1 *}) |
|
391 apply (tactic {* pair_tac @{context} "a" 1 *}) |
|
392 apply auto |
|
393 done |
|
394 |
|
395 lemmas exec_prefixclosed = |
|
396 conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp], standard] |
|
397 |
|
398 |
|
399 (* second prefix notion for Finite x *) |
|
400 |
|
401 lemma exec_prefix2closed [rule_format]: |
|
402 "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)" |
|
403 apply (tactic {* pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1 *}) |
|
404 apply (intro strip) |
|
405 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
|
406 apply (tactic {* pair_tac @{context} "a" 1 *}) |
|
407 apply auto |
|
408 done |
|
409 |
|
410 end |
|