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