1(*  Title:      HOL/IOA/IOA.thy
2    Author:     Tobias Nipkow & Konrad Slind
3    Copyright   1994  TU Muenchen
4*)
5
6section \<open>The I/O automata of Lynch and Tuttle\<close>
7
8theory IOA
9imports Asig
10begin
11
12type_synonym 'a seq = "nat => 'a"
13type_synonym 'a oseq = "nat => 'a option"
14type_synonym ('a, 'b) execution = "'a oseq * 'b seq"
15type_synonym ('a, 's) transition = "('s * 'a * 's)"
16type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
17
18(* IO automata *)
19
20definition state_trans :: "['action signature, ('action,'state)transition set] => bool"
21  where "state_trans asig R \<equiv>
22     (\<forall>triple. triple \<in> R \<longrightarrow> fst(snd(triple)) \<in> actions(asig)) \<and>
23     (\<forall>a. (a \<in> inputs(asig)) \<longrightarrow> (\<forall>s1. \<exists>s2. (s1,a,s2) \<in> R))"
24
25definition asig_of :: "('action,'state)ioa => 'action signature"
26  where "asig_of == fst"
27
28definition starts_of :: "('action,'state)ioa => 'state set"
29  where "starts_of == (fst o snd)"
30
31definition trans_of :: "('action,'state)ioa => ('action,'state)transition set"
32  where "trans_of == (snd o snd)"
33
34definition IOA :: "('action,'state)ioa => bool"
35  where "IOA(ioa) == (is_asig(asig_of(ioa)) &
36                (~ starts_of(ioa) = {}) &
37                state_trans (asig_of ioa) (trans_of ioa))"
38
39
40(* Executions, schedules, and traces *)
41
42(* An execution fragment is modelled with a pair of sequences:
43   the first is the action options, the second the state sequence.
44   Finite executions have None actions from some point on. *)
45definition is_execution_fragment :: "[('action,'state)ioa, ('action,'state)execution] => bool"
46  where "is_execution_fragment A ex \<equiv>
47     let act = fst(ex); state = snd(ex)
48     in \<forall>n a. (act(n)=None \<longrightarrow> state(Suc(n)) = state(n)) \<and>
49              (act(n)=Some(a) \<longrightarrow> (state(n),a,state(Suc(n))) \<in> trans_of(A))"
50
51definition executions :: "('action,'state)ioa => ('action,'state)execution set"
52  where "executions(ioa) \<equiv> {e. snd e 0 \<in> starts_of(ioa) \<and> is_execution_fragment ioa e}"
53
54
55definition reachable :: "[('action,'state)ioa, 'state] => bool"
56  where "reachable ioa s \<equiv> (\<exists>ex\<in>executions(ioa). \<exists>n. (snd ex n) = s)"
57
58definition invariant :: "[('action,'state)ioa, 'state=>bool] => bool"
59  where "invariant A P \<equiv> (\<forall>s. reachable A s \<longrightarrow> P(s))"
60
61
62(* Composition of action signatures and automata *)
63
64consts
65  compatible_asigs ::"('a \<Rightarrow> 'action signature) \<Rightarrow> bool"
66  asig_composition ::"('a \<Rightarrow> 'action signature) \<Rightarrow> 'action signature"
67  compatible_ioas  ::"('a \<Rightarrow> ('action,'state)ioa) \<Rightarrow> bool"
68  ioa_composition  ::"('a \<Rightarrow> ('action, 'state)ioa) \<Rightarrow> ('action,'a \<Rightarrow> 'state)ioa"
69
70
71(* binary composition of action signatures and automata *)
72
73definition compat_asigs ::"['action signature, 'action signature] => bool"
74  where "compat_asigs a1 a2 ==
75   (((outputs(a1) Int outputs(a2)) = {}) \<and>
76    ((internals(a1) Int actions(a2)) = {}) \<and>
77    ((internals(a2) Int actions(a1)) = {}))"
78
79definition compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] \<Rightarrow> bool"
80  where "compat_ioas ioa1 ioa2 \<equiv> compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
81
82definition asig_comp :: "['action signature, 'action signature] \<Rightarrow> 'action signature"
83  where "asig_comp a1 a2 \<equiv>
84      (((inputs(a1) \<union> inputs(a2)) - (outputs(a1) \<union> outputs(a2)),
85        (outputs(a1) \<union> outputs(a2)),
86        (internals(a1) \<union> internals(a2))))"
87
88definition par :: "[('a,'s)ioa, ('a,'t)ioa] \<Rightarrow> ('a,'s*'t)ioa"  (infixr "||" 10)
89  where "(ioa1 || ioa2) \<equiv>
90     (asig_comp (asig_of ioa1) (asig_of ioa2),
91      {pr. fst(pr) \<in> starts_of(ioa1) \<and> snd(pr) \<in> starts_of(ioa2)},
92      {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
93           in (a \<in> actions(asig_of(ioa1)) | a \<in> actions(asig_of(ioa2))) &
94              (if a \<in> actions(asig_of(ioa1)) then
95                 (fst(s),a,fst(t)) \<in> trans_of(ioa1)
96               else fst(t) = fst(s))
97              &
98              (if a \<in> actions(asig_of(ioa2)) then
99                 (snd(s),a,snd(t)) \<in> trans_of(ioa2)
100               else snd(t) = snd(s))})"
101
102
103(* Filtering and hiding *)
104
105(* Restrict the trace to those members of the set s *)
106definition filter_oseq :: "('a => bool) => 'a oseq => 'a oseq"
107  where "filter_oseq p s \<equiv>
108   (\<lambda>i. case s(i)
109         of None \<Rightarrow> None
110          | Some(x) \<Rightarrow> if p x then Some x else None)"
111
112definition mk_trace :: "[('action,'state)ioa, 'action oseq] \<Rightarrow> 'action oseq"
113  where "mk_trace(ioa) \<equiv> filter_oseq(\<lambda>a. a \<in> externals(asig_of(ioa)))"
114
115(* Does an ioa have an execution with the given trace *)
116definition has_trace :: "[('action,'state)ioa, 'action oseq] \<Rightarrow> bool"
117  where "has_trace ioa b \<equiv> (\<exists>ex\<in>executions(ioa). b = mk_trace ioa (fst ex))"
118
119definition NF :: "'a oseq => 'a oseq"
120  where "NF(tr) \<equiv> SOME nf. \<exists>f. mono(f) \<and> (\<forall>i. nf(i)=tr(f(i))) \<and>
121                    (\<forall>j. j \<notin> range(f) \<longrightarrow> nf(j)= None) &
122                    (\<forall>i. nf(i)=None --> (nf (Suc i)) = None)"
123
124(* All the traces of an ioa *)
125definition traces :: "('action,'state)ioa => 'action oseq set"
126  where "traces(ioa) \<equiv> {trace. \<exists>tr. trace=NF(tr) \<and> has_trace ioa tr}"
127
128
129definition restrict_asig :: "['a signature, 'a set] => 'a signature"
130  where "restrict_asig asig actns \<equiv>
131    (inputs(asig) \<inter> actns, outputs(asig) \<inter> actns,
132     internals(asig) \<union> (externals(asig) - actns))"
133
134definition restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
135  where "restrict ioa actns \<equiv>
136    (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
137
138
139
140(* Notions of correctness *)
141
142definition ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
143  where "ioa_implements ioa1 ioa2 \<equiv>
144  ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) \<and>
145     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) \<and>
146      traces(ioa1) \<subseteq> traces(ioa2))"
147
148
149(* Instantiation of abstract IOA by concrete actions *)
150
151definition rename :: "('a, 'b)ioa \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> ('c,'b)ioa"
152  where "rename ioa ren \<equiv>
153    (({b. \<exists>x. Some(x)= ren(b) \<and> x \<in> inputs(asig_of(ioa))},
154      {b. \<exists>x. Some(x)= ren(b) \<and> x \<in> outputs(asig_of(ioa))},
155      {b. \<exists>x. Some(x)= ren(b) \<and> x \<in> internals(asig_of(ioa))}),
156                starts_of(ioa)   ,
157     {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
158          in
159          \<exists>x. Some(x) = ren(a) \<and> (s,x,t) \<in> trans_of(ioa)})"
160
161
162declare Let_def [simp]
163
164lemmas ioa_projections = asig_of_def starts_of_def trans_of_def
165  and exec_rws = executions_def is_execution_fragment_def
166
167lemma ioa_triple_proj:
168    "asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z"
169  apply (simp add: ioa_projections)
170  done
171
172lemma trans_in_actions:
173  "[| IOA(A); (s1,a,s2) \<in> trans_of(A) |] ==> a \<in> actions(asig_of(A))"
174  apply (unfold IOA_def state_trans_def actions_def is_asig_def)
175  apply (erule conjE)+
176  apply (erule allE, erule impE, assumption)
177  apply simp
178  done
179
180
181lemma filter_oseq_idemp: "filter_oseq p (filter_oseq p s) = filter_oseq p s"
182  apply (simp add: filter_oseq_def)
183  apply (rule ext)
184  apply (case_tac "s i")
185  apply simp_all
186  done
187
188lemma mk_trace_thm:
189"(mk_trace A s n = None) =
190   (s(n)=None | (\<exists>a. s(n)=Some(a) \<and> a \<notin> externals(asig_of(A))))
191   &
192   (mk_trace A s n = Some(a)) =
193    (s(n)=Some(a) \<and> a \<in> externals(asig_of(A)))"
194  apply (unfold mk_trace_def filter_oseq_def)
195  apply (case_tac "s n")
196  apply auto
197  done
198
199lemma reachable_0: "s \<in> starts_of(A) \<Longrightarrow> reachable A s"
200  apply (unfold reachable_def)
201  apply (rule_tac x = "(%i. None, %i. s)" in bexI)
202  apply simp
203  apply (simp add: exec_rws)
204  done
205
206lemma reachable_n:
207  "\<And>A. [| reachable A s; (s,a,t) \<in> trans_of(A) |] ==> reachable A t"
208  apply (unfold reachable_def exec_rws)
209  apply (simp del: bex_simps)
210  apply (simp (no_asm_simp) only: split_tupled_all)
211  apply safe
212  apply (rename_tac ex1 ex2 n)
213  apply (rule_tac x = "(%i. if i<n then ex1 i else (if i=n then Some a else None) , %i. if i<Suc n then ex2 i else t)" in bexI)
214   apply (rule_tac x = "Suc n" in exI)
215   apply (simp (no_asm))
216  apply simp
217  apply (metis ioa_triple_proj less_antisym)
218  done
219
220
221lemma invariantI:
222  assumes p1: "\<And>s. s \<in> starts_of(A) \<Longrightarrow> P(s)"
223    and p2: "\<And>s t a. [|reachable A s; P(s)|] ==> (s,a,t) \<in> trans_of(A) \<longrightarrow> P(t)"
224  shows "invariant A P"
225  apply (unfold invariant_def reachable_def Let_def exec_rws)
226  apply safe
227  apply (rename_tac ex1 ex2 n)
228  apply (rule_tac Q = "reachable A (ex2 n) " in conjunct1)
229  apply simp
230  apply (induct_tac n)
231   apply (fast intro: p1 reachable_0)
232  apply (erule_tac x = na in allE)
233  apply (case_tac "ex1 na", simp_all)
234  apply safe
235   apply (erule p2 [THEN mp])
236    apply (fast dest: reachable_n)+
237  done
238
239lemma invariantI1:
240 "[| \<And>s. s \<in> starts_of(A) \<Longrightarrow> P(s);
241     \<And>s t a. reachable A s \<Longrightarrow> P(s) \<longrightarrow> (s,a,t) \<in> trans_of(A) \<longrightarrow> P(t)
242  |] ==> invariant A P"
243  apply (blast intro!: invariantI)
244  done
245
246lemma invariantE:
247  "[| invariant A P; reachable A s |] ==> P(s)"
248  apply (unfold invariant_def)
249  apply blast
250  done
251
252lemma actions_asig_comp:
253  "actions(asig_comp a b) = actions(a) \<union> actions(b)"
254  apply (auto simp add: actions_def asig_comp_def asig_projections)
255  done
256
257lemma starts_of_par:
258  "starts_of(A || B) = {p. fst(p) \<in> starts_of(A) \<and> snd(p) \<in> starts_of(B)}"
259  apply (simp add: par_def ioa_projections)
260  done
261
262(* Every state in an execution is reachable *)
263lemma states_of_exec_reachable:
264  "ex \<in> executions(A) \<Longrightarrow> \<forall>n. reachable A (snd ex n)"
265  apply (unfold reachable_def)
266  apply fast
267  done
268
269
270lemma trans_of_par4:
271"(s,a,t) \<in> trans_of(A || B || C || D) =
272  ((a \<in> actions(asig_of(A)) | a \<in> actions(asig_of(B)) | a \<in> actions(asig_of(C)) |
273    a \<in> actions(asig_of(D))) \<and>
274   (if a \<in> actions(asig_of(A)) then (fst(s),a,fst(t)) \<in> trans_of(A)
275    else fst t=fst s) \<and>
276   (if a \<in> actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))) \<in> trans_of(B)
277    else fst(snd(t))=fst(snd(s))) \<and>
278   (if a \<in> actions(asig_of(C)) then
279      (fst(snd(snd(s))),a,fst(snd(snd(t)))) \<in> trans_of(C)
280    else fst(snd(snd(t)))=fst(snd(snd(s)))) \<and>
281   (if a \<in> actions(asig_of(D)) then
282      (snd(snd(snd(s))),a,snd(snd(snd(t)))) \<in> trans_of(D)
283    else snd(snd(snd(t)))=snd(snd(snd(s)))))"
284  (*SLOW*)
285  apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff ioa_projections)
286  done
287
288lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &
289              trans_of(restrict ioa acts) = trans_of(ioa) &
290              reachable (restrict ioa acts) s = reachable ioa s"
291  apply (simp add: is_execution_fragment_def executions_def
292    reachable_def restrict_def ioa_projections)
293  done
294
295lemma asig_of_par: "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"
296  apply (simp add: par_def ioa_projections)
297  done
298
299
300lemma externals_of_par: "externals(asig_of(A1||A2)) =
301   (externals(asig_of(A1)) \<union> externals(asig_of(A2)))"
302  apply (simp add: externals_def asig_of_par asig_comp_def
303    asig_inputs_def asig_outputs_def Un_def set_diff_eq)
304  apply blast
305  done
306
307lemma ext1_is_not_int2:
308  "[| compat_ioas A1 A2; a \<in> externals(asig_of(A1))|] ==> a \<notin> internals(asig_of(A2))"
309  apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def)
310  apply auto
311  done
312
313lemma ext2_is_not_int1:
314 "[| compat_ioas A2 A1 ; a \<in> externals(asig_of(A1))|] ==> a \<notin> internals(asig_of(A2))"
315  apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def)
316  apply auto
317  done
318
319lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act]
320  and ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act]
321
322end
323