Theory OAWN_Invariants
section "Generic open invariants on sequential AWN processes"
theory OAWN_Invariants
imports Invariants OInvariants
AWN_Cterms AWN_Labels AWN_Invariants
OAWN_SOS
begin
subsection "Open invariants via labelled control terms"
lemma oseqp_sos_subterms:
assumes "wellformed Γ"
and "∃pn. p ∈ subterms (Γ pn)"
and "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i"
shows "∃pn. p' ∈ subterms (Γ pn)"
using assms
proof (induct p)
fix p1 p2
assume IH1: "∃pn. p1 ∈ subterms (Γ pn) ⟹
((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i ⟹
∃pn. p' ∈ subterms (Γ pn)"
and IH2: "∃pn. p2 ∈ subterms (Γ pn) ⟹
((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i ⟹
∃pn. p' ∈ subterms (Γ pn)"
and "∃pn. p1 ⊕ p2 ∈ subterms (Γ pn)"
and "((σ, p1 ⊕ p2), a, (σ', p')) ∈ oseqp_sos Γ i"
from ‹∃pn. p1 ⊕ p2 ∈ subterms (Γ pn)› obtain pn
where "p1 ∈ subterms (Γ pn)"
and "p2 ∈ subterms (Γ pn)" by auto
from ‹((σ, p1 ⊕ p2), a, (σ', p')) ∈ oseqp_sos Γ i›
have "((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i
∨ ((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i" by auto
thus "∃pn. p' ∈ subterms (Γ pn)"
proof
assume "((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i"
with ‹p1 ∈ subterms (Γ pn)› show ?thesis by (auto intro: IH1)
next
assume "((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i"
with ‹p2 ∈ subterms (Γ pn)› show ?thesis by (auto intro: IH2)
qed
qed auto
lemma oreachable_subterms:
assumes "wellformed Γ"
and "control_within Γ (init A)"
and "trans A = oseqp_sos Γ i"
and "(σ, p) ∈ oreachable A S U"
shows "∃pn. p ∈ subterms (Γ pn)"
using assms(4)
proof (induct rule: oreachable_pair_induct)
fix σ p
assume "(σ, p) ∈ init A"
with ‹control_within Γ (init A)› show "∃pn. p ∈ subterms (Γ pn)" ..
next
fix σ p a σ' p'
assume "(σ, p) ∈ oreachable A S U"
and "∃pn. p ∈ subterms (Γ pn)"
and 3: "((σ, p), a, (σ', p')) ∈ trans A"
and "S σ σ' a"
moreover from 3 and ‹trans A = oseqp_sos Γ i›
have "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i" by simp
ultimately show "∃pn. p' ∈ subterms (Γ pn)"
using ‹wellformed Γ›
by (auto elim: oseqp_sos_subterms)
qed
lemma onl_oinvariantI [intro]:
assumes init: "⋀σ p l. ⟦ (σ, p) ∈ init A; l ∈ labels Γ p ⟧ ⟹ P (σ, l)"
and other: "⋀σ σ' p l. ⟦ (σ, p) ∈ oreachable A S U;
∀l∈labels Γ p. P (σ, l);
U σ σ' ⟧ ⟹ ∀l∈labels Γ p. P (σ', l)"
and step: "⋀σ p a σ' p' l'.
⟦ (σ, p) ∈ oreachable A S U;
∀l∈labels Γ p. P (σ, l);
((σ, p), a, (σ', p')) ∈ trans A;
l' ∈ labels Γ p';
S σ σ' a ⟧ ⟹ P (σ', l')"
shows "A ⊨ (S, U →) onl Γ P"
proof
fix σ p
assume "(σ, p) ∈ init A"
hence "∀l∈labels Γ p. P (σ, l)" using init by simp
thus "onl Γ P (σ, p)" ..
next
fix σ p a σ' p'
assume rp: "(σ, p) ∈ oreachable A S U"
and "onl Γ P (σ, p)"
and tr: "((σ, p), a, (σ', p')) ∈ trans A"
and "S σ σ' a"
from ‹onl Γ P (σ, p)› have "∀l∈labels Γ p. P (σ, l)" ..
with rp tr ‹S σ σ' a› have "∀l'∈labels Γ p'. P (σ', l')" by (auto elim: step)
thus "onl Γ P (σ', p')" ..
next
fix σ σ' p
assume "(σ, p) ∈ oreachable A S U"
and "onl Γ P (σ, p)"
and "U σ σ'"
from ‹onl Γ P (σ, p)› have "∀l∈labels Γ p. P (σ, l)" by auto
with ‹(σ, p) ∈ oreachable A S U› have "∀l∈labels Γ p. P (σ', l)"
using ‹U σ σ'› by (rule other)
thus "onl Γ P (σ', p)" by auto
qed
lemma global_oinvariantI [intro]:
assumes init: "⋀σ p. (σ, p) ∈ init A ⟹ P σ"
and other: "⋀σ σ' p l. ⟦ (σ, p) ∈ oreachable A S U; P σ; U σ σ' ⟧ ⟹ P σ'"
and step: "⋀σ p a σ' p'.
⟦ (σ, p) ∈ oreachable A S U;
P σ;
((σ, p), a, (σ', p')) ∈ trans A;
S σ σ' a ⟧ ⟹ P σ'"
shows "A ⊨ (S, U →) (λ(σ, _). P σ)"
proof
fix σ p
assume "(σ, p) ∈ init A"
thus "(λ(σ, _). P σ) (σ, p)"
by simp (erule init)
next
fix σ p a σ' p'
assume rp: "(σ, p) ∈ oreachable A S U"
and "(λ(σ, _). P σ) (σ, p)"
and tr: "((σ, p), a, (σ', p')) ∈ trans A"
and "S σ σ' a"
from ‹(λ(σ, _). P σ) (σ, p)› have "P σ" by simp
with rp have "P σ'"
using tr ‹S σ σ' a› by (rule step)
thus "(λ(σ, _). P σ) (σ', p')" by simp
next
fix σ σ' p
assume "(σ, p) ∈ oreachable A S U"
and "(λ(σ, _). P σ) (σ, p)"
and "U σ σ'"
hence "P σ'" by simp (erule other)
thus "(λ(σ, _). P σ) (σ', p)" by simp
qed
lemma onl_oinvariantD [dest]:
assumes "A ⊨ (S, U →) onl Γ P"
and "(σ, p) ∈ oreachable A S U"
and "l ∈ labels Γ p"
shows "P (σ, l)"
using assms unfolding onl_def by auto
lemma onl_oinvariant_weakenD [dest]:
assumes "A ⊨ (S', U' →) onl Γ P"
and "(σ, p) ∈ oreachable A S U"
and "l ∈ labels Γ p"
and weakenS: "⋀s s' a. S s s' a ⟹ S' s s' a"
and weakenU: "⋀s s'. U s s' ⟹ U' s s'"
shows "P (σ, l)"
proof -
from ‹(σ, p) ∈ oreachable A S U› have "(σ, p) ∈ oreachable A S' U'"
by (rule oreachable_weakenE)
(erule weakenS, erule weakenU)
with ‹A ⊨ (S', U' →) onl Γ P› show "P (σ, l)"
using ‹l ∈ labels Γ p› ..
qed
lemma onl_oinvariant_initD [dest]:
assumes invP: "A ⊨ (S, U →) onl Γ P"
and init: "(σ, p) ∈ init A"
and pnl: "l ∈ labels Γ p"
shows "P (σ, l)"
proof -
from init have "(σ, p) ∈ oreachable A S U" ..
with invP show ?thesis using pnl ..
qed
lemma onl_oinvariant_sterms:
assumes wf: "wellformed Γ"
and il: "A ⊨ (S, U →) onl Γ P"
and rp: "(σ, p) ∈ oreachable A S U"
and "p'∈sterms Γ p"
and "l∈labels Γ p'"
shows "P (σ, l)"
proof -
from wf ‹p'∈sterms Γ p› ‹l∈labels Γ p'› have "l∈labels Γ p"
by (rule labels_sterms_labels)
with il rp show "P (σ, l)" ..
qed
lemma onl_oinvariant_sterms_weaken:
assumes wf: "wellformed Γ"
and il: "A ⊨ (S', U' →) onl Γ P"
and rp: "(σ, p) ∈ oreachable A S U"
and "p'∈sterms Γ p"
and "l∈labels Γ p'"
and weakenS: "⋀σ σ' a. S σ σ' a ⟹ S' σ σ' a"
and weakenU: "⋀σ σ'. U σ σ' ⟹ U' σ σ'"
shows "P (σ, l)"
proof -
from ‹(σ, p) ∈ oreachable A S U› have "(σ, p) ∈ oreachable A S' U'"
by (rule oreachable_weakenE)
(erule weakenS, erule weakenU)
with assms(1-2) show ?thesis using assms(4-5)
by (rule onl_oinvariant_sterms)
qed
lemma otrans_from_sterms:
assumes "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
and "wellformed Γ"
shows "∃p'∈sterms Γ p. ((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i"
using assms by (induction p rule: sterms_pinduct [OF ‹wellformed Γ›]) auto
lemma otrans_from_sterms':
assumes "((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i"
and "wellformed Γ"
and "p' ∈ sterms Γ p"
shows "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
using assms by (induction p rule: sterms_pinduct [OF ‹wellformed Γ›]) auto
lemma otrans_to_dterms:
assumes "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
and "wellformed Γ"
shows "∀r∈sterms Γ q. r ∈ dterms Γ p"
using assms by (induction q) auto
theorem cterms_includes_sterms_of_oseq_reachable:
assumes "wellformed Γ"
and "control_within Γ (init A)"
and "trans A = oseqp_sos Γ i"
shows "⋃(sterms Γ ` snd ` oreachable A S U) ⊆ cterms Γ"
proof
fix qs
assume "qs ∈ ⋃(sterms Γ ` snd ` oreachable A S U)"
then obtain ξ and q where *: "(ξ, q) ∈ oreachable A S U"
and **: "qs ∈ sterms Γ q" by auto
from * have "⋀x. x ∈ sterms Γ q ⟹ x ∈ cterms Γ"
proof (induction rule: oreachable_pair_induct)
fix σ p q
assume "(σ, p) ∈ init A"
and "q ∈ sterms Γ p"
from ‹control_within Γ (init A)› and ‹(σ, p) ∈ init A›
obtain pn where "p ∈ subterms (Γ pn)" by auto
with ‹wellformed Γ› show "q ∈ cterms Γ" using ‹q∈sterms Γ p›
by (rule subterms_sterms_in_cterms)
next
fix p σ a σ' q x
assume "(σ, p) ∈ oreachable A S U"
and IH: "⋀x. x ∈ sterms Γ p ⟹ x ∈ cterms Γ"
and "((σ, p), a, (σ', q)) ∈ trans A"
and "x ∈ sterms Γ q"
from this(3) and ‹trans A = oseqp_sos Γ i›
have step: "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i" by simp
from step ‹wellformed Γ› obtain ps
where ps: "ps ∈ sterms Γ p"
and step': "((σ, ps), a, (σ', q)) ∈ oseqp_sos Γ i"
by (rule otrans_from_sterms [THEN bexE])
from ps have "ps ∈ cterms Γ" by (rule IH)
moreover from step' ‹wellformed Γ› ‹x ∈ sterms Γ q› have "x ∈ dterms Γ ps"
by (rule otrans_to_dterms [rule_format])
ultimately show "x ∈ cterms Γ" by (rule ctermsDI)
qed
thus "qs ∈ cterms Γ" using ** .
qed
corollary oseq_reachable_in_cterms:
assumes "wellformed Γ"
and "control_within Γ (init A)"
and "trans A = oseqp_sos Γ i"
and "(σ, p) ∈ oreachable A S U"
and "p' ∈ sterms Γ p"
shows "p' ∈ cterms Γ"
using assms(1-3)
proof (rule cterms_includes_sterms_of_oseq_reachable [THEN subsetD])
from assms(4-5) show "p' ∈ ⋃(sterms Γ ` snd ` oreachable A S U)"
by (auto elim!: rev_bexI)
qed
lemma oseq_invariant_ctermI:
assumes wf: "wellformed Γ"
and cw: "control_within Γ (init A)"
and sl: "simple_labels Γ"
and sp: "trans A = oseqp_sos Γ i"
and init: "⋀σ p l. ⟦
(σ, p) ∈ init A;
l∈labels Γ p
⟧ ⟹ P (σ, l)"
and other: "⋀σ σ' p l. ⟦
(σ, p) ∈ oreachable A S U;
l∈labels Γ p;
P (σ, l);
U σ σ' ⟧ ⟹ P (σ', l)"
and local: "⋀p l σ a q l' σ' pp. ⟦
p∈cterms Γ;
l∈labels Γ p;
P (σ, l);
((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i;
((σ, p), a, (σ', q)) ∈ trans A;
l'∈labels Γ q;
(σ, pp)∈oreachable A S U;
p∈sterms Γ pp;
(σ', q)∈oreachable A S U;
S σ σ' a
⟧ ⟹ P (σ', l')"
shows "A ⊨ (S, U →) onl Γ P"
proof
fix σ p l
assume "(σ, p) ∈ init A"
and *: "l ∈ labels Γ p"
with init show "P (σ, l)" by auto
next
fix σ p a σ' q l'
assume sr: "(σ, p) ∈ oreachable A S U"
and pl: "∀l∈labels Γ p. P (σ, l)"
and tr: "((σ, p), a, (σ', q)) ∈ trans A"
and A6: "l' ∈ labels Γ q"
and "S σ σ' a"
thus "P (σ', l')"
proof -
from sr and tr and ‹S σ σ' a› have A7: "(σ', q) ∈ oreachable A S U"
by - (rule oreachable_local')
from tr and sp have tr': "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i" by simp
then obtain p' where "p' ∈ sterms Γ p"
and A4: "((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i"
by (blast dest: otrans_from_sterms [OF _ wf])
from wf cw sp sr this(1) have A1: "p'∈cterms Γ"
by (rule oseq_reachable_in_cterms)
from labels_not_empty [OF wf] obtain ll where A2: "ll∈labels Γ p'"
by blast
with ‹p'∈sterms Γ p› have "ll∈labels Γ p"
by (rule labels_sterms_labels [OF wf])
with pl have A3: "P (σ, ll)" by simp
from sr ‹p'∈sterms Γ p›
obtain pp where A7: "(σ, pp)∈oreachable A S U"
and A8: "p'∈sterms Γ pp"
by auto
from sr tr ‹S σ σ' a› have A9: "(σ', q)∈oreachable A S U"
by - (rule oreachable_local')
from sp and ‹((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i›
have A5: "((σ, p'), a, (σ', q)) ∈ trans A" by simp
from A1 A2 A3 A4 A5 A6 A7 A8 A9 ‹S σ σ' a› show ?thesis by (rule local)
qed
next
fix σ σ' p l
assume sr: "(σ, p) ∈ oreachable A S U"
and "∀l∈labels Γ p. P (σ, l)"
and "U σ σ'"
show "∀l∈labels Γ p. P (σ', l)"
proof
fix l
assume "l∈labels Γ p"
with ‹∀l∈labels Γ p. P (σ, l)› have "P (σ, l)" ..
with sr and ‹l∈labels Γ p›
show "P (σ', l)" using ‹U σ σ'› by (rule other)
qed
qed
lemma oseq_invariant_ctermsI:
assumes wf: "wellformed Γ"
and cw: "control_within Γ (init A)"
and sl: "simple_labels Γ"
and sp: "trans A = oseqp_sos Γ i"
and init: "⋀σ p l. ⟦
(σ, p) ∈ init A;
l∈labels Γ p
⟧ ⟹ P (σ, l)"
and other: "⋀σ σ' p l. ⟦
wellformed Γ;
(σ, p) ∈ oreachable A S U;
l∈labels Γ p;
P (σ, l);
U σ σ' ⟧ ⟹ P (σ', l)"
and local: "⋀p l σ a q l' σ' pp pn. ⟦
wellformed Γ;
p∈ctermsl (Γ pn);
not_call p;
l∈labels Γ p;
P (σ, l);
((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i;
((σ, p), a, (σ', q)) ∈ trans A;
l'∈labels Γ q;
(σ, pp)∈oreachable A S U;
p∈sterms Γ pp;
(σ', q)∈oreachable A S U;
S σ σ' a
⟧ ⟹ P (σ', l')"
shows "A ⊨ (S, U →) onl Γ P"
proof (rule oseq_invariant_ctermI [OF wf cw sl sp])
fix σ p l
assume "(σ, p) ∈ init A"
and "l ∈ labels Γ p"
thus "P (σ, l)" by (rule init)
next
fix σ σ' p l
assume "(σ, p) ∈ oreachable A S U"
and "l ∈ labels Γ p"
and "P (σ, l)"
and "U σ σ'"
with wf show "P (σ', l)" by (rule other)
next
fix p l σ a q l' σ' pp
assume "p ∈ cterms Γ"
and otherassms: "l ∈ labels Γ p"
"P (σ, l)"
"((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
"((σ, p), a, (σ', q)) ∈ trans A"
"l' ∈ labels Γ q"
"(σ, pp) ∈ oreachable A S U"
"p ∈ sterms Γ pp"
"(σ', q) ∈ oreachable A S U"
"S σ σ' a"
from this(1) obtain pn where "p ∈ ctermsl(Γ pn)"
and "not_call p"
unfolding cterms_def' [OF wf] by auto
with wf show "P (σ', l')"
using otherassms by (rule local)
qed
subsection "Open step invariants via labelled control terms"
lemma onll_ostep_invariantI [intro]:
assumes *: "⋀σ p l a σ' p' l'. ⟦ (σ, p)∈oreachable A S U;
((σ, p), a, (σ', p')) ∈ trans A;
S σ σ' a;
l ∈labels Γ p;
l'∈labels Γ p' ⟧
⟹ P ((σ, l), a, (σ', l'))"
shows "A ⊨⇩A (S, U →) onll Γ P"
proof
fix σ p σ' p' a
assume "(σ, p) ∈ oreachable A S U"
and "((σ, p), a, (σ', p')) ∈ trans A"
and "S σ σ' a"
hence "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((σ, l), a, (σ', l'))" by (auto elim!: *)
thus "onll Γ P ((σ, p), a, (σ', p'))" ..
qed
lemma onll_ostep_invariantE [elim]:
assumes "A ⊨⇩A (S, U →) onll Γ P"
and "(σ, p) ∈ oreachable A S U"
and "((σ, p), a, (σ', p')) ∈ trans A"
and "S σ σ' a"
and lp: "l ∈labels Γ p"
and lp': "l'∈labels Γ p'"
shows "P ((σ, l), a, (σ', l'))"
proof -
from assms(1-4) have "onll Γ P ((σ, p), a, (σ', p'))" ..
with lp lp' show "P ((σ, l), a, (σ', l'))" by auto
qed
lemma onll_ostep_invariantD [dest]:
assumes "A ⊨⇩A (S, U →) onll Γ P"
and "(σ, p) ∈ oreachable A S U"
and "((σ, p), a, (σ', p')) ∈ trans A"
and "S σ σ' a"
shows "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((σ, l), a, (σ', l'))"
using assms by auto
lemma onll_ostep_invariant_weakenD [dest]:
assumes "A ⊨⇩A (S', U' →) onll Γ P"
and "(σ, p) ∈ oreachable A S U"
and "((σ, p), a, (σ', p')) ∈ trans A"
and "S' σ σ' a"
and weakenS: "⋀s s' a. S s s' a ⟹ S' s s' a"
and weakenU: "⋀s s'. U s s' ⟹ U' s s'"
shows "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((σ, l), a, (σ', l'))"
proof -
from ‹(σ, p) ∈ oreachable A S U› have "(σ, p) ∈ oreachable A S' U'"
by (rule oreachable_weakenE)
(erule weakenS, erule weakenU)
with ‹A ⊨⇩A (S', U' →) onll Γ P› show ?thesis
using ‹((σ, p), a, (σ', p')) ∈ trans A› and ‹S' σ σ' a› ..
qed
lemma onll_ostep_to_invariantI [intro]:
assumes sinv: "A ⊨⇩A (S, U →) onll Γ Q"
and wf: "wellformed Γ"
and init: "⋀σ l p. ⟦ (σ, p) ∈ init A; l∈labels Γ p ⟧ ⟹ P (σ, l)"
and other: "⋀σ σ' p l.
⟦ (σ, p) ∈ oreachable A S U;
l∈labels Γ p;
P (σ, l);
U σ σ' ⟧ ⟹ P (σ', l)"
and local: "⋀σ p l σ' l' a.
⟦ (σ, p) ∈ oreachable A S U;
l∈labels Γ p;
P (σ, l);
Q ((σ, l), a, (σ', l'));
S σ σ' a⟧ ⟹ P (σ', l')"
shows "A ⊨ (S, U →) onl Γ P"
proof
fix σ p l
assume "(σ, p) ∈ init A" and "l∈labels Γ p"
thus "P (σ, l)" by (rule init)
next
fix σ p a σ' p' l'
assume sr: "(σ, p) ∈ oreachable A S U"
and lp: "∀l∈labels Γ p. P (σ, l)"
and tr: "((σ, p), a, (σ', p')) ∈ trans A"
and "S σ σ' a"
and lp': "l' ∈ labels Γ p'"
show "P (σ', l')"
proof -
from lp obtain l where "l∈labels Γ p" and "P (σ, l)"
using labels_not_empty [OF wf] by auto
from sinv sr tr ‹S σ σ' a› this(1) lp' have "Q ((σ, l), a, (σ', l'))" ..
with sr ‹l∈labels Γ p› ‹P (σ, l)› show "P (σ', l')" using ‹S σ σ' a› by (rule local)
qed
next
fix σ σ' p l
assume "(σ, p) ∈ oreachable A S U"
and "∀l∈labels Γ p. P (σ, l)"
and "U σ σ'"
show "∀l∈labels Γ p. P (σ', l)"
proof
fix l
assume "l∈labels Γ p"
with ‹∀l∈labels Γ p. P (σ, l)› have "P (σ, l)" ..
with ‹(σ, p) ∈ oreachable A S U› and ‹l∈labels Γ p›
show "P (σ', l)" using ‹U σ σ'› by (rule other)
qed
qed
lemma onll_ostep_invariant_sterms:
assumes wf: "wellformed Γ"
and si: "A ⊨⇩A (S, U →) onll Γ P"
and sr: "(σ, p) ∈ oreachable A S U"
and sos: "((σ, p), a, (σ', q)) ∈ trans A"
and "S σ σ' a"
and "l'∈labels Γ q"
and "p'∈sterms Γ p"
and "l∈labels Γ p'"
shows "P ((σ, l), a, (σ', l'))"
proof -
from wf ‹p'∈sterms Γ p› ‹l∈labels Γ p'› have "l∈labels Γ p"
by (rule labels_sterms_labels)
with si sr sos ‹S σ σ' a› show "P ((σ, l), a, (σ', l'))" using ‹l'∈labels Γ q› ..
qed
lemma oseq_step_invariant_sterms:
assumes inv: "A ⊨⇩A (S, U →) onll Γ P"
and wf: "wellformed Γ"
and sp: "trans A = oseqp_sos Γ i"
and "l'∈labels Γ q"
and sr: "(σ, p) ∈ oreachable A S U"
and tr: "((σ, p'), a, (σ', q)) ∈ trans A"
and "S σ σ' a"
and "p'∈sterms Γ p"
shows "∀l∈labels Γ p'. P ((σ, l), a, (σ', l'))"
proof
from assms(3, 6) have "((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i" by simp
hence "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
using wf ‹p'∈sterms Γ p› by (rule otrans_from_sterms')
with assms(3) have trp: "((σ, p), a, (σ', q)) ∈ trans A" by simp
fix l assume "l ∈ labels Γ p'"
with wf inv sr trp ‹S σ σ' a› ‹l'∈labels Γ q› ‹p'∈sterms Γ p›
show "P ((σ, l), a, (σ', l'))"
by - (erule(7) onll_ostep_invariant_sterms)
qed
lemma oseq_step_invariant_sterms_weaken:
assumes inv: "A ⊨⇩A (S, U →) onll Γ P"
and wf: "wellformed Γ"
and sp: "trans A = oseqp_sos Γ i"
and "l'∈labels Γ q"
and sr: "(σ, p) ∈ oreachable A S' U'"
and tr: "((σ, p'), a, (σ', q)) ∈ trans A"
and "S' σ σ' a"
and "p'∈sterms Γ p"
and weakenS: "⋀σ σ' a. S' σ σ' a ⟹ S σ σ' a"
and weakenU: "⋀σ σ'. U' σ σ' ⟹ U σ σ'"
shows "∀l∈labels Γ p'. P ((σ, l), a, (σ', l'))"
proof -
from ‹S' σ σ' a› have "S σ σ' a" by (rule weakenS)
from ‹(σ, p) ∈ oreachable A S' U'›
have Ir: "(σ, p) ∈ oreachable A S U"
by (rule oreachable_weakenE)
(erule weakenS, erule weakenU)
with assms(1-4) show ?thesis
using tr ‹S σ σ' a› ‹p'∈sterms Γ p›
by (rule oseq_step_invariant_sterms)
qed
lemma onll_ostep_invariant_any_sterms:
assumes wf: "wellformed Γ"
and si: "A ⊨⇩A (S, U →) onll Γ P"
and sr: "(σ, p) ∈ oreachable A S U"
and sos: "((σ, p), a, (σ', q)) ∈ trans A"
and "S σ σ' a"
and "l'∈labels Γ q"
shows "∀p'∈sterms Γ p. ∀l∈labels Γ p'. P ((σ, l), a, (σ', l'))"
by (intro ballI) (rule onll_ostep_invariant_sterms [OF assms])
lemma oseq_step_invariant_ctermI [intro]:
assumes wf: "wellformed Γ"
and cw: "control_within Γ (init A)"
and sl: "simple_labels Γ"
and sp: "trans A = oseqp_sos Γ i"
and local: "⋀p l σ a q l' σ' pp. ⟦
p∈cterms Γ;
l∈labels Γ p;
((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i;
((σ, p), a, (σ', q)) ∈ trans A;
l'∈labels Γ q;
(σ, pp) ∈ oreachable A S U;
p∈sterms Γ pp;
(σ', q) ∈ oreachable A S U;
S σ σ' a
⟧ ⟹ P ((σ, l), a, (σ', l'))"
shows "A ⊨⇩A (S, U →) onll Γ P"
proof
fix σ p l a σ' q l'
assume sr: "(σ, p) ∈ oreachable A S U"
and tr: "((σ, p), a, (σ', q)) ∈ trans A"
and "S σ σ' a"
and pl: "l ∈ labels Γ p"
and A5: "l' ∈ labels Γ q"
from this(2) and sp have "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i" by simp
then obtain p' where "p' ∈ sterms Γ p"
and A3: "((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i"
by (blast dest: otrans_from_sterms [OF _ wf])
from this(2) and sp have A4: "((σ, p'), a, (σ', q)) ∈ trans A" by simp
from wf cw sp sr ‹p'∈sterms Γ p› have A1: "p'∈cterms Γ"
by (rule oseq_reachable_in_cterms)
from sr ‹p'∈sterms Γ p›
obtain pp where A6: "(σ, pp)∈oreachable A S U"
and A7: "p'∈sterms Γ pp"
by auto
from sr tr ‹S σ σ' a› have A8: "(σ', q)∈oreachable A S U"
by - (erule(2) oreachable_local')
from wf cw sp sr have "∃pn. p ∈ subterms (Γ pn)"
by (rule oreachable_subterms)
with sl wf have "∀p'∈sterms Γ p. l ∈ labels Γ p'"
using pl by (rule simple_labels_in_sterms)
with ‹p' ∈ sterms Γ p› have "l ∈ labels Γ p'" by simp
with A1 show "P ((σ, l), a, (σ', l'))" using A3 A4 A5 A6 A7 A8 ‹S σ σ' a›
by (rule local)
qed
lemma oseq_step_invariant_ctermsI [intro]:
assumes wf: "wellformed Γ"
and "control_within Γ (init A)"
and "simple_labels Γ"
and "trans A = oseqp_sos Γ i"
and local: "⋀p l σ a q l' σ' pp pn. ⟦
wellformed Γ;
p∈ctermsl (Γ pn);
not_call p;
l∈labels Γ p;
((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i;
((σ, p), a, (σ', q)) ∈ trans A;
l'∈labels Γ q;
(σ, pp) ∈ oreachable A S U;
p∈sterms Γ pp;
(σ', q) ∈ oreachable A S U;
S σ σ' a
⟧ ⟹ P ((σ, l), a, (σ', l'))"
shows "A ⊨⇩A (S, U →) onll Γ P"
using assms(1-4) proof (rule oseq_step_invariant_ctermI)
fix p l σ a q l' σ' pp
assume "p ∈ cterms Γ"
and otherassms: "l ∈ labels Γ p"
"((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
"((σ, p), a, (σ', q)) ∈ trans A"
"l' ∈ labels Γ q"
"(σ, pp) ∈ oreachable A S U"
"p ∈ sterms Γ pp"
"(σ', q) ∈ oreachable A S U"
"S σ σ' a"
from this(1) obtain pn where "p ∈ ctermsl(Γ pn)"
and "not_call p"
unfolding cterms_def' [OF wf] by auto
with wf show "P ((σ, l), a, (σ', l'))"
using otherassms by (rule local)
qed
lemma open_seqp_action [elim]:
assumes "wellformed Γ"
and "((σ i, p), a, (σ' i, p')) ∈ seqp_sos Γ"
shows "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i"
proof -
from assms obtain ps where "ps∈sterms Γ p"
and "((σ i, ps), a, (σ' i, p')) ∈ seqp_sos Γ"
by - (drule trans_from_sterms, auto)
thus ?thesis
proof (induction p)
fix p1 p2
assume "⟦ ps ∈ sterms Γ p1; ((σ i, ps), a, σ' i, p') ∈ seqp_sos Γ ⟧
⟹ ((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i"
and "⟦ ps ∈ sterms Γ p2; ((σ i, ps), a, σ' i, p') ∈ seqp_sos Γ ⟧
⟹ ((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i"
and "ps ∈ sterms Γ (p1 ⊕ p2)"
and "((σ i, ps), a, (σ' i, p')) ∈ seqp_sos Γ"
with assms(1) show "((σ, p1 ⊕ p2), a, (σ', p')) ∈ oseqp_sos Γ i"
by simp (metis oseqp_sos.ochoiceT1 oseqp_sos.ochoiceT2)
next
fix l fip fmsg p1 p2
assume IH1: "⟦ ps ∈ sterms Γ p1; ((σ i, ps), a, σ' i, p') ∈ seqp_sos Γ ⟧
⟹ ((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i"
and IH2: "⟦ ps ∈ sterms Γ p2; ((σ i, ps), a, σ' i, p') ∈ seqp_sos Γ ⟧
⟹ ((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i"
and "ps ∈ sterms Γ ({l}unicast(fip, fmsg). p1 ▹ p2)"
and "((σ i, ps), a, (σ' i, p')) ∈ seqp_sos Γ"
from this(3-4) have "((σ i, {l}unicast(fip, fmsg). p1 ▹ p2), a, (σ' i, p')) ∈ seqp_sos Γ"
by simp
thus "((σ, {l}unicast(fip, fmsg). p1 ▹ p2), a, (σ', p')) ∈ oseqp_sos Γ i"
proof (rule seqp_unicastTE)
assume "a = unicast (fip (σ i)) (fmsg (σ i))"
and "σ' i = σ i"
and "p' = p1"
thus ?thesis by auto
next
assume "a = ¬unicast (fip (σ i))"
and "σ' i = σ i"
and "p' = p2"
thus ?thesis by auto
qed
next
fix p
assume "ps ∈ sterms Γ (call(p))"
and "((σ i, ps), a, (σ' i, p')) ∈ seqp_sos Γ"
with assms(1) have "((σ, ps), a, (σ', p')) ∈ oseqp_sos Γ i"
by (cases ps) auto
with assms(1) ‹ps ∈ sterms Γ (call(p))› have "((σ, Γ p), a, (σ', p')) ∈ oseqp_sos Γ i"
by - (rule otrans_from_sterms', simp_all)
thus "((σ, call(p)), a, (σ', p')) ∈ oseqp_sos Γ i" by auto
qed auto
qed
end