Theory AWN_Labels
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 ↝⇘Γ⇙ 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 ↝⇘Γ⇙ q}"
unfolding wellformed_def by (simp add: wf_acc_iff)
hence "p ∈ Wellfounded.acc {(q, p). p ↝⇘Γ⇙ q}" ..
hence "(Γ, p) ∈ Wellfounded.acc {((Γ, q), Γ', p). Γ = Γ' ∧ p ↝⇘Γ⇙ 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⇩1}send(m1). p1 ⊕ {l⇩2}send(m2). p2"}. The iteration over @{term
"cterms Γ"} will cover the two transitions
@{term "(l⇩1, send m1, p1)"} and
@{term "(l⇩2, send m2, p2)"},
but reachability requires the four transitions
@{term "(l⇩1, send m1, p1)"},
@{term "(l⇩1, send m2, p2)"},
@{term "(l⇩2, send m1, p1)"}, and
@{term "(l⇩2, send m2, p2)"}.
In a simply labelled process, the former is sufficient to show the latter, since
@{term "l⇩1 = l⇩2"}.
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⇩1}⟦e⟧ p) ⊕
call(pn)"}. Here @{term "l⇩1"} 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))"