author | haftmann |
Mon, 08 Feb 2010 17:12:22 +0100 | |
changeset 35045 | a77d200e6503 |
parent 27208 | 5fe899199f85 |
child 35174 | e15040ae75d7 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/LiveIOA.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
17233 | 4 |
*) |
4559 | 5 |
|
17233 | 6 |
header {* Live I/O automata -- specified by temproal formulas *} |
4559 | 7 |
|
17233 | 8 |
theory LiveIOA |
9 |
imports TLS |
|
10 |
begin |
|
11 |
||
12 |
defaultsort type |
|
4559 | 13 |
|
14 |
types |
|
17233 | 15 |
('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp" |
4559 | 16 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
17 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
18 |
validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
19 |
"validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)" |
4559 | 20 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
21 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
22 |
WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
23 |
"WF A acts = (<> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
24 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
25 |
SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
26 |
"SF A acts = ([] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)" |
4559 | 27 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
28 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
29 |
liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
30 |
"liveexecutions AP = {exec. exec : executions (fst AP) & (exec |== (snd AP))}" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
31 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
32 |
livetraces :: "('a,'s)live_ioa => 'a trace set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
33 |
"livetraces AP = {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
34 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
35 |
live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
36 |
"live_implements CL AM = ((inp (fst CL) = inp (fst AM)) & |
4559 | 37 |
(out (fst CL) = out (fst AM)) & |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
38 |
livetraces CL <= livetraces AM)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
39 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
40 |
is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
41 |
"is_live_ref_map f CL AM = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
42 |
(is_ref_map f (fst CL ) (fst AM) & |
17233 | 43 |
(! exec : executions (fst CL). (exec |== (snd CL)) --> |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
44 |
((corresp_ex (fst AM) f exec) |== (snd AM))))" |
4559 | 45 |
|
19741 | 46 |
|
47 |
declare split_paired_Ex [simp del] |
|
48 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
49 |
lemma live_implements_trans: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
50 |
"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] |
19741 | 51 |
==> live_implements (A,LA) (C,LC)" |
52 |
apply (unfold live_implements_def) |
|
53 |
apply auto |
|
54 |
done |
|
55 |
||
56 |
||
57 |
subsection "Correctness of live refmap" |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
58 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
59 |
lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
60 |
is_live_ref_map f (C,M) (A,L) |] |
19741 | 61 |
==> live_implements (C,M) (A,L)" |
62 |
apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def) |
|
26359 | 63 |
apply auto |
19741 | 64 |
apply (rule_tac x = "corresp_ex A f ex" in exI) |
26359 | 65 |
apply auto |
19741 | 66 |
(* Traces coincide, Lemma 1 *) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
67 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 68 |
apply (erule lemma_1 [THEN spec, THEN mp]) |
69 |
apply (simp (no_asm) add: externals_def) |
|
70 |
apply (auto)[1] |
|
71 |
apply (simp add: executions_def reachable.reachable_0) |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
72 |
|
19741 | 73 |
(* corresp_ex is execution, Lemma 2 *) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
74 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 75 |
apply (simp add: executions_def) |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
76 |
(* start state *) |
19741 | 77 |
apply (rule conjI) |
78 |
apply (simp add: is_ref_map_def corresp_ex_def) |
|
79 |
(* is-execution-fragment *) |
|
80 |
apply (erule lemma_2 [THEN spec, THEN mp]) |
|
81 |
apply (simp add: reachable.reachable_0) |
|
82 |
||
83 |
done |
|
4559 | 84 |
|
17233 | 85 |
end |