Theory Qmsg

(*  Title:       Qmsg.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Model the standard queuing model"

theory Qmsg
imports AWN_SOS_Labels AWN_Invariants
begin

text ‹Define the queue process›

fun Γ⇩Q⇩M⇩S⇩G :: "('m list, 'm, unit, unit label) seqp_env"
where
  "Γ⇩Q⇩M⇩S⇩G () = labelled () (receive(λmsg msgs. msgs @ [msg]). call(())
           ⊕ ⟨msgs. msgs ≠ []⟩
               (send(λmsgs. hd msgs).
                 (⟦msgs. tl msgs⟧ call(())
                  ⊕ receive(λmsg msgs. tl msgs @ [msg]). call(()))
              ⊕ receive(λmsg msgs. msgs @ [msg]). call(())))"

definition σ⇩Q⇩M⇩S⇩G :: "(('m::msg) list × ('m list, 'm, unit, unit label) seqp) set"
where "σ⇩Q⇩M⇩S⇩G ≡ {([], Γ⇩Q⇩M⇩S⇩G ())}"

abbreviation qmsg
  :: "(('m::msg) list × ('m list, 'm, unit, unit label) seqp, 'm seq_action) automaton"
where
  "qmsg ≡ ⦇ init = σ⇩Q⇩M⇩S⇩G, trans = seqp_sos Γ⇩Q⇩M⇩S⇩G ⦈"

declare Γ⇩Q⇩M⇩S⇩G.simps [simp del, code del]
lemmas Γ⇩Q⇩M⇩S⇩G_simps [simp, code] = Γ⇩Q⇩M⇩S⇩G.simps [simplified]

lemma σ⇩Q⇩M⇩S⇩G_not_empty [simp, intro]: "σ⇩Q⇩M⇩S⇩G ≠ {}"
  unfolding σ⇩Q⇩M⇩S⇩G_def by simp

lemma σ⇩Q⇩M⇩S⇩G_exists [simp]: "∃qmsg q. (qmsg, q) ∈ σ⇩Q⇩M⇩S⇩G"
  unfolding σ⇩Q⇩M⇩S⇩G_def by simp

lemma qmsg_wf [simp]: "wellformed Γ⇩Q⇩M⇩S⇩G"
  by (rule wf_no_direct_calls) auto

lemmas qmsg_labels_not_empty [simp] = labels_not_empty [OF qmsg_wf]

lemma qmsg_control_within [simp]: "control_within Γ⇩Q⇩M⇩S⇩G (init qmsg)"
  unfolding σ⇩Q⇩M⇩S⇩G_def by (rule control_withinI) (auto simp del: Γ⇩Q⇩M⇩S⇩G_simps)

lemma qmsg_simple_labels [simp]: "simple_labels Γ⇩Q⇩M⇩S⇩G"
  unfolding simple_labels_def by auto

lemma qmsg_trans: "trans qmsg = seqp_sos Γ⇩Q⇩M⇩S⇩G"
  by simp

lemma σ⇩Q⇩M⇩S⇩G_labels [simp]: "(ξ, q) ∈ σ⇩Q⇩M⇩S⇩G ⟹  labels Γ⇩Q⇩M⇩S⇩G q = {()-:0}"
  unfolding σ⇩Q⇩M⇩S⇩G_def by simp

lemma qmsg_proc_cases [dest]:
  fixes p pn
  shows "p ∈ ctermsl (Γ⇩Q⇩M⇩S⇩G pn) ⟹ p ∈ ctermsl (Γ⇩Q⇩M⇩S⇩G ())"
  by simp

declare
  Γ⇩Q⇩M⇩S⇩G_simps [cterms_env]
  qmsg_proc_cases [ctermsl_cases]
  seq_invariant_ctermsI [OF qmsg_wf qmsg_control_within qmsg_simple_labels qmsg_trans, cterms_intros]
  seq_step_invariant_ctermsI [OF qmsg_wf qmsg_control_within qmsg_simple_labels qmsg_trans, cterms_intros]

end