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 
    get_msgs_def restrict_map_def map_add_def choice_iff)
  apply(force simp add: CHO_trans_def CSHO_trans_alt_def CSHOnextConfig_def SHOmsgVectors_def 
    get_msgs_def restrict_map_def map_add_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"
  by(auto simp add: get_msgs_def K_def)

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"
  by(auto simp add: get_msgs_def)

lemma get_msgs_benign:
  "get_msgs snd_f cfg HOs HOs p = { (Some o (λq. (snd_f q p (cfg q)))) |` (HOs p)}"
  by(auto simp add: get_msgs_def restrict_map_def)

end