(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u in P''→a<c> ≺ P' ∧ (P', ([(x, c)] ∙ Q')[c::=u]) ∈ Rel" by(rule Input) then obtain P'' where L1: "∀u. ∃P'. P ⟹⇩_{l}u in P''→a<c> ≺ P' ∧ (P', ([(x, c)] ∙ Q')[c::=u]) ∈ Rel" by blast have "∀u. ∃P'. P ⟹⇩_{l}u in ([(c, x)] ∙ P'')→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" proof(auto) fix u from L1 obtain P' where PTrans: "P ⟹⇩_{l}u in P''→a<c> ≺ P'" and P'RelQ': "(P', ([(x, c)] ∙ Q')[c::=u]) ∈ Rel" by blast from PTrans xFreshP have "P ⟹⇩_{l}u 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 ⟹⇩_{l}u in ([(c, x)] ∙ P'')→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by blast qed thus "∃P''. ∀u. ∃P'. P ⟹⇩_{l}u 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u in P''→b<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by blast have "∀u. ∃P'. P ⟹⇩_{l}u in ([(x, y)] ∙ P'')→b<y> ≺ P' ∧ (P', Q''[y::=u]) ∈ Rel" proof(rule allI) fix u from L1 Eq show "∃P'. P ⟹⇩_{l}u 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 ⟹⇩_{l}u in P''→b<x> ≺ P' ∧ (P', ([(x, y)] ∙ Q'')[x::=u]) ∈ Rel" assume xFreshQ'': "x ♯ Q''" from Der obtain P' where PTrans: "P ⟹⇩_{l}u in P''→b<x> ≺ P'" and P'RelQ': "(P', ([(x, y)] ∙ Q'')[x::=u]) ∈ Rel" by force from PTrans yFreshP have "P ⟹⇩_{l}u 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u 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 tauChainStep: fixes P :: pi and P' :: pi assumes PChain: "P ⟹⇩_{τ}P'" and PineqP': "P ≠ P'" shows "∃P''. P ⟼τ ≺ P'' ∧ P'' ⟹⇩_{τ}P'" proof - from PChain have "(P, P') ∈ Id ∪ (tauActs O tauActs⇧^{*})" by(insert rtrancl_unfold, blast) with PineqP' have "(P, P') ∈ tauActs O tauActs⇧^{*}" by simp hence "(P, P') ∈ tauActs⇧^{*}O tauActs" by(simp add: r_comp_rtrancl_eq) thus ?thesis by(auto simp add: tauActs_def tauChain_def) 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u 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) ⟹⇩_{l}u 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) ⟹⇩_{l}u 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) ⟹⇩_{l}u 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 (*****************Reflexivity and transitivity*********************) 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 ⟹⇩_{l}u 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''' ⟹⇩_{l}u 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''' ⟹⇩_{l}u in P''''→a<x> ≺ P'' ∧ (P'', Q''[x::=u]) ∈ Rel" by blast have "∀u. ∃P' Q'. P ⟹⇩_{l}u 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''' ⟹⇩_{l}u 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u in P'→a<x> ≺ P'' ∧ (P'', Q'[x::=u]) ∈ Rel" proof(rule allI) fix u from PTrans have "P ⟹⇩_{l}u 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 ⟹⇩_{l}u 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 ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by(blast dest: simE) have "∀u. ∃P'. P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', R'[x::=u]) ∈ Rel''" proof(rule allI) fix u from L2 obtain P' where PTrans: "P ⟹⇩_{l}u 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 ⟹⇩_{l}u 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