1(*  Title:      HOL/HOLCF/IOA/LiveIOA.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Live I/O automata -- specified by temproal formulas\<close>
6
7theory LiveIOA
8imports TLS
9begin
10
11default_sort type
12
13type_synonym ('a, 's) live_ioa = "('a, 's)ioa \<times> ('a, 's) ioa_temp"
14
15definition 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)"
17
18definition 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
21definition 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
24definition 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)}"
26
27definition livetraces :: "('a, 's) live_ioa \<Rightarrow> 'a trace set"
28  where "livetraces AP = {mk_trace (fst AP) \<cdot> (snd ex) |ex. ex \<in> liveexecutions AP}"
29
30definition 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
35definition 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
41lemma 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)
45
46
47subsection \<open>Correctness of live refmap\<close>
48
49lemma 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>
57  apply (pair ex)
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)
62  text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
63  apply (pair ex)
64  apply (simp add: executions_def)
65  text \<open>start state\<close>
66  apply (rule conjI)
67  apply (simp add: is_ref_map_def corresp_ex_def)
68  text \<open>\<open>is_execution_fragment\<close>\<close>
69  apply (erule lemma_2 [THEN spec, THEN mp])
70  apply (simp add: reachable.reachable_0)
71  done
72
73end
74