Theory Tau_Chain
theory Tau_Chain
imports Semantics
begin
context env begin
abbreviation tauChain :: "'b ⇒ ('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi ⇒ bool" (‹_ ⊳ _ ⟹⇧^⇩τ _› [80, 80, 80] 80)
where "Ψ ⊳ P ⟹⇧^⇩τ P' ≡ (P, P') ∈ {(P, P'). Ψ ⊳ P ⟼τ ≺ P'}^*"
abbreviation tauStepChain :: "'b ⇒ ('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi ⇒ bool" (‹_ ⊳ _ ⟹⇩τ _› [80, 80, 80] 80)
where "Ψ ⊳ P ⟹⇩τ P' ≡ (P, P') ∈ {(P, P'). Ψ ⊳ P ⟼τ ≺ P'}^+"
abbreviation tauContextChain :: "('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi ⇒ bool" (‹_ ⟹⇧^⇩τ _› [80, 80] 80)
where "P ⟹⇧^⇩τ P' ≡ 𝟭 ⊳ P ⟹⇧^⇩τ P'"
abbreviation tauContextStepChain :: "('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi ⇒ bool" (‹_ ⟹⇩τ _› [80, 80] 80)
where "P ⟹⇩τ P' ≡ 𝟭 ⊳ P ⟹⇩τ P'"
lemmas tauChainInduct[consumes 1, case_names TauBase TauStep] = rtrancl.induct[of _ _ "{(P, P'). Ψ ⊳ P ⟼τ ≺ P'}", simplified] for Ψ
lemmas tauStepChainInduct[consumes 1, case_names TauBase TauStep] = trancl.induct[of _ _ "{(P, P'). Ψ ⊳ P ⟼τ ≺ P'}", simplified] for Ψ
lemma tauActTauStepChain:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ P ⟼τ ≺ P'"
shows "Ψ ⊳ P ⟹⇩τ P'"
using assms by auto
lemma tauActTauChain:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ P ⟼τ ≺ P'"
shows "Ψ ⊳ P ⟹⇧^⇩τ P'"
using assms by(auto simp add: rtrancl_eq_or_trancl)
lemma tauStepChainEqvt[eqvt]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and p :: "name prm"
assumes "Ψ ⊳ P ⟹⇩τ P'"
shows "(p ∙ Ψ) ⊳ (p ∙ P) ⟹⇩τ (p ∙ P')"
using assms
proof(induct rule: tauStepChainInduct)
case(TauBase P P')
hence "Ψ ⊳ P ⟼τ ≺ P'" by simp
thus ?case by(force dest: semantics.eqvt simp add: eqvts)
next
case(TauStep P P' P'')
hence "Ψ ⊳ P' ⟼τ ≺ P''" by simp
hence "(p ∙ Ψ) ⊳ (p ∙ P') ⟼τ ≺ (p ∙ P'')" by(force dest: semantics.eqvt simp add: eqvts)
with ‹(p ∙ Ψ) ⊳ (p ∙ P) ⟹⇩τ (p ∙ P')› show ?case
by(subst trancl.trancl_into_trancl) auto
qed
lemma tauChainEqvt[eqvt]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and p :: "name prm"
assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"
shows "(p ∙ Ψ) ⊳ (p ∙ P) ⟹⇧^⇩τ (p ∙ P')"
using assms
by(auto simp add: rtrancl_eq_or_trancl eqvts)
lemma tauStepChainEqvt'[eqvt]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and p :: "name prm"
shows "(p ∙ (Ψ ⊳ P ⟹⇩τ P')) = (p ∙ Ψ) ⊳ (p ∙ P) ⟹⇩τ (p ∙ P')"
apply(auto simp add: eqvts perm_set_def pt_bij[OF pt_name_inst, OF at_name_inst])
by(drule_tac p="rev p" in tauStepChainEqvt) auto
lemma tauChainEqvt'[eqvt]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and p :: "name prm"
shows "(p ∙ (Ψ ⊳ P ⟹⇧^⇩τ P')) = (p ∙ Ψ) ⊳ (p ∙ P) ⟹⇧^⇩τ (p ∙ P')"
apply(auto simp add: eqvts perm_set_def pt_bij[OF pt_name_inst, OF at_name_inst] rtrancl_eq_or_trancl)
by(drule_tac p="rev p" in tauStepChainEqvt) auto
lemma tauStepChainFresh:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and x :: name
assumes "Ψ ⊳ P ⟹⇩τ P'"
and "x ♯ P"
shows "x ♯ P'"
using assms
by(induct rule: trancl.induct) (auto dest: tauFreshDerivative)
lemma tauChainFresh:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and x :: name
assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"
and "x ♯ P"
shows "x ♯ P'"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainFresh)
lemma tauStepChainFreshChain:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and xvec :: "name list"
assumes "Ψ ⊳ P ⟹⇩τ P'"
and "xvec ♯* P"
shows "xvec ♯* P'"
using assms
by(induct xvec) (auto intro: tauStepChainFresh)
lemma tauChainFreshChain:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and xvec :: "name list"
assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"
and "xvec ♯* P"
shows "xvec ♯* P'"
using assms
by(induct xvec) (auto intro: tauChainFresh)
lemma tauStepChainCase:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and φ :: 'c
and Cs :: "('c × ('a, 'b, 'c) psi) list"
assumes "Ψ ⊳ P ⟹⇩τ P'"
and "(φ, P) mem Cs"
and "Ψ ⊢ φ"
and "guarded P"
shows "Ψ ⊳ (Cases Cs) ⟹⇩τ P'"
using assms
by(induct rule: trancl.induct) (auto intro: Case trancl_into_trancl)
lemma tauStepChainResPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and x :: name
assumes "Ψ ⊳ P ⟹⇩τ P'"
and "x ♯ Ψ"
shows "Ψ ⊳ ⦇νx⦈P ⟹⇩τ ⦇νx⦈P'"
using assms
by(induct rule: trancl.induct) (auto dest: Scope trancl_into_trancl)
lemma tauChainResPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and x :: name
assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"
and "x ♯ Ψ"
shows "Ψ ⊳ ⦇νx⦈P ⟹⇧^⇩τ ⦇νx⦈P'"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainResPres)
lemma tauStepChainResChainPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and xvec :: "name list"
assumes "Ψ ⊳ P ⟹⇩τ P'"
and "xvec ♯* Ψ"
shows "Ψ ⊳ ⦇ν*xvec⦈P ⟹⇩τ ⦇ν*xvec⦈P'"
using assms
by(induct xvec) (auto intro: tauStepChainResPres)
lemma tauChainResChainPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and xvec :: "name list"
assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"
and "xvec ♯* Ψ"
shows "Ψ ⊳ ⦇ν*xvec⦈P ⟹⇧^⇩τ ⦇ν*xvec⦈P'"
using assms
by(induct xvec) (auto intro: tauChainResPres)
lemma tauStepChainPar1:
fixes Ψ :: 'b
and Ψ⇩Q :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and A⇩Q :: "name list"
assumes "Ψ ⊗ Ψ⇩Q ⊳ P ⟹⇩τ P'"
and "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩"
and "A⇩Q ♯* Ψ"
and "A⇩Q ♯* P"
shows "Ψ ⊳ P ∥ Q ⟹⇩τ P' ∥ Q"
using assms
by(induct rule: trancl.induct) (auto dest: Par1 tauStepChainFreshChain trancl_into_trancl)
lemma tauChainPar1:
fixes Ψ :: 'b
and Ψ⇩Q :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and A⇩Q :: "name list"
assumes "Ψ ⊗ Ψ⇩Q ⊳ P ⟹⇧^⇩τ P'"
and "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩"
and "A⇩Q ♯* Ψ"
and "A⇩Q ♯* P"
shows "Ψ ⊳ P ∥ Q ⟹⇧^⇩τ P' ∥ Q"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainPar1)
lemma tauStepChainPar2:
fixes Ψ :: 'b
and Ψ⇩P :: 'b
and Q :: "('a, 'b, 'c) psi"
and Q' :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and A⇩P :: "name list"
assumes "Ψ ⊗ Ψ⇩P ⊳ Q ⟹⇩τ Q'"
and "extractFrame P = ⟨A⇩P, Ψ⇩P⟩"
and "A⇩P ♯* Ψ"
and "A⇩P ♯* Q"
shows "Ψ ⊳ P ∥ Q ⟹⇩τ P ∥ Q'"
using assms
by(induct rule: trancl.induct) (auto dest: Par2 trancl_into_trancl tauStepChainFreshChain)
lemma tauChainPar2:
fixes Ψ :: 'b
and Ψ⇩P :: 'b
and Q :: "('a, 'b, 'c) psi"
and Q' :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and A⇩P :: "name list"
assumes "Ψ ⊗ Ψ⇩P ⊳ Q ⟹⇧^⇩τ Q'"
and "extractFrame P = ⟨A⇩P, Ψ⇩P⟩"
and "A⇩P ♯* Ψ"
and "A⇩P ♯* Q"
shows "Ψ ⊳ P ∥ Q ⟹⇧^⇩τ P ∥ Q'"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainPar2)
lemma tauStepChainBang:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ P ∥ !P ⟹⇩τ P'"
and "guarded P"
shows "Ψ ⊳ !P ⟹⇩τ P'"
using assms
by(induct x1=="P ∥ !P" P' rule: trancl.induct) (auto intro: Bang dest: Bang trancl_into_trancl)
lemma tauStepChainStatEq:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and Ψ' :: 'b
assumes "Ψ ⊳ P ⟹⇩τ P'"
and "Ψ ≃ Ψ'"
shows "Ψ' ⊳ P ⟹⇩τ P'"
using assms
by(induct rule: trancl.induct) (auto dest: statEqTransition trancl_into_trancl)
lemma tauChainStatEq:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and Ψ' :: 'b
assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"
and "Ψ ≃ Ψ'"
shows "Ψ' ⊳ P ⟹⇧^⇩τ P'"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainStatEq)
definition weakTransition :: "'b ⇒ ('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi ⇒ 'a action ⇒ ('a, 'b, 'c) psi ⇒ bool" (‹_ : _ ⊳ _ ⟹_ ≺ _› [80, 80, 80, 80, 80] 80)
where
"Ψ : Q ⊳ P ⟹α ≺ P' ≡ ∃P''. Ψ ⊳ P ⟹⇧^⇩τ P'' ∧ (insertAssertion (extractFrame Q) Ψ) ↪⇩F (insertAssertion (extractFrame P'') Ψ) ∧
Ψ ⊳ P'' ⟼α ≺ P'"
lemma weakTransitionI:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and P'' :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ P ⟹⇧^⇩τ P''"
and "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and "Ψ ⊳ P'' ⟼α ≺ P'"
shows "Ψ : Q ⊳ P ⟹α ≺ P'"
using assms
by(auto simp add: weakTransition_def)
lemma weakTransitionE:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
assumes "Ψ : Q ⊳ P ⟹α ≺ P'"
obtains P'' where "Ψ ⊳ P ⟹⇧^⇩τ P''" and "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and "Ψ ⊳ P'' ⟼α ≺ P'"
using assms
by(auto simp add: weakTransition_def)
lemma weakTransitionClosed[eqvt]:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and p :: "name prm"
assumes "Ψ : Q ⊳ P ⟹α ≺ P'"
shows "(p ∙ Ψ) : (p ∙ Q) ⊳ (p ∙ P) ⟹(p ∙ α)≺ (p ∙ P')"
proof -
from assms obtain P'' where "Ψ ⊳ P ⟹⇧^⇩τ P''" and "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and "Ψ ⊳ P'' ⟼α ≺ P'"
by(rule weakTransitionE)
from ‹Ψ ⊳ P ⟹⇧^⇩τ P''› have "(p ∙ Ψ) ⊳ (p ∙ P) ⟹⇧^⇩τ (p ∙ P'')"
by(rule tauChainEqvt)
moreover from ‹insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ›
have "(p ∙ (insertAssertion (extractFrame Q) Ψ)) ↪⇩F (p ∙ (insertAssertion (extractFrame P'') Ψ))"
by(rule FrameStatImpClosed)
hence "insertAssertion (extractFrame(p ∙ Q)) (p ∙ Ψ) ↪⇩F insertAssertion (extractFrame(p ∙ P'')) (p ∙ Ψ)" by(simp add: eqvts)
moreover from ‹Ψ ⊳ P'' ⟼α ≺ P'› have "(p ∙ Ψ) ⊳ (p ∙ P'') ⟼(p ∙ (α ≺ P'))"
by(rule semantics.eqvt)
hence "(p ∙ Ψ) ⊳ (p ∙ P'') ⟼(p ∙ α) ≺ (p ∙ P')" by(simp add: eqvts)
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma weakOutputAlpha:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and p :: "name prm"
and yvec :: "name list"
assumes PTrans: "Ψ : Q ⊳ P ⟹M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ P'"
and S: "set p ⊆ set xvec × set(p ∙ xvec)"
and "distinctPerm p"
and "xvec ♯* P"
and "xvec ♯* (p ∙ xvec)"
and "(p ∙ xvec) ♯* M"
and "distinct xvec"
shows "Ψ : Q ⊳ P ⟹M⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P')"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and P''Trans: "Ψ ⊳ P'' ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ P'"
by(rule weakTransitionE)
note PChain QeqP''
moreover from PChain ‹xvec ♯* P› have "xvec ♯* P''" by(rule tauChainFreshChain)
with P''Trans ‹xvec ♯* (p ∙ xvec)› ‹distinct xvec› ‹(p ∙ xvec) ♯* M› have "xvec ♯* (p ∙ N)" and "xvec ♯* P'"
by(force intro: outputFreshChainDerivative)+
hence "(p ∙ xvec) ♯* (p ∙ p ∙ N)" and "(p ∙ xvec) ♯* (p ∙ P')"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])+
with ‹distinctPerm p› have "(p ∙ xvec) ♯* N" and "(p ∙ xvec) ♯* (p ∙ P')" by simp+
with P''Trans S ‹distinctPerm p› have "Ψ ⊳ P'' ⟼M⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P')"
apply(simp add: residualInject)
by(subst boundOutputChainAlpha) auto
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma weakFreshDerivative:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and x :: name
assumes PTrans: "Ψ : Q ⊳ P ⟹α ≺ P'"
and "x ♯ P"
and "x ♯ α"
and "bn α ♯* subject α"
and "distinct(bn α)"
shows "x ♯ P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
by(rule weakTransitionE)
from PChain ‹x ♯ P› have "x ♯ P''" by(rule tauChainFresh)
with P''Trans show "x ♯ P'" using ‹x ♯ α› ‹bn α ♯* subject α› ‹distinct(bn α)›
by(force intro: freeFreshDerivative)
qed
lemma weakFreshChainDerivative:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and yvec :: "name list"
assumes PTrans: "Ψ : Q ⊳ P ⟹α ≺ P'"
and "yvec ♯* P"
and "yvec ♯* α"
and "bn α ♯* subject α"
and "distinct(bn α)"
shows "yvec ♯* P'"
using assms
by(induct yvec) (auto intro: weakFreshDerivative)
lemma weakInputFreshDerivative:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and x :: name
assumes PTrans: "Ψ : Q ⊳ P ⟹M⦇N⦈ ≺ P'"
and "x ♯ P"
and "x ♯ N"
shows "x ♯ P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and P''Trans: "Ψ ⊳ P'' ⟼M⦇N⦈ ≺ P'"
by(rule weakTransitionE)
from PChain ‹x ♯ P› have "x ♯ P''" by(rule tauChainFresh)
with P''Trans show "x ♯ P'" using ‹x ♯ N›
by(force intro: inputFreshDerivative)
qed
lemma weakInputFreshChainDerivative:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and xvec :: "name list"
assumes PTrans: "Ψ : Q ⊳ P ⟹M⦇N⦈ ≺ P'"
and "xvec ♯* P"
and "xvec ♯* N"
shows "xvec ♯* P'"
using assms
by(induct xvec) (auto intro: weakInputFreshDerivative)
lemma weakOutputFreshDerivative:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and x :: name
assumes PTrans: "Ψ : Q ⊳ P ⟹M⦇ν*xvec⦈⟨N⟩ ≺ P'"
and "x ♯ P"
and "x ♯ xvec"
and "xvec ♯* M"
and "distinct xvec"
shows "x ♯ N"
and "x ♯ P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and P''Trans: "Ψ ⊳ P'' ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
by(rule weakTransitionE)
from PChain ‹x ♯ P› have "x ♯ P''" by(rule tauChainFresh)
with P''Trans show "x ♯ N" and "x ♯ P'" using ‹x ♯ xvec› ‹xvec ♯* M› ‹distinct xvec›
by(force intro: outputFreshDerivative)+
qed
lemma weakOutputFreshChainDerivative:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and yvec :: "name list"
assumes PTrans: "Ψ : Q ⊳ P ⟹M⦇ν*xvec⦈⟨N⟩ ≺ P'"
and "yvec ♯* P"
and "xvec ♯* yvec"
and "xvec ♯* M"
and "distinct xvec"
shows "yvec ♯* N"
and "yvec ♯* P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and P''Trans: "Ψ ⊳ P'' ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
by(rule weakTransitionE)
from PChain ‹yvec ♯* P› have "yvec ♯* P''" by(rule tauChainFreshChain)
with P''Trans show "yvec ♯* N" and "yvec ♯* P'" using ‹xvec ♯* yvec› ‹xvec ♯* M› ‹distinct xvec›
by(force intro: outputFreshChainDerivative)+
qed
lemma weakOutputPermSubject:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and p :: "name prm"
and yvec :: "name list"
and zvec :: "name list"
assumes PTrans: "Ψ : Q ⊳ P ⟹M⦇ν*xvec⦈⟨N⟩ ≺ P'"
and S: "set p ⊆ set yvec × set zvec"
and "yvec ♯* Ψ"
and "zvec ♯* Ψ"
and "yvec ♯* P"
and "zvec ♯* P"
shows "Ψ : Q ⊳ P ⟹(p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and P''Trans: "Ψ ⊳ P'' ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
by(rule weakTransitionE)
from PChain ‹yvec ♯* P› ‹zvec ♯* P› have "yvec ♯* P''" and "zvec ♯* P''"
by(force intro: tauChainFreshChain)+
note PChain QeqP''
moreover from P''Trans S ‹yvec ♯* Ψ› ‹zvec ♯* Ψ› ‹yvec ♯* P''› ‹zvec ♯* P''› have "Ψ ⊳ P'' ⟼(p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ P'"
by(rule_tac outputPermSubject) (assumption | auto)
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma weakInputPermSubject:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and p :: "name prm"
and yvec :: "name list"
and zvec :: "name list"
assumes PTrans: "Ψ : Q ⊳ P ⟹M⦇N⦈ ≺ P'"
and S: "set p ⊆ set yvec × set zvec"
and "yvec ♯* Ψ"
and "zvec ♯* Ψ"
and "yvec ♯* P"
and "zvec ♯* P"
shows "Ψ : Q ⊳ P ⟹(p ∙ M)⦇N⦈ ≺ P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and P''Trans: "Ψ ⊳ P'' ⟼M⦇N⦈ ≺ P'"
by(rule weakTransitionE)
from PChain ‹yvec ♯* P› ‹zvec ♯* P› have "yvec ♯* P''" and "zvec ♯* P''"
by(force intro: tauChainFreshChain)+
note PChain QeqP''
moreover from P''Trans S ‹yvec ♯* Ψ› ‹zvec ♯* Ψ› ‹yvec ♯* P''› ‹zvec ♯* P''› have "Ψ ⊳ P'' ⟼(p ∙ M)⦇N⦈ ≺ P'"
by(rule_tac inputPermSubject) auto
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma weakInput:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and M :: 'a
and K :: 'a
and xvec :: "name list"
and N :: 'a
and Tvec :: "'a list"
and P :: "('a, 'b, 'c) psi"
assumes "Ψ ⊢ M ↔ K"
and "distinct xvec"
and "set xvec ⊆ supp N"
and "length xvec = length Tvec"
and QeqΨ: "insertAssertion (extractFrame Q) Ψ ↪⇩F ⟨ε, Ψ ⊗ 𝟭⟩"
shows "Ψ : Q ⊳ M⦇λ*xvec N⦈.P ⟹K⦇(N[xvec::=Tvec])⦈ ≺ P[xvec::=Tvec]"
proof -
have "Ψ ⊳ M⦇λ*xvec N⦈.P ⟹⇧^⇩τ M⦇λ*xvec N⦈.P" by simp
moreover from QeqΨ have "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame(M⦇λ*xvec N⦈.P)) Ψ"
by auto
moreover from assms have "Ψ ⊳ M⦇λ*xvec N⦈.P ⟼K⦇(N[xvec::=Tvec])⦈ ≺ P[xvec::=Tvec]"
by(rule_tac Input)
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma weakOutput:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and M :: 'a
and K :: 'a
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "Ψ ⊢ M ↔ K"
and QeqΨ: "insertAssertion (extractFrame Q) Ψ ↪⇩F ⟨ε, Ψ ⊗ 𝟭⟩"
shows "Ψ : Q ⊳ M⟨N⟩.P ⟹K⟨N⟩ ≺ P"
proof -
have "Ψ ⊳ M⟨N⟩.P ⟹⇧^⇩τ M⟨N⟩.P" by simp
moreover from QeqΨ have "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame(M⟨N⟩.P)) Ψ"
by auto
moreover have "insertAssertion (extractFrame(M⟨N⟩.P)) Ψ ↪⇩F insertAssertion (extractFrame(M⟨N⟩.P)) Ψ" by simp
moreover from ‹Ψ ⊢ M ↔ K› have "Ψ ⊳ M⟨N⟩.P ⟼K⟨N⟩ ≺ P"
by(rule Output)
ultimately show ?thesis by(rule_tac weakTransitionI) auto
qed
lemma insertGuardedAssertion:
fixes P :: "('a, 'b, 'c) psi"
assumes "guarded P"
shows "insertAssertion(extractFrame P) Ψ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩"
proof -
obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" by(rule freshFrame)
from ‹guarded P› FrP have "Ψ⇩P ≃ 𝟭" and "supp Ψ⇩P = ({}::name set)"
by(blast dest: guardedStatEq)+
from FrP ‹A⇩P ♯* Ψ› ‹Ψ⇩P ≃ 𝟭› have "insertAssertion(extractFrame P) Ψ ≃⇩F ⟨A⇩P, Ψ ⊗ 𝟭⟩"
by simp (metis frameIntCompositionSym)
moreover from ‹A⇩P ♯* Ψ› have "⟨A⇩P, Ψ ⊗ 𝟭⟩ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩"
by(rule_tac frameResFreshChain) auto
ultimately show ?thesis by(rule FrameStatEqTrans)
qed
lemma weakCase:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes PTrans: "Ψ : Q ⊳ P ⟹α ≺ P'"
and "(φ, P) mem CsP"
and "Ψ ⊢ φ"
and "guarded P"
and RImpQ: "insertAssertion (extractFrame R) Ψ ↪⇩F insertAssertion (extractFrame Q) Ψ"
and ImpR: "insertAssertion (extractFrame R) Ψ ↪⇩F ⟨ε, Ψ⟩"
shows "Ψ : R ⊳ Cases CsP ⟹α ≺ P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''"
and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
by(rule weakTransitionE)
show ?thesis
proof(case_tac "P = P''")
assume "P = P''"
have "Ψ ⊳ Cases CsP ⟹⇧^⇩τ Cases CsP" by simp
moreover from ImpR AssertionStatEq_def have "insertAssertion(extractFrame R) Ψ ↪⇩F insertAssertion(extractFrame(Cases CsP)) Ψ"
by(rule_tac FrameStatImpTrans) (auto intro: Identity)+
moreover from P''Trans ‹(φ, P) mem CsP› ‹Ψ ⊢ φ› ‹guarded P› ‹P = P''› have "Ψ ⊳ Cases CsP ⟼α ≺ P'"
by(blast intro: Case)
ultimately show ?thesis
by(rule weakTransitionI)
next
assume "P ≠ P''"
with PChain have "Ψ ⊳ P ⟹⇩τ P''" by(simp add: rtrancl_eq_or_trancl)
hence "Ψ ⊳ Cases CsP ⟹⇩τ P''" using ‹(φ, P) mem CsP› ‹Ψ ⊢ φ› ‹guarded P›
by(rule tauStepChainCase)
hence "Ψ ⊳ Cases CsP ⟹⇧^⇩τ P''" by simp
moreover from RImpQ QeqP'' have "insertAssertion(extractFrame R) Ψ ↪⇩F insertAssertion(extractFrame P'') Ψ"
by(rule FrameStatImpTrans)
ultimately show ?thesis using P''Trans by(rule weakTransitionI)
qed
qed
lemma weakOpen:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and xvec :: "name list"
and yvec :: "name list"
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
assumes PTrans: "Ψ : Q ⊳ P ⟹M⦇ν*(xvec@yvec)⦈⟨N⟩ ≺ P'"
and "x ∈ supp N"
and "x ♯ Ψ"
and "x ♯ M"
and "x ♯ xvec"
and "x ♯ yvec"
shows "Ψ : ⦇νx⦈Q ⊳ ⦇νx⦈P ⟹M⦇ν*(xvec@x#yvec)⦈⟨N⟩ ≺ P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and P''Trans: "Ψ ⊳ P'' ⟼M⦇ν*(xvec@yvec)⦈⟨N⟩ ≺ P'"
by(rule weakTransitionE)
from PChain ‹x ♯ Ψ› have "Ψ ⊳ ⦇νx⦈P ⟹⇧^⇩τ ⦇νx⦈P''" by(rule tauChainResPres)
moreover from QeqP'' ‹x ♯ Ψ› have "insertAssertion (extractFrame(⦇νx⦈Q)) Ψ ↪⇩F insertAssertion (extractFrame(⦇νx⦈P'')) Ψ" by(force intro: frameImpResPres)
moreover from P''Trans ‹x ∈ supp N› ‹x ♯ Ψ› ‹x ♯ M› ‹x ♯ xvec› ‹x ♯ yvec› have "Ψ ⊳ ⦇νx⦈P'' ⟼M⦇ν*(xvec@x#yvec)⦈⟨N⟩ ≺ P'"
by(rule Open)
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma weakScope:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
assumes PTrans: "Ψ : Q ⊳ P ⟹α ≺ P'"
and "x ♯ Ψ"
and "x ♯ α"
shows "Ψ : ⦇νx⦈Q ⊳ ⦇νx⦈P ⟹α ≺ ⦇νx⦈P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
by(rule weakTransitionE)
from PChain ‹x ♯ Ψ› have "Ψ ⊳ ⦇νx⦈P ⟹⇧^⇩τ ⦇νx⦈P''" by(rule tauChainResPres)
moreover from QeqP'' ‹x ♯ Ψ› have "insertAssertion (extractFrame(⦇νx⦈Q)) Ψ ↪⇩F insertAssertion (extractFrame(⦇νx⦈P'')) Ψ" by(force intro: frameImpResPres)
moreover from P''Trans ‹x ♯ Ψ› ‹x ♯ α› have "Ψ ⊳ ⦇νx⦈P'' ⟼α ≺ ⦇νx⦈P'"
by(rule Scope)
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma weakPar1:
fixes Ψ :: 'b
and R :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and A⇩Q :: "name list"
and Ψ⇩Q :: 'b
assumes PTrans: "Ψ ⊗ Ψ⇩Q : R ⊳ P ⟹α ≺ P'"
and FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩"
and "bn α ♯* Q"
and "A⇩Q ♯* Ψ"
and "A⇩Q ♯* P"
and "A⇩Q ♯* α"
and "A⇩Q ♯* R"
shows "Ψ : R ∥ Q ⊳ P ∥ Q ⟹α ≺ P' ∥ Q"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ⇩Q ⊳ P ⟹⇧^⇩τ P''"
and ReqP'': "insertAssertion (extractFrame R) (Ψ ⊗ Ψ⇩Q) ↪⇩F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ⇩Q)"
and P''Trans: "Ψ ⊗ Ψ⇩Q ⊳ P'' ⟼α ≺ P'"
by(rule weakTransitionE)
from PChain ‹A⇩Q ♯* P› have "A⇩Q ♯* P''" by(rule tauChainFreshChain)
from PChain FrQ ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* P› have "Ψ ⊳ P ∥ Q ⟹⇧^⇩τ P'' ∥ Q" by(rule tauChainPar1)
moreover have "insertAssertion (extractFrame(R ∥ Q)) Ψ ↪⇩F insertAssertion (extractFrame(P'' ∥ Q)) Ψ"
proof -
obtain A⇩R Ψ⇩R where FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* A⇩Q" and "A⇩R ♯* Ψ⇩Q" and "A⇩R ♯* Ψ"
by(rule_tac C="(A⇩Q, Ψ⇩Q, Ψ)" in freshFrame) auto
obtain A⇩P'' Ψ⇩P'' where FrP'': "extractFrame P'' = ⟨A⇩P'', Ψ⇩P''⟩" and "A⇩P'' ♯* A⇩Q" and "A⇩P'' ♯* Ψ⇩Q" and "A⇩P'' ♯* Ψ"
by(rule_tac C="(A⇩Q, Ψ⇩Q, Ψ)" in freshFrame) auto
from FrR FrP'' ‹A⇩Q ♯* R› ‹A⇩Q ♯* P''› ‹A⇩R ♯* A⇩Q› ‹A⇩P'' ♯* A⇩Q› have "A⇩Q ♯* Ψ⇩R" and "A⇩Q ♯* Ψ⇩P''"
by(force dest: extractFrameFreshChain)+
have "⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q⟩ ≃⇩F ⟨A⇩R, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩"
by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
moreover from ReqP'' FrR FrP'' ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ⇩Q› ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* Ψ⇩Q›
have "⟨A⇩R, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩P''⟩" using freshCompChain by auto
moreover have "⟨A⇩P'', (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩P''⟩ ≃⇩F ⟨A⇩P'', Ψ ⊗ Ψ⇩P'' ⊗ Ψ⇩Q⟩"
by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
ultimately have "⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P'', Ψ ⊗ Ψ⇩P'' ⊗ Ψ⇩Q⟩"
by(force dest: FrameStatImpTrans simp add: FrameStatEq_def)
hence "⟨(A⇩R@A⇩Q), Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q⟩ ↪⇩F ⟨(A⇩P''@A⇩Q), Ψ ⊗ Ψ⇩P'' ⊗ Ψ⇩Q⟩"
apply(simp add: frameChainAppend)
apply(drule_tac xvec=A⇩Q in frameImpResChainPres)
by(metis frameImpChainComm FrameStatImpTrans)
with FrR FrQ FrP'' ‹A⇩R ♯* A⇩Q› ‹A⇩R ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩P'' ♯* A⇩Q› ‹A⇩P'' ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ⇩P''› ‹A⇩R ♯* Ψ› ‹A⇩P'' ♯* Ψ› ‹A⇩Q ♯* Ψ› ReqP''
show ?thesis by simp
qed
moreover from P''Trans FrQ ‹bn α ♯* Q› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* P''› ‹A⇩Q ♯* α› have "Ψ ⊳ P'' ∥ Q ⟼α ≺ (P' ∥ Q)"
by(rule Par1)
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma weakPar2:
fixes Ψ :: 'b
and R :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and M :: 'a
and xvec :: "name list"
and N :: 'a
and Q' :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and A⇩P :: "name list"
and Ψ⇩P :: 'b
assumes QTrans: "Ψ ⊗ Ψ⇩P : R ⊳ Q ⟹α ≺ Q'"
and FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩"
and "bn α ♯* P"
and "A⇩P ♯* Ψ"
and "A⇩P ♯* Q"
and "A⇩P ♯* α"
and "A⇩P ♯* R"
shows "Ψ : P ∥ R ⊳ P ∥ Q ⟹α ≺ P ∥ Q'"
proof -
from QTrans obtain Q'' where QChain: "Ψ ⊗ Ψ⇩P ⊳ Q ⟹⇧^⇩τ Q''"
and ReqQ'': "insertAssertion (extractFrame R) (Ψ ⊗ Ψ⇩P) ↪⇩F insertAssertion (extractFrame Q'') (Ψ ⊗ Ψ⇩P)"
and Q''Trans: "Ψ ⊗ Ψ⇩P ⊳ Q'' ⟼α ≺ Q'"
by(rule weakTransitionE)
from QChain ‹A⇩P ♯* Q› have "A⇩P ♯* Q''" by(rule tauChainFreshChain)
from QChain FrP ‹A⇩P ♯* Ψ› ‹A⇩P ♯* Q› have "Ψ ⊳ P ∥ Q ⟹⇧^⇩τ P ∥ Q''" by(rule tauChainPar2)
moreover have "insertAssertion (extractFrame(P ∥ R)) Ψ ↪⇩F insertAssertion (extractFrame(P ∥ Q'')) Ψ"
proof -
obtain A⇩R Ψ⇩R where FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* A⇩P" and "A⇩R ♯* Ψ⇩P" and "A⇩R ♯* Ψ"
by(rule_tac C="(A⇩P, Ψ⇩P, Ψ)" in freshFrame) auto
obtain A⇩Q'' Ψ⇩Q'' where FrQ'': "extractFrame Q'' = ⟨A⇩Q'', Ψ⇩Q''⟩" and "A⇩Q'' ♯* A⇩P" and "A⇩Q'' ♯* Ψ⇩P" and "A⇩Q'' ♯* Ψ"
by(rule_tac C="(A⇩P, Ψ⇩P, Ψ)" in freshFrame) auto
from FrR FrQ'' ‹A⇩P ♯* R› ‹A⇩P ♯* Q''› ‹A⇩R ♯* A⇩P› ‹A⇩Q'' ♯* A⇩P› have "A⇩P ♯* Ψ⇩R" and "A⇩P ♯* Ψ⇩Q''"
by(force dest: extractFrameFreshChain)+
have "⟨A⇩R, Ψ ⊗ Ψ⇩P ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩R, (Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩R⟩"
by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
moreover from ReqQ'' FrR FrQ'' ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ⇩P› ‹A⇩Q'' ♯* Ψ› ‹A⇩Q'' ♯* Ψ⇩P›
have "⟨A⇩R, (Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩Q'', (Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q''⟩" using freshCompChain by simp
moreover have "⟨A⇩Q'', (Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q''⟩ ≃⇩F ⟨A⇩Q'', Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q''⟩"
by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
ultimately have "⟨A⇩R, Ψ ⊗ Ψ⇩P ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩Q'', Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q''⟩"
by(force dest: FrameStatImpTrans simp add: FrameStatEq_def)
hence "⟨(A⇩P@A⇩R), Ψ ⊗ Ψ⇩P ⊗ Ψ⇩R⟩ ↪⇩F ⟨(A⇩P@A⇩Q''), Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q''⟩"
apply(simp add: frameChainAppend)
apply(drule_tac xvec=A⇩P in frameImpResChainPres)
by(metis frameImpChainComm FrameStatImpTrans)
with FrR FrP FrQ'' ‹A⇩R ♯* A⇩P› ‹A⇩R ♯* Ψ⇩P› ‹A⇩P ♯* Ψ⇩R› ‹A⇩Q'' ♯* A⇩P› ‹A⇩Q'' ♯* Ψ⇩P› ‹A⇩P ♯* Ψ⇩Q''› ‹A⇩R ♯* Ψ› ‹A⇩Q'' ♯* Ψ› ‹A⇩P ♯* Ψ› ReqQ''
show ?thesis by simp
qed
moreover from Q''Trans FrP ‹bn α ♯* P› ‹A⇩P ♯* Ψ› ‹A⇩P ♯* Q''› ‹A⇩P ♯* α› have "Ψ ⊳ P ∥ Q'' ⟼α ≺ (P ∥ Q')"
by(rule_tac Par2) auto
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma weakComm1:
fixes Ψ :: 'b
and R :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and A⇩Q :: "name list"
and Ψ⇩Q :: 'b
assumes PTrans: "Ψ ⊗ Ψ⇩Q : R ⊳ P ⟹M⦇N⦈ ≺ P'"
and FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩"
and QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'"
and FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩"
and MeqK: "Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K"
and "A⇩R ♯* Ψ"
and "A⇩R ♯* P"
and "A⇩R ♯* Q"
and "A⇩R ♯* R"
and "A⇩R ♯* M"
and "A⇩R ♯* A⇩Q"
and "A⇩Q ♯* Ψ"
and "A⇩Q ♯* P"
and "A⇩Q ♯* Q"
and "A⇩Q ♯* R"
and "A⇩Q ♯* K"
and "xvec ♯* P"
shows "Ψ ⊳ P ∥ Q ⟹⇩τ (⦇ν*xvec⦈(P' ∥ Q'))"
proof -
from ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* P› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* R› ‹A⇩Q ♯* K› ‹A⇩R ♯* A⇩Q›
obtain A⇩Q' where FrQ': "extractFrame Q = ⟨A⇩Q', Ψ⇩Q⟩" and "distinct A⇩Q'" and "A⇩Q' ♯* Ψ" and "A⇩Q' ♯* P"
and "A⇩Q' ♯* Q" and "A⇩Q' ♯* R" and "A⇩Q' ♯* K" and "A⇩R ♯* A⇩Q'"
by(rule_tac C="(Ψ, P, Q, R, K, A⇩R)" in distinctFrame) auto
from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ⇩Q ⊳ P ⟹⇧^⇩τ P''"
and RimpP'': "insertAssertion (extractFrame R) (Ψ ⊗ Ψ⇩Q) ↪⇩F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ⇩Q)"
and P''Trans: "Ψ ⊗ Ψ⇩Q ⊳ P'' ⟼M⦇N⦈ ≺ P'"
by(rule weakTransitionE)
from PChain ‹A⇩Q' ♯* P› have "A⇩Q' ♯* P''" by(rule tauChainFreshChain)
obtain A⇩P'' Ψ⇩P'' where FrP'': "extractFrame P'' = ⟨A⇩P'', Ψ⇩P''⟩" and "A⇩P'' ♯* (Ψ, A⇩Q', Ψ⇩Q, A⇩R, Ψ⇩R, M, N, K, R, Q, P'', xvec)" and "distinct A⇩P''"
by(rule freshFrame)
hence "A⇩P'' ♯* Ψ" and "A⇩P'' ♯* A⇩Q'" and "A⇩P'' ♯* Ψ⇩Q" and "A⇩P'' ♯* M" and "A⇩P'' ♯* R" and "A⇩P'' ♯* Q"
and "A⇩P'' ♯* N" and "A⇩P'' ♯* K" and "A⇩P'' ♯* A⇩R" and "A⇩P'' ♯* P''" and "A⇩P'' ♯* xvec" and "A⇩P'' ♯* Ψ⇩R"
by simp+
from FrR ‹A⇩R ♯* A⇩Q'› ‹A⇩Q' ♯* R› have "A⇩Q' ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto
from FrQ' ‹A⇩R ♯* A⇩Q'› ‹A⇩R ♯* Q› have "A⇩R ♯* Ψ⇩Q" by(drule_tac extractFrameFreshChain) auto
from PChain ‹xvec ♯* P› have "xvec ♯* P''" by(force intro: tauChainFreshChain)+
have "⟨A⇩R, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ≃⇩F ⟨A⇩R, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩"
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
moreover with RimpP'' FrP'' FrR ‹A⇩P'' ♯* Ψ› ‹A⇩R ♯* Ψ› ‹A⇩P'' ♯* Ψ⇩Q› ‹A⇩R ♯* Ψ⇩Q›
have "⟨A⇩R, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩P''⟩" using freshCompChain
by(simp add: freshChainSimps)
moreover have "⟨A⇩P'', (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩P''⟩ ≃⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩P'') ⊗ Ψ⇩Q⟩"
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
ultimately have RImpP'': "⟨A⇩R, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩P'') ⊗ Ψ⇩Q⟩"
by(rule FrameStatEqImpCompose)
from PChain FrQ' ‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* P› have "Ψ ⊳ P ∥ Q ⟹⇧^⇩τ P'' ∥ Q" by(rule tauChainPar1)
moreover from QTrans FrR P''Trans MeqK RImpP'' FrP'' FrQ' ‹distinct A⇩P''› ‹distinct A⇩Q'› ‹A⇩P'' ♯* A⇩Q'› ‹A⇩R ♯* A⇩Q'›
‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* P''› ‹A⇩Q' ♯* Q› ‹A⇩Q' ♯* R› ‹A⇩Q' ♯* K› ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R› ‹A⇩P'' ♯* Q›
‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* M› ‹A⇩Q ♯* R› ‹A⇩R ♯* Q› ‹A⇩R ♯* M›
obtain K' where "Ψ ⊗ Ψ⇩P'' ⊳ Q ⟼K'⦇ν*xvec⦈⟨N⟩ ≺ Q'" and "Ψ ⊗ Ψ⇩P'' ⊗ Ψ⇩Q ⊢ M ↔ K'" and "A⇩Q' ♯* K'"
by(rule_tac comm1Aux) (assumption | simp)+
with P''Trans FrP'' have "Ψ ⊳ P'' ∥ Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q')" using FrQ' ‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* P''› ‹A⇩Q' ♯* Q›
‹xvec ♯* P''› ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* Q› ‹A⇩P'' ♯* M› ‹A⇩P'' ♯* A⇩Q'›
by(rule_tac Comm1)
ultimately show ?thesis
by(drule_tac tauActTauStepChain) auto
qed
lemma weakComm2:
fixes Ψ :: 'b
and R :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and A⇩Q :: "name list"
and Ψ⇩Q :: 'b
assumes PTrans: "Ψ ⊗ Ψ⇩Q : R ⊳ P ⟹M⦇ν*xvec⦈⟨N⟩ ≺ P'"
and FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩"
and QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼K⦇N⦈ ≺ Q'"
and FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩"
and MeqK: "Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K"
and "A⇩R ♯* Ψ"
and "A⇩R ♯* P"
and "A⇩R ♯* Q"
and "A⇩R ♯* R"
and "A⇩R ♯* M"
and "A⇩R ♯* A⇩Q"
and "A⇩Q ♯* Ψ"
and "A⇩Q ♯* P"
and "A⇩Q ♯* Q"
and "A⇩Q ♯* R"
and "A⇩Q ♯* K"
and "xvec ♯* Q"
and "xvec ♯* M"
and "xvec ♯* A⇩Q"
and "xvec ♯* A⇩R"
shows "Ψ ⊳ P ∥ Q ⟹⇩τ (⦇ν*xvec⦈(P' ∥ Q'))"
proof -
from ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* P› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* R› ‹A⇩Q ♯* K› ‹A⇩R ♯* A⇩Q› ‹xvec ♯* A⇩Q›
obtain A⇩Q' where FrQ': "extractFrame Q = ⟨A⇩Q', Ψ⇩Q⟩" and "distinct A⇩Q'" and "A⇩Q' ♯* Ψ" and "A⇩Q' ♯* P"
and "A⇩Q' ♯* Q" and "A⇩Q' ♯* R" and "A⇩Q' ♯* K" and "A⇩R ♯* A⇩Q'" and "A⇩Q' ♯* xvec"
by(rule_tac C="(Ψ, P, Q, R, K, A⇩R, xvec)" in distinctFrame) auto
from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ⇩Q ⊳ P ⟹⇧^⇩τ P''"
and RimpP'': "insertAssertion (extractFrame R) (Ψ ⊗ Ψ⇩Q) ↪⇩F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ⇩Q)"
and P''Trans: "Ψ ⊗ Ψ⇩Q ⊳ P'' ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
by(rule weakTransitionE)
from PChain ‹A⇩Q' ♯* P› have "A⇩Q' ♯* P''" by(rule tauChainFreshChain)
obtain A⇩P'' Ψ⇩P'' where FrP'': "extractFrame P'' = ⟨A⇩P'', Ψ⇩P''⟩" and "A⇩P'' ♯* (Ψ, A⇩Q', Ψ⇩Q, A⇩R, Ψ⇩R, M, N, K, R, Q, P'', xvec)" and "distinct A⇩P''"
by(rule freshFrame)
hence "A⇩P'' ♯* Ψ" and "A⇩P'' ♯* A⇩Q'" and "A⇩P'' ♯* Ψ⇩Q" and "A⇩P'' ♯* M" and "A⇩P'' ♯* R" and "A⇩P'' ♯* Q"
and "A⇩P'' ♯* N" and "A⇩P'' ♯* K" and "A⇩P'' ♯* A⇩R" and "A⇩P'' ♯* P''" and "A⇩P'' ♯* xvec" and "A⇩P'' ♯* Ψ⇩R"
by simp+
from FrR ‹A⇩R ♯* A⇩Q'› ‹A⇩Q' ♯* R› have "A⇩Q' ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto
from FrQ' ‹A⇩R ♯* A⇩Q'› ‹A⇩R ♯* Q› have "A⇩R ♯* Ψ⇩Q" by(drule_tac extractFrameFreshChain) auto
have "⟨A⇩R, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ≃⇩F ⟨A⇩R, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩"
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
moreover with RimpP'' FrP'' FrR ‹A⇩P'' ♯* Ψ› ‹A⇩R ♯* Ψ› ‹A⇩P'' ♯* Ψ⇩Q› ‹A⇩R ♯* Ψ⇩Q›
have "⟨A⇩R, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩P''⟩" using freshCompChain
by(simp add: freshChainSimps)
moreover have "⟨A⇩P'', (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩P''⟩ ≃⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩P'') ⊗ Ψ⇩Q⟩"
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
ultimately have RImpP'': "⟨A⇩R, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩P'') ⊗ Ψ⇩Q⟩"
by(rule FrameStatEqImpCompose)
from PChain FrQ' ‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* P› have "Ψ ⊳ P ∥ Q ⟹⇧^⇩τ P'' ∥ Q" by(rule tauChainPar1)
moreover from QTrans FrR P''Trans MeqK RImpP'' FrP'' FrQ' ‹distinct A⇩P''› ‹distinct A⇩Q'› ‹A⇩P'' ♯* A⇩Q'› ‹A⇩R ♯* A⇩Q'›
‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* P''› ‹A⇩Q' ♯* Q› ‹A⇩Q' ♯* R› ‹A⇩Q' ♯* K› ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R› ‹A⇩P'' ♯* Q›
‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* M› ‹A⇩Q ♯* R› ‹A⇩R ♯* Q› ‹A⇩R ♯* M› ‹xvec ♯* A⇩R› ‹xvec ♯* M› ‹A⇩Q' ♯* xvec›
obtain K' where "Ψ ⊗ Ψ⇩P'' ⊳ Q ⟼K'⦇N⦈ ≺ Q'" and "Ψ ⊗ Ψ⇩P'' ⊗ Ψ⇩Q ⊢ M ↔ K'" and "A⇩Q' ♯* K'"
by(rule_tac comm2Aux) (assumption | simp)+
with P''Trans FrP'' have "Ψ ⊳ P'' ∥ Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q')" using FrQ' ‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* P''› ‹A⇩Q' ♯* Q›
‹xvec ♯* Q› ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* Q› ‹A⇩P'' ♯* M› ‹A⇩P'' ♯* A⇩Q'›
by(rule_tac Comm2)
ultimately show ?thesis
by(drule_tac tauActTauStepChain) auto
qed
lemma frameImpIntComposition:
fixes Ψ :: 'b
and Ψ' :: 'b
and A⇩F :: "name list"
and Ψ⇩F :: 'b
assumes "Ψ ≃ Ψ'"
shows "⟨A⇩F, Ψ ⊗ Ψ⇩F⟩ ↪⇩F ⟨A⇩F, Ψ' ⊗ Ψ⇩F⟩"
proof -
from assms have "⟨A⇩F, Ψ ⊗ Ψ⇩F⟩ ≃⇩F ⟨A⇩F, Ψ' ⊗ Ψ⇩F⟩" by(rule frameIntComposition)
thus ?thesis by(simp add: FrameStatEq_def)
qed
lemma insertAssertionStatImp:
fixes F :: "'b frame"
and Ψ :: 'b
and G :: "'b frame"
and Ψ' :: 'b
assumes FeqG: "insertAssertion F Ψ ↪⇩F insertAssertion G Ψ"
and "Ψ ≃ Ψ'"
shows "insertAssertion F Ψ' ↪⇩F insertAssertion G Ψ'"
proof -
obtain A⇩F Ψ⇩F where FrF: "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* Ψ" and "A⇩F ♯* Ψ'"
by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
obtain A⇩G Ψ⇩G where FrG: "G = ⟨A⇩G, Ψ⇩G⟩" and "A⇩G ♯* Ψ" and "A⇩G ♯* Ψ'"
by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
from ‹Ψ ≃ Ψ'› have "⟨A⇩F, Ψ' ⊗ Ψ⇩F⟩ ≃⇩F ⟨A⇩F, Ψ ⊗ Ψ⇩F⟩" by (metis frameIntComposition FrameStatEqSym)
moreover from ‹Ψ ≃ Ψ'› have "⟨A⇩G, Ψ ⊗ Ψ⇩G⟩ ≃⇩F ⟨A⇩G, Ψ' ⊗ Ψ⇩G⟩" by(rule frameIntComposition)
ultimately have "⟨A⇩F, Ψ' ⊗ Ψ⇩F⟩ ↪⇩F ⟨A⇩G, Ψ' ⊗ Ψ⇩G⟩" using FeqG FrF FrG ‹A⇩F ♯* Ψ› ‹A⇩G ♯* Ψ› ‹Ψ ≃ Ψ'›
by(force simp add: FrameStatEq_def dest: FrameStatImpTrans)
with FrF FrG ‹A⇩F ♯* Ψ'› ‹A⇩G ♯* Ψ'› show ?thesis by simp
qed
lemma insertAssertionStatEq:
fixes F :: "'b frame"
and Ψ :: 'b
and G :: "'b frame"
and Ψ' :: 'b
assumes FeqG: "insertAssertion F Ψ ≃⇩F insertAssertion G Ψ"
and "Ψ ≃ Ψ'"
shows "insertAssertion F Ψ' ≃⇩F insertAssertion G Ψ'"
proof -
obtain A⇩F Ψ⇩F where FrF: "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* Ψ" and "A⇩F ♯* Ψ'"
by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
obtain A⇩G Ψ⇩G where FrG: "G = ⟨A⇩G, Ψ⇩G⟩" and "A⇩G ♯* Ψ" and "A⇩G ♯* Ψ'"
by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
from FeqG FrF FrG ‹A⇩F ♯* Ψ› ‹A⇩G ♯* Ψ› ‹Ψ ≃ Ψ'›
have "⟨A⇩F, Ψ' ⊗ Ψ⇩F⟩ ≃⇩F ⟨A⇩G, Ψ' ⊗ Ψ⇩G⟩"
by simp (metis frameIntComposition FrameStatEqTrans FrameStatEqSym)
with FrF FrG ‹A⇩F ♯* Ψ'› ‹A⇩G ♯* Ψ'› show ?thesis by simp
qed
lemma weakTransitionStatEq:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and Ψ' :: 'b
assumes PTrans: "Ψ : Q ⊳ P ⟹α ≺ P'"
and "Ψ ≃ Ψ'"
shows "Ψ' : Q ⊳ P ⟹α ≺ P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''"
and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
by(rule weakTransitionE)
from PChain ‹Ψ ≃ Ψ'› have "Ψ' ⊳ P ⟹⇧^⇩τ P''" by(rule tauChainStatEq)
moreover from QeqP'' ‹Ψ ≃ Ψ'› have "insertAssertion (extractFrame Q) Ψ' ↪⇩F insertAssertion (extractFrame P'') Ψ'"
by(rule insertAssertionStatImp)
moreover from P''Trans ‹Ψ ≃ Ψ'› have "Ψ' ⊳ P'' ⟼α ≺ P'"
by(rule statEqTransition)
ultimately show ?thesis by(rule weakTransitionI)
qed
lemma transitionWeakTransition:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ P ⟼α ≺ P'"
and "insertAssertion(extractFrame Q) Ψ ↪⇩F insertAssertion(extractFrame P) Ψ"
shows "Ψ : Q ⊳ P ⟹α ≺ P'"
using assms
by(fastforce intro: weakTransitionI)
lemma weakPar1Guarded:
fixes Ψ :: 'b
and R :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes PTrans: "Ψ : R ⊳ P ⟹α ≺ P'"
and "bn α ♯* Q"
and "guarded Q"
shows "Ψ : (R ∥ Q) ⊳ P ∥ Q ⟹α ≺ P' ∥ Q"
proof -
obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* P" and "A⇩Q ♯* α" and "A⇩Q ♯* R"
by(rule_tac C="(Ψ, P, α, R)" in freshFrame) auto
from ‹guarded Q› FrQ have "Ψ⇩Q ≃ 𝟭" by(blast dest: guardedStatEq)
with PTrans have "Ψ ⊗ Ψ⇩Q : R ⊳ P ⟹α ≺ P'" by(metis weakTransitionStatEq Identity AssertionStatEqSym compositionSym)
thus ?thesis using FrQ ‹bn α ♯* Q› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* P› ‹A⇩Q ♯* α› ‹A⇩Q ♯* R›
by(rule weakPar1)
qed
lemma weakBang:
fixes Ψ :: 'b
and R :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes PTrans: "Ψ : R ⊳ P ∥ !P ⟹α ≺ P'"
and "guarded P"
shows "Ψ : R ⊳ !P ⟹α ≺ P'"
proof -
from PTrans obtain P'' where PChain: "Ψ ⊳ P ∥ !P ⟹⇧^⇩τ P''"
and RImpP'': "insertAssertion(extractFrame R) Ψ ↪⇩F insertAssertion(extractFrame P'') Ψ"
and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
by(rule weakTransitionE)
moreover obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" by(rule freshFrame)
moreover from ‹guarded P› FrP have "Ψ⇩P ≃ 𝟭" by(blast dest: guardedStatEq)
ultimately show ?thesis
proof(auto simp add: rtrancl_eq_or_trancl)
have "Ψ ⊳ !P ⟹⇧^⇩τ !P" by simp
moreover assume RimpP: "insertAssertion(extractFrame R) Ψ ↪⇩F ⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ 𝟭⟩"
have "insertAssertion(extractFrame R) Ψ ↪⇩F insertAssertion(extractFrame(!P)) Ψ"
proof -
from ‹Ψ⇩P ≃ 𝟭› have "⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ 𝟭⟩ ≃⇩F ⟨A⇩P, Ψ ⊗ 𝟭⟩"
by(metis frameIntCompositionSym frameIntAssociativity frameIntCommutativity frameIntIdentity FrameStatEqTrans FrameStatEqSym)
moreover from ‹A⇩P ♯* Ψ› have "⟨A⇩P, Ψ ⊗ 𝟭⟩ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩"
by(force intro: frameResFreshChain)
ultimately show ?thesis using RimpP by(auto simp add: FrameStatEq_def dest: FrameStatImpTrans)
qed
moreover assume "Ψ ⊳ P ∥ !P ⟼α ≺ P'"
hence "Ψ ⊳ !P ⟼α ≺ P'" using ‹guarded P› by(rule Bang)
ultimately show ?thesis by(rule weakTransitionI)
next
fix P'''
assume "Ψ ⊳ P ∥ !P ⟹⇩τ P''"
hence "Ψ ⊳ !P ⟹⇩τ P''" using ‹guarded P› by(rule tauStepChainBang)
hence "Ψ ⊳ !P ⟹⇧^⇩τ P''" by simp
moreover assume "insertAssertion(extractFrame R) Ψ ↪⇩F insertAssertion(extractFrame P'') Ψ"
and "Ψ ⊳ P'' ⟼α ≺ P'"
ultimately show ?thesis by(rule weakTransitionI)
qed
qed
lemma weakTransitionFrameImp:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes PTrans: "Ψ : Q ⊳ P ⟹α ≺ P'"
and "insertAssertion(extractFrame R) Ψ ↪⇩F insertAssertion(extractFrame Q) Ψ"
shows "Ψ : R ⊳ P ⟹α ≺ P'"
using assms
by(auto simp add: weakTransition_def intro: FrameStatImpTrans)
lemma guardedFrameStatEq:
fixes P :: "('a, 'b, 'c) psi"
assumes "guarded P"
shows "extractFrame P ≃⇩F ⟨ε, 𝟭⟩"
proof -
obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" by(rule freshFrame)
from ‹guarded P› FrP have "Ψ⇩P ≃ 𝟭" by(blast dest: guardedStatEq)
hence "⟨A⇩P, Ψ⇩P⟩ ≃⇩F ⟨A⇩P, 𝟭⟩" by(rule_tac frameResChainPres) auto
moreover have "⟨A⇩P, 𝟭⟩ ≃⇩F ⟨ε, 𝟭⟩" by(rule_tac frameResFreshChain) auto
ultimately show ?thesis using FrP by(force intro: FrameStatEqTrans)
qed
lemma weakGuardedTransition:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes PTrans: "Ψ : Q ⊳ P ⟹α ≺ P'"
and "guarded Q"
shows "Ψ : 𝟬 ⊳ P ⟹α ≺ P'"
proof -
obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" by(rule freshFrame)
moreover from ‹guarded Q› FrQ have "Ψ⇩Q ≃ 𝟭" by(blast dest: guardedStatEq)
hence "⟨A⇩Q, Ψ ⊗ Ψ⇩Q⟩ ≃⇩F ⟨A⇩Q, Ψ ⊗ 𝟭⟩" by(metis frameIntCompositionSym)
moreover from ‹A⇩Q ♯* Ψ› have "⟨A⇩Q, Ψ ⊗ 𝟭⟩ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩" by(rule_tac frameResFreshChain) auto
ultimately have "insertAssertion(extractFrame Q) Ψ ≃⇩F insertAssertion (extractFrame (𝟬)) Ψ"
using FrQ ‹A⇩Q ♯* Ψ› by simp (blast intro: FrameStatEqTrans)
with PTrans show ?thesis by(rule_tac weakTransitionFrameImp) (auto simp add: FrameStatEq_def)
qed
lemma expandTauChainFrame:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and A⇩P :: "name list"
and Ψ⇩P :: 'b
and C :: "'d::fs_name"
assumes PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'"
and FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩"
and "distinct A⇩P"
and "A⇩P ♯* P"
and "A⇩P ♯* C"
obtains Ψ' A⇩P' Ψ⇩P' where "extractFrame P' = ⟨A⇩P', Ψ⇩P'⟩" and "Ψ⇩P ⊗ Ψ' ≃ Ψ⇩P'" and "A⇩P' ♯* P'" and "A⇩P' ♯* C" and "distinct A⇩P'"
using PChain FrP ‹A⇩P ♯* P›
proof(induct arbitrary: thesis rule: tauChainInduct)
case(TauBase P)
have "Ψ⇩P ⊗ SBottom' ≃ Ψ⇩P" by(rule Identity)
with ‹extractFrame P = ⟨A⇩P, Ψ⇩P⟩› show ?case using ‹A⇩P ♯* P› ‹A⇩P ♯* C› ‹distinct A⇩P› by(rule TauBase)
next
case(TauStep P P' P'')
from ‹extractFrame P = ⟨A⇩P, Ψ⇩P⟩› ‹A⇩P ♯* P›
obtain Ψ' A⇩P' Ψ⇩P' where FrP': "extractFrame P' = ⟨A⇩P', Ψ⇩P'⟩" and "Ψ⇩P ⊗ Ψ' ≃ Ψ⇩P'"
and "A⇩P' ♯* P'" and "A⇩P' ♯* C" and "distinct A⇩P'"
by(rule_tac TauStep)
from ‹Ψ ⊳ P' ⟼τ ≺ P''› FrP' ‹distinct A⇩P'› ‹A⇩P' ♯* P'› ‹A⇩P' ♯* C›
obtain Ψ'' A⇩P'' Ψ⇩P'' where FrP'': "extractFrame P'' = ⟨A⇩P'', Ψ⇩P''⟩" and "Ψ⇩P' ⊗ Ψ'' ≃ Ψ⇩P''"
and "A⇩P'' ♯* P''" and "A⇩P'' ♯* C" and "distinct A⇩P''"
by(rule expandTauFrame)
from ‹Ψ⇩P ⊗ Ψ' ≃ Ψ⇩P'› have "(Ψ⇩P ⊗ Ψ') ⊗ Ψ'' ≃ Ψ⇩P' ⊗ Ψ''" by(rule Composition)
with ‹Ψ⇩P' ⊗ Ψ'' ≃ Ψ⇩P''› have "Ψ⇩P ⊗ Ψ' ⊗ Ψ'' ≃ Ψ⇩P''"
by(metis AssertionStatEqTrans Associativity Commutativity)
with FrP'' show ?case using ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* C› ‹distinct A⇩P''›
by(rule TauStep)
qed
lemma frameIntImpComposition:
fixes Ψ :: 'b
and Ψ' :: 'b
and A⇩F :: "name list"
and Ψ⇩F :: 'b
assumes "Ψ ≃ Ψ'"
shows "⟨A⇩F, Ψ ⊗ Ψ⇩F⟩ ↪⇩F ⟨A⇩F, Ψ' ⊗ Ψ⇩F⟩"
using assms frameIntComposition
by(simp add: FrameStatEq_def)
lemma tauChainInduct2[consumes 1, case_names TauBase TauStep]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
assumes PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'"
and cBase: "⋀P. Prop P P"
and cStep: "⋀P P' P''. ⟦Ψ ⊳ P' ⟼τ ≺ P''; Ψ ⊳ P ⟹⇧^⇩τ P'; Prop P P'⟧ ⟹ Prop P P''"
shows "Prop P P'"
using assms
by(rule tauChainInduct)
lemma tauStepChainInduct2[consumes 1, case_names TauBase TauStep]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
assumes PChain: "Ψ ⊳ P ⟹⇩τ P'"
and cBase: "⋀P P'. Ψ ⊳ P ⟼τ ≺ P' ⟹ Prop P P'"
and cStep: "⋀P P' P''. ⟦Ψ ⊳ P' ⟼τ ≺ P''; Ψ ⊳ P ⟹⇩τ P'; Prop P P'⟧ ⟹ Prop P P''"
shows "Prop P P'"
using assms
by(rule tauStepChainInduct)
lemma weakTransferTauChainFrame:
fixes Ψ⇩F :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and A⇩P :: "name list"
and Ψ⇩P :: 'b
and A⇩F :: "name list"
and A⇩G :: "name list"
and Ψ⇩G :: 'b
assumes PChain: "Ψ⇩F ⊳ P ⟹⇧^⇩τ P'"
and FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩"
and "distinct A⇩P"
and FeqG: "⋀Ψ. insertAssertion (⟨A⇩F, Ψ⇩F ⊗ Ψ⇩P⟩) Ψ ↪⇩F insertAssertion (⟨A⇩G, Ψ⇩G ⊗ Ψ⇩P⟩) Ψ"
and "A⇩F ♯* Ψ⇩G"
and "A⇩G ♯* Ψ"
and "A⇩G ♯* Ψ⇩F"
and "A⇩F ♯* A⇩G"
and "A⇩F ♯* P"
and "A⇩G ♯* P"
and "A⇩P ♯* A⇩F"
and "A⇩P ♯* A⇩G"
and "A⇩P ♯* Ψ⇩F"
and "A⇩P ♯* Ψ⇩G"
and "A⇩P ♯* P"
shows "Ψ⇩G ⊳ P ⟹⇧^⇩τ P'"
using PChain FrP ‹A⇩F ♯* P› ‹A⇩G ♯* P› ‹A⇩P ♯* P›
proof(induct rule: tauChainInduct2)
case TauBase
thus ?case by simp
next
case(TauStep P P' P'')
have FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" by fact
then have PChain: "Ψ⇩G ⊳ P ⟹⇧^⇩τ P'" using ‹A⇩F ♯* P› ‹A⇩G ♯* P› ‹A⇩P ♯* P› by(rule TauStep)
then obtain A⇩P' Ψ⇩P' Ψ' where FrP': "extractFrame P' = ⟨A⇩P', Ψ⇩P'⟩" and "Ψ⇩P ⊗ Ψ' ≃ Ψ⇩P'"
and "A⇩P' ♯* A⇩F" and "A⇩P' ♯* A⇩G" and "A⇩P' ♯* Ψ⇩F" and "A⇩P' ♯* Ψ⇩G"
and "distinct A⇩P'"
using FrP ‹distinct A⇩P› ‹A⇩P ♯* P› ‹A⇩P ♯* A⇩F› ‹A⇩P ♯* A⇩G› ‹A⇩P ♯* Ψ⇩F› ‹A⇩P ♯* Ψ⇩G›
by(rule_tac C="(A⇩F, A⇩G, Ψ⇩F, Ψ⇩G)" in expandTauChainFrame) auto
from PChain ‹A⇩F ♯* P› ‹A⇩G ♯* P› have "A⇩F ♯* P'" and "A⇩G ♯* P'" by(blast dest: tauChainFreshChain)+
with ‹A⇩F ♯* P› ‹A⇩G ♯* P› ‹A⇩P ♯* A⇩F› ‹A⇩P ♯* A⇩G›‹A⇩P' ♯* A⇩F› ‹A⇩P' ♯* A⇩G› FrP FrP'
have "A⇩F ♯* Ψ⇩P" and "A⇩G ♯* Ψ⇩P" and "A⇩F ♯* Ψ⇩P'" and "A⇩G ♯* Ψ⇩P'"
by(auto dest: extractFrameFreshChain)
from FeqG have FeqG: "insertAssertion (⟨A⇩F, Ψ⇩F ⊗ Ψ⇩P⟩) Ψ' ↪⇩F insertAssertion (⟨A⇩G, Ψ⇩G ⊗ Ψ⇩P⟩) Ψ'"
by blast
obtain p::"name prm" where "(p ∙ A⇩F) ♯* Ψ⇩F" and "(p ∙ A⇩F) ♯* Ψ⇩P" and "(p ∙ A⇩F) ♯* Ψ⇩P'" and "(p ∙ A⇩F) ♯* Ψ'"
and Sp: "(set p) ⊆ set A⇩F × set(p ∙ A⇩F)" and "distinctPerm p"
by(rule_tac xvec=A⇩F and c="(Ψ⇩F, Ψ⇩P, Ψ', Ψ⇩P')" in name_list_avoiding) auto
obtain q::"name prm" where "(q ∙ A⇩G) ♯* Ψ⇩G" and "(q ∙ A⇩G) ♯* Ψ⇩P" and "(q ∙ A⇩G) ♯* Ψ⇩P'" and "(q ∙ A⇩G) ♯* Ψ'"
and Sq: "(set q) ⊆ set A⇩G × set(q ∙ A⇩G)" and "distinctPerm q"
by(rule_tac xvec=A⇩G and c="(Ψ⇩G, Ψ⇩P, Ψ', Ψ⇩P')" in name_list_avoiding) auto
from ‹Ψ⇩P ⊗ Ψ' ≃ Ψ⇩P'› have "⟨(p ∙ A⇩F), ((p ∙ Ψ⇩F) ⊗ Ψ⇩P')⟩ ≃⇩F ⟨(p ∙ A⇩F), (p ∙ Ψ⇩F) ⊗ (Ψ⇩P ⊗ Ψ')⟩"
by(rule frameIntCompositionSym[OF AssertionStatEqSym])
hence "⟨(p ∙ A⇩F), (p ∙ Ψ⇩F) ⊗ Ψ⇩P'⟩ ≃⇩F ⟨(p ∙ A⇩F), Ψ' ⊗ ((p ∙ Ψ⇩F) ⊗ Ψ⇩P)⟩"
by(metis frameIntAssociativity FrameStatEqTrans frameIntCommutativity FrameStatEqSym)
moreover from FeqG ‹A⇩F ♯* Ψ⇩P› ‹(p ∙ A⇩F) ♯* Ψ⇩P› ‹(p ∙ A⇩F) ♯* Ψ⇩F› ‹(p ∙ A⇩F) ♯* Ψ'› Sp
have "⟨(p ∙ A⇩F), Ψ' ⊗ ((p ∙ Ψ⇩F) ⊗ Ψ⇩P)⟩ ↪⇩F insertAssertion (⟨A⇩G, Ψ⇩G ⊗ Ψ⇩P⟩) Ψ'"
apply(erule_tac rev_mp) by(subst frameChainAlpha) (auto simp add: eqvts)
hence "⟨(p ∙ A⇩F), Ψ' ⊗ ((p ∙ Ψ⇩F) ⊗ Ψ⇩P)⟩ ↪⇩F (⟨(q ∙ A⇩G), Ψ' ⊗ (q ∙ Ψ⇩G) ⊗ Ψ⇩P⟩)"
using ‹A⇩G ♯* Ψ⇩P› ‹(q ∙ A⇩G) ♯* Ψ⇩P› ‹(q ∙ A⇩G) ♯* Ψ⇩G› ‹(q ∙ A⇩G) ♯* Ψ'› Sq
apply(