Theory Weak_Late_Step_Sim
theory Weak_Late_Step_Sim
imports Weak_Late_Step_Semantics Weak_Late_Sim Strong_Late_Sim
begin
definition weakStepSimAct :: "pi ⇒ residual ⇒ ('a::fs_name) ⇒ (pi × pi) set ⇒ bool" where
"weakStepSimAct P Rs C Rel ≡ (∀Q' a x. Rs = a<νx> ≺ Q' ⟶ x ♯ C ⟶ (∃P' . P ⟹⇩la<νx> ≺ P' ∧ (P', Q') ∈ Rel)) ∧
(∀Q' a x. Rs = a<x> ≺ Q' ⟶ x ♯ C ⟶ (∃P''. ∀u. ∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel)) ∧
(∀Q' α. Rs = α ≺ Q' ⟶ (∃P'. P ⟹⇩lα ≺ P' ∧ (P', Q') ∈ Rel))"
definition weakStepSimAux :: "pi ⇒ (pi × pi) set ⇒ pi ⇒ bool" where
"weakStepSimAux P Rel Q ≡ (∀Q' a x. (Q ⟼a<νx> ≺ Q' ∧ x ♯ P) ⟶ (∃P' . P ⟹⇩la<νx> ≺ P' ∧ (P', Q') ∈ Rel)) ∧
(∀Q' a x. (Q ⟼a<x> ≺ Q' ∧ x ♯ P) ⟶ (∃P''. ∀u. ∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel)) ∧
(∀Q' α. Q ⟼α ≺ Q' ⟶ (∃P'. P ⟹⇩lα ≺ P' ∧ (P', Q') ∈ Rel))"
definition weakStepSim :: "pi ⇒ (pi × pi) set ⇒ pi ⇒ bool" ("_ ↝<_> _" [80, 80, 80] 80) where
"P ↝<Rel> Q ≡ (∀Rs. Q ⟼ Rs ⟶ weakStepSimAct P Rs P Rel)"
lemmas weakStepSimDef = weakStepSimAct_def weakStepSim_def
lemma "weakStepSimAux P Rel Q = weakStepSim P Rel Q"
by(auto simp add: weakStepSimDef weakStepSimAux_def)
lemma monotonic:
fixes A :: "(pi × pi) set"
and B :: "(pi × pi) set"
and P :: pi
and P' :: pi
assumes "P ↝<A> P'"
and "A ⊆ B"
shows "P ↝<B> P'"
using assms
apply(auto simp add: weakStepSimDef)
apply blast
apply(erule_tac x="a<x> ≺ Q'" in allE)
apply(clarsimp)
apply(rotate_tac 4)
apply(erule_tac x=Q' in allE)
apply(erule_tac x=a in allE)
apply(erule_tac x=x in allE)
by blast+
lemma simCasesCont[consumes 1, case_names Bound Input Free]:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
and C :: "'a::fs_name"
assumes Eqvt: "eqvt Rel"
and Bound: "⋀Q' a x. ⟦x ♯ C; Q ⟼a<νx> ≺ Q'⟧ ⟹ ∃P'. P ⟹⇩la<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and Input: "⋀Q' a x. ⟦x ♯ C; Q ⟼a<x> ≺ Q'⟧ ⟹ ∃P''. ∀u. ∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
and Free: "⋀Q' α. Q ⟼ α ≺ Q' ⟹ (∃P'. P ⟹⇩l α ≺ P' ∧ (P', Q') ∈ Rel)"
shows "P ↝<Rel> Q"
using Free
proof(auto simp add: weakStepSimDef)
fix Q' a x
assume xFreshP: "(x::name) ♯ P"
assume Trans: "Q ⟼ a<νx> ≺ Q'"
have "∃c::name. c ♯ (P, Q', x, C)" by(blast intro: name_exists_fresh)
then obtain c::name where cFreshP: "c ♯ P" and cFreshQ': "c ♯ Q'" and cFreshC: "c ♯ C"
and cineqx: "c ≠ x"
by(force simp add: fresh_prod)
from Trans cFreshQ' have "Q ⟼ a<νc> ≺ ([(x, c)] ∙ Q')" by(simp add: alphaBoundResidual)
with cFreshC have "∃P'. P ⟹⇩l a<νc> ≺ P' ∧ (P', [(x, c)] ∙ Q') ∈ Rel"
by(rule Bound)
then obtain P' where PTrans: "P ⟹⇩l a<νc> ≺ P'" and P'RelQ': "(P', [(x, c)] ∙ Q') ∈ Rel"
by blast
from PTrans xFreshP cineqx have xFreshP': "x ♯ P'" by(force dest: Weak_Late_Step_Semantics.freshTransition)
with PTrans have "P ⟹⇩l a<νx> ≺ ([(x, c)] ∙ P')" by(simp add: alphaBoundResidual name_swap)
moreover have "([(x, c)] ∙ P', Q') ∈ Rel" (is "?goal")
proof -
from Eqvt P'RelQ' have "([(x, c)] ∙ P', [(x, c)] ∙ [(x, c)] ∙ Q') ∈ Rel"
by(rule eqvtRelI)
with cineqx show ?goal by(simp add: name_calc)
qed
ultimately show "∃P'. P ⟹⇩la<νx> ≺ P' ∧ (P', Q') ∈ Rel" by blast
next
fix Q' a x u
assume QTrans: "Q ⟼a<x> ≺ (Q'::pi)"
and xFreshP: "x ♯ P"
have "∃c::name. c ♯ (P, Q', C, x)" by(blast intro: name_exists_fresh)
then obtain c::name where cFreshP: "c ♯ P" and cFreshQ': "c ♯ Q'" and cFreshC: "c ♯ C"
and cineqx: "c ≠ x"
by(force simp add: fresh_prod)
from QTrans cFreshQ' have "Q ⟼a<c> ≺ ([(x, c)] ∙ Q')" by(simp add: alphaBoundResidual)
with cFreshC have "∃P''. ∀u. ∃P'. P ⟹⇩lu in P''→a<c> ≺ P' ∧ (P', ([(x, c)] ∙ Q')[c::=u]) ∈ Rel"
by(rule Input)
then obtain P'' where L1: "∀u. ∃P'. P ⟹⇩lu in P''→a<c> ≺ P' ∧ (P', ([(x, c)] ∙ Q')[c::=u]) ∈ Rel" by blast
have "∀u. ∃P'. P ⟹⇩lu in ([(c, x)] ∙ P'')→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
proof(auto)
fix u
from L1 obtain P' where PTrans: "P ⟹⇩lu in P''→a<c> ≺ P'" and P'RelQ': "(P', ([(x, c)] ∙ Q')[c::=u]) ∈ Rel"
by blast
from PTrans xFreshP have "P ⟹⇩lu in ([(c, x)] ∙ P'')→a<x> ≺ P'" by(rule alphaInput)
moreover from P'RelQ' cFreshQ' have "(P', Q'[x::=u]) ∈ Rel" by(simp add: renaming[THEN sym] name_swap)
ultimately show "∃P'. P ⟹⇩lu in ([(c, x)] ∙ P'')→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by blast
qed
thus "∃P''. ∀u. ∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by blast
qed
lemma simCases[consumes 0, case_names Bound Input Free]:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
and C :: "'a::fs_name"
assumes Bound: "⋀Q' a x. ⟦Q ⟼a<νx> ≺ Q'; x ♯ P⟧ ⟹ ∃P'. P ⟹⇩la<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and Input: "⋀Q' a x. ⟦Q ⟼a<x> ≺ Q'; x ♯ P⟧ ⟹ ∃P''. ∀u. ∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
and Free: "⋀Q' α. Q ⟼ α ≺ Q' ⟹ (∃P'. P ⟹⇩l α ≺ P' ∧ (P', Q') ∈ Rel)"
shows "P ↝<Rel> Q"
using assms
by(auto simp add: weakStepSimDef)
lemma simActBoundCases[consumes 1, case_names Input BoundOutput]:
fixes P :: pi
and a :: subject
and x :: name
and Q' :: pi
and C :: "'a::fs_name"
and Rel :: "(pi × pi) set"
assumes EqvtRel: "eqvt Rel"
and DerInput: "⋀b. a = InputS b ⟹ (∃P''. ∀u. ∃P'. (P ⟹⇩lu in P''→b<x> ≺ P') ∧ (P', Q'[x::=u]) ∈ Rel)"
and DerBoundOutput: "⋀b. a = BoundOutputS b ⟹ (∃P'. (P ⟹⇩lb<νx> ≺ P') ∧ (P', Q') ∈ Rel)"
shows "weakStepSimAct P (a«x» ≺ Q') P Rel"
proof(simp add: weakStepSimAct_def fresh_prod, auto)
fix Q'' b y
assume Eq: "a«x» ≺ Q' = b<νy> ≺ Q''"
assume yFreshP: "y ♯ P"
from Eq have "a = BoundOutputS b" by(simp add: residual.inject)
from yFreshP DerBoundOutput[OF this] Eq show "∃P'. P ⟹⇩lb<νy> ≺ P' ∧ (P', Q'') ∈ Rel"
proof(cases "x=y", auto simp add: residual.inject name_abs_eq)
fix P'
assume PTrans: "P ⟹⇩lb<νx> ≺ P'"
assume P'RelQ': "(P', ([(x, y)] ∙ Q'')) ∈ Rel"
assume xineqy: "x ≠ y"
with PTrans yFreshP have yFreshP': "y ♯ P'"
by(force intro: Weak_Late_Step_Semantics.freshTransition)
hence "b<νx> ≺ P' = b<νy> ≺ [(x, y)] ∙ P'" by(rule alphaBoundResidual)
moreover have "([(x, y)] ∙ P', Q'') ∈ Rel"
proof -
from EqvtRel P'RelQ' have "([(x, y)] ∙ P', [(x, y)] ∙ ([(x, y)] ∙ Q''))∈ Rel"
by(rule eqvtRelI)
thus ?thesis by(simp add: name_calc)
qed
ultimately show "∃P'. P ⟹⇩lb<νy> ≺ P' ∧ (P', Q'') ∈ Rel" using PTrans by auto
qed
next
fix Q'' b y u
assume Eq: "a«x» ≺ Q' = b<y> ≺ Q''"
assume yFreshP: "y ♯ P"
from Eq have "a = InputS b" by(simp add: residual.inject)
from DerInput[OF this] obtain P'' where L1: "∀u. ∃P'. P ⟹⇩lu in P''→b<x> ≺ P' ∧
(P', Q'[x::=u]) ∈ Rel"
by blast
have "∀u. ∃P'. P ⟹⇩lu in ([(x, y)] ∙ P'')→b<y> ≺ P' ∧ (P', Q''[y::=u]) ∈ Rel"
proof(rule allI)
fix u
from L1 Eq show "∃P'. P ⟹⇩lu in ([(x, y)] ∙ P'')→b<y> ≺ P' ∧ (P', Q''[y::=u]) ∈ Rel"
proof(cases "x=y", auto simp add: residual.inject name_abs_eq)
assume Der: "∀u. ∃P'. P ⟹⇩lu in P''→b<x> ≺ P' ∧ (P', ([(x, y)] ∙ Q'')[x::=u]) ∈ Rel"
assume xFreshQ'': "x ♯ Q''"
from Der obtain P' where PTrans: "P ⟹⇩lu in P''→b<x> ≺ P'"
and P'RelQ': "(P', ([(x, y)] ∙ Q'')[x::=u]) ∈ Rel"
by force
from PTrans yFreshP have "P ⟹⇩lu in ([(x, y)] ∙ P'')→b<y> ≺ P'" by(rule alphaInput)
moreover from xFreshQ'' P'RelQ' have "(P', Q''[y::=u]) ∈ Rel"
by(simp add: renaming)
ultimately show ?thesis by force
qed
qed
thus "∃P''. ∀u. ∃P'. P ⟹⇩lu in P''→b<y> ≺ P' ∧ (P', Q''[y::=u]) ∈ Rel"
by blast
qed
lemma simActFreeCases[consumes 0, case_names Free]:
fixes P :: pi
and α :: freeRes
and C :: "'a::fs_name"
and Rel :: "(pi × pi) set"
assumes Der: "∃P'. (P ⟹⇩lα ≺ P') ∧ (P', Q') ∈ Rel"
shows "weakStepSimAct P (α ≺ Q') P Rel"
using assms
by(simp add: weakStepSimAct_def residual.inject)
lemma simE:
fixes P :: pi
and Rel :: "(pi × pi) set"
and Q :: pi
and a :: name
and x :: name
and u :: name
and Q' :: pi
assumes "P ↝<Rel> Q"
shows "Q ⟼a<νx> ≺ Q' ⟹ x ♯ P ⟹ ∃P'. P ⟹⇩la<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and "Q ⟼a<x> ≺ Q' ⟹ x ♯ P ⟹ ∃P''. ∀u. ∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
and "Q ⟼α ≺ Q' ⟹ (∃P'. P ⟹⇩lα ≺ P' ∧ (P', Q') ∈ Rel)"
using assms by(simp add: weakStepSimDef)+
lemma weakSimTauChain:
fixes P :: pi
and Rel :: "(pi × pi) set"
and Q :: pi
and Q' :: pi
assumes QChain: "Q ⟹⇩τ Q'"
and PRelQ: "(P, Q) ∈ Rel"
and Sim: "⋀P Q. (P, Q) ∈ Rel ⟹ P ↝<Rel> Q"
shows "∃P'. P ⟹⇩τ P' ∧ (P', Q') ∈ Rel"
proof -
from QChain show ?thesis
proof(induct rule: tauChainInduct)
case id
have "P ⟹⇩τ P" by simp
with PRelQ show ?case by blast
next
case(ih Q' Q'')
have IH: "∃P'. P ⟹⇩τ P' ∧ (P', Q') ∈ Rel" by fact
then obtain P' where PChain: "P ⟹⇩τ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from P'RelQ' have "P' ↝<Rel> Q'" by(rule Sim)
moreover have Q'Trans: "Q' ⟼τ ≺ Q''" by fact
ultimately have "∃P''. P' ⟹⇩lτ ≺ P'' ∧ (P'', Q'') ∈ Rel" by(rule simE)
then obtain P'' where P'Trans: "P' ⟹⇩lτ ≺ P''" and P''RelQ'': "(P'', Q'') ∈ Rel" by blast
from P'Trans have "P' ⟹⇩τ P''" by(rule Weak_Late_Step_Semantics.tauTransitionChain)
with PChain have "P ⟹⇩τ P''" by auto
with P''RelQ'' show ?case by blast
qed
qed
lemma strongSimWeakEqSim:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
assumes PSimQ: "P ↝[Rel] Q"
shows "P ↝<Rel> Q"
proof(auto simp add: weakStepSimDef)
fix Q' a x
assume "Q ⟼a<νx> ≺ Q'" and "x ♯ P"
with PSimQ have "∃P'. P ⟼a<νx> ≺ P' ∧ derivative P' Q' (BoundOutputS a) x Rel"
by(rule Strong_Late_Sim.simE)
then obtain P' where PTrans: "P ⟼a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(force simp add: derivative_def)
from PTrans have "P ⟹⇩la<νx> ≺ P'" by(rule Weak_Late_Step_Semantics.singleActionChain)
thus "∃P'. P ⟹⇩la<νx> ≺ P' ∧ (P', Q') ∈ Rel" using P'RelQ' by blast
next
fix Q' a x u
assume "Q ⟼a<x> ≺ Q'" and "x ♯ P"
with PSimQ have L1: "∃P'. P ⟼a<x> ≺ P' ∧ derivative P' Q' (InputS a) x Rel"
by(blast intro: Strong_Late_Sim.simE)
then obtain P' where PTrans: "P ⟼a<x> ≺ P'" and PDer: "derivative P' Q' (InputS a) x Rel"
by blast
have "∀u. ∃P''. P ⟹⇩lu in P'→a<x> ≺ P'' ∧ (P'', Q'[x::=u]) ∈ Rel"
proof(rule allI)
fix u
from PTrans have "P ⟹⇩lu in P'→a<x> ≺ P'[x::=u]" by(blast intro: Weak_Late_Step_Semantics.singleActionChain)
moreover from PDer have "(P'[x::=u], Q'[x::=u]) ∈ Rel" by(force simp add: derivative_def)
ultimately show "∃P''. P ⟹⇩lu in P'→a<x> ≺ P'' ∧ (P'', Q'[x::=u]) ∈ Rel" by auto
qed
thus "∃P''. ∀u. ∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by blast
next
fix Q' α
assume "Q ⟼α ≺ Q'"
with PSimQ have "∃P'. P ⟼α ≺ P' ∧ (P', Q') ∈ Rel" by(rule Strong_Late_Sim.simE)
then obtain P' where PTrans: "P ⟼α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from PTrans have "P ⟹⇩lα ≺ P'" by(rule Weak_Late_Step_Semantics.singleActionChain)
thus "∃P'. P ⟹⇩lα ≺ P' ∧ (P', Q') ∈ Rel" using P'RelQ' by blast
qed
lemma weakSimWeakEqSim:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
assumes "P ↝<Rel> Q"
shows "P ↝⇧^<Rel> Q"
using assms
by(force simp add: weakStepSimDef simDef weakTransition_def)
lemma eqvtI:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
and perm :: "name prm"
assumes Sim: "P ↝<Rel> Q"
and RelRel': "Rel ⊆ Rel'"
and EqvtRel': "eqvt Rel'"
shows "(perm ∙ P) ↝<Rel'> (perm ∙ Q)"
using EqvtRel'
proof(induct rule: simCasesCont[of _ "perm ∙ P"])
case(Bound Q' a x)
have QTrans: "(perm ∙ Q) ⟼ a<νx> ≺ Q'" by fact
have xFreshP: "x ♯ perm ∙ P" by fact
from QTrans have "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (a<νx> ≺ Q')"
by(rule eqvts)
hence "Q ⟼ (rev perm ∙ a)<ν(rev perm ∙ x)> ≺ (rev perm ∙ Q')"
by(simp add: name_rev_per)
moreover from xFreshP have "(rev perm ∙ x) ♯ P" by(simp add: name_fresh_left)
ultimately obtain P' where PTrans: "P ⟹⇩l (rev perm ∙ a)<ν(rev perm ∙ x)> ≺ P'"
and P'RelQ': "(P', rev perm ∙ Q') ∈ Rel" using Sim
by(blast dest: simE)
from PTrans have "(perm ∙ P) ⟹⇩l perm ∙ ((rev perm ∙ a)<ν(rev perm ∙ x)> ≺ P')"
by(rule Weak_Late_Step_Semantics.eqvtI)
hence "(perm ∙ P) ⟹⇩l a<νx> ≺ (perm ∙ P')" by(simp add: name_per_rev)
moreover have "(perm ∙ P', Q') ∈ Rel'"
proof -
from P'RelQ' RelRel' have "(P', rev perm ∙ Q') ∈ Rel'" by blast
with EqvtRel' have "(perm ∙ P', perm ∙ (rev perm ∙ Q')) ∈ Rel'"
by(rule eqvtRelI)
thus ?thesis by(simp add: name_per_rev)
qed
ultimately show ?case by blast
next
case(Input Q' a x)
have QTrans: "(perm ∙ Q) ⟼a<x> ≺ Q'" by fact
have xFreshP: "x ♯ perm ∙ P" by fact
from QTrans have "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (a<x> ≺ Q')"
by(rule eqvts)
hence "Q ⟼ (rev perm ∙ a)<(rev perm ∙ x)> ≺ (rev perm ∙ Q')"
by(simp add: name_rev_per)
moreover from xFreshP have xFreshP: "(rev perm ∙ x) ♯ P" by(simp add: name_fresh_left)
ultimately obtain P''
where L1: "∀u. ∃P'. P ⟹⇩lu in P''→(rev perm ∙ a)<(rev perm ∙ x)> ≺ P' ∧
(P', (rev perm ∙ Q')[(rev perm ∙ x)::=u]) ∈ Rel" using Sim
by(blast dest: simE)
have "∀u. ∃P'. (perm ∙ P) ⟹⇩lu in (perm ∙ P'')→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'"
proof(rule allI)
fix u
from L1 obtain P' where PTrans: "P ⟹⇩l(rev perm ∙ u) in P''→(rev perm ∙ a)<(rev perm ∙ x)> ≺ P'"
and P'RelQ': "(P', (rev perm ∙ Q')[(rev perm ∙ x)::=(rev perm ∙ u)]) ∈ Rel" by blast
from PTrans have "(perm ∙ P) ⟹⇩l(perm ∙ (rev perm ∙ u)) in (perm ∙ P'')→(perm ∙ rev perm ∙ a)<(perm ∙ rev perm ∙ x)> ≺ (perm ∙ P')"
by(rule_tac Weak_Late_Step_Semantics.eqvtI, auto)
hence "(perm ∙ P) ⟹⇩lu in (perm ∙ P'')→a<x> ≺ (perm ∙ P')" by(simp add: name_per_rev)
moreover have "(perm ∙ P', Q'[x::=u]) ∈ Rel'"
proof -
from P'RelQ' RelRel' have "(P', (rev perm ∙ Q')[(rev perm ∙ x)::=(rev perm ∙ u)]) ∈ Rel'" by blast
with EqvtRel' have "(perm ∙ P', perm ∙ ((rev perm ∙ Q')[(rev perm ∙ x)::=(rev perm ∙ u)])) ∈ Rel'"
by(rule eqvtRelI)
thus ?thesis by(simp add: name_per_rev eqvt_subs[THEN sym] name_calc)
qed
ultimately show "∃P'. (perm ∙ P) ⟹⇩lu in (perm ∙ P'')→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" by blast
qed
thus ?case by blast
next
case(Free Q' α)
have QTrans: "(perm ∙ Q) ⟼ α ≺ Q'" by fact
from QTrans have "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (α ≺ Q')"
by(rule eqvts)
hence "Q ⟼ (rev perm ∙ α) ≺ (rev perm ∙ Q')"
by(simp add: name_rev_per)
with Sim obtain P' where PTrans: "P ⟹⇩l (rev perm ∙ α) ≺ P'" and PRel: "(P', (rev perm ∙ Q')) ∈ Rel"
by(blast dest: simE)
from PTrans have "(perm ∙ P) ⟹⇩l perm ∙ ((rev perm ∙ α)≺ P')"
by(rule Weak_Late_Step_Semantics.eqvtI)
hence "(perm ∙ P) ⟹⇩l α ≺ (perm ∙ P')" by(simp add: name_per_rev)
moreover have "((perm ∙ P'), Q') ∈ Rel'"
proof -
from PRel EqvtRel' RelRel' have "((perm ∙ P'), (perm ∙ (rev perm ∙ Q'))) ∈ Rel'"
by(force intro: eqvtRelI)
thus ?thesis by(simp add: name_per_rev)
qed
ultimately show ?case by blast
qed
lemma simE2:
fixes P :: pi
and Rel :: "(pi × pi) set"
and Q :: pi
and a :: name
and x :: name
and Q' :: pi
assumes PSimQ: "P ↝<Rel> Q"
and Sim: "⋀P Q. (P, Q) ∈ Rel ⟹ P ↝⇧^<Rel> Q"
and Eqvt: "eqvt Rel"
and PRelQ: "(P, Q) ∈ Rel"
shows "Q ⟹⇩la<νx> ≺ Q' ⟹ x ♯ P ⟹ ∃P'. P ⟹⇩la<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and "Q ⟹⇩lα ≺ Q' ⟹ ∃P'. P ⟹⇩lα ≺ P' ∧ (P', Q') ∈ Rel"
proof -
assume QTrans: "Q ⟹⇩la<νx> ≺ Q'"
assume xFreshP: "x ♯ P"
have Goal: "⋀P Q a x Q'. ⟦P ↝<Rel> Q; Q ⟹⇩la<νx> ≺ Q'; x ♯ P; x ♯ Q; (P, Q) ∈ Rel⟧ ⟹
∃P'. P ⟹⇩la<νx> ≺ P' ∧ (P', Q') ∈ Rel"
proof -
fix P Q a x Q'
assume PSimQ: "P ↝<Rel> Q"
assume QTrans: "Q ⟹⇩la<νx> ≺ Q'"
assume xFreshP: "x ♯ P"
assume xFreshQ: "x ♯ Q"
assume PRelQ: "(P, Q) ∈ Rel"
from QTrans xFreshQ obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼a<νx> ≺ Q'''"
and Q'''Chain: "Q''' ⟹⇩τ Q'"
by(force dest: transitionE simp add: weakTransition_def)
from QChain PRelQ Sim have "∃P''. P ⟹⇩τ P'' ∧ (P'', Q'') ∈ Rel"
by(rule Weak_Late_Sim.weakSimTauChain)
then obtain P'' where PChain: "P ⟹⇩τ P''" and P''RelQ'': "(P'', Q'') ∈ Rel" by blast
from PChain xFreshP have xFreshP'': "x ♯ P''" by(rule freshChain)
from P''RelQ'' have "P'' ↝⇧^<Rel> Q''" by(rule Sim)
hence "∃P'''. P'' ⟹⇩l⇧^a<νx> ≺ P''' ∧ (P''', Q''') ∈ Rel" using Q''Trans xFreshP''
by(rule Weak_Late_Sim.simE)
then obtain P''' where P''Trans: "P'' ⟹⇩la<νx> ≺ P'''" and P'''RelQ''': "(P''', Q''') ∈ Rel"
by(force simp add: weakTransition_def)
have "∃P'. P''' ⟹⇩τ P' ∧ (P', Q') ∈ Rel" using Q'''Chain P'''RelQ''' Sim
by(rule Weak_Late_Sim.weakSimTauChain)
then obtain P' where P'''Chain: "P''' ⟹⇩τ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from PChain P''Trans P'''Chain xFreshP'' have "P ⟹⇩la<νx> ≺ P'"
by(blast dest: Weak_Late_Step_Semantics.chainTransitionAppend)
with P'RelQ' show "∃P'. P ⟹⇩l a<νx> ≺ P' ∧ (P', Q') ∈ Rel" by blast
qed
have "∃c::name. c ♯ (Q, Q', P, x)" by(blast intro: name_exists_fresh)
then obtain c::name where cFreshQ: "c ♯ Q" and cFreshQ': "c ♯ Q'" and cFreshP: "c ♯ P"
and xineqc: "x ≠ c"
by(force simp add: fresh_prod)
from QTrans cFreshQ' have "Q ⟹⇩la<νc> ≺ ([(x, c)] ∙ Q')" by(simp add: alphaBoundResidual)
with PSimQ have "∃P'. P ⟹⇩la<νc> ≺ P' ∧ (P', [(x, c)] ∙ Q') ∈ Rel" using cFreshP cFreshQ PRelQ
by(rule Goal)
then obtain P' where PTrans: "P ⟹⇩la<νc> ≺ P'" and P'RelQ': "(P', [(x, c)] ∙ Q') ∈ Rel"
by force
have "P ⟹⇩la<νx> ≺ ([(x, c)] ∙ P')"
proof -
from PTrans xFreshP xineqc have "x ♯ P'" by(rule Weak_Late_Step_Semantics.freshTransition)
with PTrans show ?thesis by(simp add: alphaBoundResidual name_swap)
qed
moreover have "([(x, c)] ∙ P', Q') ∈ Rel"
proof -
from Eqvt P'RelQ' have "([(x, c)] ∙ P', [(x, c)] ∙ [(x, c)] ∙ Q') ∈ Rel"
by(rule eqvtRelI)
thus ?thesis by simp
qed
ultimately show "∃P'. P ⟹⇩l a<νx> ≺ P' ∧ (P', Q') ∈ Rel" by blast
next
assume QTrans: "Q ⟹⇩lα ≺ Q'"
then obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼α ≺ Q'''"
and Q'''Chain: "Q''' ⟹⇩τ Q'"
by(blast dest: transitionE)
thus "∃P'. P ⟹⇩l α ≺ P' ∧ (P', Q') ∈ Rel"
proof(induct arbitrary: α Q''' Q' rule: tauChainInduct)
case(id α Q''')
from PSimQ ‹Q ⟼α ≺ Q'''› have "∃P'. P ⟹⇩lα ≺ P' ∧ (P', Q''') ∈ Rel"
by(blast dest: simE)
then obtain P''' where PTrans: "P ⟹⇩lα ≺ P'''" and P'RelQ''': "(P''', Q''') ∈ Rel"
by blast
have "∃P'. P''' ⟹⇩τ P' ∧ (P', Q') ∈ Rel" using ‹Q''' ⟹⇩τ Q'› P'RelQ''' Sim
by(rule Weak_Late_Sim.weakSimTauChain)
then obtain P' where P'''Chain: "P''' ⟹⇩τ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from P'''Chain PTrans have "P ⟹⇩lα ≺ P'"
by(blast dest: Weak_Late_Step_Semantics.chainTransitionAppend)
with P'RelQ' show ?case by blast
next
case(ih Q'''' Q''' α Q'' Q')
have "Q''' ⟹⇩τ Q'''" by simp
with ‹Q'''' ⟼τ ≺ Q'''› obtain P''' where PTrans: "P ⟹⇩lτ ≺ P'''" and P'''RelQ''': "(P''', Q''') ∈ Rel"
by(drule_tac ih) auto
from P'''RelQ''' ‹Q''' ⟼α ≺ Q''› obtain P'' where
P'''Trans: "P''' ⟹⇩l⇧^α ≺ P''" and P''RelQ'': "(P'', Q'') ∈ Rel"
by(blast dest: Weak_Late_Sim.simE Sim)
from P''RelQ'' ‹Q'' ⟹⇩τ Q'› Sim obtain P' where
P''Chain: "P'' ⟹⇩τ P'" and P'RelQ': "(P', Q')∈ Rel"
by(drule_tac Weak_Late_Sim.weakSimTauChain) auto
from PTrans P'''Trans P''Chain have "P ⟹⇩lα ≺ P'"
apply(auto simp add: weakTransition_def residual.inject)
apply(drule_tac Weak_Late_Step_Semantics.tauTransitionChain, auto)
apply(drule_tac Weak_Late_Step_Semantics.chainTransitionAppend, simp)
apply(rule Weak_Late_Step_Semantics.chainTransitionAppend, auto)
by(drule_tac Weak_Late_Step_Semantics.chainTransitionAppend, auto)
with ‹(P', Q') ∈ Rel› show ?case by blast
qed
qed
lemma reflexive:
fixes P :: pi
and Rel :: "(pi × pi) set"
assumes "Id ⊆ Rel"
shows "P ↝<Rel> P"
using assms
by(auto intro: Weak_Late_Step_Semantics.singleActionChain simp add: weakStepSimDef)
lemma transitive:
fixes P :: pi
and Q :: pi
and R :: pi
and Rel :: "(pi × pi) set"
and Rel' :: "(pi × pi) set"
and Rel'' :: "(pi × pi) set"
assumes PSimQ: "P ↝<Rel> Q"
and QSimR: "Q ↝<Rel'> R"
and Eqvt: "eqvt Rel"
and Eqvt': "eqvt Rel''"
and Trans: "Rel O Rel' ⊆ Rel''"
and Sim: "⋀P Q. (P, Q) ∈ Rel ⟹ P ↝⇧^<Rel> Q"
and PRelQ: "(P, Q) ∈ Rel"
shows "P ↝<Rel''> R"
using Eqvt'
proof(induct rule: simCasesCont[of _ "(P, Q)"])
case(Bound R' a x)
have RTrans: "R ⟼ a<νx> ≺ R'" by fact
have "x ♯ (P, Q)" by fact
hence xFreshP: "x ♯ P" and xFreshQ: "x ♯ Q" by(simp add: fresh_prod)+
from QSimR RTrans xFreshQ obtain Q' where QTrans: "Q ⟹⇩la<νx> ≺ Q'"
and Q'RelR': "(Q', R') ∈ Rel'"
by(blast dest: simE)
from PSimQ Sim Eqvt PRelQ QTrans xFreshP obtain P' where PTrans: "P ⟹⇩la<νx> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE2)
moreover from P'RelQ' Q'RelR' Trans have "(P', R') ∈ Rel''" by blast
ultimately show ?case by blast
next
case(Input R' a x)
have RTrans: "R ⟼ a<x> ≺ R'" by fact
have "x ♯ (P, Q)" by fact
hence xFreshP: "x ♯ P" and xFreshQ: "x ♯ Q" by(simp add: fresh_prod)+
from QSimR RTrans xFreshQ obtain Q''
where "∀u. ∃Q'. Q ⟹⇩lu in Q''→a<x> ≺ Q' ∧ (Q', R'[x::=u]) ∈ Rel'"
by(blast dest: simE)
hence "∃Q'''. Q ⟹⇩τ Q''' ∧ Q'''⟼a<x> ≺ Q'' ∧ (∀u. ∃Q'. Q''[x::=u]⟹⇩τ Q' ∧ (Q', R'[x::=u]) ∈ Rel')"
by(simp add: inputTransition_def, blast)
then obtain Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<x> ≺ Q''"
and L1: "∀u. ∃Q'. Q''[x::=u]⟹⇩τ Q' ∧ (Q', R'[x::=u]) ∈ Rel'"
by blast
from QChain PRelQ Sim obtain P''' where PChain: "P ⟹⇩τ P'''" and P'''RelQ''': "(P''', Q''') ∈ Rel"
by(drule_tac Weak_Late_Sim.weakSimTauChain) auto
from PChain xFreshP have xFreshP''': "x ♯ P'''" by(rule freshChain)
from P'''RelQ''' have "P''' ↝⇧^<Rel> Q'''" by(rule Sim)
with xFreshP''' Q'''Trans obtain P'''' where L2: "∀u. ∃P''. P''' ⟹⇩lu in P''''→a<x> ≺ P'' ∧ (P'', Q''[x::=u]) ∈ Rel"
by(blast dest: Weak_Late_Sim.simE)
have "∀u. ∃P' Q'. P ⟹⇩lu in P''''→a<x> ≺ P' ∧ (P', R'[x::=u]) ∈ Rel''"
proof(rule allI)
fix u
from L1 obtain Q' where Q''Chain: "Q''[x::=u] ⟹⇩τ Q'" and Q'RelR': "(Q', R'[x::=u]) ∈ Rel'"
by blast
from L2 obtain P'' where P'''Trans: "P''' ⟹⇩lu in P''''→a<x> ≺ P''"
and P''RelQ'': "(P'', Q''[x::=u]) ∈ Rel"
by blast
from P''RelQ'' have "P'' ↝⇧^<Rel> Q''[x::=u]" by(rule Sim)
have "∃P'. P'' ⟹⇩τ P' ∧ (P', Q') ∈ Rel" using Q''Chain P''RelQ'' Sim
by(rule Weak_Late_Sim.weakSimTauChain)
then obtain P' where P''Chain: "P'' ⟹⇩τ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from PChain P'''Trans P''Chain have "P ⟹⇩lu in P''''→a<x> ≺ P'"
by(blast dest: Weak_Late_Step_Semantics.chainTransitionAppend)
moreover from P'RelQ' Q'RelR' have "(P', R'[x::=u]) ∈ Rel''" by(insert Trans, auto)
ultimately show "∃P' Q'. P ⟹⇩lu in P''''→a<x> ≺ P' ∧ (P', R'[x::=u]) ∈ Rel''" by blast
qed
thus ?case by force
next
case(Free R' α)
have RTrans: "R ⟼ α ≺ R'" by fact
with QSimR obtain Q' where QTrans: "Q ⟹⇩lα ≺ Q'" and Q'RelR': "(Q', R') ∈ Rel'"
by(blast dest: simE)
from PSimQ Sim Eqvt PRelQ QTrans obtain P' where PTrans: "P ⟹⇩lα ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE2)
from P'RelQ' Q'RelR' Trans have "(P', R') ∈ Rel''" by blast
with PTrans show ?case by blast
qed
end