(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Simulation
  imports Semantics
begin

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(auto simp add: simulation_def)
  fix α Q'
  assume "Ψ ⊳ Q ⟼α ≺ Q'" and "bn α ♯* Ψ" and "bn α ♯* P"
  thus "∃P'. Ψ ⊳ P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
  proof(nominal_induct α rule: action.strong_induct)
    case(In M N)
    thus ?case by(rule_tac Sim) auto
  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_tac xvec=xvec and c="(Ψ, M, Q, N, P, Q', xvec, C)" in name_list_avoiding)
          (auto simp add: eqvts fresh_star_prod)

      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 hence "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(drule_tac Sim) auto
      hence "(p ∙ Ψ) ⊳ (p ∙ P) ⟼(p ∙ (M(ν*(p ∙ xvec))⟨(p ∙ N)⟩ ≺ P'))"
        by(rule_tac 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(rule_tac outputPermSubject)
         (simp add: fresh_star_def | assumption)+

      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_tac x="(Ψ, P', p ∙ Q')" in ballE)
        apply(erule_tac x="p" in allE)
        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
    thus ?case by(rule_tac Sim) auto
  qed
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 add: freshChainSym)+ 
  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_tac c="(Ψ, P, Q, α)" and xvec=xvec in name_list_avoiding) 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(fastforce 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(rule_tac inputFreshChainDerivative)
    ultimately have "∃P'. Ψ ⊳ P ⟼ (p ∙ M)((p ∙ N)) ≺ P' ∧ (Ψ, P', (p ∙ Q')) ∈ Rel"
      by(rule_tac Sim) (assumption | simp)+
    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(fastforce 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')"
      by(drule_tac outputFreshChainDerivative(2)) (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(rule_tac Sim) auto
    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 by(drule_tac Sim) auto
  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(rule_tac xvec="[x]" and C=C in simIChainFresh) auto

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)
  hence "Ψ ⊳ 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)
  hence "(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