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