62008
|
1 |
(* Title: HOL/HOLCF/IOA/LiveIOA.thy
|
40945
|
2 |
Author: Olaf Müller
|
17233
|
3 |
*)
|
4559
|
4 |
|
62002
|
5 |
section \<open>Live I/O automata -- specified by temproal formulas\<close>
|
4559
|
6 |
|
17233
|
7 |
theory LiveIOA
|
|
8 |
imports TLS
|
|
9 |
begin
|
|
10 |
|
36452
|
11 |
default_sort type
|
4559
|
12 |
|
62192
|
13 |
type_synonym ('a, 's) live_ioa = "('a, 's)ioa \<times> ('a, 's) ioa_temp"
|
4559
|
14 |
|
62192
|
15 |
definition validLIOA :: "('a, 's) live_ioa \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool"
|
|
16 |
where "validLIOA AL P \<longleftrightarrow> validIOA (fst AL) (snd AL \<^bold>\<longrightarrow> P)"
|
4559
|
17 |
|
62192
|
18 |
definition WF :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa_temp"
|
|
19 |
where "WF A acts = (\<diamond>\<box>\<langle>\<lambda>(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (\<lambda>a. a \<in> acts))\<rangle>)"
|
|
20 |
|
|
21 |
definition SF :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa_temp"
|
|
22 |
where "SF A acts = (\<box>\<diamond>\<langle>\<lambda>(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (\<lambda>a. a \<in> acts))\<rangle>)"
|
|
23 |
|
|
24 |
definition liveexecutions :: "('a, 's) live_ioa \<Rightarrow> ('a, 's) execution set"
|
|
25 |
where "liveexecutions AP = {exec. exec \<in> executions (fst AP) \<and> (exec \<TTurnstile> snd AP)}"
|
4559
|
26 |
|
62192
|
27 |
definition livetraces :: "('a, 's) live_ioa \<Rightarrow> 'a trace set"
|
|
28 |
where "livetraces AP = {mk_trace (fst AP) $ (snd ex) |ex. ex \<in> liveexecutions AP}"
|
|
29 |
|
|
30 |
definition live_implements :: "('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool"
|
|
31 |
where "live_implements CL AM \<longleftrightarrow>
|
|
32 |
inp (fst CL) = inp (fst AM) \<and> out (fst CL) = out (fst AM) \<and>
|
|
33 |
livetraces CL \<subseteq> livetraces AM"
|
|
34 |
|
|
35 |
definition is_live_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool"
|
|
36 |
where "is_live_ref_map f CL AM \<longleftrightarrow>
|
|
37 |
is_ref_map f (fst CL ) (fst AM) \<and>
|
|
38 |
(\<forall>exec \<in> executions (fst CL). (exec \<TTurnstile> (snd CL)) \<longrightarrow>
|
|
39 |
(corresp_ex (fst AM) f exec \<TTurnstile> snd AM))"
|
|
40 |
|
|
41 |
lemma live_implements_trans:
|
|
42 |
"live_implements (A, LA) (B, LB) \<Longrightarrow> live_implements (B, LB) (C, LC) \<Longrightarrow>
|
|
43 |
live_implements (A, LA) (C, LC)"
|
|
44 |
by (auto simp: live_implements_def)
|
4559
|
45 |
|
19741
|
46 |
|
62192
|
47 |
subsection \<open>Correctness of live refmap\<close>
|
19741
|
48 |
|
62192
|
49 |
lemma live_implements:
|
|
50 |
"inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_live_ref_map f (C, M) (A, L)
|
|
51 |
\<Longrightarrow> live_implements (C, M) (A, L)"
|
|
52 |
apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
|
|
53 |
apply auto
|
|
54 |
apply (rule_tac x = "corresp_ex A f ex" in exI)
|
|
55 |
apply auto
|
|
56 |
text \<open>Traces coincide, Lemma 1\<close>
|
62195
|
57 |
apply (pair ex)
|
19741
|
58 |
apply (erule lemma_1 [THEN spec, THEN mp])
|
|
59 |
apply (simp (no_asm) add: externals_def)
|
|
60 |
apply (auto)[1]
|
|
61 |
apply (simp add: executions_def reachable.reachable_0)
|
62192
|
62 |
text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
|
62195
|
63 |
apply (pair ex)
|
19741
|
64 |
apply (simp add: executions_def)
|
62192
|
65 |
text \<open>start state\<close>
|
19741
|
66 |
apply (rule conjI)
|
|
67 |
apply (simp add: is_ref_map_def corresp_ex_def)
|
62192
|
68 |
text \<open>\<open>is_execution_fragment\<close>\<close>
|
19741
|
69 |
apply (erule lemma_2 [THEN spec, THEN mp])
|
|
70 |
apply (simp add: reachable.reachable_0)
|
62192
|
71 |
done
|
4559
|
72 |
|
17233
|
73 |
end
|