# Theory Traces

theory Traces
imports Sequence Automata
```(*  Title:      HOL/HOLCF/IOA/Traces.thy
Author:     Olaf MÃ¼ller
*)

section ‹Executions and Traces of I/O automata in HOLCF›

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 × 'a signature"
type_synonym 'a trace_module = "'a trace set × 'a signature"

subsection ‹Executions›

definition is_exec_fragC :: "('a, 's) ioa ⇒ ('a, 's) pairs → 's ⇒ tr"
where "is_exec_fragC A =
(fix ⋅
(LAM h ex.
(λs.
case ex of
nil ⇒ TT
| x ## xs ⇒ flift1 (λp. Def ((s, p) ∈ trans_of A) andalso (h ⋅ xs) (snd p)) ⋅ 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 ‹Schedules›

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 ‹Traces›

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 ‹Fair Traces›

definition laststate :: "('a, 's) execution ⇒ 's"
where "laststate ex =
(case Last ⋅ (snd ex) of
UU ⇒ fst ex
| Def at ⇒ snd at)"

text ‹A predicate holds infinitely (finitely) often in a sequence.›
definition inf_often :: "('a ⇒ bool) ⇒ 'a Seq ⇒ bool"
where "inf_often P s ⟷ Infinite (Filter P ⋅ s)"

text ‹Filtering ‹P› yields a finite or partial sequence.›
definition fin_often :: "('a ⇒ bool) ⇒ 'a Seq ⇒ bool"
where "fin_often P s ⟷ ¬ inf_often P s"

subsection ‹Fairness of executions›

text ‹
Note that partial execs cannot be ‹wfair› as the inf_often predicate in the
else branch prohibits it. However they can be ‹sfair› in the case when all
‹W› are only finitely often enabled: Is this the right model?

See 🗏‹LiveIOA.thy› for solution conforming with the literature and
superseding this one.
›

definition is_wfair :: "('a, 's) ioa ⇒ 'a set ⇒ ('a, 's) execution ⇒ bool"
where "is_wfair A W ex ⟷
(inf_often (λx. fst x ∈ W) (snd ex) ∨
inf_often (λx. ¬ Enabled A W (snd x)) (snd ex))"

definition wfair_ex :: "('a, 's) ioa ⇒ ('a, 's) execution ⇒ bool"
where "wfair_ex A ex ⟷
(∀W ∈ wfair_of A.
if Finite (snd ex)
then ¬ 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 (λx. fst x ∈ W) (snd ex) ∨
fin_often (λx. Enabled A W (snd x)) (snd ex))"

definition sfair_ex :: "('a, 's)ioa ⇒ ('a, 's) execution ⇒ bool"
where "sfair_ex A ex ⟷
(∀W ∈ sfair_of A.
if Finite (snd ex)
then ¬ 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 ‹Fair behavior sets.›

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 ‹Implementation›

subsubsection ‹Notions of implementation›

definition ioa_implements :: "('a, 's1) ioa ⇒ ('a, 's2) ioa ⇒ bool"  (infixr "=<|" 12)
where "(ioa1 =<| ioa2) ⟷
(inputs (asig_of ioa1) = inputs (asig_of ioa2) ∧
outputs (asig_of ioa1) = outputs (asig_of ioa2)) ∧
traces ioa1 ⊆ traces ioa2"

definition fair_implements :: "('a, 's1) ioa ⇒ ('a, 's2) ioa ⇒ bool"
where "fair_implements C A ⟷
inp C = inp A ∧ out C = out A ∧ fairtraces C ⊆ fairtraces A"

lemma implements_trans: "A =<| B ⟹ B =<| C ⟹ A =<| C"

subsection ‹Modules›

subsubsection ‹Execution, schedule and trace modules›

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 ‹map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")›

lemmas exec_rws = executions_def is_exec_frag_def

subsection ‹Recursive equations of operators›

subsubsection ‹‹filter_act››

lemma filter_act_UU: "filter_act ⋅ UU = UU"

lemma filter_act_nil: "filter_act ⋅ nil = nil"

lemma filter_act_cons: "filter_act ⋅ (x ↝ xs) = fst x ↝ filter_act ⋅ xs"

declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp]

subsubsection ‹‹mk_trace››

lemma mk_trace_UU: "mk_trace A ⋅ UU = UU"

lemma mk_trace_nil: "mk_trace A ⋅ nil = nil"

lemma mk_trace_cons:
"mk_trace A ⋅ (at ↝ xs) =
(if fst at ∈ ext A
then fst at ↝ mk_trace A ⋅ xs
else mk_trace A ⋅ xs)"

declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp]

subsubsection ‹‹is_exec_fragC››

lemma is_exec_fragC_unfold:
"is_exec_fragC A =
(LAM ex.
(λs.
case ex of
nil ⇒ TT
| x ## xs ⇒
(flift1 (λp. Def ((s, p) ∈ trans_of A) andalso (is_exec_fragC A⋅xs) (snd p)) ⋅ x)))"
apply (rule trans)
apply (rule fix_eq4)
apply (rule is_exec_fragC_def)
apply (rule beta_cfun)
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) ∈ trans_of A) andalso (is_exec_fragC A ⋅ xs) (snd pr))"
apply (rule trans)
apply (subst is_exec_fragC_unfold)
apply simp
done

declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp]

subsubsection ‹‹is_exec_frag››

lemma is_exec_frag_UU: "is_exec_frag A (s, UU)"

lemma is_exec_frag_nil: "is_exec_frag A (s, nil)"

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)"

declare is_exec_frag_UU [simp] is_exec_frag_nil [simp] is_exec_frag_cons [simp]

subsubsection ‹‹laststate››

lemma laststate_UU: "laststate (s, UU) = s"

lemma laststate_nil: "laststate (s, nil) = s"

lemma laststate_cons: "Finite ex ⟹ laststate (s, at ↝ ex) = laststate (snd at, ex)"
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 ‹‹has_trace› ‹mk_trace››

(*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 ‹Signatures and executions, schedules›

text ‹
All executions of ‹A› have only actions of ‹A›. This is only true because of
the predicate ‹state_trans› (part of the predicate ‹IOA›): We have no
dependent types. For executions of parallel automata this assumption is not
needed, as in ‹par_def› this condition is included once more. (See Lemmas
1.1.1c in CompoExecs for example.)
›

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 ‹main case›
done

lemma exec_in_sig:
"is_trans_of A ⟹ x ∈ executions A ⟹ Forall (λa. a ∈ act A) (filter_act ⋅ (snd x))"
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 ‹Executions are prefix closed›

(*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
```