(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Strong_Early_Late_Comp imports Strong_Late_Bisim_Subst_SC Strong_Early_Bisim_Subst begin abbreviation TransitionsLate_judge (‹_ ⟼⇩_{l}_› [80, 80] 80) where "P ⟼⇩_{l}Rs ≡ transitions P Rs" abbreviation TransitionsEarly_judge (‹_ ⟼⇩_{e}_› [80, 80] 80) where "P ⟼⇩_{e}Rs ≡ TransitionsEarly P Rs" abbreviation Transitions_InputjudgeLate (‹_<_> ≺⇩_{l}_› [80, 80] 80) where "a<x> ≺⇩_{l}P' ≡ (Late_Semantics.BoundR (Late_Semantics.InputS a) x P')" abbreviation Transitions_OutputjudgeLate (‹_[_] ≺⇩_{l}_› [80, 80] 80) where "a[b] ≺⇩_{l}P' ≡ (Late_Semantics.FreeR (Late_Semantics.OutputR a b) P')" abbreviation Transitions_BoundOutputjudgeLate (‹_<ν_> ≺⇩_{l}_› [80, 80] 80) where "a<νx> ≺⇩_{l}P' ≡ (Late_Semantics.BoundR (Late_Semantics.BoundOutputS a) x P')" abbreviation Transitions_TaujudgeLate (‹τ ≺⇩_{l}_› 80) where "τ ≺⇩_{l}P' ≡ (Late_Semantics.FreeR Late_Semantics.TauR P')" abbreviation Transitions_InputjudgeEarly (‹_<_> ≺⇩_{e}_› [80, 80] 80) where "a<x> ≺⇩_{e}P' ≡ (Early_Semantics.FreeR (Early_Semantics.InputR a x) P')" abbreviation Transitions_OutputjudgeEarly (‹_[_] ≺⇩_{e}_› [80, 80] 80) where "a[b] ≺⇩_{e}P' ≡ (Early_Semantics.FreeR (Early_Semantics.OutputR a b) P')" abbreviation Transitions_BoundOutputjudgeEarly (‹_<ν_> ≺⇩_{e}_› [80, 80] 80) where "a<νx> ≺⇩_{e}P' ≡(Early_Semantics.BoundOutputR a x P')" abbreviation Transitions_TaujudgeEarly (‹τ ≺⇩_{e}_› 80) where "τ ≺⇩_{e}P' ≡ (Early_Semantics.FreeR Early_Semantics.TauR P')" lemma earlyLateOutput: fixes P :: pi and a :: name and b :: name and P' :: pi assumes "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" shows "P ⟼⇩_{l}a[b] ≺⇩_{l}P'" using assms proof(nominal_induct rule: Early_Semantics.outputInduct) case(Output a b P) show ?case by(rule Late_Semantics.Output) next case(Match P a b P' c) have "P ⟼⇩_{l}a[b] ≺⇩_{l}P'" by fact thus ?case by(rule Late_Semantics.Match) next case(Mismatch P a b P' c d) from ‹P ⟼⇩_{l}a[b] ≺⇩_{l}P'› ‹c ≠ d› show ?case by(rule Late_Semantics.Mismatch) next case(Sum1 P a b P' Q) have "P ⟼⇩_{l}a[b] ≺⇩_{l}P'" by fact thus ?case by(rule Late_Semantics.Sum1) next case(Sum2 Q a b Q' P) have "Q ⟼⇩_{l}a[b] ≺⇩_{l}Q'" by fact thus ?case by(rule Late_Semantics.Sum2) next case(Par1 P a b P' Q) have "P ⟼⇩_{l}a[b] ≺⇩_{l}P'" by fact thus ?case by(rule Late_Semantics.Par1F) next case(Par2 Q a b Q' P) have "Q ⟼⇩_{l}a[b] ≺⇩_{l}Q'" by fact thus ?case by(rule Late_Semantics.Par2F) next case(Res P a b P' x) have "P ⟼⇩_{l}a[b] ≺⇩_{l}P'" and "x ≠ a" and "x ≠ b" by fact+ thus ?case by(force intro: Late_Semantics.ResF) next case(Bang P a b P') have "P ∥ !P ⟼⇩_{l}a[b] ≺⇩_{l}P'" by fact thus ?case by(rule Late_Semantics.Bang) qed lemma lateEarlyOutput: fixes P :: pi and a :: name and b :: name and P' :: pi assumes "P ⟼⇩_{l}a[b] ≺⇩_{l}P'" shows "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" using assms proof(nominal_induct rule: Late_Semantics.outputInduct) case(Output a b P) thus ?case by(rule Early_Semantics.Output) next case(Match P a b P' c) have "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" by fact thus ?case by(rule Early_Semantics.Match) next case(Mismatch P a b P' c d) have "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" and "c ≠ d" by fact+ thus ?case by(rule Early_Semantics.Mismatch) next case(Sum1 P a b P' Q) have "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" by fact thus ?case by(rule Early_Semantics.Sum1) next case(Sum2 Q a b Q' P) have "Q ⟼⇩_{e}a[b] ≺⇩_{e}Q'" by fact thus ?case by(rule Early_Semantics.Sum2) next case(Par1 P a b P' Q) have "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" by fact thus ?case by(rule Early_Semantics.Par1F) next case(Par2 Q a b Q' P) have "Q ⟼⇩_{e}a[b] ≺⇩_{e}Q'" by fact thus ?case by(rule Early_Semantics.Par2F) next case(Res P a b P' x) have "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" and "x ≠ a" and "x ≠ b" by fact+ thus ?case by(force intro: Early_Semantics.ResF) next case(Bang P a b P') have "P ∥ !P ⟼⇩_{e}a[b] ≺⇩_{e}P'" by fact thus ?case by(rule Early_Semantics.Bang) qed lemma outputEq: fixes P :: pi and a :: name and b :: name and P' :: pi shows "P ⟼⇩_{e}a[b] ≺⇩_{e}P' = P ⟼⇩_{l}a[b] ≺⇩_{l}P'" by(auto intro: lateEarlyOutput earlyLateOutput) lemma lateEarlyBoundOutput: fixes P :: pi and a :: name and x :: name and P' :: pi assumes "P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" shows "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" proof - have Goal: "⋀P a x P'. ⟦P ⟼⇩_{l}a<νx> ≺⇩_{l}P'; x ♯ P⟧ ⟹ P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" proof - fix P a x P' assume "P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" and "x ♯ P" thus "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" proof(nominal_induct rule: Late_Semantics.boundOutputInduct) case(Match P a x P' b) have "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" by fact thus ?case by(rule Early_Semantics.Match) next case(Mismatch P a x P' b c) have "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" and "b ≠ c" by fact+ thus ?case by(rule Early_Semantics.Mismatch) next case(Open P a x P') have "P ⟼⇩_{l}a[x] ≺⇩_{l}P'" by fact hence "P ⟼⇩_{e}a[x] ≺⇩_{e}P'" by(rule lateEarlyOutput) moreover have "a ≠ x" by fact ultimately show ?case by(rule Early_Semantics.Open) next case(Sum1 P Q a x P') have "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" by fact thus ?case by(rule Early_Semantics.Sum1) next case(Sum2 P Q a x Q') have "Q ⟼⇩_{e}a<νx> ≺⇩_{e}Q'" by fact thus ?case by(rule Early_Semantics.Sum2) next case(Par1 P P' Q a x) have "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" and "x ♯ Q" by fact+ thus ?case by(rule Early_Semantics.Par1B) next case(Par2 P Q Q' a x) have "Q ⟼⇩_{e}a<νx> ≺⇩_{e}Q'" and "x ♯ P" by fact+ thus ?case by(rule Early_Semantics.Par2B) next case(Res P P' a x y) have "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" and "y ≠ a" and "y ≠ x" by fact+ thus ?case by(force intro: Early_Semantics.ResB) next case(Bang P a x P') have "P ∥ !P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" by fact thus ?case by(rule Early_Semantics.Bang) qed qed have "∃c::name. c ♯ (P, P', x)" by(blast intro: name_exists_fresh) then obtain c::name where cFreshP: "c ♯ P" and cFreshP': "c ♯ P'" and "c ≠ x" by(force simp add: fresh_prod) from assms cFreshP' have "P ⟼⇩_{l}a<νc> ≺⇩_{l}([(x, c)] ∙ P')" by(simp add: Late_Semantics.alphaBoundResidual) hence "P ⟼⇩_{e}a<νc> ≺⇩_{e}([(x, c)] ∙ P')" using cFreshP by(rule Goal) moreover from cFreshP' ‹c ≠ x› have "x ♯ [(x, c)] ∙ P'" by(simp add: name_fresh_left name_calc) ultimately show ?thesis by(simp add: Early_Semantics.alphaBoundOutput name_swap) qed lemma earlyLateBoundOutput: fixes P :: pi and a :: name and x :: name and P' :: pi assumes "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" shows "P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" proof - have Goal: "⋀P a x P'. ⟦P ⟼⇩_{e}a<νx> ≺⇩_{e}P'; x ♯ P⟧ ⟹ P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" proof - fix P a x P' assume "P ⟼⇩_{e}a<νx> ≺ P'" and "x ♯ P" thus "P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" proof(nominal_induct rule: Early_Semantics.boundOutputInduct) case(Match P a x P' b) have "P ⟼⇩_{l}a<νx> ≺ P'" by fact thus ?case by(rule Late_Semantics.Match) next case(Mismatch P a x P' b c) have "P ⟼⇩_{l}a<νx> ≺ P'" and "b ≠ c" by fact+ thus ?case by(rule Late_Semantics.Mismatch) next case(Open P a x P') have "P ⟼⇩_{e}a[x] ≺⇩_{e}P'" by fact hence "P ⟼⇩_{l}a[x] ≺⇩_{l}P'" by(rule earlyLateOutput) moreover have "a ≠ x" by fact ultimately show ?case by(rule Late_Semantics.Open) next case(Sum1 P Q a x P') have "P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" by fact thus ?case by(rule Late_Semantics.Sum1) next case(Sum2 P Q a x Q') have "Q ⟼⇩_{l}a<νx> ≺⇩_{l}Q'" by fact thus ?case by(rule Late_Semantics.Sum2) next case(Par1 P P' Q a x) have "P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" and "x ♯ Q" by fact+ thus ?case by(rule Late_Semantics.Par1B) next case(Par2 P Q Q' a x) have "Q ⟼⇩_{l}a<νx> ≺⇩_{l}Q'" and "x ♯ P" by fact+ thus ?case by(rule Late_Semantics.Par2B) next case(Res P P' a x y) have "P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" and "y ≠ a" and "y ≠ x" by fact+ thus ?case by(force intro: Late_Semantics.ResB) next case(Bang P a x P') have "P ∥ !P ⟼⇩_{l}a<νx> ≺ P'" by fact thus ?case by(rule Late_Semantics.Bang) qed qed have "∃c::name. c ♯ (P, P', x)" by(blast intro: name_exists_fresh) then obtain c::name where cFreshP: "c ♯ P" and cFreshP': "c ♯ P'" and "c ≠ x" by(force simp add: fresh_prod) from assms cFreshP' have "P ⟼⇩_{e}a<νc> ≺⇩_{e}([(x, c)] ∙ P')" by(simp add: Early_Semantics.alphaBoundOutput) hence "P ⟼⇩_{l}a<νc> ≺⇩_{l}([(x, c)] ∙ P')" using cFreshP by(rule Goal) moreover from cFreshP' ‹c ≠ x› have "x ♯ [(x, c)] ∙ P'" by(simp add: name_fresh_left name_calc) ultimately show ?thesis by(simp add: Late_Semantics.alphaBoundResidual name_swap) qed lemma BoundOutputEq: fixes P :: pi and a :: name and x :: name and P' :: pi shows "P ⟼⇩_{e}a<νx> ≺⇩_{e}P' = P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" by(auto intro: earlyLateBoundOutput lateEarlyBoundOutput) lemma lateEarlyInput: fixes P :: pi and a :: name and x :: name and P' :: pi and u :: name assumes PTrans: "P ⟼⇩_{l}a<x> ≺⇩_{l}P'" shows "P ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u])" proof - have Goal: "⋀P a x P' u. ⟦P ⟼⇩_{l}a<x> ≺⇩_{l}P'; x ♯ P⟧ ⟹ P ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u])" proof - fix P a x P' u assume "P ⟼⇩_{l}a<x> ≺⇩_{l}P'" and "x ♯ P" thus "P ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u])" proof(nominal_induct avoiding: u rule: Late_Semantics.inputInduct) case(Input a x P) thus ?case by(rule Early_Semantics.Input) next case(Match P a x P' b u) have "P ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u])" by fact thus ?case by(rule Early_Semantics.Match) next case(Mismatch P a x P' b c u) have "P ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u])" by fact moreover have "b≠c" by fact ultimately show ?case by(rule Early_Semantics.Mismatch) next case(Sum1 P Q a x P') have "P ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u])" by fact thus ?case by(rule Early_Semantics.Sum1) next case(Sum2 P Q a x Q') have "Q ⟼⇩_{e}a<u> ≺⇩_{e}(Q'[x::=u])" by fact thus ?case by(rule Early_Semantics.Sum2) next case(Par1 P P' Q a x) have "P ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u])" by fact hence "P ∥ Q ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u] ∥ Q)" by(rule Early_Semantics.Par1F) moreover have "x ♯ Q" by fact ultimately show ?case by(simp add: forget) next case(Par2 P Q Q' a x) have "Q ⟼⇩_{e}a<u> ≺⇩_{e}(Q'[x::=u])" by fact hence "P ∥ Q ⟼⇩_{e}a<u> ≺⇩_{e}(P ∥ Q'[x::=u])" by(rule Early_Semantics.Par2F) moreover have "x ♯ P" by fact ultimately show ?case by(simp add: forget) next case(Res P P' a x y u) have "P ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u])" and "y ≠ a" and yinequ: "y ♯ u" by fact+ hence "<νy>P ⟼⇩_{e}a<u> ≺⇩_{e}<νy>(P'[x::=u])" by(force intro: Early_Semantics.ResF) moreover have "y ≠ x" by fact ultimately show ?case using yinequ by simp next case(Bang P a x P' u) have "P ∥ !P ⟼⇩_{e}a<u> ≺⇩_{e}(P'[x::=u])" by fact thus ?case by(rule Early_Semantics.Bang) qed qed have "∃c::name. c ♯ (P, P')" by(blast intro: name_exists_fresh) then obtain c::name where cFreshP: "c ♯ P" and cFreshP': "c ♯ P'" by(force simp add: fresh_prod) from assms cFreshP' have "P ⟼⇩_{l}a<c> ≺⇩_{l}([(x, c)] ∙ P')" by(simp add: Late_Semantics.alphaBoundResidual) hence "P ⟼⇩_{e}a<u> ≺⇩_{e}([(x, c)] ∙ P')[c::=u]" using cFreshP by(rule Goal) with cFreshP' show ?thesis by(simp add: renaming name_swap) qed lemma earlyLateInput: fixes P :: pi and a :: name and x :: name and P' :: pi and u :: name and C :: "'a::fs_name" assumes "P ⟼⇩_{e}a<u> ≺⇩_{e}P'" and "x ♯ P" shows "∃P''. P ⟼⇩_{l}a<x> ≺⇩_{l}P'' ∧ P' = P''[x::=u]" proof - { fix P a u P' assume "P ⟼⇩_{e}a<u> ≺⇩_{e}P'" hence "∃P'' x. P ⟼⇩_{l}a<x> ≺⇩_{l}P'' ∧ P' = P''[x::=u]" proof(nominal_induct rule: Early_Semantics.inputInduct) case(cInput a x P u) have "a<x>.P ⟼⇩_{l}a<x> ≺ P" by(rule Late_Semantics.Input) thus ?case by blast next case(cMatch P a u P' b) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast from PTrans have "[b⌢b]P ⟼⇩_{l}a<x> ≺ P''" by(rule Late_Semantics.Match) with P'eqP'' show ?case by blast next case(cMismatch P a u P' b c) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast have "b ≠ c" by fact with PTrans have "[b≠c]P ⟼⇩_{l}a<x> ≺ P''" by(rule Late_Semantics.Mismatch) with P'eqP'' show ?case by blast next case(cSum1 P a u P' Q) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast from PTrans have "P ⊕ Q ⟼⇩_{l}a<x> ≺ P''" by(rule Late_Semantics.Sum1) with P'eqP'' show ?case by blast next case(cSum2 Q a u Q' P) have "∃Q'' x. Q ⟼⇩_{l}a<x> ≺ Q'' ∧ Q' = Q''[x::=u]" by fact then obtain Q'' x where QTrans: "Q ⟼⇩_{l}a<x> ≺ Q''" and Q'eqQ'': "Q' = Q''[x::=u]" by blast from QTrans have "P ⊕ Q ⟼⇩_{l}a<x> ≺ Q''" by(rule Late_Semantics.Sum2) with Q'eqQ'' show ?case by blast next case(cPar1 P a u P' Q) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast have "∃c::name. c ♯ (Q, P'')" by(blast intro: name_exists_fresh) then obtain c::name where cFreshQ: "c ♯ Q" and cFreshP'': "c ♯ P''" by(force simp add: fresh_prod) from PTrans cFreshP'' have "P ⟼⇩_{l}a<c> ≺ [(x, c)] ∙ P''" by(simp add: Late_Semantics.alphaBoundResidual) hence "P ∥ Q ⟼⇩_{l}a<c> ≺ ([(x, c)] ∙ P'') ∥ Q" using ‹c ♯ Q› by(rule Late_Semantics.Par1B) moreover from cFreshQ cFreshP'' P'eqP'' have "P' ∥ Q = (([(x, c)] ∙ P'') ∥ Q)[c::=u]" by(simp add: forget renaming name_swap) ultimately show ?case by blast next case(cPar2 Q a u Q' P) have "∃Q'' x. Q ⟼⇩_{l}a<x> ≺ Q'' ∧ Q' = Q''[x::=u]" by fact then obtain Q'' x where QTrans: "Q ⟼⇩_{l}a<x> ≺ Q''" and Q'eqQ'': "Q' = Q''[x::=u]" by blast have "∃c::name. c ♯ (P, Q'')" by(blast intro: name_exists_fresh) then obtain c::name where cFreshP: "c ♯ P" and cFreshQ'': "c ♯ Q''" by(force simp add: fresh_prod) from QTrans cFreshQ'' have "Q ⟼⇩_{l}a<c> ≺ [(x, c)] ∙ Q''" by(simp add: Late_Semantics.alphaBoundResidual) hence "P ∥ Q ⟼⇩_{l}a<c> ≺ P ∥ ([(x, c)] ∙ Q'')" using ‹c ♯ P› by(rule Late_Semantics.Par2B) moreover from cFreshP cFreshQ'' Q'eqQ'' have "P ∥ Q' = (P ∥ ([(x, c)] ∙ Q''))[c::=u]" by(simp add: forget renaming name_swap) ultimately show ?case by blast next case(cRes P a u P' y) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast have yinequ: "y ≠ u" by fact have "∃c::name. c ♯ (y, P'')" by(blast intro: name_exists_fresh) then obtain c::name where cineqy: "c ≠ y" and cFreshP'': "c ♯ P''" by(force simp add: fresh_prod) from PTrans cFreshP'' have "P ⟼⇩_{l}a<c> ≺ [(x, c)] ∙ P''" by(simp add: Late_Semantics.alphaBoundResidual) moreover have "y ≠ a" by fact ultimately have "<νy>P ⟼⇩_{l}a<c> ≺ <νy>(([(x, c)] ∙ P''))" using cineqy by(force intro: Late_Semantics.ResB) moreover from cineqy cFreshP'' P'eqP'' yinequ have "<νy>P' = (<νy>([(x, c)] ∙ P''))[c::=u]" by(simp add: renaming name_swap) ultimately show ?case by blast next case(cBang P a u P') have "∃P'' x. P ∥ !P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ∥ !P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast from PTrans have "!P ⟼⇩_{l}a<x> ≺ P''" by(rule Late_Semantics.Bang) with P'eqP'' show ?case by blast qed } with assms obtain P'' y where PTrans: "P ⟼⇩_{l}a<y> ≺ P''" and P'eqP'': "P' = P''[y::=u]" by blast show ?thesis proof(cases "x=y") case True from PTrans P'eqP'' ‹x = y› show ?thesis by blast next case False from PTrans ‹x ≠ y› ‹x ♯ P› have "x ♯ P''" by(fastforce dest: freshBoundDerivative simp add: residual.inject) with PTrans have "P ⟼⇩_{l}a<x> ≺⇩_{l}([(x, y)] ∙ P'')" by(simp add: Late_Semantics.alphaBoundResidual) moreover from ‹x ♯ P''› have "P''[y::=u] = ([(x, y)] ∙ P'')[x::=u]" by(simp add: renaming name_swap) ultimately show ?thesis using P'eqP'' by blast qed qed (* lemma earlyLateInput: fixes P :: pi and a :: name and x :: name and P' :: pi and u :: name and C :: "'a::fs_name" assumes PTrans: "P ⟼⇩_{e}a<u> ≺⇩_{e}P'" shows "∃P'' x. P ⟼⇩_{l}a<x> ≺⇩_{l}P'' ∧ P' = P''[x::=u] ∧ x ♯ C" proof - have "⋀P a u P'. P ⟼⇩_{e}a<u> ≺⇩_{e}P' ⟹ ∃P'' x. P ⟼⇩_{l}a<x> ≺⇩_{l}P'' ∧ P' = P''[x::=u]" proof - fix P a u P' assume "P ⟼⇩_{e}a<u> ≺⇩_{e}P'" thus "∃P'' x. P ⟼⇩_{l}a<x> ≺⇩_{l}P'' ∧ P' = P''[x::=u]" proof(nominal_induct rule: Early_Semantics.inputInduct) case(cInput a x P u) have "a<x>.P ⟼⇩_{l}a<x> ≺ P" by(rule Late_Semantics.Input) thus ?case by blast next case(cMatch P a u P' b) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast from PTrans have "[b⌢b]P ⟼⇩_{l}a<x> ≺ P''" by(rule Late_Semantics.Match) with P'eqP'' show ?case by blast next case(cMismatch P a u P' b c) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast have "b ≠ c" by fact with PTrans have "[b≠c]P ⟼⇩_{l}a<x> ≺ P''" by(rule Late_Semantics.Mismatch) with P'eqP'' show ?case by blast next case(cSum1 P a u P' Q) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast from PTrans have "P ⊕ Q ⟼⇩_{l}a<x> ≺ P''" by(rule Late_Semantics.Sum1) with P'eqP'' show ?case by blast next case(cSum2 Q a u Q' P) have "∃Q'' x. Q ⟼⇩_{l}a<x> ≺ Q'' ∧ Q' = Q''[x::=u]" by fact then obtain Q'' x where QTrans: "Q ⟼⇩_{l}a<x> ≺ Q''" and Q'eqQ'': "Q' = Q''[x::=u]" by blast from QTrans have "P ⊕ Q ⟼⇩_{l}a<x> ≺ Q''" by(rule Late_Semantics.Sum2) with Q'eqQ'' show ?case by blast next case(cPar1 P a u P' Q) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast have "∃c::name. c ♯ (Q, P'')" by(blast intro: name_exists_fresh) then obtain c::name where cFreshQ: "c ♯ Q" and cFreshP'': "c ♯ P''" by(force simp add: fresh_prod) from PTrans cFreshP'' have "P ⟼⇩_{l}a<c> ≺ [(x, c)] ∙ P''" by(simp add: Late_Semantics.alphaBoundResidual) hence "P ∥ Q ⟼⇩_{l}a<c> ≺ ([(x, c)] ∙ P'') ∥ Q" using `c ♯ Q` by(rule Late_Semantics.Par1B) moreover from cFreshQ cFreshP'' P'eqP'' have "P' ∥ Q = (([(x, c)] ∙ P'') ∥ Q)[c::=u]" by(simp add: forget renaming name_swap) ultimately show ?case by blast next case(cPar2 Q a u Q' P) have "∃Q'' x. Q ⟼⇩_{l}a<x> ≺ Q'' ∧ Q' = Q''[x::=u]" by fact then obtain Q'' x where QTrans: "Q ⟼⇩_{l}a<x> ≺ Q''" and Q'eqQ'': "Q' = Q''[x::=u]" by blast have "∃c::name. c ♯ (P, Q'')" by(blast intro: name_exists_fresh) then obtain c::name where cFreshP: "c ♯ P" and cFreshQ'': "c ♯ Q''" by(force simp add: fresh_prod) from QTrans cFreshQ'' have "Q ⟼⇩_{l}a<c> ≺ [(x, c)] ∙ Q''" by(simp add: Late_Semantics.alphaBoundResidual) hence "P ∥ Q ⟼⇩_{l}a<c> ≺ P ∥ ([(x, c)] ∙ Q'')" using `c ♯ P` by(rule Late_Semantics.Par2B) moreover from cFreshP cFreshQ'' Q'eqQ'' have "P ∥ Q' = (P ∥ ([(x, c)] ∙ Q''))[c::=u]" by(simp add: forget renaming name_swap) ultimately show ?case by blast next case(cRes P a u P' y) have "∃P'' x. P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast have yinequ: "y ≠ u" by fact have "∃c::name. c ♯ (y, P'')" by(blast intro: name_exists_fresh) then obtain c::name where cineqy: "c ≠ y" and cFreshP'': "c ♯ P''" by(force simp add: fresh_prod) from PTrans cFreshP'' have "P ⟼⇩_{l}a<c> ≺ [(x, c)] ∙ P''" by(simp add: Late_Semantics.alphaBoundResidual) moreover have "y ≠ a" by fact ultimately have "<νy>P ⟼⇩_{l}a<c> ≺ <νy>(([(x, c)] ∙ P''))" using cineqy by(force intro: Late_Semantics.ResB) moreover from cineqy cFreshP'' P'eqP'' yinequ have "<νy>P' = (<νy>([(x, c)] ∙ P''))[c::=u]" by(simp add: renaming name_swap) ultimately show ?case by blast next case(cBang P a u P') have "∃P'' x. P ∥ !P ⟼⇩_{l}a<x> ≺ P'' ∧ P' = P''[x::=u]" by fact then obtain P'' x where PTrans: "P ∥ !P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast from PTrans have "!P ⟼⇩_{l}a<x> ≺ P''" by(rule Late_Semantics.Bang) with P'eqP'' show ?case by blast qed qed with PTrans obtain P'' x where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast have "∃c::name. c ♯ (P'', C)" by(blast intro: name_exists_fresh) then obtain c::name where cFreshP'': "c ♯ P''" and cFreshC: "c ♯ C" by force from cFreshP'' PTrans have "P ⟼⇩_{l}a<c> ≺⇩_{l}([(x, c)] ∙ P'')" by(simp add: Late_Semantics.alphaBoundResidual) moreover from cFreshP'' have "P''[x::=u] = ([(x, c)] ∙ P'')[c::=u]" by(simp add: renaming name_swap) ultimately show ?thesis using P'eqP'' cFreshC by blast qed *) lemma lateEarlyTau: fixes P :: pi and P' :: pi assumes "P ⟼⇩_{l}τ ≺⇩_{l}P'" shows "P ⟼⇩_{e}τ ≺⇩_{e}P'" using assms proof(nominal_induct rule: Late_Semantics.tauInduct) case(Tau P) thus ?case by(rule Early_Semantics.Tau) next case(Match P P' a) have "P ⟼⇩_{e}τ ≺⇩_{e}P'" by fact thus "[a⌢a]P ⟼⇩_{e}τ ≺⇩_{e}P'" by(rule Early_Semantics.Match) next case(Mismatch P P' a b) have "P ⟼⇩_{e}τ ≺⇩_{e}P'" by fact moreover have "a ≠ b" by fact ultimately show "[a≠b]P ⟼⇩_{e}τ ≺⇩_{e}P'" by(rule Early_Semantics.Mismatch) next case(Sum1 P P' Q) have "P ⟼⇩_{e}τ ≺⇩_{e}P'" by fact thus "P ⊕ Q ⟼⇩_{e}τ ≺⇩_{e}P'" by(rule Early_Semantics.Sum1) next case(Sum2 Q Q' P) have "Q ⟼⇩_{e}τ ≺⇩_{e}Q'" by fact thus "P ⊕ Q ⟼⇩_{e}τ ≺⇩_{e}Q'" by(rule Early_Semantics.Sum2) next case(Par1 P P' Q) have "P ⟼⇩_{e}τ ≺⇩_{e}P'" by fact thus "P ∥ Q ⟼⇩_{e}τ ≺⇩_{e}P' ∥ Q" by(rule Early_Semantics.Par1F) next case(Par2 Q Q' P) have "Q ⟼⇩_{e}τ ≺⇩_{e}Q'" by fact thus "P ∥ Q ⟼⇩_{e}τ ≺⇩_{e}P ∥ Q'" by(rule Early_Semantics.Par2F) next case(Comm1 P a x P' Q b Q') have "P ⟼⇩_{e}a<b> ≺⇩_{e}P'[x::=b]" proof - have "P ⟼⇩_{l}a<x> ≺ P'" by fact thus ?thesis by(rule lateEarlyInput) qed moreover have "Q ⟼⇩_{e}a[b] ≺⇩_{e}Q'" proof - have "Q ⟼⇩_{l}a[b] ≺⇩_{l}Q'" by fact thus ?thesis by(rule lateEarlyOutput) qed ultimately show ?case by(rule Early_Semantics.Comm1) next case(Comm2 P a b P' Q x Q') have "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" proof - have "P ⟼⇩_{l}a[b] ≺⇩_{l}P'" by fact thus ?thesis by(rule lateEarlyOutput) qed moreover have "Q ⟼⇩_{e}a<b> ≺⇩_{e}Q'[x::=b]" proof - have "Q ⟼⇩_{l}a<x> ≺⇩_{l}Q'" by fact thus ?thesis by(rule lateEarlyInput) qed ultimately show ?case by(rule Early_Semantics.Comm2) next case(Close1 P a x P' Q y Q') have "P ⟼⇩_{e}a<y> ≺⇩_{e}P'[x::=y]" proof - have "P ⟼⇩_{l}a<x> ≺ P'" by fact thus ?thesis by(rule lateEarlyInput) qed moreover have "Q ⟼⇩_{e}a<νy> ≺ Q'" proof - have "Q ⟼⇩_{l}a<νy> ≺⇩_{l}Q'" by fact thus ?thesis by(rule lateEarlyBoundOutput) qed moreover have "y ♯ P" by fact ultimately show ?case by(rule Early_Semantics.Close1) next case(Close2 P a y P' Q x Q') have "P ⟼⇩_{e}a<νy> ≺ P'" proof - have "P ⟼⇩_{l}a<νy> ≺⇩_{l}P'" by fact thus ?thesis by(rule lateEarlyBoundOutput) qed moreover have "Q ⟼⇩_{e}a<y> ≺⇩_{e}Q'[x::=y]" proof - have "Q ⟼⇩_{l}a<x> ≺⇩_{l}Q'" by fact thus ?thesis by(rule lateEarlyInput) qed moreover have "y ♯ Q" by fact ultimately show ?case by(rule Early_Semantics.Close2) next case(Res P P' x) have "P ⟼⇩_{e}τ ≺⇩_{e}P'" by fact thus ?case by(force intro: Early_Semantics.ResF) next case(Bang P P') have "P ∥ !P ⟼⇩_{e}τ ≺⇩_{e}P'" by fact thus ?case by(rule Early_Semantics.Bang) qed lemma earlyLateTau: fixes P :: pi and P' :: pi assumes "P ⟼⇩_{e}τ ≺⇩_{e}P'" shows "P ⟼⇩_{l}τ ≺⇩_{l}P'" using assms proof(nominal_induct rule: Early_Semantics.tauInduct) case(Tau P) thus ?case by(rule Late_Semantics.Tau) next case(Match P P' a) have "P ⟼⇩_{l}τ ≺⇩_{l}P'" by fact thus ?case by(rule Late_Semantics.Match) next case(Mismatch P P' a b) have "P ⟼⇩_{l}τ ≺⇩_{l}P'" by fact moreover have "a ≠ b" by fact ultimately show ?case by(rule Late_Semantics.Mismatch) next case(Sum1 P P' Q) have "P ⟼⇩_{l}τ ≺⇩_{l}P'" by fact thus ?case by(rule Late_Semantics.Sum1) next case(Sum2 Q Q' P) have "Q ⟼⇩_{l}τ ≺⇩_{l}Q'" by fact thus ?case by(rule Late_Semantics.Sum2) next case(Par1 P P' Q) have "P ⟼⇩_{l}τ ≺⇩_{l}P'" by fact thus ?case by(rule Late_Semantics.Par1F) next case(Par2 Q Q' P) have "Q ⟼⇩_{l}τ ≺⇩_{l}Q'" by fact thus ?case by(rule Late_Semantics.Par2F) next case(Comm1 P a b P' Q Q') have "P ⟼⇩_{e}a<b> ≺⇩_{e}P'" by fact moreover obtain x::name where "x ♯ P" by(generate_fresh "name") auto ultimately obtain P'' where PTrans: "P ⟼⇩_{l}a<x> ≺ P''" and P'eqP'': "P' = P''[x::=b]" by(blast dest: earlyLateInput) have "Q ⟼⇩_{e}a[b] ≺⇩_{e}Q'" by fact hence "Q ⟼⇩_{l}a[b] ≺⇩_{l}Q'" by(rule earlyLateOutput) with PTrans P'eqP'' show ?case by(blast intro: Late_Semantics.Comm1) next case(Comm2 P a b P' Q Q') have "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" by fact hence QTrans: "P ⟼⇩_{l}a[b] ≺⇩_{l}P'" by(rule earlyLateOutput) have "Q ⟼⇩_{e}a<b> ≺⇩_{e}Q'" by fact moreover obtain x::name where "x ♯ Q" by(generate_fresh "name") auto ultimately obtain Q'' x where "Q ⟼⇩_{l}a<x> ≺ Q''" and "Q' = Q''[x::=b]" by(blast dest: earlyLateInput) with QTrans show ?case by(blast intro: Late_Semantics.Comm2) next case(Close1 P a x P' Q Q') have "P ⟼⇩_{e}a<x> ≺⇩_{e}P'" and "x ♯ P" by fact+ then obtain P'' where "P ⟼⇩_{l}a<x> ≺ P''" and "P' = P''[x::=x]" by(blast dest: earlyLateInput) moreover have "Q ⟼⇩_{e}a<νx> ≺⇩_{e}Q'" by fact hence "Q ⟼⇩_{l}a<νx> ≺⇩_{l}Q'" by(rule earlyLateBoundOutput) moreover have "x ♯ P" by fact ultimately show ?case by(blast intro: Late_Semantics.Close1) next case(Close2 P a x P' Q Q') have "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" by fact hence PTrans: "P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" by(rule earlyLateBoundOutput) have "Q ⟼⇩_{e}a<x> ≺⇩_{e}Q'" and "x ♯ Q" by fact+ then obtain Q'' y where "Q ⟼⇩_{l}a<x> ≺ Q''" and "Q' = Q''[x::=x]" by(blast dest: earlyLateInput) moreover have "x ♯ Q" by fact ultimately show ?case using PTrans by(blast intro: Late_Semantics.Close2) next case(Res P P' x) have "P ⟼⇩_{l}τ ≺⇩_{l}P'" by fact thus ?case by(force intro: Late_Semantics.ResF) next case(Bang P P') have "P ∥ !P ⟼⇩_{l}τ ≺⇩_{l}P'" by fact thus ?case by(force intro: Late_Semantics.Bang) qed lemma tauEq: fixes P :: pi and P' :: pi shows "P ⟼⇩_{e}(Early_Semantics.FreeR Early_Semantics.TauR P') = P ⟼τ ≺⇩_{l}P'" by(auto intro: earlyLateTau lateEarlyTau) (****************** Simulation ******************) abbreviation simLate_judge (‹_ ↝⇩_{l}[_] _› [80, 80, 80] 80) where "P ↝⇩_{l}[Rel] Q ≡ Strong_Late_Sim.simulation P Rel Q" abbreviation simEarly_judge (‹_ ↝⇩_{e}[_] _› [80, 80, 80] 80) where "P ↝⇩_{e}[Rel] Q ≡ Strong_Early_Sim.strongSimEarly P Rel Q" lemma lateEarlySim: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" assumes PSimQ: "P ↝⇩_{l}[Rel] Q" shows "P ↝⇩_{e}[Rel] Q" proof(induct rule: Strong_Early_Sim.simCases) case(Bound a x Q') have "Q ⟼⇩_{e}a<νx> ≺⇩_{e}Q'" by fact hence "Q ⟼⇩_{l}a<νx> ≺⇩_{l}Q'" by(rule earlyLateBoundOutput) moreover have "x ♯ P" by fact ultimately obtain P' where PTrans: "P ⟼⇩_{l}a<νx> ≺⇩_{l}P'" and P'RelQ': "(P', Q') ∈ Rel" using PSimQ by(force dest: Strong_Late_Sim.simE simp add: derivative_def) from PTrans have "P ⟼⇩_{e}a<νx> ≺⇩_{e}P'" by(rule lateEarlyBoundOutput) with P'RelQ' show ?case by blast next case(Free α Q') have "Q ⟼⇩_{e}Early_Semantics.residual.FreeR α Q'" by fact thus ?case proof(nominal_induct α rule: freeRes.strong_induct) case(InputR a u) obtain x::name where "x ♯ Q" and "x ♯ P" by(generate_fresh "name") auto with ‹Q ⟼⇩_{e}a<u> ≺⇩_{e}Q'› obtain Q'' where QTrans: "Q ⟼⇩_{l}a<x> ≺⇩_{l}Q''" and Q'eqQ'': "Q' = Q''[x::=u]" by(blast dest: earlyLateInput) from PSimQ QTrans ‹x ♯ P› obtain P' where PTrans: "P ⟼⇩_{l}a<x> ≺ P'" and P'RelQ': "(P'[x::=u], Q''[x::=u]) ∈ Rel" by(force dest: Strong_Late_Sim.simE simp add: derivative_def) from PTrans have "P ⟼⇩_{e}a<u> ≺⇩_{e}P'[x::=u]" by(rule lateEarlyInput) with P'RelQ' Q'eqQ'' show "∃P'. P ⟼⇩_{e}a<u> ≺⇩_{e}P' ∧ (P', Q') ∈ Rel" by blast next case(OutputR a b) from ‹Q ⟼⇩_{e}a[b] ≺⇩_{e}Q'› have "Q ⟼⇩_{l}a[b] ≺⇩_{l}Q'" by(rule earlyLateOutput) with PSimQ obtain P' where PTrans: "P ⟼⇩_{l}a[b] ≺⇩_{l}P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: Strong_Late_Sim.simE) from PTrans have "P ⟼⇩_{e}a[b] ≺⇩_{e}P'" by(rule lateEarlyOutput) with P'RelQ' show "∃P'. P ⟼⇩_{e}a[b] ≺⇩_{e}P' ∧ (P', Q') ∈ Rel" by blast next case TauR from ‹Q ⟼⇩_{e}τ ≺⇩_{e}Q'› have "Q ⟼⇩_{l}τ ≺⇩_{l}Q'" by(rule earlyLateTau) with PSimQ obtain P' where PTrans: "P ⟼⇩_{l}τ ≺⇩_{l}P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: Strong_Late_Sim.simE) from PTrans have "P ⟼⇩_{e}τ ≺⇩_{e}P'" by(rule lateEarlyTau) with P'RelQ' show "∃P'. P ⟼⇩_{e}τ ≺⇩_{e}P' ∧ (P', Q') ∈ Rel" by blast qed qed (*************** Bisimulation ***************) abbreviation bisimLate_judge (‹_ ∼⇩_{l}_› [80, 80] 80) where "P ∼⇩_{l}Q ≡ (P, Q) ∈ Strong_Late_Bisim.bisim" abbreviation bisimEarly_judge (‹_ ∼⇩_{e}_› [80, 80] 80) where "P ∼⇩_{e}Q ≡ (P, Q) ∈ Strong_Early_Bisim.bisim" lemma lateEarlyBisim: fixes P :: pi and Q :: pi assumes "P ∼⇩_{l}Q" shows "P ∼⇩_{e}Q" using assms by(coinduct rule: Strong_Early_Bisim.weak_coinduct) (auto dest: Strong_Late_Bisim.bisimE Strong_Late_Bisim.symmetric intro: lateEarlySim) (*************** Congruence ***************) abbreviation congLate_judge (‹_ ∼⇧^{s}⇩_{l}_› [80, 80] 80) where "P ∼⇧^{s}⇩_{l}Q ≡ (P, Q) ∈ (substClosed Strong_Late_Bisim.bisim)" abbreviation congEarly_judge (‹_ ∼⇧^{s}⇩_{e}_› [80, 80] 80) where "P ∼⇧^{s}⇩_{e}Q ≡ (P, Q) ∈ (substClosed Strong_Early_Bisim.bisim)" lemma lateEarlyCong: fixes P :: pi and Q :: pi assumes "P ∼⇧^{s}⇩_{l}Q" shows "P ∼⇧^{s}⇩_{e}Q" using assms by(auto simp add: substClosed_def intro: lateEarlyBisim) lemma earlyCongStructCong: fixes P :: pi and Q :: pi assumes "P ≡⇩_{s}Q" shows "P ∼⇧^{s}⇩_{e}Q" using assms lateEarlyCong bisimSubstStructCong by blast lemma earlyBisimStructCong: fixes P :: pi and Q :: pi assumes "P ≡⇩_{s}Q" shows "P ∼⇩_{e}Q" using assms lateEarlyBisim structCongBisim by blast end