Theory Broadcast_Thms

theory Broadcast_Thms
  imports Broadcast_Chain Broadcast_Frame Semantics Simulation Bisimulation Sim_Pres
  Sim_Struct_Cong Bisim_Pres Bisim_Struct_Cong Bisim_Subst
begin

context env
begin

  subsection ‹Syntax›

  subsubsection ‹Psi calculus agents~-- Definition~2›

  text ‹
    @{term M}, @{term N} range over message terms. @{term P}, @{term Q} range over processes.
    @{term C} ranges over cases.

    ▪ Output: @{term "M⟨N⟩.P"}
    ▪ Input: @{term "M⦇λ*xvec N⦈.P"}
    ▪ Case: @{term "Case C"}
    ▪ Par: @{term "(P ∥ Q)"}
    ▪ Res: @{term "⦇νx⦈(P::('a,'b,'c) psi)"}
    ▪ Assert: @{term "⦃Ψ⦄"}
    ▪ Bang: @{term "!P"}
  ›

  text ‹
    ▪ Cases: @{term "□ φ ⇒ P C"}
  ›

  subsubsection ‹Parameters~-- Definition~1›

  text ‹
    ▪ Channel equivalence: @{term "M ↔ N"}
    ▪ Composition: @{term "Ψ⇩P ⊗ Ψ⇩Q"}
    ▪ Unit: @{term "𝟭"}
    ▪ Entailment: @{term "Ψ ⊢ φ"}
  ›

  subsubsection ‹Extra predicates for broadcast~-- Definition~5›

  text ‹
    ▪ Output connectivity: @{term "M ≼ N"}
    ▪ Input connectivity: @{term "M ≽ N"}
  ›

  subsubsection ‹Transitions~-- Definition~3›

  text ‹
    ▪ @{term "Ψ ⊳ P ⟼α P'"}
  ›

  subsubsection ‹Actions (\texorpdfstring{@{term α}}{alpha})~-- Definition~7›

  text ‹
    ▪ Input: @{term "M⦇N⦈"}
    ▪ Output: @{term "M⦇ν*xvec⦈⟨N⟩"}
    ▪ Broadcast input: @{term "¿M⦇N⦈"}
    ▪ Broadcast output: @{term "¡M⦇ν*xvec⦈⟨N⟩"}
    ▪ Silent action: @{term "τ"}
  ›

  subsection ‹Semantics›

  subsubsection ‹Basic Psi semantics~-- Table~1›

  text ‹
    ▪ Theorem {\it Input}:
      @{thm [display] Input[no_vars]}
    ▪ Theorem {\it Output}:
      @{thm [display] Output[no_vars]}
    ▪ Theorem {\it Case}:
      @{thm [display] Case[no_vars]}
    ▪ Theorems {\it Par1} and {\it Par2}:
      @{thm [display] Par1[no_vars]}
      @{thm [display] Par2[no_vars]}
    ▪ Theorems {\it Comm1} and {\it Comm2}:
      @{thm [display] Comm1[no_vars]}
      @{thm [display] Comm2[no_vars]}
    ▪ Theorem {\it Open}:
      @{thm [display] Open[no_vars]}
    ▪ Theorem {\it Scope}:
      @{thm [display] Scope[no_vars]}
    ▪ Theorem {\it Bang}:
      @{thm [display] Bang[no_vars]}
  ›

  subsubsection ‹Broadcast rules~-- Table~2›

  text ‹
    ▪ Theorem {\it BrInput}:
      @{thm [display] BrInput[no_vars]}
    ▪ Theorem {\it BrOutput}:
      @{thm [display] BrOutput[no_vars]}
    ▪ Theorem {\it BrMerge}:
      @{thm [display] BrMerge[no_vars]}
    ▪ Theorems {\it BrComm1} and {\it BrComm2}:
      @{thm [display] BrComm1[no_vars]}
      @{thm [display] BrComm2[no_vars]}
    ▪ Theorem {\it BrClose}:
      @{thm [display] BrClose[no_vars]}
    ▪ Theorem {\it BrOpen}:
      @{thm [display] BrOpen[no_vars]}
  ›

  subsubsection ‹Requirements for broadcast~-- Definition~6›

  text ‹
    ▪ Theorem {\it chanOutConSupp}:
      @{thm [display] chanOutConSupp[no_vars]}
    ▪ Theorem {\it chanInConSupp}:
      @{thm [display] chanInConSupp[no_vars]}
  ›

  subsubsection ‹Strong bisimulation~-- Definition~4›

  text ‹
    ▪ Theorem {\it bisim.step}:
      @{thm [display] bisim.step[no_vars]}
  ›

  subsection ‹Theorems›

  subsubsection ‹Congruence properties of strong bisimulation~-- Theorem~8›

  text ‹
    ▪ Theorem {\it bisimOutputPres}:
      @{thm [display] bisimOutputPres[no_vars]}
    ▪ Theorem {\it bisimInputPres}:
      @{thm [display] bisimInputPres[no_vars]}
    ▪ Theorem {\it bisimCasePres}:
      @{thm [display] bisimCasePres[no_vars]}
    ▪ Theorems {\it bisimParPres} and {\it bisimParPresSym}:
      @{thm [display] bisimParPres[no_vars]}
      @{thm [display] bisimParPresSym[no_vars]}
    ▪ Theorem {\it bisimResPres}:
      @{thm [display] bisimResPres[no_vars]}
    ▪ Theorem {\it bisimBangPres}:
      @{thm [display] bisimBangPres[no_vars]}
  ›

  subsubsection ‹Strong congruence, bisimulation closed under substitution~-- Definition~9›

  text ‹
    ▪ Theorem {\it closeSubst\_def}:
      @{thm [display] closeSubst_def[no_vars]}
    ▪ @{term "Ψ ⊳ P ∼⇩s Q"}
  ›

  subsubsection ‹Strong congruence is a process congruence for all \texorpdfstring{@{term Ψ}}{Psi}~-- Theorem~10›

  text ‹
    ▪ Theorem {\it bisimSubstOutputPres}:
      @{thm [display] bisimSubstOutputPres[no_vars]}
    ▪ Theorem {\it bisimSubstInputPres}:
      @{thm [display] bisimSubstInputPres[no_vars]}
    ▪ Theorem {\it bisimSubstCasePres}:
      @{thm [display] bisimSubstCasePres[no_vars]}
    ▪ Theorem {\it bisimSubstParPres}:
      @{thm [display] bisimSubstParPres[no_vars]}
    ▪ Theorem {\it bisimSubstResPres}:
      @{thm [display] bisimSubstResPres[no_vars]}
    ▪ Theorem {\it bisimSubstBangPres}:
      @{thm [display] bisimSubstBangPres[no_vars]}
  ›

  subsubsection ‹Structural equivalence~-- Theorem~11›

  text ‹
    ▪ Theorem {\it bisimCasePushRes}:
      @{thm [display] bisimCasePushRes[no_vars]}
    ▪ Theorem {\it bisimInputPushRes}:
      @{thm [display] bisimInputPushRes[no_vars]}
    ▪ Theorem {\it bisimOutputPushRes}:
      @{thm [display] bisimOutputPushRes[no_vars]}
    ▪ Theorem {\it bisimParAssoc}:
      @{thm [display] bisimParAssoc[no_vars]}
    ▪ Theorem {\it bisimParComm}:
      @{thm [display] bisimParComm[no_vars]}
    ▪ Theorem {\it bisimResNil}:
      @{thm [display] bisimResNil[no_vars]}
    ▪ Theorem {\it bisimScopeExt}:
      @{thm [display] bisimScopeExt[no_vars]}
    ▪ Theorem {\it bisimResComm}:
      @{thm [display] bisimResComm[no_vars]}
    ▪ Theorem {\it bangExt}:
      @{thm [display] bangExt[no_vars]}
    ▪ Theorem {\it bisimParNil}:
      @{thm [display] bisimParNil[no_vars]}
  ›

  subsubsection ‹Support of processes in broadcast transitions~-- Lemma~14›

  text ‹
    ▪ Theorem {\it brInputTermSupp}:
      @{thm [display] brInputTermSupp[no_vars]}
    ▪ Theorem {\it brOutputTermSupp}:
      @{thm [display] brOutputTermSupp[no_vars]}
  ›

end

end