Theory Tau_Laws_Weak
theory Tau_Laws_Weak
imports Weaken_Bisimulation Weak_Congruence Tau_Sim Tau_Stat_Imp
begin
context weakTauLaws begin
lemma tauLaw1:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ τ.(P) ≈ P"
proof -
let ?X = "{(Ψ, τ.(P), P) | Ψ P. True}" let ?Y = "{(Ψ, P, τ.(P)) | Ψ P. True}"
have "(Ψ, τ.(P), P) ∈ ?X ∪ ?Y" by auto
moreover have "eqvt(?X ∪ ?Y)" by(auto simp add: eqvt_def simp add: eqvts)
ultimately have "Ψ ⊳ τ.(P) ≈⇩w P"
proof(coinduct rule: weakenTransitiveCoinduct)
case(cStatImp Ψ P Q)
show ?case
proof(cases "(Ψ, P, Q) ∈ ?X")
case True
{
fix Ψ P
have "Ψ ⊳ P ⪅⇩w<(?X ∪ ?Y ∪ weakBisim)> P" by(auto simp add: weakenStatImp_def intro: weakBisimReflexive)
moreover have "(Ψ, τ.(P), P) ∈ ?X ∪ ?Y ∪ weakBisim" by auto
ultimately have "Ψ ⊳ τ.(P) ⪅⇩w<(?X ∪ ?Y ∪ weakBisim)> P"
by(rule tauLaw1StatImpLeft)
}
with ‹(Ψ, P, Q) ∈ ?X› show ?thesis by auto
next
case False
from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by auto
{
fix Ψ P
have "Ψ ⊳ P ⪅<weakBisim> P" using weakBisimReflexive
by(rule weakBisimE)
moreover have "⋀Ψ P Q R. ⟦Ψ ⊳ P ≈ Q; Ψ ⊳ Q ∼ R⟧ ⟹ (Ψ, P, R) ∈ ?X ∪ ?Y ∪ weakBisim"
by(fastforce intro: weakBisimTransitive strongBisimWeakBisim)
ultimately have "Ψ ⊳ P ⪅<( ?X ∪ ?Y ∪ weakBisim)> τ.(P)" by(rule tauLaw1StatImpRight)
moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?X ∪ ?Y ∪ weakBisim; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?X ∪ ?Y ∪ weakBisim"
by(auto dest: statEqWeakBisim)
ultimately have "Ψ ⊳ P ⪅⇩w<( ?X ∪ ?Y ∪ weakBisim)> τ.(P)" by(rule weakStatImpWeakenStatImp)
}
with ‹(Ψ, P, Q) ∈ ?Y› show ?thesis by auto
qed
next
case(cSim Ψ P Q)
let ?Z = "{(Ψ, P, Q) | Ψ P Q. ∃P' Q'. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ ?X ∪ ?Y ∪ weakenBisim ∧ Ψ ⊳ Q' ∼ Q}"
have "eqvt ?Z"
apply auto
apply(auto simp add: eqvt_def eqvts)
apply(rule_tac x="(p ∙ (τ.(Q')))" in exI)
apply(auto intro: bisimClosed)
apply(simp add: eqvts)
apply(blast intro: bisimClosed weakBisimClosed)
apply(rule_tac x="(p ∙ P')" in exI)
apply(auto intro: bisimClosed)
apply(rule_tac x="τ.(p ∙ P')" in exI)
apply auto
apply(drule_tac p=p and Q=b in bisimClosed)
apply(simp add: eqvts)
apply(rule_tac x="(p ∙ P')" in exI)
apply(auto intro: bisimClosed)
apply(rule_tac x="p ∙ Q'" in exI)
apply auto
by(blast intro: bisimClosed dest: weakBisimClosed)+
show ?case
proof(cases "(Ψ, P, Q) ∈ ?X")
case True
{
fix P
have "Ψ ⊳ P ↝<?Z> P" using weakenBisimEqWeakBisim by(blast intro: weakSimReflexive weakBisimReflexive bisimReflexive)
moreover note ‹eqvt ?Z›
moreover have "⋀Ψ P Q R. ⟦Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ ?Z⟧ ⟹ (Ψ, P, R) ∈ ?Z"
by(blast intro: bisimTransitive)
ultimately have "Ψ ⊳ τ.(P) ↝<?Z> P"
by(rule tauLaw1SimLeft)
moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?Z"
by simp (blast intro: statEqWeakBisim statEqBisim)
ultimately have "Ψ ⊳ τ.(P) ↝⇩w<?Z> P" by(rule weakSimWeakenSim)
}
with ‹(Ψ, P, Q) ∈ ?X› show ?thesis by auto
next
case False
from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by auto
moreover {
fix P
note ‹eqvt ?Z›
moreover have "(Ψ, P, P) ∈ ?Z" by simp (blast intro: weakBisimReflexive bisimReflexive)
moreover have "⋀Ψ P Q R. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ⊳ Q ∼ R⟧ ⟹ (Ψ, P, R) ∈ ?Z"
by(blast intro: bisimTransitive)
ultimately have "Ψ ⊳ P ↝<?Z> τ.(P)" by(rule tauLaw1SimRight)
moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?Z"
by simp (blast intro: statEqWeakBisim statEqBisim)
ultimately have "Ψ ⊳ P ↝⇩w<?Z> τ.(P)" by(rule weakSimWeakenSim)
}
ultimately show ?thesis by auto
qed
next
case(cExt Ψ P Q Ψ')
thus ?case by auto
next
case(cSym Ψ P Q)
thus ?case by auto
qed
thus ?thesis by simp
qed
lemma tauLaw3:
fixes Ψ :: 'b
and α :: "'a prefix"
and P :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ α⋅(τ.(P)) ≈ α⋅P"
proof -
let ?X = "({(Ψ, α⋅(τ.(P)), α⋅P) | Ψ α P. True})"
let ?Y = "({(Ψ, α⋅P, α⋅(τ.(P))) | Ψ α P. True})"
have "(Ψ, α⋅(τ.(P)), α⋅P) ∈ ?X ∪ ?Y" by blast
moreover have "eqvt(?X ∪ ?Y)" by(fastforce simp add: eqvt_def simp add: eqvts)
ultimately have "Ψ ⊳ α⋅(τ.(P)) ≈⇩w α⋅P"
proof(coinduct rule: weakenTransitiveCoinduct)
case(cStatImp Ψ P Q)
show ?case
proof(cases "(Ψ, P, Q) ∈ ?X")
case True
{
fix Ψ α P
have "⋀Ψ'. (Ψ ⊗ Ψ', α⋅(τ.(P)), α⋅P) ∈ ?X ∪ ?Y ∪ weakenBisim" by auto
hence "Ψ ⊳ α⋅(τ.(P)) ⪅<(?X ∪ ?Y ∪ weakenBisim)> α⋅P" by(rule tauLaw3StatImpLeft)
moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?X ∪ ?Y ∪ weakenBisim; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?X ∪ ?Y ∪ weakenBisim"
by(fastforce intro: statEqWeakBisim)
ultimately have "Ψ ⊳ α⋅(τ.(P)) ⪅⇩w<(?X ∪ ?Y ∪ weakenBisim)> α⋅P" by(rule weakStatImpWeakenStatImp)
}
with ‹(Ψ, P, Q) ∈ ?X› show ?thesis by blast
next
case False
{
fix Ψ α P
have "⋀Ψ'. (Ψ ⊗ Ψ', α⋅P, α⋅(τ.(P))) ∈ ?X ∪ ?Y ∪ weakenBisim" by auto
hence "Ψ ⊳ α⋅P ⪅<(?X ∪ ?Y ∪ weakenBisim)> α⋅(τ.(P))" by(rule tauLaw3StatImpRight)
moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?X ∪ ?Y ∪ weakenBisim; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?X ∪ ?Y ∪ weakenBisim"
by(fastforce intro: statEqWeakBisim)
ultimately have "Ψ ⊳ α⋅P ⪅⇩w<(?X ∪ ?Y ∪ weakenBisim)> α⋅(τ.(P))" by(rule weakStatImpWeakenStatImp)
}
moreover from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by blast
ultimately show ?thesis by auto
qed
next
case(cSim Ψ P Q)
let ?Z = "{(Ψ, P, Q) | Ψ P Q. ∃P' Q'. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ ?X ∪ ?Y ∪ weakenBisim ∧ Ψ ⊳ Q' ∼ Q}"
have "eqvt ?Z"
apply(clarsimp simp add: eqvt_def)
apply(elim disjE)
apply(rule_tac x="p ∙ P'" in exI)
apply(clarsimp simp add: bisimClosed eqvts)
apply(blast intro: bisimClosed eqvts)
apply(rule_tac x="p ∙ P'" in exI)
apply(clarsimp simp add: bisimClosed eqvts)
apply(rule_tac x="p ∙ (α⋅(τ.(P)))" in exI)
apply(clarsimp simp add: eqvts)
apply(rule conjI)
apply(rule disjI2)
apply(blast intro: bisimClosed eqvts)
apply(drule_tac p=p in bisimClosed)
apply(drule_tac p=p in bisimClosed)
apply(simp add: eqvts)
by(blast dest: bisimClosed weakBisimClosed)
show ?case
proof(cases "(Ψ, P, Q) ∈ ?X")
case True
note ‹(Ψ, P, Q) ∈ ?X›
moreover {
fix Ψ P α
note ‹eqvt ?Z›
moreover have "(Ψ, P, P) ∈ ?Z" using weakenBisimEqWeakBisim by(blast intro: weakBisimReflexive bisimReflexive)
moreover have "⋀xvec Tvec. length xvec = length Tvec ⟹ (Ψ, P[xvec::=Tvec], P[xvec::=Tvec]) ∈ ?Z"
using weakenBisimEqWeakBisim by(blast intro: weakBisimReflexive bisimReflexive)
moreover have "⋀Ψ P Q R S. ⟦Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ ?Z; Ψ ⊳ R ∼ S⟧ ⟹ (Ψ, P, S) ∈ ?Z" by(blast intro: bisimTransitive)
moreover have "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ ?Z ⟹ (Ψ ⊗ Ψ', P, Q) ∈ ?Z" by(blast dest: weakenBisimE(3) bisimE(3))
ultimately have "Ψ ⊳ α⋅(τ.(P)) ↝<?Z> α⋅P" by(rule tauLaw3SimLeft)
moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?Z" by simp (blast dest: statEqWeakBisim statEqBisim)
ultimately have "Ψ ⊳ α⋅(τ.(P)) ↝⇩w<?Z> α⋅P" by(rule weakSimWeakenSim)
}
ultimately show ?thesis by auto
next
case False
from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by blast
moreover {
fix Ψ P α
note ‹eqvt ?Z›
moreover have "⋀Ψ xvec Tvec. length xvec=length Tvec ⟹ (Ψ, P[xvec::=Tvec], τ.(P[xvec::=Tvec])) ∈ ?Z"
by simp (blast intro: weakBisimE(4) bisimReflexive tauLaw1)
moreover have "⋀Ψ P Q R S. ⟦Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ ?Z; Ψ ⊳ R ∼ S⟧ ⟹ (Ψ, P, S) ∈ ?Z" by(blast intro: bisimTransitive)
moreover have "⋀Ψ. (Ψ, P, τ.(P)) ∈ ?Z" by simp (blast intro: weakBisimE(4) bisimReflexive tauLaw1)
ultimately have "Ψ ⊳ α⋅P ↝<?Z> α⋅(τ.(P))" by(rule tauLaw3SimRight)
moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?Z" by simp (blast dest: statEqWeakBisim statEqBisim)
ultimately have "Ψ ⊳ α⋅P ↝⇩w<?Z> α⋅(τ.(P))" by(rule weakSimWeakenSim)
}
ultimately show ?thesis by auto
qed
next
case(cExt Ψ P Q Ψ')
thus ?case by auto
next
case(cSym Ψ P Q)
thus ?case by blast
qed
thus ?thesis by simp
qed
lemma tauLaw3PsiCong:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ α⋅(τ.(P)) ≐ α⋅P"
proof(induct rule: weakPsiCongI)
case cWeakBisim
show ?case by(rule tauLaw3)
next
case cSimLeft
have "Ψ ⊳ P ≈ P" by(rule weakBisimReflexive)
moreover have "⋀Ψ P Q R S. ⟦Ψ ⊳ P ∼ Q; Ψ ⊳ Q ≈ R; Ψ ⊳ R ∼ S⟧ ⟹ Ψ ⊳ P ≈ S"
by(blast intro: weakBisimTransitive strongBisimWeakBisim)
ultimately show ?case using weakBisimE(3) by(rule tauLaw3CongSimLeft)
next
case cSimRight
have "Ψ ⊳ P ≈ P" by(rule weakBisimReflexive)
moreover have "⋀Ψ P Q R S. ⟦Ψ ⊳ P ∼ Q; Ψ ⊳ Q ≈ R; Ψ ⊳ R ∼ S⟧ ⟹ Ψ ⊳ P ≈ S"
by(blast intro: weakBisimTransitive strongBisimWeakBisim)
ultimately show ?case using tauLaw1[THEN weakBisimE(4)]
by(rule tauLaw3CongSimRight)
qed
lemma tauLaw3Cong:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
shows "α⋅(τ.(P)) ≐⇩c α⋅P"
proof(induct rule: weakCongI)
case(cWeakPsiCong Ψ σ)
show ?case
proof(nominal_induct α rule: prefix.strong_inducts)
next
case(pInput M yvec N)
obtain p where "set p ⊆ set yvec × set(p ∙ yvec)" and "(p ∙ yvec) ♯* N" and "(p ∙ yvec) ♯* P" and "(p ∙ yvec) ♯* σ"
by(rule_tac xvec=yvec and c="(N, P, σ)" in name_list_avoiding) auto
thus ?case using ‹wellFormedSubst σ› tauLaw3PsiCong[where α="pInput (substTerm.seqSubst M σ) (p ∙ yvec) (substTerm.seqSubst (p ∙ N) σ)"]
by(simp add: inputChainAlpha' eqvts)
next
case(pOutput M N)
thus ?case using ‹wellFormedSubst σ› tauLaw3PsiCong[where α="pOutput (substTerm.seqSubst M σ) (substTerm.seqSubst N σ)"]
by simp
next
case pTau
thus ?case using ‹wellFormedSubst σ› tauLaw3PsiCong[where α="pTau"]
by simp
qed
qed
end
end