# Theory HO_Transition_System

```(*<*)
theory HO_Transition_System
imports Heard_Of.HOModel Refinement
begin
(*>*)

subsection ‹Transition system semantics for HO models›

text ‹The HO development already defines two trace semantics for algorithms in this model, the
coarse- and fine-grained ones. However, both of these are defined on infinite traces. Since the
semantics of our transition systems are defined on finite traces, we also provide such a semantics
for the HO model. Since we only use refinement for safety properties, the result also extend to
infinite traces (although we do not prove this in Isabelle).›

definition CHO_trans where
"CHO_trans A HOs SHOs coord =
{((r, st), (r', st'))|r r' st st'.
r' = Suc r
∧ CSHOnextConfig A r st (HOs r) (SHOs r) (coord r) st'
}"

definition CHO_to_TS ::
"('proc, 'pst, 'msg) CHOAlgorithm
⇒ (nat ⇒ 'proc HO)
⇒ (nat ⇒ 'proc HO)
⇒ (nat ⇒ 'proc coord)
⇒ (nat × ('proc ⇒ 'pst)) TS"
where
"CHO_to_TS A HOs SHOs coord ≡ ⦇
init = {(0, st)|st. CHOinitConfig A st (coord 0)},
trans = CHO_trans A HOs SHOs coord
⦈"

definition get_msgs ::
"('proc ⇒ 'proc ⇒ 'pst ⇒ 'msg)
⇒ ('proc ⇒ 'pst)
⇒ 'proc HO
⇒ 'proc HO
⇒ 'proc ⇒ ('proc ⇀ 'msg)set"
where
"get_msgs snd_f cfg HO SHO ≡ λp.
{μ. (∀q. q ∈ HO p ⟷ μ q ≠ None)
∧ (∀q. q ∈ SHO p ∩ HO p ⟶ μ q = Some (snd_f q p (cfg q)))}"

definition CSHO_trans_alt
::
"(nat ⇒ 'proc ⇒ 'proc ⇒ 'pst ⇒ 'msg)
⇒ (nat ⇒ 'proc ⇒ 'pst ⇒ ('proc ⇀ 'msg) ⇒ 'proc ⇒ 'pst ⇒ bool)
⇒ (nat ⇒ 'proc HO)
⇒ (nat ⇒ 'proc HO)
⇒ (nat ⇒ 'proc ⇒ 'proc)
⇒ ((nat × ('proc ⇒ 'pst)) × (nat × ('proc ⇒ 'pst)))set"
where
"CSHO_trans_alt snd_f nxt_st HOs SHOs coords ≡
⋃r μ. {((r, cfg), (Suc r, cfg'))|cfg cfg'. ∀p.
μ p ∈ (get_msgs (snd_f r) cfg (HOs r) (SHOs r) p)
∧ (∀p. nxt_st r p (cfg p) (μ p) (coords r p) (cfg' p))
}"

lemma CHO_trans_alt:
"CHO_trans A HOs SHOs coords = CSHO_trans_alt (sendMsg A) (CnextState A) HOs SHOs coords"
apply(rule equalityI)
apply(force simp add: CHO_trans_def CSHO_trans_alt_def CSHOnextConfig_def SHOmsgVectors_def
apply(force simp add: CHO_trans_def CSHO_trans_alt_def CSHOnextConfig_def SHOmsgVectors_def
done

definition K where
"K y ≡ λx. y"

lemma SHOmsgVectors_get_msgs:
"SHOmsgVectors A r p cfg HOp SHOp = get_msgs (sendMsg A r) cfg (K HOp) (K SHOp) p"
by(auto simp add: SHOmsgVectors_def get_msgs_def K_def)

lemma get_msgs_K:
"get_msgs snd_f cfg (K (HOs r p)) (K (SHOs r p)) p
= get_msgs snd_f cfg (HOs r) (SHOs r) p"

lemma CSHORun_get_msgs:
"CSHORun (A ::  ('proc, 'pst, 'msg) CHOAlgorithm) rho HOs SHOs coords = (
CHOinitConfig A (rho 0) (coords 0)
∧ (∀r. ∃μ.
(∀p.
μ p ∈ get_msgs (sendMsg A r) (rho r) (HOs r) (SHOs r) p
∧ CnextState A r p (rho r p) (μ p) (coords (Suc r) p) (rho (Suc r) p))))"
by(auto simp add: CSHORun_def CSHOnextConfig_def SHOmsgVectors_get_msgs nextState_def get_msgs_K
Bex_def choice_iff)

lemmas CSHORun_step = CSHORun_get_msgs[THEN iffD1, THEN conjunct2]

lemma get_msgs_dom:
"msgs ∈ get_msgs send s HOs SHOs p ⟹ dom msgs = HOs p"