Theory Strong_Early_Late_Comp

(* 
   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 ⟼⇩ea[b] ≺⇩e P'"

  shows "P ⟼⇩la[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 ⟼⇩la[b] ≺⇩l P'" by fact
  thus ?case by(rule Late_Semantics.Match)
next
  case(Mismatch P a b P' c d)
  from ‹P ⟼⇩la[b] ≺⇩l P'› ‹c ≠ d›
  show ?case by(rule Late_Semantics.Mismatch)
next
  case(Sum1 P a b P' Q)
  have "P ⟼⇩la[b] ≺⇩l P'" by fact
  thus ?case by(rule Late_Semantics.Sum1)
next
  case(Sum2 Q a b Q' P)
  have "Q ⟼⇩la[b] ≺⇩l Q'" by fact
  thus ?case by(rule Late_Semantics.Sum2)
next
  case(Par1 P a b P' Q)
  have "P ⟼⇩la[b] ≺⇩l P'" by fact
  thus ?case by(rule Late_Semantics.Par1F)
next
  case(Par2 Q a b Q' P)
  have "Q ⟼⇩la[b] ≺⇩l Q'" by fact
  thus ?case by(rule Late_Semantics.Par2F)
next
  case(Res P a b P' x)
  have "P ⟼⇩la[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 ⟼⇩la[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 ⟼⇩la[b] ≺⇩l P'"

  shows "P ⟼⇩ea[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 ⟼⇩ea[b] ≺⇩e P'" by fact
  thus ?case by(rule Early_Semantics.Match)
next
  case(Mismatch P a b P' c d)
  have "P ⟼⇩ea[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 ⟼⇩ea[b] ≺⇩e P'" by fact
  thus ?case by(rule Early_Semantics.Sum1)
next
  case(Sum2 Q a b Q' P)
  have "Q ⟼⇩ea[b] ≺⇩e Q'" by fact
  thus ?case by(rule Early_Semantics.Sum2)
next
  case(Par1 P a b P' Q)
  have "P ⟼⇩ea[b] ≺⇩e P'" by fact
  thus ?case by(rule Early_Semantics.Par1F)
next
  case(Par2 Q a b Q' P)
  have "Q ⟼⇩ea[b] ≺⇩e Q'" by fact
  thus ?case by(rule Early_Semantics.Par2F)
next
  case(Res P a b P' x)
  have "P ⟼⇩ea[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 ⟼⇩ea[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 ⟼⇩ea[b] ≺⇩e P' = P ⟼⇩la[b] ≺⇩l P'"
by(auto intro: lateEarlyOutput earlyLateOutput)

lemma lateEarlyBoundOutput:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi

  assumes "P ⟼⇩la<νx> ≺⇩l P'"

  shows "P ⟼⇩ea<νx> ≺⇩e P'"
proof -
  have Goal: "⋀P a x P'. ⟦P ⟼⇩la<νx> ≺⇩l P'; x ♯ P⟧ ⟹ P ⟼⇩ea<νx> ≺⇩e P'"
  proof -
    fix P a x P'
    assume "P ⟼⇩l a<νx> ≺⇩l P'" and "x ♯ P"
    thus "P ⟼⇩ea<ν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 ⟼⇩la[x] ≺⇩l P'" by fact
      hence "P ⟼⇩ea[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 ⟼⇩la<ν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 ⟼⇩ea<νx> ≺⇩e P'"

  shows "P ⟼⇩la<νx> ≺⇩l P'"
proof -
  have Goal: "⋀P a x P'. ⟦P ⟼⇩ea<νx> ≺⇩e P'; x ♯ P⟧ ⟹ P ⟼⇩la<νx> ≺⇩l P'"
  proof -
    fix P a x P'
    assume "P ⟼⇩e a<νx> ≺ P'" and "x ♯ P"
    thus "P ⟼⇩la<ν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 ⟼⇩ea[x] ≺⇩e P'" by fact
      hence "P ⟼⇩la[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 ⟼⇩ea<ν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 ⟼⇩ea<νx> ≺⇩e P' = P ⟼⇩la<ν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 ⟼⇩ea<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 ⟼⇩ea<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 ⟼⇩ea<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 ⟼⇩ea<u> ≺⇩e (P'[x::=u])" by fact
      thus ?case by(rule Early_Semantics.Sum1)
    next
      case(Sum2 P Q a x Q')
      have "Q ⟼⇩ea<u> ≺⇩e (Q'[x::=u])" by fact
      thus ?case by(rule Early_Semantics.Sum2)
    next
      case(Par1 P P' Q a x)
      have "P ⟼⇩ea<u> ≺⇩e (P'[x::=u])" by fact
      hence "P ∥ Q ⟼⇩ea<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 ⟼⇩ea<u> ≺⇩e (Q'[x::=u])" by fact
      hence "P ∥ Q ⟼⇩ea<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 ⟼⇩ea<u> ≺⇩e (P'[x::=u])" and "y ≠ a" and yinequ: "y ♯ u" by fact+
      hence "<νy>P ⟼⇩ea<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 ⟼⇩ea<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 ⟼⇩la<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 ⟼⇩ea<u> ≺⇩e P'"
  and     "x ♯ P"

  shows "∃P''. P ⟼⇩la<x> ≺⇩l P'' ∧ P' = P''[x::=u]"
proof -
  {
    fix P a u P'
    assume "P ⟼⇩ea<u> ≺⇩e P'"
    hence "∃P'' x. P ⟼⇩la<x> ≺⇩l P'' ∧ P' = P''[x::=u]"
    proof(nominal_induct rule: Early_Semantics.inputInduct)
      case(cInput a x P u)
      have "a<x>.P ⟼⇩la<x> ≺ P" by(rule Late_Semantics.Input)
      thus ?case by blast
    next
      case(cMatch P a u P' b)
      have "∃P'' x. P ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast
      from PTrans have "[b⌢b]P ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast
      have "b ≠ c" by fact
      with PTrans have "[b≠c]P ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast
      from PTrans have "P ⊕ Q ⟼⇩la<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 ⟼⇩la<x> ≺ Q'' ∧ Q' = Q''[x::=u]" by fact
      then obtain Q'' x where QTrans: "Q ⟼⇩la<x> ≺ Q''" and Q'eqQ'': "Q' = Q''[x::=u]" by blast
      from QTrans have "P ⊕ Q ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<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 ⟼⇩la<c> ≺ [(x, c)] ∙ P''" by(simp add: Late_Semantics.alphaBoundResidual)
      hence "P ∥ Q ⟼⇩la<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 ⟼⇩la<x> ≺ Q'' ∧ Q' = Q''[x::=u]" by fact
      then obtain Q'' x where QTrans: "Q ⟼⇩la<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 ⟼⇩la<c> ≺ [(x, c)] ∙ Q''" by(simp add: Late_Semantics.alphaBoundResidual)
      hence "P ∥ Q ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<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 ⟼⇩la<c> ≺ [(x, c)] ∙ P''" by(simp add: Late_Semantics.alphaBoundResidual)
      moreover have "y ≠ a" by fact
      ultimately have "<νy>P ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ∥ !P ⟼⇩la<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast
      from PTrans have "!P ⟼⇩la<x> ≺ P''" by(rule Late_Semantics.Bang)
      with P'eqP'' show ?case by blast
    qed
  }
  with assms obtain P'' y where PTrans: "P ⟼⇩la<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 ⟼⇩la<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 ⟼⇩ea<u> ≺⇩e P'"

  shows "∃P'' x. P ⟼⇩la<x> ≺⇩l P'' ∧ P' = P''[x::=u] ∧ x ♯ C"
proof -
  have "⋀P a u P'. P ⟼⇩ea<u> ≺⇩e P' ⟹ ∃P'' x. P ⟼⇩la<x> ≺⇩l P'' ∧ P' = P''[x::=u]"
  proof -
    fix P a u P'
    assume "P ⟼⇩ea<u> ≺⇩e P'"
    thus "∃P'' x. P ⟼⇩la<x> ≺⇩l P'' ∧ P' = P''[x::=u]"
    proof(nominal_induct rule: Early_Semantics.inputInduct)
      case(cInput a x P u)
      have "a<x>.P ⟼⇩la<x> ≺ P" by(rule Late_Semantics.Input)
      thus ?case by blast
    next
      case(cMatch P a u P' b)
      have "∃P'' x. P ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast
      from PTrans have "[b⌢b]P ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast
      have "b ≠ c" by fact
      with PTrans have "[b≠c]P ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast
      from PTrans have "P ⊕ Q ⟼⇩la<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 ⟼⇩la<x> ≺ Q'' ∧ Q' = Q''[x::=u]" by fact
      then obtain Q'' x where QTrans: "Q ⟼⇩la<x> ≺ Q''" and Q'eqQ'': "Q' = Q''[x::=u]" by blast
      from QTrans have "P ⊕ Q ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<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 ⟼⇩la<c> ≺ [(x, c)] ∙ P''" by(simp add: Late_Semantics.alphaBoundResidual)
      hence "P ∥ Q ⟼⇩la<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 ⟼⇩la<x> ≺ Q'' ∧ Q' = Q''[x::=u]" by fact
      then obtain Q'' x where QTrans: "Q ⟼⇩la<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 ⟼⇩la<c> ≺ [(x, c)] ∙ Q''" by(simp add: Late_Semantics.alphaBoundResidual)
      hence "P ∥ Q ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ⟼⇩la<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 ⟼⇩la<c> ≺ [(x, c)] ∙ P''" by(simp add: Late_Semantics.alphaBoundResidual)
      moreover have "y ≠ a" by fact
      ultimately have "<νy>P ⟼⇩la<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 ⟼⇩la<x> ≺ P'' ∧ P' = P''[x::=u]" by fact
      then obtain P'' x where PTrans: "P ∥ !P ⟼⇩la<x> ≺ P''" and P'eqP'': "P' = P''[x::=u]" by blast
      from PTrans have "!P ⟼⇩la<x> ≺ P''" by(rule Late_Semantics.Bang)
      with P'eqP'' show ?case by blast
    qed
  qed
  with PTrans obtain P'' x where PTrans: "P ⟼⇩la<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 ⟼⇩la<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 ⟼⇩ea<b> ≺⇩e P'[x::=b]"
  proof -
    have "P ⟼⇩l a<x> ≺ P'" by fact
    thus ?thesis by(rule lateEarlyInput)
  qed
  moreover have "Q ⟼⇩ea[b] ≺⇩e Q'"
  proof -
    have "Q ⟼⇩la[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 ⟼⇩ea[b] ≺⇩e P'"
  proof -
    have "P ⟼⇩la[b] ≺⇩l P'" by fact
    thus ?thesis by(rule lateEarlyOutput)
  qed
  moreover have "Q ⟼⇩ea<b> ≺⇩e Q'[x::=b]"
  proof -
    have "Q ⟼⇩la<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 ⟼⇩ea<y> ≺⇩e P'[x::=y]"
  proof -
    have "P ⟼⇩l a<x> ≺ P'" by fact
    thus ?thesis by(rule lateEarlyInput)
  qed
  moreover have "Q ⟼⇩ea<νy> ≺ Q'"
  proof -
    have "Q ⟼⇩la<ν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 ⟼⇩ea<νy> ≺ P'"
  proof -
    have "P ⟼⇩la<νy> ≺⇩l P'" by fact
    thus ?thesis by(rule lateEarlyBoundOutput)
  qed
  moreover have "Q ⟼⇩ea<y> ≺⇩e Q'[x::=y]"
  proof -
    have "Q ⟼⇩la<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 ⟼⇩ea<b> ≺⇩e P'" by fact
  moreover obtain x::name  where "x ♯ P" by(generate_fresh "name") auto
  ultimately obtain P'' where PTrans: "P ⟼⇩la<x> ≺ P''" and P'eqP'': "P' = P''[x::=b]"
    by(blast dest: earlyLateInput)
  have "Q ⟼⇩ea[b] ≺⇩e Q'" by fact
  hence "Q ⟼⇩la[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 ⟼⇩ea[b] ≺⇩e P'" by fact
  hence QTrans: "P ⟼⇩la[b] ≺⇩l P'" by(rule earlyLateOutput)
  have "Q ⟼⇩ea<b> ≺⇩e Q'" by fact
  moreover obtain x::name  where "x ♯ Q" by(generate_fresh "name") auto
  ultimately obtain Q'' x where "Q ⟼⇩la<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 ⟼⇩ea<x> ≺⇩e P'" and "x ♯ P" by fact+
  then obtain P'' where "P ⟼⇩la<x> ≺ P''" and "P' = P''[x::=x]"
    by(blast dest: earlyLateInput)
  
  moreover have "Q ⟼⇩ea<νx> ≺⇩e Q'" by fact
  hence "Q ⟼⇩la<ν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 ⟼⇩ea<νx> ≺⇩e P'" by fact
  hence PTrans: "P ⟼⇩la<νx> ≺⇩l P'" by(rule earlyLateBoundOutput)

  have "Q ⟼⇩ea<x> ≺⇩e Q'" and "x ♯ Q" by fact+
  then obtain Q'' y where "Q ⟼⇩la<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 ⟼⇩ea<νx> ≺⇩e Q'" by fact
  hence "Q ⟼⇩la<νx> ≺⇩l Q'" by(rule earlyLateBoundOutput)
  moreover have "x ♯ P" by fact
  ultimately obtain P' where PTrans: "P ⟼⇩la<ν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 ⟼⇩ea<ν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 ⟼⇩ea<u> ≺⇩e Q'› obtain Q'' where QTrans: "Q ⟼⇩la<x> ≺⇩l Q''" and Q'eqQ'': "Q' = Q''[x::=u]"
      by(blast dest: earlyLateInput)
    from PSimQ QTrans ‹x ♯ P›  obtain P' where PTrans: "P ⟼⇩la<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 ⟼⇩ea<u> ≺⇩e P'[x::=u]" by(rule lateEarlyInput)
    with P'RelQ' Q'eqQ'' show "∃P'. P ⟼⇩ea<u> ≺⇩e P' ∧ (P', Q') ∈ Rel" by blast
  next
    case(OutputR a b)
    from ‹Q ⟼⇩ea[b] ≺⇩e Q'› have "Q ⟼⇩la[b] ≺⇩l Q'" by(rule earlyLateOutput)
    with PSimQ obtain P' where PTrans: "P ⟼⇩la[b] ≺⇩l P'" and P'RelQ': "(P', Q') ∈ Rel"
      by(blast dest: Strong_Late_Sim.simE)
    from PTrans have "P ⟼⇩ea[b] ≺⇩e P'" by(rule lateEarlyOutput)
    with P'RelQ' show "∃P'. P ⟼⇩ea[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