author  wenzelm 
Wed, 19 Mar 2008 22:47:35 +0100  
changeset 26339  7825c83c9eff 
parent 22808  a7daa74e2980 
child 26359  6d437bde2f1d 
permissions  rwrr 
3071  1 
(* Title: HOLCF/IOA/meta_theory/Traces.thy 
3275  2 
ID: $Id$ 
12218  3 
Author: Olaf Müller 
17233  4 
*) 
3071  5 

17233  6 
header {* Executions and Traces of I/O automata in HOLCF *} 
3071  7 

17233  8 
theory Traces 
9 
imports Sequence Automata 

10 
begin 

3071  11 

17233  12 
defaultsort type 
13 

14 
types 

3071  15 
('a,'s)pairs = "('a * 's) Seq" 
16 
('a,'s)execution = "'s * ('a,'s)pairs" 

17 
'a trace = "'a Seq" 

3521  18 

19 
('a,'s)execution_module = "('a,'s)execution set * 'a signature" 

20 
'a schedule_module = "'a trace set * 'a signature" 

21 
'a trace_module = "'a trace set * 'a signature" 

17233  22 

3071  23 
consts 
24 

25 
(* Executions *) 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

26 

17233  27 
is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs > 's => tr" 
28 
is_exec_frag ::"[('a,'s)ioa, ('a,'s)execution] => bool" 

3071  29 
has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool" 
30 
executions :: "('a,'s)ioa => ('a,'s)execution set" 

31 

32 
(* Schedules and traces *) 

33 
filter_act ::"('a,'s)pairs > 'a trace" 

17233  34 
has_schedule :: "[('a,'s)ioa, 'a trace] => bool" 
3071  35 
has_trace :: "[('a,'s)ioa, 'a trace] => bool" 
17233  36 
schedules :: "('a,'s)ioa => 'a trace set" 
3071  37 
traces :: "('a,'s)ioa => 'a trace set" 
38 
mk_trace :: "('a,'s)ioa => ('a,'s)pairs > 'a trace" 

39 

4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

40 
laststate ::"('a,'s)execution => 's" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

41 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

42 
(* A predicate holds infinitely (finitely) often in a sequence *) 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

43 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

44 
inf_often ::"('a => bool) => 'a Seq => bool" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

45 
fin_often ::"('a => bool) => 'a Seq => bool" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

46 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

47 
(* fairness of executions *) 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

48 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

49 
wfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

50 
sfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

51 
is_wfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

52 
is_sfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

53 
fair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

54 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

55 
(* fair behavior sets *) 
17233  56 

4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

57 
fairexecutions ::"('a,'s)ioa => ('a,'s)execution set" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

58 
fairtraces ::"('a,'s)ioa => 'a trace set" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

59 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

60 
(* Notions of implementation *) 
22808  61 
ioa_implements :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "=<" 12) 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

62 
fair_implements :: "('a,'s1)ioa => ('a,'s2)ioa => bool" 
3071  63 

3521  64 
(* Execution, schedule and trace modules *) 
65 
Execs :: "('a,'s)ioa => ('a,'s)execution_module" 

66 
Scheds :: "('a,'s)ioa => 'a schedule_module" 

67 
Traces :: "('a,'s)ioa => 'a trace_module" 

68 

3071  69 

70 
defs 

71 

72 

73 
(*  Executions  *) 

74 

75 

17233  76 
is_exec_frag_def: 
10835  77 
"is_exec_frag A ex == ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)" 
3071  78 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

79 

17233  80 
is_exec_fragC_def: 
81 
"is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of 

3071  82 
nil => TT 
17233  83 
 x##xs => (flift1 
84 
(%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) 

10835  85 
$x) 
17233  86 
)))" 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

87 

2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

88 

2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

89 

17233  90 
executions_def: 
91 
"executions ioa == {e. ((fst e) : starts_of(ioa)) & 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset

92 
is_exec_frag ioa e}" 
3071  93 

94 

95 
(*  Schedules  *) 

96 

97 

17233  98 
filter_act_def: 
3071  99 
"filter_act == Map fst" 
100 

17233  101 
has_schedule_def: 
102 
"has_schedule ioa sch == 

10835  103 
(? ex:executions ioa. sch = filter_act$(snd ex))" 
3071  104 

17233  105 
schedules_def: 
3071  106 
"schedules ioa == {sch. has_schedule ioa sch}" 
107 

108 

109 
(*  Traces  *) 

110 

17233  111 
has_trace_def: 
112 
"has_trace ioa tr == 

10835  113 
(? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)" 
17233  114 

115 
traces_def: 

3071  116 
"traces ioa == {tr. has_trace ioa tr}" 
117 

118 

17233  119 
mk_trace_def: 
120 
"mk_trace ioa == LAM tr. 

10835  121 
Filter (%a. a:ext(ioa))$(filter_act$tr)" 
3071  122 

123 

4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

124 
(*  Fair Traces  *) 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

125 

17233  126 
laststate_def: 
10835  127 
"laststate ex == case Last$(snd ex) of 
12028  128 
UU => fst ex 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

129 
 Def at => snd at" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

130 

17233  131 
inf_often_def: 
10835  132 
"inf_often P s == Infinite (Filter P$s)" 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

133 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

134 
(* filtering P yields a finite or partial sequence *) 
17233  135 
fin_often_def: 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

136 
"fin_often P s == ~inf_often P s" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

137 

17233  138 
(* Note that partial execs cannot be wfair as the inf_often predicate in the 
139 
else branch prohibits it. However they can be sfair in the case when all W 

140 
are only finitely often enabled: Is this the right model? 

5976  141 
See LiveIOA for solution conforming with the literature and superseding this one *) 
17233  142 
wfair_ex_def: 
143 
"wfair_ex A ex == ! W : wfair_of A. 

144 
if Finite (snd ex) 

4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

145 
then ~Enabled A W (laststate ex) 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

146 
else is_wfair A W ex" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

147 

17233  148 
is_wfair_def: 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

149 
"is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex) 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

150 
 inf_often (%x.~Enabled A W (snd x)) (snd ex))" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

151 

17233  152 
sfair_ex_def: 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

153 
"sfair_ex A ex == ! W : sfair_of A. 
17233  154 
if Finite (snd ex) 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

155 
then ~Enabled A W (laststate ex) 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

156 
else is_sfair A W ex" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

157 

17233  158 
is_sfair_def: 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

159 
"is_sfair A W ex == (inf_often (%x. fst x:W) (snd ex) 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

160 
 fin_often (%x. Enabled A W (snd x)) (snd ex))" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

161 

17233  162 
fair_ex_def: 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

163 
"fair_ex A ex == wfair_ex A ex & sfair_ex A ex" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

164 

17233  165 
fairexecutions_def: 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

166 
"fairexecutions A == {ex. ex:executions A & fair_ex A ex}" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

167 

17233  168 
fairtraces_def: 
10835  169 
"fairtraces A == {mk_trace A$(snd ex)  ex. ex:fairexecutions A}" 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

170 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

171 

3071  172 
(*  Implementation  *) 
173 

17233  174 
ioa_implements_def: 
175 
"ioa1 =< ioa2 == 

176 
(((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & 

3071  177 
(outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) & 
178 
traces(ioa1) <= traces(ioa2))" 

179 

17233  180 
fair_implements_def: 
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

181 
"fair_implements C A == inp(C) = inp(A) & out(C)=out(A) & 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

182 
fairtraces(C) <= fairtraces(A)" 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset

183 

3521  184 
(*  Modules  *) 
185 

17233  186 
Execs_def: 
3521  187 
"Execs A == (executions A, asig_of A)" 
188 

17233  189 
Scheds_def: 
3521  190 
"Scheds A == (schedules A, asig_of A)" 
191 

17233  192 
Traces_def: 
3521  193 
"Traces A == (traces A,asig_of A)" 
194 

19741  195 

196 
lemmas [simp del] = ex_simps all_simps split_paired_Ex 

197 
declare Let_def [simp] 

26339  198 
declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *} 
19741  199 

200 
lemmas exec_rws = executions_def is_exec_frag_def 

201 

202 

203 

204 
subsection "recursive equations of operators" 

205 

206 
(*  *) 

207 
(* filter_act *) 

208 
(*  *) 

209 

210 

211 
lemma filter_act_UU: "filter_act$UU = UU" 

212 
apply (simp add: filter_act_def) 

213 
done 

214 

215 
lemma filter_act_nil: "filter_act$nil = nil" 

216 
apply (simp add: filter_act_def) 

217 
done 

218 

219 
lemma filter_act_cons: "filter_act$(x>>xs) = (fst x) >> filter_act$xs" 

220 
apply (simp add: filter_act_def) 

221 
done 

222 

223 
declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp] 

224 

225 

226 
(*  *) 

227 
(* mk_trace *) 

228 
(*  *) 

229 

230 
lemma mk_trace_UU: "mk_trace A$UU=UU" 

231 
apply (simp add: mk_trace_def) 

232 
done 

233 

234 
lemma mk_trace_nil: "mk_trace A$nil=nil" 

235 
apply (simp add: mk_trace_def) 

236 
done 

237 

238 
lemma mk_trace_cons: "mk_trace A$(at >> xs) = 

239 
(if ((fst at):ext A) 

240 
then (fst at) >> (mk_trace A$xs) 

241 
else mk_trace A$xs)" 

242 

243 
apply (simp add: mk_trace_def) 

244 
done 

245 

246 
declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp] 

247 

248 
(*  *) 

249 
(* is_exec_fragC *) 

250 
(*  *) 

251 

252 

253 
lemma is_exec_fragC_unfold: "is_exec_fragC A = (LAM ex. (%s. case ex of 

254 
nil => TT 

255 
 x##xs => (flift1 

256 
(%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p)) 

257 
$x) 

258 
))" 

259 
apply (rule trans) 

260 
apply (rule fix_eq2) 

261 
apply (rule is_exec_fragC_def) 

262 
apply (rule beta_cfun) 

263 
apply (simp add: flift1_def) 

264 
done 

265 

266 
lemma is_exec_fragC_UU: "(is_exec_fragC A$UU) s=UU" 

267 
apply (subst is_exec_fragC_unfold) 

268 
apply simp 

269 
done 

270 

271 
lemma is_exec_fragC_nil: "(is_exec_fragC A$nil) s = TT" 

272 
apply (subst is_exec_fragC_unfold) 

273 
apply simp 

274 
done 

275 

276 
lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr>>xs)) s = 

277 
(Def ((s,pr):trans_of A) 

278 
andalso (is_exec_fragC A$xs)(snd pr))" 

279 
apply (rule trans) 

280 
apply (subst is_exec_fragC_unfold) 

281 
apply (simp add: Consq_def flift1_def) 

282 
apply simp 

283 
done 

284 

285 

286 
declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp] 

287 

288 

289 
(*  *) 

290 
(* is_exec_frag *) 

291 
(*  *) 

292 

293 
lemma is_exec_frag_UU: "is_exec_frag A (s, UU)" 

294 
apply (simp add: is_exec_frag_def) 

295 
done 

296 

297 
lemma is_exec_frag_nil: "is_exec_frag A (s, nil)" 

298 
apply (simp add: is_exec_frag_def) 

299 
done 

300 

301 
lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)>>ex) = 

302 
(((s,a,t):trans_of A) & 

303 
is_exec_frag A (t, ex))" 

304 
apply (simp add: is_exec_frag_def) 

305 
done 

306 

307 

308 
(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *) 

309 
declare is_exec_frag_UU [simp] is_exec_frag_nil [simp] is_exec_frag_cons [simp] 

310 

311 
(*  *) 

312 
section "laststate" 

313 
(*  *) 

314 

315 
lemma laststate_UU: "laststate (s,UU) = s" 

316 
apply (simp add: laststate_def) 

317 
done 

318 

319 
lemma laststate_nil: "laststate (s,nil) = s" 

320 
apply (simp add: laststate_def) 

321 
done 

322 

323 
lemma laststate_cons: "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)" 

324 
apply (simp (no_asm) add: laststate_def) 

325 
apply (case_tac "ex=nil") 

326 
apply (simp (no_asm_simp)) 

327 
apply (simp (no_asm_simp)) 

328 
apply (drule Finite_Last1 [THEN mp]) 

329 
apply assumption 

330 
apply (tactic "def_tac 1") 

331 
done 

332 

333 
declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp] 

334 

335 
lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)" 

336 
apply (tactic "Seq_Finite_induct_tac 1") 

337 
done 

338 

339 

340 
subsection "has_trace, mk_trace" 

341 

342 
(* alternative definition of has_trace tailored for the refinement proof, as it does not 

343 
take the detour of schedules *) 

344 

345 
lemma has_trace_def2: 

346 
"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))" 

347 
apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def) 

348 
apply (tactic "safe_tac set_cs") 

349 
(* 1 *) 

350 
apply (rule_tac x = "ex" in bexI) 

351 
apply (simplesubst beta_cfun) 

352 
apply (tactic "cont_tacR 1") 

353 
apply (simp (no_asm)) 

354 
apply (simp (no_asm_simp)) 

355 
(* 2 *) 

356 
apply (rule_tac x = "filter_act$ (snd ex) " in bexI) 

357 
apply (simplesubst beta_cfun) 

358 
apply (tactic "cont_tacR 1") 

359 
apply (simp (no_asm)) 

360 
apply (tactic "safe_tac set_cs") 

361 
apply (rule_tac x = "ex" in bexI) 

362 
apply simp_all 

363 
done 

364 

365 

366 
subsection "signatures and executions, schedules" 

367 

368 
(* All executions of A have only actions of A. This is only true because of the 

369 
predicate state_trans (part of the predicate IOA): We have no dependent types. 

370 
For executions of parallel automata this assumption is not needed, as in par_def 

371 
this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *) 

372 

373 
lemma execfrag_in_sig: 

374 
"!! A. is_trans_of A ==> 

375 
! s. is_exec_frag A (s,xs) > Forall (%a. a:act A) (filter_act$xs)" 

376 
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def", 

377 
thm "Forall_def", thm "sforall_def"] 1 *}) 

378 
(* main case *) 

379 
apply (rename_tac ss a t) 

380 
apply (tactic "safe_tac set_cs") 

381 
apply (simp_all add: is_trans_of_def) 

382 
done 

383 

384 
lemma exec_in_sig: 

385 
"!! A.[ is_trans_of A; x:executions A ] ==> 

386 
Forall (%a. a:act A) (filter_act$(snd x))" 

387 
apply (simp add: executions_def) 

388 
apply (tactic {* pair_tac "x" 1 *}) 

389 
apply (rule execfrag_in_sig [THEN spec, THEN mp]) 

390 
apply auto 

391 
done 

392 

393 
lemma scheds_in_sig: 

394 
"!! A.[ is_trans_of A; x:schedules A ] ==> 

395 
Forall (%a. a:act A) x" 

396 
apply (unfold schedules_def has_schedule_def) 

397 
apply (fast intro!: exec_in_sig) 

398 
done 

399 

400 

401 
subsection "executions are prefix closed" 

402 

403 
(* only admissible in y, not if done in x !! *) 

404 
lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x > is_exec_frag A (s,y)" 

405 
apply (tactic {* pair_induct_tac "y" [thm "is_exec_frag_def"] 1 *}) 

406 
apply (intro strip) 

407 
apply (tactic {* Seq_case_simp_tac "xa" 1 *}) 

408 
apply (tactic {* pair_tac "a" 1 *}) 

409 
apply auto 

410 
done 

411 

412 
lemmas exec_prefixclosed = 

413 
conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp], standard] 

414 

415 

416 
(* second prefix notion for Finite x *) 

417 

418 
lemma exec_prefix2closed [rule_format]: 

419 
"! y s. is_exec_frag A (s,x@@y) > is_exec_frag A (s,x)" 

420 
apply (tactic {* pair_induct_tac "x" [thm "is_exec_frag_def"] 1 *}) 

421 
apply (intro strip) 

422 
apply (tactic {* Seq_case_simp_tac "s" 1 *}) 

423 
apply (tactic {* pair_tac "a" 1 *}) 

424 
apply auto 

425 
done 

426 

3071  427 

17233  428 
end 