Quelle  Simulation.thy

(* 
   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›\<open>bn α ♯* xvec› ‹bn α ♯* C› ‹yvec ♯* M› ‹α=M(ν*yvec)⟨N⟩› ‹distinct yvec›
      by(rule_tac Sim) auto
    then obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*yvec\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'" and P'RelQ': "(\<Psi>, P', (p \<bullet> Q')) \<in> Rel"
      by blast
    from PTrans have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<longmapsto> (p \<bullet> ((p \<bullet> M)\<lparr>\<nu>*yvec\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'))"
      by(rule semantics.eqvt)
    with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> S \<open>distinctPerm p\<close> \<open>bn \<alpha> \<sharp>* xvec\<close> \<open>(p \<bullet> xvec) \<sharp>* \<alpha>\<close> \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close>
    have "\<Psi> \<rhd> P \<longmapsto> M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle> \<prec> (p \<bullet> P')" by(simp add: eqvts)
    moreover from P'RelQ' \<open>eqvt Rel\<close> have "(p \<bullet> \<Psi>, p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel"
      by(auto simp add: eqvt_def)
    with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> S \<open>distinctPerm p\<close>
    have "(\<Psi>, p \<bullet> P', Q') \<in> Rel" by simp
    ultimately show ?thesis using \<open>\<alpha>=M\<lparr>\<nu>*yvec\<rparr>\<langle>N\<rangle>\<close> by blast
  next
    case cTau
    from \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<alpha> = \<tau>\<close> \<open>xvec \<sharp>* Q\<close> have "xvec \<sharp>* Q'"
      by(blast dest: tauFreshChainDerivative)
    with \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<alpha> = \<tau>\<close> 
    show ?thesis by(drule_tac Sim) auto
  qed
qed

lemma simIFresh[consumes 4, case_names cSim]:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('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 \<sharp> \<Psi>"
  and     "x \<sharp> P"
  and     "x \<sharp> Q"
  and     "\<And>\<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* \<Psi>;
                    bn \<alpha> \<sharp>* subject \<alpha>; distinct(bn \<alpha>); bn \<alpha> \<sharp>* C; x \<sharp> \<alpha>; x \<sharp> Q'\<rbrakk> \<Longrightarrow>
                    \<exists>P'. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel"

  shows "\<Psi> \<rhd> P \<leadsto>[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 \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<leadsto>[Rel] Q"

  shows "\<And>\<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P' \<and> (\<Psi>, P', Q') \<in> Rel"
using assms
by(auto simp add: simulation_def)

lemma simClosedAux:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   p   :: "name prm"

  assumes EqvtRel: "eqvt Rel"
  and     PSimQ: "\<Psi> \<rhd> P \<leadsto>[Rel] Q"

  shows "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<leadsto>[Rel] (p \<bullet> Q)"
using EqvtRel
proof(induct rule: simI[of _ _ _ _ "(\<Psi>, P, p)"])
  case(cSim \<alpha> Q')
  from \<open>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto>\<alpha> \<prec> Q'\<close> 
  have "(rev p \<bullet> p \<bullet> \<Psi>) \<rhd> (rev p \<bullet> p \<bullet> Q) \<longmapsto>(rev p \<bullet> (\<alpha> \<prec> Q'))"
    by(blast dest: semantics.eqvt)
  hence "\<Psi> \<rhd> Q \<longmapsto>(rev p \<bullet> \<alpha>) \<prec> (rev p \<bullet> Q')"
    by(simp add: eqvts)
  moreover with \<open>bn \<alpha> \<sharp>* (\<Psi>, P, p)\<close> have "bn \<alpha> \<sharp>* \<Psi>" and "bn \<alpha> \<sharp>* P" and "bn \<alpha> \<sharp>* p" by simp+
  ultimately obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto>(rev p \<bullet> \<alpha>) \<prec> P'"
                         and P'RelQ': "(\<Psi>, P', rev p \<bullet> Q') \<in> Rel"
    using PSimQ
    by(force dest: simE freshChainPermSimp simp add: eqvts)
  from PTrans have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<longmapsto>(p \<bullet> ((rev p \<bullet> \<alpha>) \<prec> P'))"
    by(rule semantics.eqvt)
  with \<open>bn \<alpha> \<sharp>* p\<close> have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<longmapsto>\<alpha> \<prec> (p \<bullet> P')"
    by(simp add: eqvts freshChainPermSimp)
  moreover from P'RelQ' EqvtRel have "(p \<bullet> (\<Psi>, P', rev p \<bullet> Q')) \<in> Rel"
    by(simp only: eqvt_def)
  hence "(p \<bullet> \<Psi>, p \<bullet> P', Q') \<in> Rel" by simp
  ultimately show ?case by blast
qed

lemma simClosed:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   p   :: "name prm"

  assumes EqvtRel: "eqvt Rel"

  shows "\<Psi> \<rhd> P \<leadsto>[Rel] Q \<Longrightarrow> (p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<leadsto>[Rel] (p \<bullet> Q)"
  and   "P \<leadsto>[Rel] Q \<Longrightarrow> (p \<bullet> P) \<leadsto>[Rel] (p \<bullet> Q)"
using EqvtRel
by(force dest: simClosedAux simp add: permBottom)+

lemma reflexive:
  fixes Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"

  assumes "{(\<Psi>, P, P) | \<Psi> P. True} \<subseteq> Rel"

  shows "\<Psi> \<rhd> P \<leadsto>[Rel] P"
using assms
by(auto simp add: simulation_def)

lemma transitive:
  fixes \<Psi>     :: 'b
  and   P     :: "('a, 'b, 'c) psi"
  and   Rel   :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q     :: "('a, 'b, 'c) psi"
  and   Rel'  :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   R     :: "('a, 'b, 'c) psi"
  and   Rel'' :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"

  assumes PSimQ: "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
  and     QSimR: "\<Psi> \<rhd> Q \<leadsto>[Rel'] R"
  and     Eqvt: "eqvt Rel''"
  and     Set: "{(\<Psi>, P, R) | \<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''"

  shows "\<Psi> \<rhd> P \<leadsto>[Rel''] R"
using \<open>eqvt Rel''\<close>
proof(induct rule: simI[where C=Q])
  case(cSim \<alpha> R')
  from QSimR \<open>\<Psi> \<rhd> R \<longmapsto>\<alpha> \<prec> R'\<close> \<open>(bn \<alpha>) \<sharp>* \<Psi>\<close> \<open>(bn \<alpha>) \<sharp>* Q\<close>
  obtain Q' where QTrans: "\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'" and Q'Rel'R': "(\<Psi>, Q', R') \<in> Rel'"
    by(blast dest: simE)
  from PSimQ QTrans \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close>
  obtain P' where PTrans: "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
    by(blast dest: simE)
  with PTrans Q'Rel'R' P'RelQ' Set
  show ?case by blast
qed

lemma statEqSim:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   \<Psi>'  :: 'b

  assumes PSimQ: "\<Psi> \<rhd> P \<leadsto>[Rel] Q"
  and     "eqvt Rel'"
  and     "\<Psi> \<simeq> \<Psi>'"
  and     C1: "\<And>\<Psi>'' R S \<Psi>'''. \<lbrakk>(\<Psi>'', R, S) \<in> Rel; \<Psi>'' \<simeq> \<Psi>'''\<rbrakk> \<Longrightarrow> (\<Psi>''', R, S) \<in> Rel'"

  shows "\<Psi>' \<rhd> P \<leadsto>[Rel'] Q"
using \<open>eqvt Rel'\<close>
proof(induct rule: simI[of _ _ _ _ \<Psi>])
  case(cSim \<alpha> Q')
  from \<open>\<Psi>' \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close>
  have "\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'" by(metis statEqTransition AssertionStatEqSym)
  with PSimQ \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close>
  obtain P' where "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'" and "(\<Psi>, P', Q') \<in> Rel"
    by(blast dest: simE)
  
  from \<open>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close> have "\<Psi>' \<rhd> P \<longmapsto>\<alpha> \<prec> P'"
    by(rule statEqTransition)
  moreover from \<open>(\<Psi>, P', Q') \<in> Rel\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close> have "(\<Psi>', P', Q') \<in> Rel'"
    by(rule C1)
  ultimately show ?case by blast
qed

lemma monotonic: 
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   A :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q :: "('a, 'b, 'c) psi"
  and   B :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"

  assumes "\<Psi> \<rhd> P \<leadsto>[A] Q"
  and     "A \<subseteq> B"

  shows "\<Psi> \<rhd> P \<leadsto>[B] Q"
using assms
by(simp (no_asm) add: simulation_def) (auto dest: simE)

end

end