Quelle  AWN_Labels.thy

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

section "Labelling sequential processes"

theory AWN_Labels
imports AWN AWN_Cterms
begin

subsection "Labels "

text ‹
 Labels serve two main purposes. They allow the substitution of @{term sterm}s in
 @{term invariant} proofs. They also allow the strengthening (control state dependent)
 of invariants.
 ›

function (domintros) labels
  :: "('s, 'm, 'p, 'l) seqp_env ==> ('s, 'm, 'p, 'l) seqp ==> 'l set"
  where
    "labels Γ ({l}⟨fg⟩ p) = {l}"
  | "labels Γ ({l}[fa] p) = {l}"
  | "labels Γ (p1 ⊕ p2) = labels Γ p1 ∪ labels Γ p2"
  | "labels Γ ({l}unicast(fip, fmsg).p ▹ q) = {l}"
  | "labels Γ ({l}broadcast(fmsg). p) = {l}"
  | "labels Γ ({l}groupcast(fips, fmsg). p) = {l}"
  | "labels Γ ({l}send(fmsg).p) = {l}"
  | "labels Γ ({l}deliver(fdata).p) = {l}"
  | "labels Γ ({l}receive(fmsg).p) = {l}"
  | "labels Γ (call(pn)) = labels Γ (Γ pn)"
  by pat_completeness auto

lemma labels_dom_basic [simp]:
  assumes "not_call p"
      and "not_choice p"
  shows "labels_dom (Γ, p)"
  proof (rule accpI)
    fix y
    assume "labels_rel y (Γ, p)"
    with assms show "labels_dom y"
      by (cases p) (auto simp: labels_rel.simps)
  qed

lemma labels_termination:
    fixes Γ p
  assumes "wellformed(Γ)"
    shows "labels_dom (Γ, p)"
  proof -
    have labels_rel': "labels_rel = (λgq gp. (gq, gp) ∈ {((Γ, q), (Γ', p)). Γ = Γ' ∧ p ↝_<Gamma> q})"
      by (rule ext)+ (auto simp: labels_rel.simps intro: microstep.intros elim: microstep.cases)
    from ‹wellformed(Γ)› have "∀x. x ∈ Wellfounded.acc {(q, p). p ↝_<Gamma> q}"
      unfolding wellformed_def by (simp add: wf_iff_acc)
    hence "p ∈ Wellfounded.acc {(q, p). p ↝_<Gamma> q}" ..
    hence "(Γ, p) ∈ Wellfounded.acc {((Γ, q), Γ', p). Γ = Γ' ∧ p ↝_<Gamma> q}"
      by (rule acc_induct) (auto intro: accI)
    thus "labels_dom (Γ, p)"
      unfolding labels_rel' by (subst accp_acc_eq)
  qed

declare labels.psimps[simp]

lemmas labels_pinduct = labels.pinduct [OF labels_termination]
   and labels_psimps[simp] = labels.psimps [OF labels_termination]

lemma labels_not_empty:
    fixes Γ p
  assumes "wellformed Γ"
    shows "labels Γ p ≠ {}"
   by (induct p rule: labels_pinduct [OF ‹wellformed Γ›]) simp_all

lemma has_label [dest]:
    fixes Γ p
  assumes "wellformed Γ"
    shows "∃l. l ∈ labels Γ p"
  using labels_not_empty [OF assms] by auto

lemma singleton_labels [simp]:
  "∧Γ l l' f p. l ∈ labels Γ ({l'}⟨f⟩ p) = (l = l')"
  "∧Γ l l' f p. l ∈ labels Γ ({l'}[f] p) = (l = l')"
  "∧Γ l l' fip fmsg p q. l ∈ labels Γ ({l'}unicast(fip, fmsg).p ▹ q) = (l = l')"
  "∧Γ l l' fmsg p. l ∈ labels Γ ({l'}broadcast(fmsg). p) = (l = l')"
  "∧Γ l l' fips fmsg p. l ∈ labels Γ ({l'}groupcast(fips, fmsg). p) = (l = l')"
  "∧Γ l l' fmsg p. l ∈ labels Γ ({l'}send(fmsg).p) = (l = l')"
  "∧Γ l l' fdata p. l ∈ labels Γ ({l'}deliver(fdata).p) = (l = l')"
  "∧Γ l l' fmsg p. l ∈ labels Γ ({l'}receive(fmsg).p) = (l = l')"
  by auto

lemma in_labels_singletons [dest!]:
  "∧Γ l l' f p. l ∈ labels Γ ({l'}⟨f⟩ p) ==> l = l'"
  "∧Γ l l' f p. l ∈ labels Γ ({l'}[f] p) ==> l = l'"
  "∧Γ l l' fip fmsg p q. l ∈ labels Γ ({l'}unicast(fip, fmsg).p ▹ q) ==> l = l'"
  "∧Γ l l' fmsg p. l ∈ labels Γ ({l'}broadcast(fmsg). p) ==> l = l'"
  "∧Γ l l' fips fmsg p. l ∈ labels Γ ({l'}groupcast(fips, fmsg). p) ==> l = l'"
  "∧Γ l l' fmsg p. l ∈ labels Γ ({l'}send(fmsg).p) ==> l = l'"
  "∧Γ l l' fdata p. l ∈ labels Γ ({l'}deliver(fdata).p) ==> l = l'"
  "∧Γ l l' fmsg p. l ∈ labels Γ ({l'}receive(fmsg).p) ==> l = l'"
  by auto

definition
  simple_labels :: "('s, 'm, 'p, 'l) seqp_env ==> bool"
where
  "simple_labels Γ ≡ ∀pn. ∀p∈subterms (Γ pn). (∃!l. labels Γ p = {l})"

lemma simple_labelsI [intro]:
  assumes "∧pn p. p∈subterms (Γ pn) ==> ∃!l. labels Γ p = {l}"
  shows "simple_labels Γ"
  using assms unfolding simple_labels_def by auto

text ‹
 The @{term "simple_labels Γ"} property is necessary to transfer results shown over the
 @{term "cterms"} of a process specification @{term "Γ"} to the reachable actions of
 that process.

 Consider the process @{term "{l₁}send(m1). p1 ⊕ {l₂}send(m2). p2"}. The iteration over @{term
 "cterms Γ"} will cover the two transitions
 @{term "(l₁, send m1, p1)"} and
 @{term "(l₂, send m2, p2)"},
 but reachability requires the four transitions
 @{term "(l₁, send m1, p1)"},
 @{term "(l₁, send m2, p2)"},
 @{term "(l₂, send m1, p1)"}, and
 @{term "(l₂, send m2, p2)"}.

 In a simply labelled process, the former is sufficient to show the latter, since
 @{term "l₁ = l₂"}.

 This requirement seems really only to be restrictive for processes where a @{term "call(pn)"}
 occurs as a direct subterm of a choice operator. Consider, for instance, @{term "({l₁}[e] p) ⊕
 call(pn)"}. Here @{term "l₁"} must equal the label of @{term "Γ(pn)"}, which can then not be
 distinguished from any other subterm that calls @{term "pn"} in any other process.

 This limitation stems from the fact that the "call points" of a process are effectively treated as
 the root of the called process. This is by design; we try to treat call sites as "syntactic
 pastings" of process terms, giving rise, conceptually, to an infinite tree structure. But this
 prejudices the alternative view that process calls are used as "join points" of "process threads",
 in complement to the "fork points" of the @{term "p1 ⊕ p2"} operator.
 ›

lemma simple_labels_in_sterms:
    fixes Γ l p
  assumes "simple_labels Γ"
      and "wellformed Γ"
      and "∃pn. p∈subterms (Γ pn)"
      and "l∈labels Γ p"
    shows "∀p'∈sterms Γ p. l∈labels Γ p'"
  using assms
  proof (induct p rule: labels_pinduct [OF ‹wellformed Γ›])
    fix Γ p1 p2
    assume sl: "simple_labels Γ"
       and wf: "wellformed Γ"
       and IH1: "[ simple_labels Γ; wellformed Γ;
                   ∃pn. p1 ∈ subterms (Γ pn); l ∈ labels Γ p1 ]
                 ==> ∀p'∈sterms Γ p1. l ∈ labels Γ p'"
       and IH2: "[ simple_labels Γ; wellformed Γ;
                   ∃pn. p2 ∈ subterms (Γ pn); l ∈ labels Γ p2 ]
                 ==> ∀p'∈sterms Γ p2. l ∈ labels Γ p'"
       and ein: "∃pn. p1 ⊕ p2 ∈ subterms (Γ pn)"
       and l12: "l ∈ labels Γ (p1 ⊕ p2)"
    from sl ein l12 have "labels Γ (p1 ⊕ p2) = {l}"
      unfolding simple_labels_def by (metis empty_iff insert_iff)
    with wf have "labels Γ p1 ∪ labels Γ p2 = {l}" by simp
    moreover have "labels Γ p1 ≠ {}" and "labels Γ p2 ≠ {}"
      using wf by (metis labels_not_empty)+
    ultimately have "l ∈ labels Γ p1" and "l ∈ labels Γ p2"
      by (metis Un_iff empty_iff insert_iff set_eqI)+
    moreover from ein have "∃pn. p1 ∈ subterms (Γ pn)"
                       and "∃pn. p2 ∈ subterms (Γ pn)"
       by auto
    ultimately show "∀p'∈sterms Γ (p1 ⊕ p2). l∈labels Γ p'"
      using wf IH1 [OF sl wf] IH2 [OF sl wf] by auto
  qed auto

lemma labels_in_sterms:
    fixes Γ l p
  assumes "wellformed Γ"
      and "l∈labels Γ p"
    shows "∃p'∈sterms Γ p. l∈labels Γ p'"
  using assms
  by (induct p rule: labels_pinduct [OF ‹wellformed Γ›]) (auto intro: Un_iff)

lemma labels_sterms_labels:
    fixes Γ p p' l
  assumes "wellformed Γ"
      and "p' ∈ sterms Γ p"
      and "l ∈ labels Γ p'"
    shows "l ∈ labels Γ p"
  using assms
  by (induct p rule: labels_pinduct [OF ‹wellformed Γ›]) auto

primrec labelfrom :: "int ==> int ==> ('s, 'm, 'p, 'a) seqp ==> int × ('s, 'm, 'p, int) seqp"
where
   "labelfrom n nn ({_}⟨f⟩ p) =
      (let (nn', p') = labelfrom nn (nn + 1) p in
       (nn', {n}⟨f⟩ p'))"
 | "labelfrom n nn ({_}[f] p) =
      (let (nn', p') = labelfrom nn (nn + 1) p in
       (nn', {n}[f] p'))"
 | "labelfrom n nn (p ⊕ q) =
      (let (nn', p') = labelfrom n nn p in
       let (nn'', q') = labelfrom n nn' q in
       (nn'', p' ⊕ q'))"
 | "labelfrom n nn ({_}unicast(fip, fmsg). p ▹ q) =
      (let (nn', p') = labelfrom nn (nn + 1) p in
       let (nn'', q') = labelfrom nn' (nn' + 1) q in
       (nn'', {n}unicast(fip, fmsg). p' ▹ q'))"
 | "labelfrom n nn ({_}broadcast(fmsg). p) =
      (let (nn', p') = labelfrom nn (nn + 1) p in
       (nn', {n}broadcast(fmsg). p'))"
 | "labelfrom n nn ({_}groupcast(fipset, fmsg). p) =
      (let (nn', p') = labelfrom nn (nn + 1) p in
       (nn', {n}groupcast(fipset, fmsg). p'))"
 | "labelfrom n nn ({_}send(fmsg). p) =
      (let (nn', p') = labelfrom nn (nn + 1) p in
       (nn', {n}send(fmsg). p'))"
 | "labelfrom n nn ({_}deliver(fdata). p) =
      (let (nn', p') = labelfrom nn (nn + 1) p in
       (nn', {n}deliver(fdata). p'))"
 | "labelfrom n nn ({_}receive(fmsg). p) =
      (let (nn', p') = labelfrom nn (nn + 1) p in
       (nn', {n}receive(fmsg). p'))"
 | "labelfrom n nn (call(fargs)) = (nn - 1, call(fargs))"

datatype 'pn label =
    LABEL 'pn int  (‹_-:_› [1000, 1000] 999)

instantiation "label" :: (ord) ord
begin

fun less_eq_label :: "'a label ==> 'a label ==> bool"
where "(l1-:n1) ≤ (l2-:n2) = (l1 = l2 ∧ n1 ≤ n2)"

definition less_label: "(l1::'a label) < l2 ⟷ l1 ≤ l2 ∧ ¬ (l1 ≤ l2)"

instance ..
end

abbreviation labelled :: "'p ==> ('s, 'm, 'p, 'a) seqp ==> ('s, 'm, 'p, 'p label) seqp"
where "labelled pn p ≡ labelmap (λl. LABEL pn l) (snd (labelfrom 0 1 p))"

end