Theory Weak_Simulation
theory Weak_Simulation
imports Simulation Tau_Chain
begin
context env begin
definition
"weakSimulation" :: "'b ⇒ ('a, 'b, 'c) psi ⇒
('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set ⇒
('a, 'b, 'c) psi ⇒ bool" (‹_ ⊳ _ ↝<_> _› [80, 80, 80, 80] 80)
where
"Ψ ⊳ P ↝<Rel> Q ≡ (∀Ψ' α Q'. Ψ ⊳ Q ⟼α ≺ Q' ⟶ bn α ♯* Ψ ⟶ bn α ♯* P ⟶ α ≠ τ ⟶
(∃P''. Ψ : Q ⊳ P ⟹α ≺ P'' ∧ (∃P'. Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P' ∧ (Ψ ⊗ Ψ', P', Q') ∈ Rel))) ∧
(∀Q'. Ψ ⊳ Q ⟼τ ≺ Q' ⟶ (∃P'. Ψ ⊳ P ⟹⇧^⇩τ P' ∧ (Ψ, P', Q') ∈ Rel))"
abbreviation
weakSimulationNilJudge (‹_ ↝<_> _› [80, 80, 80] 80) where "P ↝<Rel> Q ≡ SBottom' ⊳ P ↝<Rel> Q"
lemma weakSimI[consumes 1, case_names cAct cTau]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and C :: "'d::fs_name"
assumes Eqvt: "eqvt Rel"
and rAct: "⋀Ψ' α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* Ψ; bn α ♯* P; bn α ♯* Q;
bn α ♯* subject α; bn α ♯* C; distinct(bn α); α ≠ τ⟧ ⟹
∃P''. Ψ : Q ⊳ P ⟹α ≺ P'' ∧ (∃P'. Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P' ∧ (Ψ ⊗ Ψ', P', Q') ∈ Rel)"
and rTau: "⋀Q'. Ψ ⊳ Q ⟼τ ≺ Q' ⟹ ∃P'. Ψ ⊳ P ⟹⇧^⇩τ P' ∧ (Ψ, P', Q') ∈ Rel"
shows "Ψ ⊳ P ↝<Rel> Q"
proof(auto simp add: weakSimulation_def)
fix Ψ' α Q'
assume "Ψ ⊳ Q ⟼α ≺ Q'" and "bn α ♯* Ψ" and "bn α ♯* P" and "α ≠ τ"
thus "∃P''. Ψ : Q ⊳ P ⟹α ≺ P'' ∧ (∃P'. Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P' ∧ (Ψ ⊗ Ψ', P', Q') ∈ Rel)"
proof(nominal_induct α rule: action.strong_induct)
case(In M N)
thus ?case by(rule_tac rAct) auto
next
case(Out M xvec N)
from ‹bn(M⦇ν*xvec⦈⟨N⟩) ♯* Ψ› ‹bn(M⦇ν*xvec⦈⟨N⟩) ♯* P› have "xvec ♯* Ψ" and "xvec ♯* P" by simp+
from ‹Ψ ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'› have "distinct xvec" by(force dest: boundOutputDistinct)
obtain p where "(p ∙ xvec) ♯* Ψ" and "(p ∙ xvec) ♯* M" and "(p ∙ xvec) ♯* xvec"
and"(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* Q'" and "(p ∙ xvec) ♯* Ψ'"
and "(p ∙ xvec) ♯* C" and "(p ∙ xvec) ♯* xvec" and "(p ∙ xvec) ♯* N"
and S: "(set p) ⊆ (set xvec) × (set(p ∙ xvec))" and "distinctPerm p"
by(rule_tac xvec=xvec and c="(Ψ, M, Q, N, P, Q', xvec, C, Ψ')" in name_list_avoiding)
(auto simp add: eqvts fresh_star_prod)
from ‹distinct xvec› have "distinct(p ∙ xvec)" by simp
from ‹Ψ ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'› ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* Q'› S
have "Ψ ⊳ Q ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ Q')" by(simp add: boundOutputChainAlpha'' residualInject)
then obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ P''"
and P''Chain: "Ψ ⊗ (p ∙ Ψ') ⊳ P'' ⟹⇧^⇩τ P'"
and P'RelQ': "(Ψ ⊗ (p ∙ Ψ'), P', p ∙ Q') ∈ Rel"
using ‹(p ∙ xvec) ♯* Ψ› ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› ‹(p ∙ xvec) ♯* M› ‹(p ∙ xvec) ♯* C› ‹distinct(p ∙ xvec)›
by(drule_tac Ψ'="p ∙ Ψ'" in rAct) auto
from PTrans S ‹distinctPerm p› ‹xvec ♯* P› ‹(p ∙ xvec) ♯* xvec› ‹(p ∙ xvec) ♯* M› ‹distinct xvec›
have "Ψ : Q ⊳ P ⟹M⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P'')"
by(rule_tac weakOutputAlpha) auto
moreover from P''Chain have "(p ∙ (Ψ ⊗ (p ∙ Ψ'))) ⊳ (p ∙ P'') ⟹⇧^⇩τ (p ∙ P')" by(rule eqvts)
with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ'› S ‹distinctPerm p›
have "Ψ ⊗ Ψ' ⊳ (p ∙ P'') ⟹⇧^⇩τ (p ∙ P')" by(simp add: eqvts)
moreover from P'RelQ' Eqvt S ‹distinctPerm p› have "(p ∙ (Ψ ⊗ (p ∙ Ψ')), p ∙ P', p ∙ p ∙ Q') ∈ Rel"
apply(simp add: eqvt_def eqvts)
apply(erule_tac x="(Ψ ⊗ (p ∙ Ψ'), P', p ∙ Q')" in ballE)
apply(erule_tac x="p" in allE)
by(auto simp add: eqvts)
with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S ‹distinctPerm p›
have "(Ψ ⊗ Ψ', p ∙ P', Q') ∈ Rel" by(simp add: eqvts)
ultimately show ?case by blast
next
case Tau
thus ?case by simp
qed
next
fix Q'
assume "Ψ ⊳ Q ⟼τ ≺ Q'"
thus "∃P'. Ψ ⊳ P ⟹⇧^⇩τ P' ∧ (Ψ, P', Q') ∈ Rel"
by(rule rTau)
qed
lemma weakSimI2[case_names cAct cTau]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and C :: "'d::fs_name"
assumes rOutput: "⋀Ψ' α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* Ψ; bn α ♯* P; α ≠ τ⟧ ⟹
∃P''. Ψ : Q ⊳ P ⟹α ≺ P'' ∧ (∃P'. Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P' ∧ (Ψ ⊗ Ψ', P', Q') ∈ Rel)"
and rTau: "⋀Q'. Ψ ⊳ Q ⟼τ ≺ Q' ⟹ ∃P'. Ψ ⊳ P ⟹⇧^⇩τ P' ∧ (Ψ, P', Q') ∈ Rel"
shows "Ψ ⊳ P ↝<Rel> Q"
using assms by(simp add: weakSimulation_def)
lemma weakSimIChainFresh[consumes 4, case_names cOutput cInput]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and yvec :: "name list"
and C :: "'d::fs_name"
assumes Eqvt: "eqvt Rel"
and "yvec ♯* Ψ"
and "yvec ♯* P"
and "yvec ♯* Q"
and rAct: "⋀Ψ' α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* Ψ; bn α ♯* P; bn α ♯* Q; α ≠ τ;
bn α ♯* subject α; bn α ♯* C; yvec ♯* α; yvec ♯* Q'; yvec ♯* Ψ'⟧ ⟹
∃P''. Ψ : Q ⊳ P ⟹α ≺ P'' ∧ (∃P'. Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P' ∧ (Ψ ⊗ Ψ', P', Q') ∈ Rel)"
and rTau: "⋀Q'. ⟦Ψ ⊳ Q ⟼τ ≺ Q'; yvec ♯* Q'⟧ ⟹ ∃P'. Ψ ⊳ P ⟹⇧^⇩τ P' ∧ (Ψ, P', Q') ∈ Rel"
shows "Ψ ⊳ P ↝<Rel> Q"
using ‹eqvt Rel›
proof(induct rule: weakSimI[of _ _ _ _ "(yvec, C)"])
case(cAct Ψ' α Q')
obtain p::"name prm" where "(p ∙ yvec) ♯* Ψ" and "(p ∙ yvec) ♯* P" and "(p ∙ yvec) ♯* Q"
and "(p ∙ yvec) ♯* α" and "(p ∙ yvec) ♯* Ψ'"
and "(p ∙ yvec) ♯* Q'" and S: "(set p) ⊆ set yvec × set(p ∙ yvec)"
and "distinctPerm p"
by(rule_tac c="(Ψ, P, Q, α, Q', Ψ')" and xvec=yvec in name_list_avoiding) auto
from ‹bn α ♯* (yvec, C)› have "bn α ♯* yvec" and "bn α ♯* C" by(simp add: freshChainSym)+
show ?case
proof(cases rule: actionCases[where α = α])
case(cInput M N)
from ‹(p ∙ yvec) ♯* α› ‹α = M⦇N⦈› have "(p ∙ yvec) ♯* M" and "(p ∙ yvec) ♯* N" by simp+
from ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹α = M⦇N⦈› ‹yvec ♯* Ψ› ‹(p ∙ yvec) ♯* Ψ› ‹yvec ♯* Q› ‹(p ∙ yvec) ♯* Q› S
have "Ψ ⊳ Q ⟼(p ∙ M)⦇(p ∙ N)⦈ ≺ (p ∙ Q')"
by(drule_tac pi=p in semantics.eqvt) (simp add: eqvts)
moreover from ‹(p ∙ yvec) ♯* M› have "(p ∙ (p ∙ yvec)) ♯* (p ∙ M)"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹distinctPerm p› have "yvec ♯* (p ∙ M)" by simp
moreover from ‹(p ∙ yvec) ♯* N› have "(p ∙ p ∙ yvec) ♯* (p ∙ N)"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹distinctPerm p› have "yvec ♯* (p ∙ N)" by simp
moreover from ‹(p ∙ yvec) ♯* Q'› have "(p ∙ p ∙ yvec) ♯* (p ∙ Q')"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹distinctPerm p› have "yvec ♯* (p ∙ Q')" by simp
moreover from ‹(p ∙ yvec) ♯* Ψ'› have "(p ∙ p ∙ yvec) ♯* (p ∙ Ψ')"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹distinctPerm p› have "yvec ♯* (p ∙ Ψ')" by simp
ultimately obtain P' P'' where PTrans: "Ψ : Q ⊳ P ⟹(p ∙ M)⦇(p ∙ N)⦈ ≺ P''" and P''Chain: "Ψ ⊗ (p ∙ Ψ') ⊳ P'' ⟹⇧^⇩τ P'"
and P'RelQ': "(Ψ ⊗ (p ∙ Ψ'), P', (p ∙ Q')) ∈ Rel"
by(auto dest: rAct)
from PTrans have "(p ∙ Ψ) : (p ∙ Q) ⊳ (p ∙ P) ⟹p ∙ ((p ∙ M)⦇(p ∙ N)⦈) ≺ (p ∙ P'')"
by(rule weakTransitionClosed)
with S ‹yvec ♯* Ψ› ‹(p ∙ yvec) ♯* Ψ› ‹yvec ♯* Q› ‹(p ∙ yvec) ♯* Q› ‹yvec ♯* P› ‹(p ∙ yvec) ♯* P› ‹distinctPerm p›
have "Ψ : Q ⊳ P ⟹M⦇N⦈ ≺ (p ∙ P'')" by(simp add: eqvts)
moreover from P''Chain have "(p ∙ (Ψ ⊗ (p ∙ Ψ'))) ⊳ (p ∙ P'') ⟹⇧^⇩τ (p ∙ P')" by(rule eqvts)
with ‹yvec ♯* Ψ› ‹(p ∙ yvec) ♯* Ψ› S ‹distinctPerm p›
have "Ψ ⊗ Ψ' ⊳ (p ∙ P'') ⟹⇧^⇩τ (p ∙ P')" by(simp add: eqvts)
moreover from P'RelQ' Eqvt have "(p ∙ (Ψ ⊗ (p ∙ Ψ')), p ∙ P', p ∙ p ∙ Q') ∈ Rel"
apply(simp add: eqvt_def eqvts)
apply(erule_tac x="(Ψ ⊗ (p ∙ Ψ'), P', p ∙ Q')" in ballE)
apply(erule_tac x="p" in allE)
by(auto simp add: eqvts)
with ‹yvec ♯* Ψ› ‹(p ∙ yvec) ♯* Ψ› S ‹distinctPerm p› have "(Ψ ⊗ Ψ', p ∙ P', Q') ∈ Rel" by(simp add: eqvts)
ultimately show ?thesis using ‹α=M⦇N⦈› by blast
next
case(cOutput M xvec N)
from ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* Q› ‹bn α ♯* subject α› ‹α=M⦇ν*xvec⦈⟨N⟩› ‹bn α ♯* yvec›
‹(p ∙ yvec) ♯* α› ‹bn α ♯* C› ‹bn α ♯* subject α› ‹distinct(bn α)›
have "xvec ♯* Ψ" and "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* M" and "yvec ♯* xvec"
and "(p ∙ yvec) ♯* M" and "(p ∙ yvec) ♯* xvec" and "xvec ♯* C" and "xvec ♯* M" and "(p ∙ yvec) ♯* N"
and "distinct xvec" by simp+
from ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹yvec ♯* Ψ› ‹(p ∙ yvec) ♯* Ψ› ‹yvec ♯* Q› ‹(p ∙ yvec) ♯* Q› S ‹α=M⦇ν*xvec⦈⟨N⟩›
have "Ψ ⊳ Q ⟼(p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ Q'"
by(rule_tac outputPermSubject) (assumption | simp add: fresh_star_def)+
moreover note ‹xvec ♯* Ψ› ‹xvec ♯* P›
moreover note ‹xvec ♯* Q›
moreover from ‹xvec ♯* M› have "(p ∙ xvec) ♯* (p ∙ M)"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹yvec ♯* xvec› ‹(p ∙ yvec) ♯* xvec› S have "xvec ♯* (p ∙ M)"
by simp
moreover note ‹xvec ♯* C›
moreover from ‹(p ∙ yvec) ♯* M› have "(p ∙ (p ∙ yvec)) ♯* (p ∙ M)"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹distinctPerm p› have "yvec ♯* (p ∙ M)" by simp
moreover note ‹yvec ♯* xvec›
moreover from ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹yvec ♯* Q› ‹yvec ♯* xvec› ‹α=M⦇ν*xvec⦈⟨N⟩› ‹xvec ♯* M› ‹distinct xvec›
have "yvec ♯* N" and "yvec ♯* Q'" by(force dest: outputFreshChainDerivative)+
moreover from ‹(p ∙ yvec) ♯* Ψ'› have "(p ∙ p ∙ yvec) ♯* (p ∙ Ψ')"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹distinctPerm p› have "yvec ♯* (p ∙ Ψ')" by simp
ultimately obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹(p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ P''"
and PChain: "Ψ ⊗ (p ∙ Ψ') ⊳ P'' ⟹⇧^⇩τ P'"
and P'RelQ': "(Ψ ⊗ (p ∙ Ψ'), P', Q') ∈ Rel"
by(drule_tac rAct) auto
from PTrans have "(p ∙ Ψ) : (p ∙ Q) ⊳ (p ∙ P) ⟹(p ∙ ((p ∙ M)⦇ν*xvec⦈⟨N⟩)) ≺ (p ∙ P'')"
by(rule eqvts)
with S ‹yvec ♯* Ψ› ‹(p ∙ yvec) ♯* Ψ› ‹yvec ♯* P› ‹(p ∙ yvec) ♯* P› ‹yvec ♯* Q› ‹(p ∙ yvec) ♯* Q› ‹yvec ♯* xvec› ‹(p ∙ yvec) ♯* xvec›
‹yvec ♯* N› ‹(p ∙ yvec) ♯* N› ‹distinctPerm p› have "Ψ : Q ⊳ P ⟹M⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P'')"
by(simp add: eqvts)
moreover from PChain have "(p ∙ (Ψ ⊗ (p ∙ Ψ'))) ⊳ (p ∙ P'') ⟹⇧^⇩τ (p ∙ P')" by(rule eqvts)
with S ‹yvec ♯* Ψ› ‹(p ∙ yvec) ♯* Ψ› ‹distinctPerm p› have "Ψ ⊗ Ψ' ⊳ (p ∙ P'') ⟹⇧^⇩τ (p ∙ P')" by(simp add: eqvts)
moreover from P'RelQ' ‹eqvt Rel› have "p ∙ (Ψ ⊗ (p ∙ Ψ'), P', Q') ∈ Rel"
by(simp add: eqvt_def) auto
with ‹yvec ♯* Ψ› ‹(p ∙ yvec) ♯* Ψ›‹yvec ♯* Q'› ‹(p ∙ yvec) ♯* Q'› S ‹distinctPerm p›
have "(Ψ ⊗ Ψ', p ∙ P', Q') ∈ Rel" by(simp add: eqvts)
ultimately show ?thesis using ‹α=M⦇ν*xvec⦈⟨N⟩› by blast
next
case cTau
from ‹α = τ› ‹α ≠ τ› have "False" by simp
thus ?thesis by simp
qed
next
case(cTau Q')
from ‹Ψ ⊳ Q ⟼τ ≺ Q'› ‹yvec ♯* Q› have "yvec ♯* Q'"
by(force dest: tauFreshChainDerivative)
with ‹Ψ ⊳ Q ⟼τ ≺ Q'› show ?case
by(rule rTau)
qed
lemma weakSimIFresh[consumes 4, case_names cAct cTau]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and x :: name
and C :: "'d::fs_name"
assumes Eqvt: "eqvt Rel"
and "x ♯ Ψ"
and "x ♯ P"
and "x ♯ Q"
and "⋀α Q' Ψ'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* Ψ; bn α ♯* P; bn α ♯* Q; α ≠ τ;
bn α ♯* subject α; bn α ♯* C; x ♯ α; x ♯ Q'; x ♯ Ψ'⟧ ⟹
∃P''. Ψ : Q ⊳ P ⟹α ≺ P'' ∧ (∃P'. Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P' ∧ (Ψ ⊗ Ψ', P', Q') ∈ Rel)"
and "⋀Q'. ⟦Ψ ⊳ Q ⟼τ ≺ Q'; x ♯ Q'⟧ ⟹ ∃P'. Ψ ⊳ P ⟹⇧^⇩τ P' ∧ (Ψ, P', Q') ∈ Rel"
shows "Ψ ⊳ P ↝<Rel> Q"
using assms
by(rule_tac yvec="[x]" and C=C in weakSimIChainFresh) auto
lemma weakSimE:
fixes F :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ P ↝<Rel> Q"
shows "⋀Ψ' α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* Ψ; bn α ♯* P; α ≠ τ⟧ ⟹
∃P''. Ψ : Q ⊳ P ⟹α ≺ P'' ∧ (∃P'. Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P' ∧ (Ψ ⊗ Ψ', P', Q') ∈ Rel)"
and "⋀Q'. Ψ ⊳ Q ⟼τ ≺ Q' ⟹ ∃P'. Ψ ⊳ P ⟹⇧^⇩τ P' ∧ (Ψ, P', Q') ∈ Rel"
using assms
by(auto simp add: weakSimulation_def)
lemma weakSimClosedAux:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and p :: "name prm"
assumes EqvtRel: "eqvt Rel"
and PSimQ: "Ψ ⊳ P ↝<Rel> Q"
shows "(p ∙ Ψ) ⊳ (p ∙ P) ↝<Rel> (p ∙ Q)"
using EqvtRel
proof(induct rule: weakSimI[of _ _ _ _ "(Ψ, P, p)"])
case(cAct Ψ' α Q')
from ‹p ∙ Ψ ⊳ p ∙ Q ⟼α ≺ Q'›
have "(rev p ∙ p ∙ Ψ) ⊳ (rev p ∙ p ∙ Q) ⟼(rev p ∙ (α ≺ Q'))"
by(blast dest: semantics.eqvt)
hence "Ψ ⊳ Q ⟼(rev p ∙ α) ≺ (rev p ∙ Q')"
by(simp add: eqvts)
moreover with ‹bn α ♯* (Ψ, P, p)› have "bn α ♯* Ψ" and "bn α ♯* P" and "bn α ♯* p" by simp+
moreover from ‹α ≠ τ› have "(rev p ∙ α) ≠ τ"
by(cases rule: actionCases[where α=α]) auto
ultimately obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹(rev p ∙ α) ≺ P''"
and P''Chain: "Ψ ⊗ (rev p ∙ Ψ') ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ (rev p ∙ Ψ'), P', rev p ∙ Q') ∈ Rel"
using ‹α ≠ τ› PSimQ
by(drule_tac Ψ'="rev p ∙ Ψ'" in weakSimE(1)) (auto simp add: freshChainPermSimp bnEqvt[symmetric])
from PTrans have "(p ∙ Ψ) : (p ∙ Q) ⊳ (p ∙ P) ⟹(p ∙ (rev p ∙ α)) ≺ (p ∙ P'')"
by(rule eqvts)
hence "(p ∙ Ψ) : (p ∙ Q) ⊳ (p ∙ P) ⟹α ≺ (p ∙ P'')" by(simp add: eqvts freshChainPermSimp)
moreover from P''Chain have "(p ∙ (Ψ ⊗ (rev p ∙ Ψ'))) ⊳ (p ∙ P'') ⟹⇧^⇩τ (p ∙ P')" by(rule eqvts)
hence "(p ∙ Ψ) ⊗ Ψ' ⊳ (p ∙ P'') ⟹⇧^⇩τ (p ∙ P')" by(simp add: eqvts)
moreover from P'RelQ' EqvtRel have "(p ∙ ((Ψ ⊗ (rev p ∙ Ψ')), P', rev p ∙ Q')) ∈ Rel"
by(simp only: eqvt_def)
hence "((p ∙ Ψ) ⊗ Ψ', p ∙ P', Q') ∈ Rel" by(simp add: eqvts)
ultimately show ?case by blast
next
case(cTau Q')
from ‹p ∙ Ψ ⊳ p ∙ Q ⟼τ ≺ Q'›
have "(rev p ∙ p ∙ Ψ) ⊳ (rev p ∙ p ∙ Q) ⟼(rev p ∙ (τ ≺ Q'))"
by(blast dest: semantics.eqvt)
hence "Ψ ⊳ Q ⟼τ ≺ (rev p ∙ Q')" by(simp add: eqvts)
with PSimQ obtain P' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ, P', rev p ∙ Q') ∈ Rel"
by(blast dest: weakSimE)
from PChain have "(p ∙ Ψ) ⊳ (p ∙ P) ⟹⇧^⇩τ (p ∙ P')" by(rule tauChainEqvt)
moreover from P'RelQ' EqvtRel have "(p ∙ (Ψ, P', rev p ∙ Q')) ∈ Rel"
by(simp only: eqvt_def)
hence "(p ∙ Ψ, p ∙ P', Q') ∈ Rel" by(simp add: eqvts)
ultimately show ?case
by blast
qed
lemma weakSimClosed:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and p :: "name prm"
assumes EqvtRel: "eqvt Rel"
shows "Ψ ⊳ P ↝<Rel> Q ⟹ (p ∙ Ψ) ⊳ (p ∙ P) ↝<Rel> (p ∙ Q)"
and "P ↝<Rel> Q ⟹ (p ∙ P) ↝<Rel> (p ∙ Q)"
using EqvtRel
by(force dest: weakSimClosedAux simp add: permBottom)+
lemma weakSimReflexive:
fixes Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
assumes "{(Ψ, P, P) | Ψ P. True} ⊆ Rel"
shows "Ψ ⊳ P ↝<Rel> P"
using assms
by(auto simp add: weakSimulation_def weakTransition_def dest: rtrancl_into_rtrancl) force+
lemma weakSimTauChain:
fixes Ψ :: 'b
and Q :: "('a, 'b, 'c) psi"
and Q' :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes "Ψ ⊳ Q ⟹⇧^⇩τ Q'"
and "(Ψ, P, Q) ∈ Rel"
and Sim: "⋀Ψ' R S. (Ψ', R, S) ∈ Rel ⟹ Ψ' ⊳ R ↝<Rel> S"
obtains P' where "Ψ ⊳ P ⟹⇧^⇩τ P'" and "(Ψ, P', Q') ∈ Rel"
proof -
assume A: "⋀P'. ⟦Ψ ⊳ P ⟹⇧^⇩τ P'; (Ψ, P', Q') ∈ Rel⟧ ⟹ thesis"
from ‹Ψ ⊳ Q ⟹⇧^⇩τ Q'› ‹(Ψ, P, Q) ∈ Rel› A show ?thesis
proof(induct arbitrary: P thesis rule: tauChainInduct)
case(TauBase Q P)
moreover have "Ψ ⊳ P ⟹⇧^⇩τ P" by simp
ultimately show ?case by blast
next
case(TauStep Q Q' Q'' P)
from ‹(Ψ, P, Q) ∈ Rel› obtain P' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'" and "(Ψ, P', Q') ∈ Rel"
by(rule TauStep)
from ‹(Ψ, P', Q') ∈ Rel› have "Ψ ⊳ P' ↝<Rel> Q'" by(rule Sim)
then obtain P'' where P'Chain: "Ψ ⊳ P' ⟹⇧^⇩τ P''" and "(Ψ, P'', Q'') ∈ Rel"
using ‹Ψ ⊳ Q' ⟼τ ≺ Q''› by(blast dest: weakSimE)
from PChain P'Chain have "Ψ ⊳ P ⟹⇧^⇩τ P''" by simp
thus ?case using ‹(Ψ, P'', Q'') ∈ Rel› by(rule TauStep)
qed
qed
lemma weakSimE2:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
assumes PRelQ: "(Ψ, P, Q) ∈ Rel"
and Sim: "⋀Ψ' R S. (Ψ', R, S) ∈ Rel ⟹ Ψ' ⊳ R ↝<Rel> S"
and QTrans: "Ψ : R ⊳ Q ⟹α ≺ Q'"
and "bn α ♯* Ψ"
and "bn α ♯* P"
and "α ≠ τ"
obtains P'' P' where "Ψ : R ⊳ P ⟹α ≺ P''" and "Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'" and "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
proof -
assume A: "⋀P'' P'. ⟦Ψ : R ⊳ P ⟹α ≺ P''; Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'; (Ψ ⊗ Ψ', P', Q') ∈ Rel⟧ ⟹ thesis"
from QTrans obtain Q''
where QChain: "Ψ ⊳ Q ⟹⇧^⇩τ Q''"
and ReqQ'': "insertAssertion (extractFrame R) Ψ ↪⇩F insertAssertion (extractFrame Q'') Ψ"
and Q''Trans: "Ψ ⊳ Q'' ⟼α ≺ Q'"
by(rule weakTransitionE)
from QChain PRelQ Sim
obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and P''RelQ'': "(Ψ, P'', Q'') ∈ Rel" by(rule weakSimTauChain)
from PChain ‹bn α ♯* P› have "bn α ♯* P''" by(rule tauChainFreshChain)
from P''RelQ'' have "Ψ ⊳ P'' ↝<Rel> Q''" by(rule Sim)
with Q''Trans ‹bn α ♯* Ψ› ‹bn α ♯* P''› ‹α ≠ τ›
obtain P''' P' where P''Trans: "Ψ : Q'' ⊳ P'' ⟹α ≺ P'''" and P'''Chain: "Ψ ⊗ Ψ' ⊳ P''' ⟹⇧^⇩τ P'"
and P'RelQ': "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
by(blast dest: weakSimE)
from P''Trans obtain P'''' where P''Chain: "Ψ ⊳ P'' ⟹⇧^⇩τ P''''"
and Q''eqP'''': "insertAssertion (extractFrame Q'') Ψ ↪⇩F insertAssertion (extractFrame P'''') Ψ"
and P''''Trans: "Ψ ⊳ P'''' ⟼α ≺ P'''"
by(rule weakTransitionE)
from PChain P''Chain have "Ψ ⊳ P ⟹⇧^⇩τ P''''" by simp
moreover from ReqQ'' Q''eqP'''' have "insertAssertion (extractFrame R) Ψ ↪⇩F insertAssertion (extractFrame P'''') Ψ"
by(rule FrameStatImpTrans)
ultimately have "Ψ : R ⊳ P ⟹α ≺ P'''" using P''''Trans by(rule weakTransitionI)
with P'''Chain P'RelQ' A show ?thesis by blast
qed
lemma weakSimTransitive:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and T :: "('a, 'b, 'c) psi"
and Rel'' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes PRelQ: "(Ψ, P, Q) ∈ Rel"
and QSimR: "Ψ ⊳ Q ↝<Rel'> R"
and Eqvt: "eqvt Rel''"
and Set: "{(Ψ, P, R) | Ψ P R. ∃Q. (Ψ, P, Q) ∈ Rel ∧ (Ψ, Q, R) ∈ Rel'} ⊆ Rel''"
and Sim: "⋀Ψ' R S. (Ψ', R, S) ∈ Rel ⟹ Ψ' ⊳ R ↝<Rel> S"
shows "Ψ ⊳ P ↝<Rel''> R"
using ‹eqvt Rel''›
proof(induct rule: weakSimI[of _ _ _ _ Q])
case(cAct Ψ' α R')
from QSimR ‹Ψ ⊳ R ⟼α ≺ R'› ‹bn α ♯* Ψ› ‹bn α ♯* Q› ‹α ≠ τ›
obtain Q'' Q' where QTrans: "Ψ : R ⊳ Q ⟹α ≺ Q''" and Q''Chain: "Ψ ⊗ Ψ' ⊳ Q'' ⟹⇧^⇩τ Q'"
and Q'RelR': "(Ψ ⊗ Ψ', Q', R') ∈ Rel'"
by(blast dest: weakSimE)
with PRelQ Sim QTrans ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹α ≠ τ›
obtain P''' P'' where PTrans: "Ψ : R ⊳ P ⟹α ≺ P'''"
and P'''Chain: "Ψ ⊗ Ψ' ⊳ P''' ⟹⇧^⇩τ P''" and P''RelQ'': "(Ψ ⊗ Ψ', P'', Q'') ∈ Rel"
by(drule_tac weakSimE2) auto
note PTrans
moreover from Q''Chain P''RelQ'' Sim obtain P' where P''Chain: "Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
by(rule weakSimTauChain)
from P'''Chain P''Chain have "Ψ ⊗ Ψ' ⊳ P''' ⟹⇧^⇩τ P'" by simp
moreover from P'RelQ' Q'RelR' Set have "(Ψ ⊗ Ψ', P', R') ∈ Rel''" by blast
ultimately show ?case by blast
next
case(cTau R')
from QSimR ‹Ψ ⊳ R ⟼τ ≺ R'› obtain Q' where QChain: "Ψ ⊳ Q ⟹⇧^⇩τ Q'" and Q'RelR': "(Ψ, Q', R') ∈ Rel'"
by(blast dest: weakSimE)
from QChain PRelQ Sim obtain P' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
by(rule weakSimTauChain)
note PChain
moreover from P'RelQ' Q'RelR' Set have "(Ψ, P', R') ∈ Rel''" by blast
ultimately show ?case by blast
qed
lemma weakSimStatEq:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and Ψ' :: 'b
assumes PSimQ: "Ψ ⊳ P ↝<Rel> Q"
and "eqvt Rel'"
and "Ψ ≃ Ψ'"
and C1: "⋀Ψ' R S Ψ''. ⟦(Ψ', R, S) ∈ Rel; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', R, S) ∈ Rel'"
shows "Ψ' ⊳ P ↝<Rel'> Q"
using ‹eqvt Rel'›
proof(induct rule: weakSimI[of _ _ _ _ Ψ])
case(cAct Ψ'' α Q')
from ‹Ψ' ⊳ Q ⟼α ≺ Q'› ‹Ψ ≃ Ψ'›
have "Ψ ⊳ Q ⟼α ≺ Q'" by(metis statEqTransition AssertionStatEqSym)
with PSimQ ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹α ≠ τ›
obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹α ≺ P''" and P''Chain: "Ψ ⊗ Ψ'' ⊳ P'' ⟹⇧^⇩τ P'"
and P'RelQ': "(Ψ ⊗ Ψ'', P', Q') ∈ Rel"
by(blast dest: weakSimE)
from PTrans ‹Ψ ≃ Ψ'› have "Ψ' : Q ⊳ P ⟹α ≺ P''" by(rule weakTransitionStatEq)
moreover from P''Chain ‹Ψ ≃ Ψ'› have "Ψ' ⊗ Ψ'' ⊳ P'' ⟹⇧^⇩τ P'" by(metis tauChainStatEq Composition)
moreover from P'RelQ' ‹Ψ ≃ Ψ'› have "(Ψ' ⊗ Ψ'', P', Q') ∈ Rel'"
by(metis C1 Composition)
ultimately show ?case
by blast
next
case(cTau Q')
from ‹Ψ' ⊳ Q ⟼τ ≺ Q'› ‹Ψ ≃ Ψ'›
have "Ψ ⊳ Q ⟼τ ≺ Q'" by(metis statEqTransition AssertionStatEqSym)
with PSimQ obtain P' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
by(blast dest: weakSimE)
from PChain ‹Ψ ≃ Ψ'› have "Ψ' ⊳ P ⟹⇧^⇩τ P'" by(rule tauChainStatEq)
moreover from ‹(Ψ, P', Q') ∈ Rel› ‹Ψ ≃ Ψ'› have "(Ψ', P', Q') ∈ Rel'"
by(rule C1)
ultimately show ?case by blast
qed
lemma weakSimMonotonic:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and A :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and B :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes "Ψ ⊳ P ↝<A> Q"
and "A ⊆ B"
shows "Ψ ⊳ P ↝<B> Q"
using assms
by(simp (no_asm) add: weakSimulation_def) (blast dest: weakSimE)+
lemma strongSimWeakSim:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes PRelQ: "(Ψ, P, Q) ∈ Rel"
and StatImp: "⋀Ψ' R S. (Ψ', R, S) ∈ Rel ⟹ insertAssertion(extractFrame S) Ψ' ↪⇩F insertAssertion(extractFrame R) Ψ'"
and Sim: "⋀Ψ' R S. (Ψ', R, S) ∈ Rel ⟹ Ψ' ⊳ R ↝[Rel] S"
and Ext: "⋀Ψ' R S Ψ''. (Ψ', R, S) ∈ Rel ⟹ (Ψ' ⊗ Ψ'', R, S) ∈ Rel"
shows "Ψ ⊳ P ↝<Rel> Q"
proof(induct rule: weakSimI2)
case(cAct Ψ' α Q')
from PRelQ have "Ψ ⊳ P ↝[Rel] Q" by(rule Sim)
with ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹bn α ♯* Ψ› ‹bn α ♯* P›
obtain P' where PTrans: "Ψ ⊳ P ⟼α ≺ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
by(blast dest: simE)
from PRelQ have "insertAssertion(extractFrame Q) Ψ ↪⇩F insertAssertion(extractFrame P) Ψ" by(rule StatImp)
with PTrans have "Ψ : Q ⊳ P ⟹α ≺ P'" by(rule transitionWeakTransition)
moreover from P'RelQ' have "∀Ψ'. ∃P''. Ψ ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ P'' ∧ (Ψ ⊗ Ψ', P'', Q') ∈ Rel"
by(force intro: Ext)
ultimately show ?case by blast
next
case(cTau Q')
from PRelQ have "Ψ ⊳ P ↝[Rel] Q" by(rule Sim)
with ‹Ψ ⊳ Q ⟼τ ≺ Q'› obtain P' where PTrans: "Ψ ⊳ P ⟼τ ≺ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
by(force dest: simE)
with PTrans have "Ψ ⊳ P ⟹⇧^⇩τ P'" by auto
thus ?case using P'RelQ' by blast
qed
lemma strongAppend:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Rel'' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes PSimQ: "Ψ ⊳ P ↝<Rel> Q"
and QSimR: "Ψ ⊳ Q ↝[Rel'] R"
and Eqvt'': "eqvt Rel''"
and RimpQ: "insertAssertion (extractFrame R) Ψ ↪⇩F insertAssertion (extractFrame Q) Ψ"
and Set: "{(Ψ, P, R) | Ψ P R. ∃Q. (Ψ, P, Q) ∈ Rel ∧ (Ψ, Q, R) ∈ Rel'} ⊆ Rel''"
and C1: "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ Rel' ⟹ (Ψ ⊗ Ψ', P, Q) ∈ Rel'"
shows "Ψ ⊳ P ↝<Rel''> R"
proof -
from Eqvt'' show ?thesis
proof(induct rule: weakSimI[of _ _ _ _ Q])
case(cAct Ψ' α R')
from ‹Ψ ⊳ Q ↝[Rel'] R› ‹Ψ ⊳ R ⟼α ≺ R'› ‹bn α ♯* Ψ› ‹bn α ♯* Q›
obtain Q' where QTrans: "Ψ ⊳ Q ⟼α ≺ Q'" and "(Ψ, Q', R') ∈ Rel'"
by(blast dest: simE)
from ‹(Ψ, Q', R') ∈ Rel'› have Q'RelR': "(Ψ ⊗ Ψ', Q', R') ∈ Rel'" by(rule C1)
from ‹Ψ ⊳ P ↝<Rel> Q› QTrans ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹α ≠ τ›
obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹α ≺ P''" and P''Chain: "Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'"
and P'RelQ': "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
by(blast dest: weakSimE)
from PTrans RimpQ have "Ψ : R ⊳ P ⟹α ≺ P''" by(rule weakTransitionFrameImp)
moreover note P''Chain
moreover from P'RelQ' Q'RelR' Set have "(Ψ ⊗ Ψ', P', R') ∈ Rel''" by blast
ultimately show ?case by blast
next
case(cTau R')
from ‹Ψ ⊳ Q ↝[Rel'] R› ‹Ψ ⊳ R ⟼τ ≺ R'›
obtain Q' where QTrans: "Ψ ⊳ Q ⟼τ ≺ Q'" and Q'RelR': "(Ψ, Q', R') ∈ Rel'"
by(force dest: simE)
from ‹Ψ ⊳ P ↝<Rel> Q› QTrans
obtain P' where PTrans: "Ψ ⊳ P ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
by(blast dest: weakSimE)
note PTrans
moreover from P'RelQ' Q'RelR' Set have "(Ψ, P', R') ∈ Rel''" by blast
ultimately show ?case by blast
qed
qed
lemma quietSim:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
assumes "quiet P"
and "eqvt Rel"
and cQuiet: "⋀P. quiet P ⟹ (Ψ, 𝟬, P) ∈ Rel"
shows "Ψ ⊳ 𝟬 ↝<Rel> P"
using ‹eqvt Rel›
proof(induct rule: weakSimI[of _ _ _ _ "()"])
case(cAct Ψ' α P')
from ‹Ψ ⊳ P ⟼α ≺ P'› ‹α ≠ τ› have False using ‹quiet P›
by(cases rule: actionCases[where α=α]) (auto intro: quietOutput quietInput)
thus ?case by simp
next
case(cTau P')
from ‹Ψ ⊳ P ⟼τ ≺ P'› ‹quiet P› have "quiet P'"
by(erule_tac quiet.cases) (force simp add: residualInject)
have "Ψ ⊳ P ⟹⇧^⇩τ P" by simp
moreover from ‹quiet P'› have "(Ψ, 𝟬, P') ∈ Rel" by(rule cQuiet)
ultimately show ?case by blast
qed
end
end