Theory Weak_Late_Sim
theory Weak_Late_Sim
imports Weak_Late_Semantics Strong_Late_Sim
begin
definition weakSimAct :: "pi ⇒ residual ⇒ ('a::fs_name) ⇒ (pi × pi) set ⇒ bool" where
"weakSimAct P Rs C Rel ≡ (∀Q' a x. Rs = a<νx> ≺ Q' ⟶ x ♯ C ⟶ (∃P' . P ⟹⇩l⇧^a<ν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 weakSimAux :: "pi ⇒ (pi × pi) set ⇒ pi ⇒ bool" where
"weakSimAux P Rel Q ≡ (∀Q' a x. (Q ⟼ a<νx> ≺ Q' ∧ x ♯ P) ⟶ (∃P' . P ⟹⇩l⇧^a<ν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 weakSimulation :: "pi ⇒ (pi × pi) set ⇒ pi ⇒ bool" (‹_ ↝⇧^<_> _› [80, 80, 80] 80) where
"P ↝⇧^<Rel> Q ≡ (∀Rs. Q ⟼ Rs ⟶ weakSimAct P Rs P Rel)"
lemmas simDef = weakSimAct_def weakSimulation_def
lemma "weakSimAux P Rel Q = weakSimulation P Rel Q"
by(auto simp add: weakSimAux_def simDef)
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: simDef)
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 ⟹⇩l⇧^a<ν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: simDef)
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: 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 ⟹⇩l⇧^a<ν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[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 ⟹⇩l⇧^a<ν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: simDef)
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 ⟹⇩l⇧^b<νx> ≺ P') ∧ (P', Q') ∈ Rel)"
shows "weakSimAct P (a«x» ≺ Q') P Rel"
proof(simp add: weakSimAct_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 ⟹⇩l⇧^b<νy> ≺ P' ∧ (P', Q'') ∈ Rel"
proof(cases "x=y", auto simp add: residual.inject name_abs_eq)
fix P'
assume PTrans: "P ⟹⇩l⇧^b<νx> ≺ P'"
assume P'RelQ': "(P', ([(x, y)] ∙ Q'')) ∈ Rel"
assume xineqy: "x ≠ y"
with PTrans yFreshP have yFreshP': "y ♯ P'"
by(force intro: 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 ⟹⇩l⇧^b<ν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 Der]:
fixes P :: pi
and α :: freeRes
and Q' :: pi
and Rel :: "(pi × pi) set"
assumes "∃P'. (P ⟹⇩l⇧^α ≺ P') ∧ (P', Q') ∈ Rel"
shows "weakSimAct P (α ≺ Q') P Rel"
using assms
by(simp add: residual.inject weakSimAct_def fresh_prod)
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 ⟹⇩l⇧^a<ν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: simDef)+
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 tauTransitionChain)
with PChain have "P ⟹⇩τ P''" by auto
with P''RelQ'' show ?case by blast
qed
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 ⟹⇩l⇧^a<νx> ≺ Q' ⟹ x ♯ P ⟹ ∃P'. P ⟹⇩l⇧^a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and "Q ⟹⇩l⇧^α ≺ Q' ⟹ ∃P'. P ⟹⇩l⇧^α ≺ P' ∧ (P', Q') ∈ Rel"
proof -
assume QTrans: "Q ⟹⇩l⇧^a<νx> ≺ Q'"
assume xFreshP: "x ♯ P"
have Goal: "⋀P Q a x Q'. ⟦P ↝⇧^<Rel> Q; Q ⟹⇩l⇧^a<νx> ≺ Q'; x ♯ P; x ♯ Q; (P, Q) ∈ Rel⟧ ⟹
∃P'. P ⟹⇩l⇧^a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
proof -
fix P Q a x Q'
assume PSimQ: "P ↝⇧^<Rel> Q"
assume QTrans: "Q ⟹⇩l⇧^a<ν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: Weak_Late_Step_Semantics.transitionE simp add: weakTransition_def)
from QChain PRelQ Sim have "∃P''. P ⟹⇩τ P'' ∧ (P'', Q'') ∈ Rel"
by(rule 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 simE)
then obtain P''' where P''Trans: "P'' ⟹⇩l⇧^a<νx> ≺ P'''" and P'''RelQ''': "(P''', Q''') ∈ Rel"
by blast
from P'''RelQ''' have "P''' ↝⇧^<Rel> Q'''" by(rule Sim)
have "∃P'. P''' ⟹⇩τ P' ∧ (P', Q') ∈ Rel" using Q'''Chain P'''RelQ''' Sim
by(rule 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 ⟹⇩l⇧^a<νx> ≺ P'"
by(blast dest: 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 ⟹⇩l⇧^a<νc> ≺ ([(x, c)] ∙ Q')" by(simp add: alphaBoundResidual)
with PSimQ have "∃P'. P ⟹⇩l⇧^a<νc> ≺ P' ∧ (P', [(x, c)] ∙ Q') ∈ Rel" using cFreshP cFreshQ ‹(P, Q) ∈ Rel›
by(rule Goal)
then obtain P' where PTrans: "P ⟹⇩l⇧^a<νc> ≺ P'" and P'RelQ': "(P', [(x, c)] ∙ Q') ∈ Rel"
by force
have "P ⟹⇩l⇧^a<νx> ≺ ([(x, c)] ∙ P')"
proof -
from PTrans xFreshP xineqc have "x ♯ P'" by(rule 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'"
thus "∃P'. P ⟹⇩l⇧^α ≺ P' ∧ (P', Q') ∈ Rel"
proof(induct rule: transitionCases)
case Step
have "Q ⟹⇩lα ≺ Q'" by fact
then obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼α ≺ Q'''"
and Q'''Chain: "Q''' ⟹⇩τ Q'"
by(blast dest: Weak_Late_Step_Semantics.transitionE)
from QChain PRelQ Sim have "∃P''. P ⟹⇩τ P'' ∧ (P'', Q'') ∈ Rel"
by(rule weakSimTauChain)
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)
hence "∃P'''. P'' ⟹⇩l⇧^α ≺ P''' ∧ (P''', Q''') ∈ Rel" using Q''Trans
by(rule simE)
then obtain P''' where P''Trans: "P'' ⟹⇩l⇧^α ≺ P'''" and P'''RelQ''': "(P''', Q''') ∈ Rel"
by blast
from P'''RelQ''' have "P''' ↝⇧^<Rel> Q'''" by(rule Sim)
have "∃P'. P''' ⟹⇩τ P' ∧ (P', Q') ∈ Rel" using Q'''Chain P'''RelQ''' Sim
by(rule 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 ⟹⇩l⇧^α ≺ P'"
by(blast dest: chainTransitionAppend)
with P'RelQ' show ?case by blast
next
case Stay
have "α ≺ Q' = τ ≺ Q" by fact
hence "Q = Q'" and "α = τ" by(simp add: residual.inject)+
moreover have "P ⟹⇩l⇧^τ ≺ P" by(simp add: weakTransition_def)
ultimately show ?case using PRelQ by blast
qed
qed
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)"
proof -
from EqvtRel' show ?thesis
proof(induct rule: simCasesCont[of _ "(perm ∙ P)"])
case(Bound Q' a x)
have Trans: "(perm ∙ Q) ⟼ a<νx> ≺ Q'" and xFreshP: "x ♯ perm ∙ P" by fact+
from Trans 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 have "∃P'. P ⟹⇩l⇧^ (rev perm ∙ a)<ν(rev perm ∙ x)> ≺ P' ∧ (P', rev perm ∙ Q') ∈ Rel" using Sim
by(force intro: simE)
then obtain P' where PTrans: "P ⟹⇩l⇧^ (rev perm ∙ a)<ν(rev perm ∙ x)> ≺ P'" and P'RelQ': "(P', rev perm ∙ Q') ∈ Rel" by blast
from PTrans have "(perm ∙ P) ⟹⇩l⇧^ perm ∙ ((rev perm ∙ a)<ν(rev perm ∙ x)> ≺ P')"
by(rule Weak_Late_Semantics.eqvtI)
hence L1: "(perm ∙ P) ⟹⇩l⇧^ a<νx> ≺ (perm ∙ P')" by(simp add: name_per_rev)
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)
hence "(perm ∙ P', Q') ∈ Rel'" by(simp add: name_per_rev)
with L1 show ?case by blast
next
case(Input Q' a x)
have Trans: "(perm ∙ Q) ⟼a<x> ≺ Q'" and xFreshP: "x ♯ perm ∙ P" by fact+
from Trans 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 have "∃P''. ∀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(force intro: simE)
then 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"
by blast
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 L2: "(perm ∙ P) ⟹⇩lu in (perm ∙ P'')→a<x> ≺ (perm ∙ P')" by(simp add: name_per_rev)
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)
hence "(perm ∙ P', Q'[x::=u]) ∈ Rel'" by(simp add: name_per_rev eqvt_subs[THEN sym] name_calc)
with L2 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 Trans: "(perm ∙ Q) ⟼ α ≺ Q'" by fact
from Trans 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 have "(∃P'. P ⟹⇩l⇧^ (rev perm ∙ α) ≺ P' ∧ (P', (rev perm ∙ Q')) ∈ Rel)"
by(rule simE)
then obtain P' where PTrans: "P ⟹⇩l⇧^ (rev perm ∙ α) ≺ P'" and PRel: "(P', (rev perm ∙ Q')) ∈ Rel" by blast
from PTrans have "(perm ∙ P) ⟹⇩l⇧^ perm ∙ ((rev perm ∙ α)≺ P')"
by(rule Weak_Late_Semantics.eqvtI)
hence L1: "(perm ∙ P) ⟹⇩l⇧^ α ≺ (perm ∙ P')" by(simp add: name_per_rev)
from PRel EqvtRel' RelRel' have "((perm ∙ P'), (perm ∙ (rev perm ∙ Q'))) ∈ Rel'"
by(force intro: eqvtRelI)
hence "((perm ∙ P'), Q') ∈ Rel'" by(simp add: name_per_rev)
with L1 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: simDef weakTransition_def)
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 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"
proof -
from PRelQ have PSimQ: "P ↝⇧^<Rel> Q" by(rule Sim)
from Eqvt' show ?thesis
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 have "∃Q'. Q ⟹⇩l⇧^a<νx> ≺ Q' ∧ (Q', R') ∈ Rel'"
by(rule simE)
then obtain Q' where QTrans: "Q ⟹⇩l⇧^a<νx> ≺ Q'" and Q'RelR': "(Q', R') ∈ Rel'" by blast
from PSimQ Sim Eqvt PRelQ QTrans xFreshP have "∃P'. P ⟹⇩l⇧^a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
by(rule simE2)
then obtain P' where PTrans: "P ⟹⇩l⇧^a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
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 have "∃P'''. P ⟹⇩τ P''' ∧ (P''', Q''') ∈ Rel"
by(rule 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''''. ∀u. ∃P''. P''' ⟹⇩lu in P''''→a<x> ≺ P'' ∧ (P'', Q''[x::=u]) ∈ Rel" using Q'''Trans xFreshP'''
by(rule simE)
then obtain P'''' where L2: "∀u. ∃P''. P''' ⟹⇩lu in P''''→a<x> ≺ P'' ∧ (P'', Q''[x::=u]) ∈ Rel"
by blast
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 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 have "∃Q'. Q ⟹⇩l⇧^α ≺ Q' ∧ (Q', R') ∈ Rel'" by(rule simE)
then obtain Q' where QTrans: "Q ⟹⇩l⇧^α ≺ Q'" and Q'RelR': "(Q', R') ∈ Rel'" by blast
from PSimQ Sim Eqvt PRelQ QTrans have "∃P'. P ⟹⇩l⇧^α ≺ P' ∧ (P', Q') ∈ Rel" by(rule simE2)
then obtain P' where PTrans: "P ⟹⇩l⇧^α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from P'RelQ' Q'RelR' Trans have "(P', R') ∈ Rel''" by blast
with PTrans show "∃P'. P ⟹⇩l⇧^α ≺ P' ∧ (P', R') ∈ Rel''" by blast
qed
qed
lemma strongSimWeakSim:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
assumes PSimQ: "P ↝[Rel] Q"
shows "P ↝⇧^<Rel> Q"
proof(induct rule: simCases)
case(Bound Q' a x)
have "Q ⟼a<νx> ≺ Q'" and "x ♯ P" by fact+
with PSimQ obtain P' where PTrans: "P ⟼a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(force dest: Strong_Late_Sim.simE simp add: derivative_def)
from PTrans have "P ⟹⇩l⇧^a<νx> ≺ P'"
by(force intro: Weak_Late_Step_Semantics.singleActionChain simp add: weakTransition_def)
with P'RelQ' show ?case by blast
next
case(Input Q' a x)
assume "Q ⟼a<x> ≺ Q'" and "x ♯ P"
with PSimQ obtain P' where PTrans: "P ⟼a<x> ≺ P'" and PDer: "derivative P' Q' (InputS a) x Rel"
by(blast dest: Strong_Late_Sim.simE)
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 ?case by blast
next
case(Free Q' α)
have "Q ⟼α ≺ Q'" by fact
with PSimQ obtain P' where PTrans: "P ⟼α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: Strong_Late_Sim.simE)
from PTrans have "P ⟹⇩l⇧^α ≺ P'" by(rule Weak_Late_Semantics.singleActionChain)
with P'RelQ' show ?case by blast
qed
lemma strongAppend:
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 Trans: "Rel O Rel' ⊆ Rel''"
shows "P ↝⇧^<Rel''> R"
proof -
from Eqvt'' show ?thesis
proof(induct rule: simCasesCont[of _ "(P, Q)"])
case(Bound R' a x)
have "x ♯ (P, Q)" by fact
hence xFreshP: "x ♯ P" and xFreshQ: "x ♯ Q" by(simp add: fresh_prod)+
have RTrans: "R ⟼a<νx> ≺ R'" by fact
from xFreshQ QSimR RTrans obtain Q' where QTrans: "Q ⟼a<νx> ≺ Q'"
and Q'Rel'R': "(Q', R') ∈ Rel'"
by(force dest: Strong_Late_Sim.simE simp add: derivative_def)
with PSimQ QTrans xFreshP have "∃P'. P ⟹⇩l⇧^ a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
by(blast intro: simE)
then obtain P' where PTrans: "P ⟹⇩l⇧^ a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
moreover from P'RelQ' Q'Rel'R' 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 QTrans: "Q ⟼a<x> ≺ Q'" and Q'Der: "derivative Q' R' (InputS a) x Rel'"
by(blast dest: Strong_Late_Sim.simE)
from QTrans PSimQ xFreshP obtain P'' where L2: "∀u. ∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
by(blast dest: simE)
have "∀u. ∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', R'[x::=u]) ∈ Rel''"
proof(rule allI)
fix u
from L2 obtain P' where PTrans: "P ⟹⇩lu in P''→a<x> ≺ P'"
and P'RelQ': "(P', Q'[x::=u]) ∈ Rel"
by blast
moreover from Q'Der have "(Q'[x::=u], R'[x::=u]) ∈ Rel'" by(simp add: derivative_def)
ultimately show "∃P'. P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', R'[x::=u]) ∈ Rel''" using Trans by blast
qed
thus ?case by force
next
case(Free R' α)
have RTrans: "R ⟼ α ≺ R'" by fact
with QSimR obtain Q' where QTrans: "Q ⟼α ≺ Q'" and Q'RelR': "(Q', R') ∈ Rel'"
by(blast dest: Strong_Late_Sim.simE)
from PSimQ QTrans have "∃P'. P ⟹⇩l⇧^ α ≺ P' ∧ (P', Q') ∈ Rel"
by(blast intro: simE)
then obtain P' where PTrans: "P ⟹⇩l⇧^ α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from P'RelQ' Q'RelR' Trans have "(P', R') ∈ Rel''" by blast
with PTrans show ?case by blast
qed
qed
end