Theory AWN_SOS_Labels

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

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

theory AWN_SOS_Labels
imports AWN_SOS Inv_Cterms
begin

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

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

lemma elimder_ucast:
  assumes "p = {l}unicast(fip, fmsg).q1 ▹ q2"
      and "l' ∈ labels Γ q"
      and "((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ"
  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 seqpTEs, auto)

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

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

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

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

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

lemmas elimders = 
   elimder_guard
   elimder_assign
   elimder_ucast
   elimder_bcast
   elimder_gcast
   elimder_send
   elimder_deliver
   elimder_receive

declare
  seqpTEs [cterms_seqte]
  elimders [cterms_elimders]

end