Theory Simulation

theory Simulation
  imports Semantics
begin

text ‹This file is a (heavily modified) variant of the theory {\it Psi\_Calculi.Simulation}
from~\cite{DBLP:journals/afp/Bengtson12}.›

context env begin

definition
  "simulation" :: "'b ⇒ ('a, 'b, 'c) psi ⇒
                   ('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set ⇒
                   ('a, 'b, 'c) psi ⇒ bool" ("_ ⊳ _ ↝[_] _" [80, 80, 80, 80] 80)
  where
    "Ψ ⊳ P ↝[Rel] Q ≡ ∀α Q'. Ψ ⊳ Q ⟼α ≺ Q' ⟶ bn α ♯* Ψ ⟶ bn α ♯* P ⟶ (∃P'. Ψ ⊳ P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel)"

abbreviation
  simulationNilJudge ("_ ↝[_] _" [80, 80, 80] 80) where "P ↝[Rel] Q ≡ SBottom' ⊳ P ↝[Rel] Q"

lemma simI[consumes 1, case_names cSim]:
  fixes Ψ   :: 'b
    and P   :: "('a, 'b, 'c) psi"
    and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q   :: "('a, 'b, 'c) psi"
    and C   :: "'d::fs_name"

assumes Eqvt: "eqvt Rel"
  and   Sim: "⋀α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* P; bn α ♯* Q; bn α  ♯* Ψ; distinct(bn α);
                         bn α ♯* (subject α); bn α ♯* C⟧ ⟹ ∃P'. Ψ ⊳ P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"

shows "Ψ ⊳ P ↝[Rel] Q"
proof -
  {
    fix α Q'
    assume "Ψ ⊳ Q ⟼α ≺ Q'" and "bn α ♯* Ψ" and "bn α ♯* P"
    then have "∃P'. Ψ ⊳ P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
    proof(nominal_induct α rule: action.strong_induct)
      case(In M N)
      then show ?case by(auto simp add: Sim)
    next
      case(BrIn M N)
      then show ?case by(auto simp add: Sim)
    next
      case(Out M xvec N)
      moreover {
        fix M xvec N Q'
        assume "(xvec::name list) ♯* Ψ" and "xvec ♯* P"
        obtain p where xvecFreshPsi: "((p::name prm) ∙ (xvec::name list)) ♯* Ψ"
        and xvecFreshM: "(p ∙ xvec) ♯* (M::'a)"
        and xvecFreshN: "(p ∙ xvec) ♯* (N::'a)"
        and xvecFreshP: "(p ∙ xvec) ♯* P"
        and xvecFreshQ: "(p ∙ xvec) ♯* Q"
        and xvecFreshQ': "(p ∙ xvec) ♯* (Q'::('a, 'b, 'c) psi)"
        and xvecFreshC: "(p ∙ xvec) ♯* C"
        and xvecFreshxvec: "(p ∙ xvec) ♯* xvec"
        and S: "(set p) ⊆ (set xvec) × (set(p ∙ xvec))"
        and dpr: "distinctPerm p"
          by(rule name_list_avoiding[where xvec="xvec" and c="(Ψ, M, Q, N, P, Q', xvec, C)"]) auto
        from ‹(p ∙ xvec) ♯* M› ‹distinctPerm p› have "xvec ♯* (p ∙ M)"
          by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, where pi=p, symmetric]) simp

        assume Trans: "Ψ ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'"
        with xvecFreshN xvecFreshQ' S
        have "Ψ ⊳ Q ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ Q')"
          by(simp add: boundOutputChainAlpha'' residualInject)
        moreover then have "distinct(p ∙ xvec)"  by(auto dest: boundOutputDistinct)

        moreover note xvecFreshPsi xvecFreshP xvecFreshQ xvecFreshM xvecFreshC
        ultimately obtain P' where PTrans: "Ψ ⊳ P ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ P'"
        and P'RelQ': "(Ψ, P', p ∙ Q') ∈ Rel"
          using Sim by (metis bn.simps(3) optionFreshChain(1) subject.simps(3))
        then have "(p ∙ Ψ) ⊳ (p ∙ P) ⟼(p ∙ (M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ P'))"
          by(simp add: semantics.eqvt)
        with ‹xvec ♯* Ψ› xvecFreshPsi ‹xvec ♯* P› xvecFreshP S dpr
        have "Ψ ⊳ P ⟼(p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P')"
          by(simp add: eqvts name_set_fresh_fresh)
        with ‹xvec ♯* Ψ› xvecFreshPsi ‹xvec ♯* P› xvecFreshP S ‹xvec ♯* (p ∙ M)›
        have "Ψ ⊳ P ⟼(p ∙ p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P')"
          by(simp add: outputPermSubject)

        with dpr have "Ψ ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P')"
          by simp

        moreover from P'RelQ' Eqvt have "(p ∙ Ψ, p ∙ P', p ∙ p ∙ Q') ∈ Rel"
          apply(simp add: eqvt_def eqvts)
          apply(erule ballE[where x="(Ψ, P', p ∙ Q')"])
           apply(erule allE[where x="p"])
          by(auto simp add: eqvts)

        with ‹xvec ♯* Ψ› xvecFreshPsi S dpr have "(Ψ, p ∙ P', Q') ∈ Rel"
          by simp
        ultimately have "∃P'. Ψ ⊳ P ⟼ M⦇ν*xvec⦈⟨N⟩ ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
          by blast
      }
      ultimately show ?case by force
    next
      case(BrOut M xvec N)
      moreover {
        fix M xvec N Q'
        assume "(xvec::name list) ♯* Ψ" and "xvec ♯* P"
        obtain p where xvecFreshPsi: "((p::name prm) ∙ (xvec::name list)) ♯* Ψ"
        and xvecFreshM: "(p ∙ xvec) ♯* (M::'a)"
        and xvecFreshN: "(p ∙ xvec) ♯* (N::'a)"
        and xvecFreshP: "(p ∙ xvec) ♯* P"
        and xvecFreshQ: "(p ∙ xvec) ♯* Q"
        and xvecFreshQ': "(p ∙ xvec) ♯* (Q'::('a, 'b, 'c) psi)"
        and xvecFreshC: "(p ∙ xvec) ♯* C"
        and xvecFreshxvec: "(p ∙ xvec) ♯* xvec"
        and S: "(set p) ⊆ (set xvec) × (set(p ∙ xvec))"
        and dpr: "distinctPerm p"
          by(rule name_list_avoiding[where xvec="xvec" and c="(Ψ, M, Q, N, P, Q', xvec, C)"]) auto

        from ‹(p ∙ xvec) ♯* M› ‹distinctPerm p› have "xvec ♯* (p ∙ M)"
          by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, where pi=p, symmetric]) simp

        assume Trans: "Ψ ⊳ Q ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ Q'"
        with xvecFreshN xvecFreshQ' S
        have "Ψ ⊳ Q ⟼¡M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ Q')"
          by(simp add: boundOutputChainAlpha'' residualInject)
        moreover then have "distinct(p ∙ xvec)"
          by(auto dest: boundOutputDistinct)

        moreover note xvecFreshPsi xvecFreshP xvecFreshQ xvecFreshM xvecFreshC
        ultimately obtain P' where PTrans: "Ψ ⊳ P ⟼¡M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ P'"
        and P'RelQ': "(Ψ, P', p ∙ Q') ∈ Rel"
          by(auto dest: Sim)
        then have "(p ∙ Ψ) ⊳ (p ∙ P) ⟼(p ∙ (¡M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ P'))"
          by(metis semantics.eqvt)
        with ‹xvec ♯* Ψ› xvecFreshPsi ‹xvec ♯* P› xvecFreshP S dpr
        have "Ψ ⊳ P ⟼¡(p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P')"
          by(simp add: eqvts name_set_fresh_fresh)
        with ‹xvec ♯* Ψ› xvecFreshPsi ‹xvec ♯* P› xvecFreshP S ‹xvec ♯* (p ∙ M)›
        have "Ψ ⊳ P ⟼¡(p ∙ p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P')"
          by(simp add: broutputPermSubject)

        with dpr have "Ψ ⊳ P ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ (p ∙ P')"
          by simp

        moreover from P'RelQ' Eqvt have "(p ∙ Ψ, p ∙ P', p ∙ p ∙ Q') ∈ Rel"
          apply(simp add: eqvt_def eqvts)
          apply(erule ballE[where x="(Ψ, P', p ∙ Q')"])
           apply(erule allE[where x="p"])
          by(auto simp add: eqvts)

        with ‹xvec ♯* Ψ› xvecFreshPsi S dpr have "(Ψ, p ∙ P', Q') ∈ Rel"
          by simp
        ultimately have "∃P'. Ψ ⊳ P ⟼ ¡M⦇ν*xvec⦈⟨N⟩ ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
          by blast
      }
      ultimately show ?case by force
    next
      case Tau
      then show ?case by (auto simp add: Sim)
    qed
  }
  then show ?thesis
    by (auto simp add: simulation_def)
qed

lemma simI2[case_names cSim]:
  fixes Ψ   :: 'b
    and P   :: "('a, 'b, 'c) psi"
    and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q   :: "('a, 'b, 'c) psi"
    and C   :: "'d::fs_name"

assumes Sim: "⋀α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* P; bn α  ♯* Ψ; distinct(bn α)⟧ ⟹ ∃P'. Ψ ⊳ P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"

shows "Ψ ⊳ P ↝[Rel] Q"
  using assms
  by(auto simp add: simulation_def dest: boundOutputDistinct)

lemma simIChainFresh[consumes 4, case_names cSim]:
  fixes Ψ    :: 'b
    and P    :: "('a, 'b, 'c) psi"
    and Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q    :: "('a, 'b, 'c) psi"
    and xvec :: "name list"
    and C    :: "'d::fs_name"

assumes Eqvt: "eqvt Rel"
  and   "xvec ♯* Ψ"
  and   "xvec ♯* P"
  and   "xvec ♯* Q"
  and   Sim: "⋀α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* P; bn α ♯* Q; bn α ♯* Ψ;
                         bn α ♯* subject α; distinct(bn α); bn α ♯* C; xvec ♯* α; xvec ♯* Q'⟧ ⟹
                         ∃P'. Ψ ⊳ P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
shows "Ψ ⊳ P ↝[Rel] Q"
  using ‹eqvt Rel›
proof(induct rule: simI[where C="(xvec, C)"])
  case(cSim α Q')
  from ‹bn α ♯* (xvec, C)› have "bn α ♯* xvec" and "bn α ♯* C" by simp+
  obtain p::"name prm" where "(p ∙ xvec) ♯* Ψ" and  "(p ∙ xvec) ♯* P" and  "(p ∙ xvec) ♯* Q"
    and  "(p ∙ xvec) ♯* α" and S: "set p ⊆ set xvec × set(p ∙ xvec)"
    and "distinctPerm p"
    by(rule name_list_avoiding[where c="(Ψ, P, Q, α)" and xvec=xvec]) auto
  show ?case
  proof(cases rule: actionCases[where α=α])
    case(cInput M N)
    from ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹α=M⦇N⦈› have "(p ∙ Ψ) ⊳ (p ∙ Q) ⟼(p ∙ (M⦇N⦈ ≺ Q'))"
      by(auto intro: semantics.eqvt)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› S
    have QTrans: "Ψ ⊳ Q ⟼(p ∙ M)⦇(p ∙ N)⦈ ≺ (p ∙ Q')"
      by(simp add: eqvts)
    moreover from ‹(p ∙ xvec) ♯* α› have "(p ∙ (p ∙ xvec)) ♯* (p ∙ α)"
      by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with ‹distinctPerm p› ‹α=M⦇N⦈› have "xvec ♯* (p ∙ M)" and "xvec ♯* (p ∙ N)" by simp+
    moreover with QTrans ‹xvec ♯* Q› have "xvec ♯* (p ∙ Q')"
      by(metis inputFreshChainDerivative)
    ultimately have "∃P'. Ψ ⊳ P ⟼ (p ∙ M)⦇(p ∙ N)⦈ ≺ P' ∧ (Ψ, P', (p ∙ Q')) ∈ Rel"
      by(simp add: Sim)
    then obtain P' where PTrans: "Ψ ⊳ P ⟼ (p ∙ M)⦇(p ∙ N)⦈ ≺ P'" and P'RelQ': "(Ψ, P', (p ∙ Q')) ∈ Rel"
      by blast
    from PTrans have "(p ∙ Ψ) ⊳ (p ∙ P) ⟼ (p ∙ ((p ∙ M)⦇(p ∙ N)⦈ ≺ P'))"
      by(rule semantics.eqvt)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› S ‹distinctPerm p›
    have "Ψ ⊳ P ⟼ M⦇N⦈ ≺ (p ∙ P')" by(simp add: eqvts)
    moreover from P'RelQ' ‹eqvt Rel› have "(p ∙ Ψ, p ∙ P', p ∙ p ∙ Q') ∈ Rel"
      by(auto simp add: eqvt_def)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S ‹distinctPerm p›
    have "(Ψ, p ∙ P', Q') ∈ Rel" by simp
    ultimately show ?thesis using ‹α=M⦇N⦈› by blast
  next
    case(cBrInput M N)
    from ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹α=¿M⦇N⦈› have "(p ∙ Ψ) ⊳ (p ∙ Q) ⟼(p ∙ (¿M⦇N⦈ ≺ Q'))"
      by(auto intro: semantics.eqvt)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› S
    have QTrans: "Ψ ⊳ Q ⟼¿(p ∙ M)⦇(p ∙ N)⦈ ≺ (p ∙ Q')"
      by(simp add: eqvts)
    moreover from ‹(p ∙ xvec) ♯* α› have "(p ∙ (p ∙ xvec)) ♯* (p ∙ α)"
      by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with ‹distinctPerm p› ‹α=¿M⦇N⦈› have "xvec ♯* (p ∙ M)" and "xvec ♯* (p ∙ N)" by simp+
    moreover with QTrans ‹xvec ♯* Q› have "xvec ♯* (p ∙ Q')" by(metis brinputFreshChainDerivative)
    ultimately have "∃P'. Ψ ⊳ P ⟼ ¿(p ∙ M)⦇(p ∙ N)⦈ ≺ P' ∧ (Ψ, P', (p ∙ Q')) ∈ Rel"
      by(simp add: Sim)
    then obtain P' where PTrans: "Ψ ⊳ P ⟼ ¿(p ∙ M)⦇(p ∙ N)⦈ ≺ P'" and P'RelQ': "(Ψ, P', (p ∙ Q')) ∈ Rel"
      by blast
    from PTrans have "(p ∙ Ψ) ⊳ (p ∙ P) ⟼ (p ∙ (¿(p ∙ M)⦇(p ∙ N)⦈ ≺ P'))"
      by(rule semantics.eqvt)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› S ‹distinctPerm p›
    have "Ψ ⊳ P ⟼ ¿M⦇N⦈ ≺ (p ∙ P')" by(simp add: eqvts)
    moreover from P'RelQ' ‹eqvt Rel› have "(p ∙ Ψ, p ∙ P', p ∙ p ∙ Q') ∈ Rel"
      by(auto simp add: eqvt_def)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S ‹distinctPerm p›
    have "(Ψ, p ∙ P', Q') ∈ Rel" by simp
    ultimately show ?thesis using ‹α=¿M⦇N⦈› by blast
  next
    case(cOutput M yvec N)
    from ‹distinct(bn α)› ‹bn α ♯* subject α› ‹α=M⦇ν*yvec⦈⟨N⟩› have "distinct yvec" and "yvec ♯* M" by simp+
    from ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹α=M⦇ν*yvec⦈⟨N⟩› have "(p ∙ Ψ) ⊳ (p ∙ Q) ⟼(p ∙ (M⦇ν*yvec⦈⟨N⟩ ≺ Q'))"
      by(auto intro: semantics.eqvt)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› S
    have QTrans: "Ψ ⊳ Q ⟼(p ∙ M)⦇ν*(p ∙ yvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ Q')"
      by(simp add: eqvts)
    with S ‹bn α ♯* xvec› ‹(p ∙ xvec) ♯* α› ‹α=M⦇ν*yvec⦈⟨N⟩› have "Ψ ⊳ Q ⟼(p ∙ M)⦇ν*yvec⦈⟨(p ∙ N)⟩ ≺ (p ∙ Q')"
      by simp
    moreover from ‹(p ∙ xvec) ♯* α› have "(p ∙ (p ∙ xvec)) ♯* (p ∙ α)"
      by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with ‹distinctPerm p› ‹α=M⦇ν*yvec⦈⟨N⟩› have "xvec ♯* (p ∙ M)" and "xvec ♯* (p ∙ N)" and "xvec ♯* (p ∙ yvec)" by simp+
    moreover with QTrans ‹xvec ♯* Q› ‹distinct yvec› ‹yvec ♯* M› have "xvec ♯* (p ∙ Q')"
      apply(drule_tac outputFreshChainDerivative(2))
      by(auto simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    moreover from ‹yvec ♯* M› S ‹bn α ♯* xvec› ‹(p ∙ xvec) ♯* α› ‹α=M⦇ν*yvec⦈⟨N⟩› ‹distinctPerm p›
    have "yvec ♯* (p ∙ M)" by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, symmetric, where pi=p]) simp
    ultimately have "∃P'. Ψ ⊳ P ⟼ (p ∙ M)⦇ν*yvec⦈⟨(p ∙ N)⟩ ≺ P' ∧ (Ψ, P', (p ∙ Q')) ∈ Rel"
      using ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* Q›‹bn α ♯* xvec› ‹bn α ♯* C› ‹yvec ♯* M› ‹α=M⦇ν*yvec⦈⟨N⟩› ‹distinct yvec›
      by(simp add: Sim)
    then obtain P' where PTrans: "Ψ ⊳ P ⟼ (p ∙ M)⦇ν*yvec⦈⟨(p ∙ N)⟩ ≺ P'" and P'RelQ': "(Ψ, P', (p ∙ Q')) ∈ Rel"
      by blast
    from PTrans have "(p ∙ Ψ) ⊳ (p ∙ P) ⟼ (p ∙ ((p ∙ M)⦇ν*yvec⦈⟨(p ∙ N)⟩ ≺ P'))"
      by(rule semantics.eqvt)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› S ‹distinctPerm p› ‹bn α ♯* xvec› ‹(p ∙ xvec) ♯* α› ‹α=M⦇ν*yvec⦈⟨N⟩›
    have "Ψ ⊳ P ⟼ M⦇ν*yvec⦈⟨N⟩ ≺ (p ∙ P')" by(simp add: eqvts)
    moreover from P'RelQ' ‹eqvt Rel› have "(p ∙ Ψ, p ∙ P', p ∙ p ∙ Q') ∈ Rel"
      by(auto simp add: eqvt_def)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S ‹distinctPerm p›
    have "(Ψ, p ∙ P', Q') ∈ Rel" by simp
    ultimately show ?thesis using ‹α=M⦇ν*yvec⦈⟨N⟩› by blast
  next
    case(cBrOutput M yvec N)
    from ‹distinct(bn α)› ‹bn α ♯* subject α› ‹α=¡M⦇ν*yvec⦈⟨N⟩› have "distinct yvec" and "yvec ♯* M" by simp+
    from ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹α=¡M⦇ν*yvec⦈⟨N⟩› have "(p ∙ Ψ) ⊳ (p ∙ Q) ⟼(p ∙ (¡M⦇ν*yvec⦈⟨N⟩ ≺ Q'))"
      by(auto intro: semantics.eqvt)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› S
    have QTrans: "Ψ ⊳ Q ⟼¡(p ∙ M)⦇ν*(p ∙ yvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ Q')"
      by(simp add: eqvts)
    with S ‹bn α ♯* xvec› ‹(p ∙ xvec) ♯* α› ‹α=¡M⦇ν*yvec⦈⟨N⟩› have "Ψ ⊳ Q ⟼¡(p ∙ M)⦇ν*yvec⦈⟨(p ∙ N)⟩ ≺ (p ∙ Q')"
      by simp
    moreover from ‹(p ∙ xvec) ♯* α› have "(p ∙ (p ∙ xvec)) ♯* (p ∙ α)"
      by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with ‹distinctPerm p› ‹α=¡M⦇ν*yvec⦈⟨N⟩› have "xvec ♯* (p ∙ M)" and "xvec ♯* (p ∙ N)" and "xvec ♯* (p ∙ yvec)" by simp+
    moreover with QTrans ‹xvec ♯* Q› ‹distinct yvec› ‹yvec ♯* M› have "xvec ♯* (p ∙ Q')"
      apply(drule_tac broutputFreshChainDerivative(2))
      by (auto simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    moreover from ‹yvec ♯* M› S ‹bn α ♯* xvec› ‹(p ∙ xvec) ♯* α› ‹α=¡M⦇ν*yvec⦈⟨N⟩› ‹distinctPerm p›
    have "yvec ♯* (p ∙ M)" by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, symmetric, where pi=p]) simp
    ultimately have "∃P'. Ψ ⊳ P ⟼ ¡(p ∙ M)⦇ν*yvec⦈⟨(p ∙ N)⟩ ≺ P' ∧ (Ψ, P', (p ∙ Q')) ∈ Rel"
      using ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* Q›‹bn α ♯* xvec› ‹bn α ♯* C› ‹yvec ♯* M› ‹α=¡M⦇ν*yvec⦈⟨N⟩› ‹distinct yvec›
      by(simp add: Sim)
    then obtain P' where PTrans: "Ψ ⊳ P ⟼ ¡(p ∙ M)⦇ν*yvec⦈⟨(p ∙ N)⟩ ≺ P'" and P'RelQ': "(Ψ, P', (p ∙ Q')) ∈ Rel"
      by blast
    from PTrans have "(p ∙ Ψ) ⊳ (p ∙ P) ⟼ (p ∙ (¡(p ∙ M)⦇ν*yvec⦈⟨(p ∙ N)⟩ ≺ P'))"
      by(rule semantics.eqvt)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› S ‹distinctPerm p› ‹bn α ♯* xvec› ‹(p ∙ xvec) ♯* α› ‹α=¡M⦇ν*yvec⦈⟨N⟩›
    have "Ψ ⊳ P ⟼ ¡M⦇ν*yvec⦈⟨N⟩ ≺ (p ∙ P')" by(simp add: eqvts)
    moreover from P'RelQ' ‹eqvt Rel› have "(p ∙ Ψ, p ∙ P', p ∙ p ∙ Q') ∈ Rel"
      by(auto simp add: eqvt_def)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S ‹distinctPerm p›
    have "(Ψ, p ∙ P', Q') ∈ Rel" by simp
    ultimately show ?thesis using ‹α=¡M⦇ν*yvec⦈⟨N⟩› by blast
  next
    case cTau
    from ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹α = τ› ‹xvec ♯* Q› have "xvec ♯* Q'"
      by(blast dest: tauFreshChainDerivative)
    with ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹α = τ›
    show ?thesis
      using Sim by simp
  qed
qed

lemma simIFresh[consumes 4, case_names cSim]:
  fixes Ψ   :: 'b
    and P   :: "('a, 'b, 'c) psi"
    and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q   :: "('a, 'b, 'c) psi"
    and x   :: name
    and C   :: "'d::fs_name"

assumes Eqvt: "eqvt Rel"
  and   "x ♯ Ψ"
  and   "x ♯ P"
  and   "x ♯ Q"
  and   "⋀α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* P; bn α ♯* Q; bn α ♯* Ψ;
                    bn α ♯* subject α; distinct(bn α); bn α ♯* C; x ♯ α; x ♯ Q'⟧ ⟹
                    ∃P'. Ψ ⊳ P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"

shows "Ψ ⊳ P ↝[Rel] Q"
  using assms
  by (auto intro: simIChainFresh[where xvec="[x]" and C=C])

lemma simE:
  fixes F   :: 'b
    and P   :: "('a, 'b, 'c) psi"
    and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q   :: "('a, 'b, 'c) psi"

assumes "Ψ ⊳ P ↝[Rel] Q"

shows "⋀α Q'. ⟦Ψ ⊳ Q ⟼α ≺ Q'; bn α ♯* Ψ; bn α ♯* P⟧ ⟹ ∃P'. Ψ ⊳ P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
  using assms
  by(auto simp add: simulation_def)

lemma simClosedAux:
  fixes Ψ   :: 'b
    and P   :: "('a, 'b, 'c) psi"
    and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q   :: "('a, 'b, 'c) psi"
    and p   :: "name prm"

assumes EqvtRel: "eqvt Rel"
  and   PSimQ: "Ψ ⊳ P ↝[Rel] Q"

shows "(p ∙ Ψ) ⊳ (p ∙ P) ↝[Rel] (p ∙ Q)"
  using EqvtRel
proof(induct rule: simI[of _ _ _ _ "(Ψ, P, p)"])
  case(cSim α Q')
  from ‹p ∙ Ψ ⊳ p ∙ Q ⟼α ≺ Q'›
  have "(rev p ∙ p ∙ Ψ) ⊳ (rev p ∙ p ∙ Q) ⟼(rev p ∙ (α ≺ Q'))"
    by(blast dest: semantics.eqvt)
  then have "Ψ ⊳ Q ⟼(rev p ∙ α) ≺ (rev p ∙ Q')"
    by(simp add: eqvts)
  moreover with ‹bn α ♯* (Ψ, P, p)› have "bn α ♯* Ψ" and "bn α ♯* P" and "bn α ♯* p" by simp+
  ultimately obtain P' where PTrans: "Ψ ⊳ P ⟼(rev p ∙ α) ≺ P'"
    and P'RelQ': "(Ψ, P', rev p ∙ Q') ∈ Rel"
    using PSimQ
    by(force dest: simE freshChainPermSimp simp add: eqvts)
  from PTrans have "(p ∙ Ψ) ⊳ (p ∙ P) ⟼(p ∙ ((rev p ∙ α) ≺ P'))"
    by(rule semantics.eqvt)
  with ‹bn α ♯* p› have "(p ∙ Ψ) ⊳ (p ∙ P) ⟼α ≺ (p ∙ P')"
    by(simp add: eqvts freshChainPermSimp)
  moreover from P'RelQ' EqvtRel have "(p ∙ (Ψ, P', rev p ∙ Q')) ∈ Rel"
    by(simp only: eqvt_def)
  then have "(p ∙ Ψ, p ∙ P', Q') ∈ Rel" by simp
  ultimately show ?case by blast
qed

lemma simClosed:
  fixes Ψ   :: 'b
    and P   :: "('a, 'b, 'c) psi"
    and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q   :: "('a, 'b, 'c) psi"
    and p   :: "name prm"

assumes EqvtRel: "eqvt Rel"

shows "Ψ ⊳ P ↝[Rel] Q ⟹ (p ∙ Ψ) ⊳ (p ∙ P) ↝[Rel] (p ∙ Q)"
  and "P ↝[Rel] Q ⟹ (p ∙ P) ↝[Rel] (p ∙ Q)"
  using EqvtRel
  by(force dest: simClosedAux simp add: permBottom)+

lemma reflexive:
  fixes Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Ψ   :: 'b
    and P   :: "('a, 'b, 'c) psi"

assumes "{(Ψ, P, P) | Ψ P. True} ⊆ Rel"

shows "Ψ ⊳ P ↝[Rel] P"
  using assms
  by(auto simp add: simulation_def)

lemma transitive:
  fixes Ψ     :: 'b
    and P     :: "('a, 'b, 'c) psi"
    and Rel   :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q     :: "('a, 'b, 'c) psi"
    and Rel'  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and R     :: "('a, 'b, 'c) psi"
    and Rel'' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

assumes PSimQ: "Ψ ⊳ P ↝[Rel] Q"
  and   QSimR: "Ψ ⊳ Q ↝[Rel'] R"
  and   Eqvt: "eqvt Rel''"
  and   Set: "{(Ψ, P, R) | Ψ P R. ∃Q. (Ψ, P, Q) ∈ Rel ∧ (Ψ, Q, R) ∈ Rel'} ⊆ Rel''"

shows "Ψ ⊳ P ↝[Rel''] R"
  using ‹eqvt Rel''›
proof(induct rule: simI[where C=Q])
  case(cSim α R')
  from QSimR ‹Ψ ⊳ R ⟼α ≺ R'› ‹(bn α) ♯* Ψ› ‹(bn α) ♯* Q›
  obtain Q' where QTrans: "Ψ ⊳ Q ⟼α ≺ Q'" and Q'Rel'R': "(Ψ, Q', R') ∈ Rel'"
    by(blast dest: simE)
  from PSimQ QTrans ‹bn α ♯* Ψ› ‹bn α ♯* P›
  obtain P' where PTrans: "Ψ ⊳ P ⟼α ≺ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
    by(blast dest: simE)
  with PTrans Q'Rel'R' P'RelQ' Set
  show ?case by blast
qed

lemma statEqSim:
  fixes Ψ   :: 'b
    and P   :: "('a, 'b, 'c) psi"
    and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q   :: "('a, 'b, 'c) psi"
    and Ψ'  :: 'b

assumes PSimQ: "Ψ ⊳ P ↝[Rel] Q"
  and   "eqvt Rel'"
  and   "Ψ ≃ Ψ'"
  and   C1: "⋀Ψ'' R S Ψ'''. ⟦(Ψ'', R, S) ∈ Rel; Ψ'' ≃ Ψ'''⟧ ⟹ (Ψ''', R, S) ∈ Rel'"

shows "Ψ' ⊳ P ↝[Rel'] Q"
  using ‹eqvt Rel'›
proof(induct rule: simI[of _ _ _ _ Ψ])
  case(cSim α Q')
  from ‹Ψ' ⊳ Q ⟼α ≺ Q'› ‹Ψ ≃ Ψ'›
  have "Ψ ⊳ Q ⟼α ≺ Q'" by(metis statEqTransition AssertionStatEqSym)
  with PSimQ ‹bn α ♯* Ψ› ‹bn α ♯* P›
  obtain P' where "Ψ ⊳ P ⟼α ≺ P'" and "(Ψ, P', Q') ∈ Rel"
    by(blast dest: simE)

  from ‹Ψ ⊳ P ⟼α ≺ P'› ‹Ψ ≃ Ψ'› have "Ψ' ⊳ P ⟼α ≺ P'"
    by(rule statEqTransition)
  moreover from ‹(Ψ, P', Q') ∈ Rel› ‹Ψ ≃ Ψ'› have "(Ψ', P', Q') ∈ Rel'"
    by(rule C1)
  ultimately show ?case by blast
qed

lemma monotonic:
  fixes Ψ :: 'b
    and P :: "('a, 'b, 'c) psi"
    and A :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and Q :: "('a, 'b, 'c) psi"
    and B :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

assumes "Ψ ⊳ P ↝[A] Q"
  and   "A ⊆ B"

shows "Ψ ⊳ P ↝[B] Q"
  using assms
  by(simp (no_asm) add: simulation_def) (auto dest: simE)

end

end