1(* Title: HOL/HOLCF/IOA/Traces.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Executions and Traces of I/O automata in HOLCF\<close> 6 7theory Traces 8imports Sequence Automata 9begin 10 11default_sort type 12 13type_synonym ('a, 's) pairs = "('a \<times> 's) Seq" 14type_synonym ('a, 's) execution = "'s \<times> ('a, 's) pairs" 15type_synonym 'a trace = "'a Seq" 16type_synonym ('a, 's) execution_module = "('a, 's) execution set \<times> 'a signature" 17type_synonym 'a schedule_module = "'a trace set \<times> 'a signature" 18type_synonym 'a trace_module = "'a trace set \<times> 'a signature" 19 20 21subsection \<open>Executions\<close> 22 23definition is_exec_fragC :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<rightarrow> 's \<Rightarrow> tr" 24 where "is_exec_fragC A = 25 (fix \<cdot> 26 (LAM h ex. 27 (\<lambda>s. 28 case ex of 29 nil \<Rightarrow> TT 30 | x ## xs \<Rightarrow> flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (h \<cdot> xs) (snd p)) \<cdot> x)))" 31 32definition is_exec_frag :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool" 33 where "is_exec_frag A ex \<longleftrightarrow> (is_exec_fragC A \<cdot> (snd ex)) (fst ex) \<noteq> FF" 34 35definition executions :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution set" 36 where "executions ioa = {e. fst e \<in> starts_of ioa \<and> is_exec_frag ioa e}" 37 38 39subsection \<open>Schedules\<close> 40 41definition filter_act :: "('a, 's) pairs \<rightarrow> 'a trace" 42 where "filter_act = Map fst" 43 44definition has_schedule :: "('a, 's) ioa \<Rightarrow> 'a trace \<Rightarrow> bool" 45 where "has_schedule ioa sch \<longleftrightarrow> (\<exists>ex \<in> executions ioa. sch = filter_act \<cdot> (snd ex))" 46 47definition schedules :: "('a, 's) ioa \<Rightarrow> 'a trace set" 48 where "schedules ioa = {sch. has_schedule ioa sch}" 49 50 51subsection \<open>Traces\<close> 52 53definition has_trace :: "('a, 's) ioa \<Rightarrow> 'a trace \<Rightarrow> bool" 54 where "has_trace ioa tr \<longleftrightarrow> (\<exists>sch \<in> schedules ioa. tr = Filter (\<lambda>a. a \<in> ext ioa) \<cdot> sch)" 55 56definition traces :: "('a, 's) ioa \<Rightarrow> 'a trace set" 57 where "traces ioa \<equiv> {tr. has_trace ioa tr}" 58 59definition mk_trace :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<rightarrow> 'a trace" 60 where "mk_trace ioa = (LAM tr. Filter (\<lambda>a. a \<in> ext ioa) \<cdot> (filter_act \<cdot> tr))" 61 62 63subsection \<open>Fair Traces\<close> 64 65definition laststate :: "('a, 's) execution \<Rightarrow> 's" 66 where "laststate ex = 67 (case Last \<cdot> (snd ex) of 68 UU \<Rightarrow> fst ex 69 | Def at \<Rightarrow> snd at)" 70 71text \<open>A predicate holds infinitely (finitely) often in a sequence.\<close> 72definition inf_often :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool" 73 where "inf_often P s \<longleftrightarrow> Infinite (Filter P \<cdot> s)" 74 75text \<open>Filtering \<open>P\<close> yields a finite or partial sequence.\<close> 76definition fin_often :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool" 77 where "fin_often P s \<longleftrightarrow> \<not> inf_often P s" 78 79 80subsection \<open>Fairness of executions\<close> 81 82text \<open> 83 Note that partial execs cannot be \<open>wfair\<close> as the inf_often predicate in the 84 else branch prohibits it. However they can be \<open>sfair\<close> in the case when all 85 \<open>W\<close> are only finitely often enabled: Is this the right model? 86 87 See \<^file>\<open>LiveIOA.thy\<close> for solution conforming with the literature and 88 superseding this one. 89\<close> 90 91definition is_wfair :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) execution \<Rightarrow> bool" 92 where "is_wfair A W ex \<longleftrightarrow> 93 (inf_often (\<lambda>x. fst x \<in> W) (snd ex) \<or> 94 inf_often (\<lambda>x. \<not> Enabled A W (snd x)) (snd ex))" 95 96definition wfair_ex :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool" 97 where "wfair_ex A ex \<longleftrightarrow> 98 (\<forall>W \<in> wfair_of A. 99 if Finite (snd ex) 100 then \<not> Enabled A W (laststate ex) 101 else is_wfair A W ex)" 102 103definition is_sfair :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) execution \<Rightarrow> bool" 104 where "is_sfair A W ex \<longleftrightarrow> 105 (inf_often (\<lambda>x. fst x \<in> W) (snd ex) \<or> 106 fin_often (\<lambda>x. Enabled A W (snd x)) (snd ex))" 107 108definition sfair_ex :: "('a, 's)ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool" 109 where "sfair_ex A ex \<longleftrightarrow> 110 (\<forall>W \<in> sfair_of A. 111 if Finite (snd ex) 112 then \<not> Enabled A W (laststate ex) 113 else is_sfair A W ex)" 114 115definition fair_ex :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool" 116 where "fair_ex A ex \<longleftrightarrow> wfair_ex A ex \<and> sfair_ex A ex" 117 118 119text \<open>Fair behavior sets.\<close> 120 121definition fairexecutions :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution set" 122 where "fairexecutions A = {ex. ex \<in> executions A \<and> fair_ex A ex}" 123 124definition fairtraces :: "('a, 's) ioa \<Rightarrow> 'a trace set" 125 where "fairtraces A = {mk_trace A \<cdot> (snd ex) | ex. ex \<in> fairexecutions A}" 126 127 128subsection \<open>Implementation\<close> 129 130subsubsection \<open>Notions of implementation\<close> 131 132definition ioa_implements :: "('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" (infixr "=<|" 12) 133 where "(ioa1 =<| ioa2) \<longleftrightarrow> 134 (inputs (asig_of ioa1) = inputs (asig_of ioa2) \<and> 135 outputs (asig_of ioa1) = outputs (asig_of ioa2)) \<and> 136 traces ioa1 \<subseteq> traces ioa2" 137 138definition fair_implements :: "('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 139 where "fair_implements C A \<longleftrightarrow> 140 inp C = inp A \<and> out C = out A \<and> fairtraces C \<subseteq> fairtraces A" 141 142lemma implements_trans: "A =<| B \<Longrightarrow> B =<| C \<Longrightarrow> A =<| C" 143 by (auto simp add: ioa_implements_def) 144 145 146subsection \<open>Modules\<close> 147 148subsubsection \<open>Execution, schedule and trace modules\<close> 149 150definition Execs :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution_module" 151 where "Execs A = (executions A, asig_of A)" 152 153definition Scheds :: "('a, 's) ioa \<Rightarrow> 'a schedule_module" 154 where "Scheds A = (schedules A, asig_of A)" 155 156definition Traces :: "('a, 's) ioa \<Rightarrow> 'a trace_module" 157 where "Traces A = (traces A, asig_of A)" 158 159lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex 160declare Let_def [simp] 161setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close> 162 163lemmas exec_rws = executions_def is_exec_frag_def 164 165 166subsection \<open>Recursive equations of operators\<close> 167 168subsubsection \<open>\<open>filter_act\<close>\<close> 169 170lemma filter_act_UU: "filter_act \<cdot> UU = UU" 171 by (simp add: filter_act_def) 172 173lemma filter_act_nil: "filter_act \<cdot> nil = nil" 174 by (simp add: filter_act_def) 175 176lemma filter_act_cons: "filter_act \<cdot> (x \<leadsto> xs) = fst x \<leadsto> filter_act \<cdot> xs" 177 by (simp add: filter_act_def) 178 179declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp] 180 181 182subsubsection \<open>\<open>mk_trace\<close>\<close> 183 184lemma mk_trace_UU: "mk_trace A \<cdot> UU = UU" 185 by (simp add: mk_trace_def) 186 187lemma mk_trace_nil: "mk_trace A \<cdot> nil = nil" 188 by (simp add: mk_trace_def) 189 190lemma mk_trace_cons: 191 "mk_trace A \<cdot> (at \<leadsto> xs) = 192 (if fst at \<in> ext A 193 then fst at \<leadsto> mk_trace A \<cdot> xs 194 else mk_trace A \<cdot> xs)" 195 by (simp add: mk_trace_def) 196 197declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp] 198 199 200subsubsection \<open>\<open>is_exec_fragC\<close>\<close> 201 202lemma is_exec_fragC_unfold: 203 "is_exec_fragC A = 204 (LAM ex. 205 (\<lambda>s. 206 case ex of 207 nil \<Rightarrow> TT 208 | x ## xs \<Rightarrow> 209 (flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (is_exec_fragC A\<cdot>xs) (snd p)) \<cdot> x)))" 210 apply (rule trans) 211 apply (rule fix_eq4) 212 apply (rule is_exec_fragC_def) 213 apply (rule beta_cfun) 214 apply (simp add: flift1_def) 215 done 216 217lemma is_exec_fragC_UU: "(is_exec_fragC A \<cdot> UU) s = UU" 218 apply (subst is_exec_fragC_unfold) 219 apply simp 220 done 221 222lemma is_exec_fragC_nil: "(is_exec_fragC A \<cdot> nil) s = TT" 223 apply (subst is_exec_fragC_unfold) 224 apply simp 225 done 226 227lemma is_exec_fragC_cons: 228 "(is_exec_fragC A \<cdot> (pr \<leadsto> xs)) s = 229 (Def ((s, pr) \<in> trans_of A) andalso (is_exec_fragC A \<cdot> xs) (snd pr))" 230 apply (rule trans) 231 apply (subst is_exec_fragC_unfold) 232 apply (simp add: Consq_def flift1_def) 233 apply simp 234 done 235 236declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp] 237 238 239subsubsection \<open>\<open>is_exec_frag\<close>\<close> 240 241lemma is_exec_frag_UU: "is_exec_frag A (s, UU)" 242 by (simp add: is_exec_frag_def) 243 244lemma is_exec_frag_nil: "is_exec_frag A (s, nil)" 245 by (simp add: is_exec_frag_def) 246 247lemma is_exec_frag_cons: 248 "is_exec_frag A (s, (a, t) \<leadsto> ex) \<longleftrightarrow> (s, a, t) \<in> trans_of A \<and> is_exec_frag A (t, ex)" 249 by (simp add: is_exec_frag_def) 250 251declare is_exec_frag_UU [simp] is_exec_frag_nil [simp] is_exec_frag_cons [simp] 252 253 254subsubsection \<open>\<open>laststate\<close>\<close> 255 256lemma laststate_UU: "laststate (s, UU) = s" 257 by (simp add: laststate_def) 258 259lemma laststate_nil: "laststate (s, nil) = s" 260 by (simp add: laststate_def) 261 262lemma laststate_cons: "Finite ex \<Longrightarrow> laststate (s, at \<leadsto> ex) = laststate (snd at, ex)" 263 apply (simp add: laststate_def) 264 apply (cases "ex = nil") 265 apply simp 266 apply simp 267 apply (drule Finite_Last1 [THEN mp]) 268 apply assumption 269 apply defined 270 done 271 272declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp] 273 274lemma exists_laststate: "Finite ex \<Longrightarrow> \<forall>s. \<exists>u. laststate (s, ex) = u" 275 by Seq_Finite_induct 276 277 278subsection \<open>\<open>has_trace\<close> \<open>mk_trace\<close>\<close> 279 280(*alternative definition of has_trace tailored for the refinement proof, as it does not 281 take the detour of schedules*) 282lemma has_trace_def2: "has_trace A b \<longleftrightarrow> (\<exists>ex \<in> executions A. b = mk_trace A \<cdot> (snd ex))" 283 apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def [abs_def]) 284 apply auto 285 done 286 287 288subsection \<open>Signatures and executions, schedules\<close> 289 290text \<open> 291 All executions of \<open>A\<close> have only actions of \<open>A\<close>. This is only true because of 292 the predicate \<open>state_trans\<close> (part of the predicate \<open>IOA\<close>): We have no 293 dependent types. For executions of parallel automata this assumption is not 294 needed, as in \<open>par_def\<close> this condition is included once more. (See Lemmas 295 1.1.1c in CompoExecs for example.) 296\<close> 297 298lemma execfrag_in_sig: 299 "is_trans_of A \<Longrightarrow> \<forall>s. is_exec_frag A (s, xs) \<longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act \<cdot> xs)" 300 apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def) 301 text \<open>main case\<close> 302 apply (auto simp add: is_trans_of_def) 303 done 304 305lemma exec_in_sig: 306 "is_trans_of A \<Longrightarrow> x \<in> executions A \<Longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act \<cdot> (snd x))" 307 apply (simp add: executions_def) 308 apply (pair x) 309 apply (rule execfrag_in_sig [THEN spec, THEN mp]) 310 apply auto 311 done 312 313lemma scheds_in_sig: "is_trans_of A \<Longrightarrow> x \<in> schedules A \<Longrightarrow> Forall (\<lambda>a. a \<in> act A) x" 314 apply (unfold schedules_def has_schedule_def [abs_def]) 315 apply (fast intro!: exec_in_sig) 316 done 317 318 319subsection \<open>Executions are prefix closed\<close> 320 321(*only admissible in y, not if done in x!*) 322lemma execfrag_prefixclosed: "\<forall>x s. is_exec_frag A (s, x) \<and> y \<sqsubseteq> x \<longrightarrow> is_exec_frag A (s, y)" 323 apply (pair_induct y simp: is_exec_frag_def) 324 apply (intro strip) 325 apply (Seq_case_simp x) 326 apply (pair a) 327 apply auto 328 done 329 330lemmas exec_prefixclosed = 331 conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp]] 332 333(*second prefix notion for Finite x*) 334lemma exec_prefix2closed [rule_format]: 335 "\<forall>y s. is_exec_frag A (s, x @@ y) \<longrightarrow> is_exec_frag A (s, x)" 336 apply (pair_induct x simp: is_exec_frag_def) 337 apply (intro strip) 338 apply (Seq_case_simp s) 339 apply (pair a) 340 apply auto 341 done 342 343end 344