Theory OAWN_SOS_Labels

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

section "Configure the inv-cterms tactic for open sequential processes"

theory OAWN_SOS_Labels
imports OAWN_SOS Inv_Cterms
begin

lemma oelimder_guard:
  assumes "p = {l}⟨fg⟩ qq"
      and "l' ∈ labels Γ q"
      and "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
  obtains p' where "p = {l}⟨fg⟩ p'"
               and "l' ∈ labels Γ qq"
  using assms by auto

lemma oelimder_assign:
  assumes "p = {l}⟦fa⟧ qq"
      and "l' ∈ labels Γ q"
      and "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
  obtains p' where "p = {l}⟦fa⟧ p'"
               and "l' ∈ labels Γ qq"
  using assms by auto

lemma oelimder_ucast:
  assumes "p = {l}unicast(fip, fmsg).q1 ▹ q2"
      and "l' ∈ labels Γ q"
      and "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
  obtains p' pp' where "p = {l}unicast(fip, fmsg).p' ▹ pp'"
                   and "case a of unicast _ _ ⇒ l' ∈ labels Γ q1
                                        | _ ⇒ l' ∈ labels Γ q2"
  using assms by simp (erule oseqpTEs, auto)

lemma oelimder_bcast:
  assumes "p = {l}broadcast(fmsg).qq"
      and "l' ∈ labels Γ q"
      and "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
  obtains p' where "p = {l}broadcast(fmsg). p'"
               and "l' ∈ labels Γ qq"
  using assms by auto

lemma oelimder_gcast:
  assumes "p = {l}groupcast(fips, fmsg).qq"
      and "l' ∈ labels Γ q"
      and "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
  obtains p' where "p = {l}groupcast(fips, fmsg). p'"
               and "l' ∈ labels Γ qq"
  using assms by auto

lemma oelimder_send:
  assumes "p = {l}send(fmsg).qq"
      and "l' ∈ labels Γ q"
      and "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
  obtains p' where "p = {l}send(fmsg). p'"
               and "l' ∈ labels Γ qq"
  using assms by auto

lemma oelimder_deliver:
  assumes "p = {l}deliver(fdata).qq"
      and "l' ∈ labels Γ q"
      and "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
  obtains p' where "p = {l}deliver(fdata).p'"
               and "l' ∈ labels Γ qq"
  using assms by auto

lemma oelimder_receive:
  assumes "p = {l}receive(fmsg).qq"
      and "l' ∈ labels Γ q"
      and "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
  obtains p' where "p = {l}receive(fmsg).p'"
               and "l' ∈ labels Γ qq"
  using assms by auto

lemmas oelimders =
   oelimder_guard
   oelimder_assign
   oelimder_ucast
   oelimder_bcast
   oelimder_gcast
   oelimder_send
   oelimder_deliver
   oelimder_receive

declare
  oseqpTEs [cterms_seqte]
  oelimders [cterms_elimders]

end