(* Title: HOL/HOLCF/IOA/Traces.thy
Author: Olaf Müller
*)
section \<open>Executions and Traces of I/O automata in HOLCF\<close>
theory Traces
imports Sequence Automata
begin
default_sort type
type_synonym ('a, 's) pairs = "('a \ 's) Seq"
type_synonym ('a, 's) execution = "'s \ ('a, 's) pairs"
type_synonym 'a trace = "'a Seq"
type_synonym ('a, 's) execution_module = "('a, 's) execution set \ 'a signature"
type_synonym 'a schedule_module = "'a trace set \<times> 'a signature"
type_synonym 'a trace_module = "'a trace set \<times> 'a signature"
subsection \<open>Executions\<close>
definition is_exec_fragC :: "('a, 's) ioa \ ('a, 's) pairs \ 's \ tr"
where "is_exec_fragC A =
(fix \<cdot>
(LAM h ex.
(\<lambda>s.
case ex of
nil \<Rightarrow> TT
| x ## xs \<Rightarrow> flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (h \<cdot> xs) (snd p)) \<cdot> x)))"
definition is_exec_frag :: "('a, 's) ioa \ ('a, 's) execution \ bool"
where "is_exec_frag A ex \ (is_exec_fragC A \ (snd ex)) (fst ex) \ FF"
definition executions :: "('a, 's) ioa \ ('a, 's) execution set"
where "executions ioa = {e. fst e \ starts_of ioa \ is_exec_frag ioa e}"
subsection \<open>Schedules\<close>
definition filter_act :: "('a, 's) pairs \ 'a trace"
where "filter_act = Map fst"
definition has_schedule :: "('a, 's) ioa \ 'a trace \ bool"
where "has_schedule ioa sch \ (\ex \ executions ioa. sch = filter_act \ (snd ex))"
definition schedules :: "('a, 's) ioa \ 'a trace set"
where "schedules ioa = {sch. has_schedule ioa sch}"
subsection \<open>Traces\<close>
definition has_trace :: "('a, 's) ioa \ 'a trace \ bool"
where "has_trace ioa tr \ (\sch \ schedules ioa. tr = Filter (\a. a \ ext ioa) \ sch)"
definition traces :: "('a, 's) ioa \ 'a trace set"
where "traces ioa \ {tr. has_trace ioa tr}"
definition mk_trace :: "('a, 's) ioa \ ('a, 's) pairs \ 'a trace"
where "mk_trace ioa = (LAM tr. Filter (\a. a \ ext ioa) \ (filter_act \ tr))"
subsection \<open>Fair Traces\<close>
definition laststate :: "('a, 's) execution \ 's"
where "laststate ex =
(case Last \<cdot> (snd ex) of
UU \<Rightarrow> fst ex
| Def at \<Rightarrow> snd at)"
text \<open>A predicate holds infinitely (finitely) often in a sequence.\<close>
definition inf_often :: "('a \ bool) \ 'a Seq \ bool"
where "inf_often P s \ Infinite (Filter P \ s)"
text \<open>Filtering \<open>P\<close> yields a finite or partial sequence.\<close>
definition fin_often :: "('a \ bool) \ 'a Seq \ bool"
where "fin_often P s \ \ inf_often P s"
subsection \<open>Fairness of executions\<close>
text \<open>
Note that partial execs cannot be \<open>wfair\<close> as the inf_often predicate in the
else branch prohibits it. However they can be \<open>sfair\<close> in the case when all
\<open>W\<close> are only finitely often enabled: Is this the right model?
See \<^file>\<open>LiveIOA.thy\<close> for solution conforming with the literature and
superseding this one.
\<close>
definition is_wfair :: "('a, 's) ioa \ 'a set \ ('a, 's) execution \ bool"
where "is_wfair A W ex \
(inf_often (\<lambda>x. fst x \<in> W) (snd ex) \<or>
inf_often (\<lambda>x. \<not> Enabled A W (snd x)) (snd ex))"
definition wfair_ex :: "('a, 's) ioa \ ('a, 's) execution \ bool"
where "wfair_ex A ex \
(\<forall>W \<in> wfair_of A.
if Finite (snd ex)
then \<not> Enabled A W (laststate ex)
else is_wfair A W ex)"
definition is_sfair :: "('a, 's) ioa \ 'a set \ ('a, 's) execution \ bool"
where "is_sfair A W ex \
(inf_often (\<lambda>x. fst x \<in> W) (snd ex) \<or>
fin_often (\<lambda>x. Enabled A W (snd x)) (snd ex))"
definition sfair_ex :: "('a, 's)ioa \ ('a, 's) execution \ bool"
where "sfair_ex A ex \
(\<forall>W \<in> sfair_of A.
if Finite (snd ex)
then \<not> Enabled A W (laststate ex)
else is_sfair A W ex)"
definition fair_ex :: "('a, 's) ioa \ ('a, 's) execution \ bool"
where "fair_ex A ex \ wfair_ex A ex \ sfair_ex A ex"
text \<open>Fair behavior sets.\<close>
definition fairexecutions :: "('a, 's) ioa \ ('a, 's) execution set"
where "fairexecutions A = {ex. ex \ executions A \ fair_ex A ex}"
definition fairtraces :: "('a, 's) ioa \ 'a trace set"
where "fairtraces A = {mk_trace A \ (snd ex) | ex. ex \ fairexecutions A}"
subsection \<open>Implementation\<close>
subsubsection \<open>Notions of implementation\<close>
definition ioa_implements :: "('a, 's1) ioa \ ('a, 's2) ioa \ bool" (infixr "=<|" 12)
where "(ioa1 =<| ioa2) \
(inputs (asig_of ioa1) = inputs (asig_of ioa2) \<and>
outputs (asig_of ioa1) = outputs (asig_of ioa2)) \<and>
traces ioa1 \<subseteq> traces ioa2"
definition fair_implements :: "('a, 's1) ioa \ ('a, 's2) ioa \ bool"
where "fair_implements C A \
inp C = inp A \<and> out C = out A \<and> fairtraces C \<subseteq> fairtraces A"
lemma implements_trans: "A =<| B \ B =<| C \ A =<| C"
by (auto simp add: ioa_implements_def)
subsection \<open>Modules\<close>
subsubsection \<open>Execution, schedule and trace modules\<close>
definition Execs :: "('a, 's) ioa \ ('a, 's) execution_module"
where "Execs A = (executions A, asig_of A)"
definition Scheds :: "('a, 's) ioa \ 'a schedule_module"
where "Scheds A = (schedules A, asig_of A)"
definition Traces :: "('a, 's) ioa \ 'a trace_module"
where "Traces A = (traces A, asig_of A)"
lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
declare Let_def [simp]
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
lemmas exec_rws = executions_def is_exec_frag_def
subsection \<open>Recursive equations of operators\<close>
subsubsection \<open>\<open>filter_act\<close>\<close>
lemma filter_act_UU: "filter_act \ UU = UU"
by (simp add: filter_act_def)
lemma filter_act_nil: "filter_act \ nil = nil"
by (simp add: filter_act_def)
lemma filter_act_cons: "filter_act \ (x \ xs) = fst x \ filter_act \ xs"
by (simp add: filter_act_def)
declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp]
subsubsection \<open>\<open>mk_trace\<close>\<close>
lemma mk_trace_UU: "mk_trace A \ UU = UU"
by (simp add: mk_trace_def)
lemma mk_trace_nil: "mk_trace A \ nil = nil"
by (simp add: mk_trace_def)
lemma mk_trace_cons:
"mk_trace A \ (at \ xs) =
(if fst at \<in> ext A
then fst at \<leadsto> mk_trace A \<cdot> xs
else mk_trace A \<cdot> xs)"
by (simp add: mk_trace_def)
declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp]
subsubsection \<open>\<open>is_exec_fragC\<close>\<close>
lemma is_exec_fragC_unfold:
"is_exec_fragC A =
(LAM ex.
(\<lambda>s.
case ex of
nil \<Rightarrow> TT
| x ## xs \<Rightarrow>
(flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (is_exec_fragC A\<cdot>xs) (snd p)) \<cdot> x)))"
apply (rule trans)
apply (rule fix_eq4)
apply (rule is_exec_fragC_def)
apply (rule beta_cfun)
apply (simp add: flift1_def)
done
lemma is_exec_fragC_UU: "(is_exec_fragC A \ UU) s = UU"
apply (subst is_exec_fragC_unfold)
apply simp
done
lemma is_exec_fragC_nil: "(is_exec_fragC A \ nil) s = TT"
apply (subst is_exec_fragC_unfold)
apply simp
done
lemma is_exec_fragC_cons:
"(is_exec_fragC A \ (pr \ xs)) s =
(Def ((s, pr) \<in> trans_of A) andalso (is_exec_fragC A \<cdot> xs) (snd pr))"
apply (rule trans)
apply (subst is_exec_fragC_unfold)
apply (simp add: Consq_def flift1_def)
apply simp
done
declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp]
subsubsection \<open>\<open>is_exec_frag\<close>\<close>
lemma is_exec_frag_UU: "is_exec_frag A (s, UU)"
by (simp add: is_exec_frag_def)
lemma is_exec_frag_nil: "is_exec_frag A (s, nil)"
by (simp add: is_exec_frag_def)
lemma is_exec_frag_cons:
"is_exec_frag A (s, (a, t) \ ex) \ (s, a, t) \ trans_of A \ is_exec_frag A (t, ex)"
by (simp add: is_exec_frag_def)
declare is_exec_frag_UU [simp] is_exec_frag_nil [simp] is_exec_frag_cons [simp]
subsubsection \<open>\<open>laststate\<close>\<close>
lemma laststate_UU: "laststate (s, UU) = s"
by (simp add: laststate_def)
lemma laststate_nil: "laststate (s, nil) = s"
by (simp add: laststate_def)
lemma laststate_cons: "Finite ex \ laststate (s, at \ ex) = laststate (snd at, ex)"
apply (simp add: laststate_def)
apply (cases "ex = nil")
apply simp
apply simp
apply (drule Finite_Last1 [THEN mp])
apply assumption
apply defined
done
declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
lemma exists_laststate: "Finite ex \ \s. \u. laststate (s, ex) = u"
by Seq_Finite_induct
subsection \<open>\<open>has_trace\<close> \<open>mk_trace\<close>\<close>
(*alternative definition of has_trace tailored for the refinement proof, as it does not
take the detour of schedules*)
lemma has_trace_def2: "has_trace A b \ (\ex \ executions A. b = mk_trace A \ (snd ex))"
apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def [abs_def])
apply auto
done
subsection \<open>Signatures and executions, schedules\<close>
text \<open>
All executions of \<open>A\<close> have only actions of \<open>A\<close>. This is only true because of
the predicate \<open>state_trans\<close> (part of the predicate \<open>IOA\<close>): We have no
dependent types. For executions of parallel automata this assumption is not
needed, as in \<open>par_def\<close> this condition is included once more. (See Lemmas
1.1.1c in CompoExecs for example.)
\<close>
lemma execfrag_in_sig:
"is_trans_of A \ \s. is_exec_frag A (s, xs) \ Forall (\a. a \ act A) (filter_act \ xs)"
apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def)
text \<open>main case\<close>
apply (auto simp add: is_trans_of_def)
done
lemma exec_in_sig:
"is_trans_of A \ x \ executions A \ Forall (\a. a \ act A) (filter_act \ (snd x))"
apply (simp add: executions_def)
apply (pair x)
apply (rule execfrag_in_sig [THEN spec, THEN mp])
apply auto
done
lemma scheds_in_sig: "is_trans_of A \ x \ schedules A \ Forall (\a. a \ act A) x"
apply (unfold schedules_def has_schedule_def [abs_def])
apply (fast intro!: exec_in_sig)
done
subsection \<open>Executions are prefix closed\<close>
(*only admissible in y, not if done in x!*)
lemma execfrag_prefixclosed: "\x s. is_exec_frag A (s, x) \ y \ x \ is_exec_frag A (s, y)"
apply (pair_induct y simp: is_exec_frag_def)
apply (intro strip)
apply (Seq_case_simp x)
apply (pair a)
apply auto
done
lemmas exec_prefixclosed =
conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp]]
(*second prefix notion for Finite x*)
lemma exec_prefix2closed [rule_format]:
"\y s. is_exec_frag A (s, x @@ y) \ is_exec_frag A (s, x)"
apply (pair_induct x simp: is_exec_frag_def)
apply (intro strip)
apply (Seq_case_simp s)
apply (pair a)
apply auto
done
end
¤ Dauer der Verarbeitung: 0.6 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
