Theory Weak_Simulation

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

context env begin

definition
  "weakSimulation" :: "'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''. Ψ : Q  P α  P''  (P'. Ψ  Ψ'  P'' ^τ P'  (Ψ  Ψ', P', Q')  Rel)))  
                      (Q'. Ψ  Q τ  Q'  (P'. Ψ  P ^τ P'  (Ψ, P', Q')  Rel))"

abbreviation
  weakSimulationNilJudge ("_ ↝<_> _" [80, 80, 80] 80) where "P ↝<Rel> Q  SBottom'  P ↝<Rel> Q"

lemma weakSimI[consumes 1, case_names cAct cTau]:
  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     rAct: "Ψ' α Q'. Ψ  Q α  Q';  bn α ♯* Ψ; bn α ♯* P; bn α ♯* Q;
                              bn α ♯* subject α; bn α ♯* C; distinct(bn α); α  τ 
                                         
                              P''. Ψ : Q  P α  P''  (P'. Ψ  Ψ'  P'' ^τ P'  (Ψ  Ψ', P', Q')  Rel)"
  and     rTau:  "Q'. Ψ  Q τ  Q'  P'. Ψ  P ^τ P'  (Ψ, P', Q')  Rel"

  shows "Ψ  P ↝<Rel> Q"
proof(auto simp add: weakSimulation_def)
  fix Ψ' α Q'
  assume "Ψ  Q α  Q'" and "bn α ♯* Ψ" and "bn α ♯* P" and "α  τ"
  thus "P''. Ψ : Q  P α  P''  (P'. Ψ  Ψ'  P'' ^τ P'  (Ψ  Ψ', P', Q')  Rel)"
  proof(nominal_induct α rule: action.strong_induct)
    case(In M N)
    thus ?case by(rule_tac rAct) auto
  next
    case(Out M xvec N)
    from bn(M⦇ν*xvec⦈⟨N) ♯* Ψ bn(M⦇ν*xvec⦈⟨N) ♯* P have "xvec ♯* Ψ" and "xvec ♯* P" by simp+
    from Ψ  Q M⦇ν*xvec⦈⟨N  Q' have "distinct xvec" by(force dest: boundOutputDistinct)
    obtain p where "(p  xvec) ♯* Ψ" and "(p  xvec) ♯* M" and "(p  xvec) ♯* xvec"
               and"(p  xvec) ♯* P" and "(p  xvec) ♯* Q" and "(p  xvec) ♯* Q'" and "(p  xvec) ♯* Ψ'"
               and "(p  xvec) ♯* C" and "(p  xvec) ♯* xvec" and "(p  xvec) ♯* N"
               and S: "(set p)  (set xvec) × (set(p  xvec))" and "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 distinct xvec have "distinct(p  xvec)" by simp
    from Ψ  Q M⦇ν*xvec⦈⟨N  Q' (p  xvec) ♯* N (p  xvec) ♯* Q' S 
    have "Ψ  Q M⦇ν*(p  xvec)⦈⟨(p  N)  (p  Q')" by(simp add: boundOutputChainAlpha'' residualInject)

    then obtain P'' P' where PTrans: "Ψ : Q  P M⦇ν*(p  xvec)⦈⟨(p  N)  P''" 
                         and P''Chain: "Ψ  (p  Ψ')  P'' ^τ P'"
                         and P'RelQ': "(Ψ  (p  Ψ'), P', p  Q')  Rel"
      using (p  xvec) ♯* Ψ (p  xvec) ♯* P (p  xvec) ♯* Q (p  xvec) ♯* M (p  xvec) ♯* C distinct(p  xvec)
      by(drule_tac Ψ'="p  Ψ'" in rAct) auto

    from PTrans S distinctPerm p xvec ♯* P (p  xvec) ♯* xvec (p  xvec) ♯* M distinct xvec 
    have "Ψ : Q  P M⦇ν*xvec⦈⟨N  (p  P'')" 
      by(rule_tac weakOutputAlpha) auto
    moreover from P''Chain have "(p  (Ψ  (p  Ψ')))  (p  P'') ^τ (p  P')" by(rule eqvts)
    with xvec ♯* Ψ (p  xvec) ♯* Ψ (p  xvec) ♯* Ψ' S distinctPerm p
    have "Ψ  Ψ'  (p  P'') ^τ (p  P')" by(simp add: eqvts)
    moreover from P'RelQ' Eqvt S distinctPerm p have "(p  (Ψ  (p  Ψ')), p  P', p  p  Q')  Rel"
      apply(simp add: eqvt_def eqvts)
      apply(erule_tac x="(Ψ  (p  Ψ'), P', p  Q')" in ballE)
      apply(erule_tac x="p" in allE)
      by(auto simp add: eqvts)
    with xvec ♯* Ψ (p  xvec) ♯* Ψ S distinctPerm p
    have "(Ψ  Ψ', p  P', Q')  Rel" by(simp add: eqvts)
    ultimately show ?case by blast
  next
    case Tau
    thus ?case by simp
  qed
next
  fix Q'
  assume "Ψ  Q τ  Q'"
  thus "P'. Ψ  P ^τ P'  (Ψ, P', Q')  Rel"
    by(rule rTau)
qed

lemma weakSimI2[case_names cAct cTau]:
  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 rOutput: "Ψ' α Q'. Ψ  Q α  Q';  bn α ♯* Ψ; bn α ♯* P; α  τ 
                                P''. Ψ : Q  P α  P''  (P'. Ψ  Ψ'  P'' ^τ P'  (Ψ  Ψ', P', Q')  Rel)"
  and     rTau:  "Q'. Ψ  Q τ  Q'  P'. Ψ  P ^τ P'  (Ψ, P', Q')  Rel"

  shows "Ψ  P ↝<Rel> Q"
using assms by(simp add: weakSimulation_def)

lemma weakSimIChainFresh[consumes 4, case_names cOutput cInput]:
  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   yvec :: "name list"
  and   C    :: "'d::fs_name"

  assumes Eqvt: "eqvt Rel"
  and     "yvec ♯* Ψ"
  and     "yvec ♯* P"
  and     "yvec ♯* Q"
  and     rAct: "Ψ' α Q'. Ψ  Q α  Q'; bn α ♯* Ψ; bn α ♯* P; bn α ♯* Q; α  τ;
                             bn α ♯* subject α; bn α ♯* C; yvec ♯* α; yvec ♯* Q'; yvec ♯* Ψ' 
                             P''. Ψ : Q  P α  P''  (P'. Ψ  Ψ'  P'' ^τ P'  (Ψ  Ψ', P', Q')  Rel)"
  and     rTau: "Q'. Ψ  Q τ  Q'; yvec ♯* Q'  P'. Ψ  P ^τ P'  (Ψ, P', Q')  Rel"

  shows "Ψ  P ↝<Rel> Q"
using eqvt Rel
proof(induct rule: weakSimI[of _ _ _ _ "(yvec, C)"])
  case(cAct Ψ' α Q')
  obtain p::"name prm" where "(p  yvec) ♯* Ψ" and "(p  yvec) ♯* P" and  "(p  yvec) ♯* Q"
                         and  "(p  yvec) ♯* α" and "(p  yvec) ♯* Ψ'"
                         and "(p  yvec) ♯* Q'" and S: "(set p)  set yvec × set(p  yvec)"
                         and "distinctPerm p"
    by(rule_tac c="(Ψ, P, Q, α, Q', Ψ')" and xvec=yvec in name_list_avoiding) auto
  from bn α ♯* (yvec, C) have "bn α ♯* yvec" and "bn α ♯* C" by(simp add: freshChainSym)+ 
  show ?case
  proof(cases rule: actionCases[where α = α])
    case(cInput M N)
    from (p  yvec) ♯* α α = MN have "(p  yvec) ♯* M" and  "(p  yvec) ♯* N" by simp+
    from Ψ  Q α  Q' α = MN yvec ♯* Ψ (p  yvec) ♯* Ψ yvec ♯* Q (p  yvec) ♯* Q S
    have "Ψ  Q (p  M)(p  N)  (p  Q')" 
      by(drule_tac pi=p in semantics.eqvt) (simp add: eqvts)
    moreover from (p  yvec) ♯* M have "(p  (p  yvec)) ♯* (p  M)"
      by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with distinctPerm p have "yvec ♯* (p  M)" by simp
    moreover from (p  yvec) ♯* N have "(p  p  yvec) ♯* (p  N)" 
      by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with distinctPerm p have "yvec ♯* (p  N)" by simp
    moreover from (p  yvec) ♯* Q' have "(p  p  yvec) ♯* (p  Q')" 
      by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with distinctPerm p have "yvec ♯* (p  Q')" by simp
    moreover from (p  yvec) ♯* Ψ' have "(p  p  yvec) ♯* (p  Ψ')"
      by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with distinctPerm p have "yvec ♯* (p  Ψ')" by simp
    ultimately obtain P' P'' where PTrans: "Ψ : Q  P (p  M)(p  N)  P''" and P''Chain: "Ψ  (p  Ψ')  P'' ^τ P'"
                               and P'RelQ': "(Ψ  (p  Ψ'), P', (p  Q'))  Rel"
      by(auto dest: rAct)
    from PTrans have "(p  Ψ) : (p  Q)  (p  P) p  ((p  M)(p  N))  (p  P'')"
      by(rule weakTransitionClosed)
    with S yvec ♯* Ψ (p  yvec) ♯* Ψ yvec ♯* Q (p  yvec) ♯* Q yvec ♯* P (p  yvec) ♯* P distinctPerm p
    have "Ψ : Q  P MN  (p  P'')" by(simp add: eqvts)
    moreover from P''Chain have  "(p  (Ψ  (p  Ψ')))  (p  P'') ^τ (p  P')" by(rule eqvts)
    with yvec ♯* Ψ (p  yvec) ♯* Ψ S distinctPerm p 
    have "Ψ  Ψ'  (p  P'') ^τ (p  P')" by(simp add: eqvts)
    moreover from P'RelQ' Eqvt have "(p  (Ψ  (p  Ψ')), p  P', p  p  Q')  Rel"
      apply(simp add: eqvt_def eqvts)
      apply(erule_tac x="(Ψ  (p  Ψ'), P', p  Q')" in ballE)
      apply(erule_tac x="p" in allE)
      by(auto simp add: eqvts)
    with yvec ♯* Ψ (p  yvec) ♯* Ψ S distinctPerm p have "(Ψ  Ψ', p  P', Q')  Rel" by(simp add: eqvts)
    ultimately show ?thesis using α=MN by blast
  next
    case(cOutput M xvec N)
    from bn α ♯* Ψ bn α ♯* P bn α ♯* Q  bn α ♯* subject α α=M⦇ν*xvec⦈⟨N bn α ♯* yvec
         (p  yvec) ♯* α bn α ♯* C bn α ♯* subject α distinct(bn α)
    have "xvec ♯* Ψ" and "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* M" and "yvec ♯* xvec"
     and "(p  yvec) ♯* M" and "(p  yvec) ♯* xvec" and "xvec ♯* C" and "xvec ♯* M" and "(p  yvec) ♯* N" 
     and "distinct xvec" by simp+
    from Ψ  Q α  Q' yvec ♯* Ψ (p  yvec) ♯* Ψ yvec ♯* Q (p  yvec) ♯* Q S α=M⦇ν*xvec⦈⟨N
    have "Ψ  Q (p  M)⦇ν*xvec⦈⟨N  Q'"
      by(rule_tac outputPermSubject) (assumption | simp add: fresh_star_def)+
    moreover note xvec ♯* Ψ xvec ♯* P 
    moreover note xvec ♯* Q
    moreover from xvec ♯* M have "(p  xvec) ♯* (p  M)"
      by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with yvec ♯* xvec (p  yvec) ♯* xvec S have "xvec ♯* (p  M)"
      by simp
    moreover note xvec ♯* C
    moreover from (p  yvec) ♯* M have "(p  (p  yvec)) ♯* (p  M)"
      by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with distinctPerm p have "yvec ♯* (p  M)" by simp
    moreover note yvec ♯* xvec
    moreover from Ψ  Q α  Q' yvec ♯* Q yvec ♯* xvec α=M⦇ν*xvec⦈⟨N xvec ♯* M distinct xvec
    have "yvec ♯* N" and "yvec ♯* Q'"  by(force dest: outputFreshChainDerivative)+
    moreover from (p  yvec) ♯* Ψ' have "(p  p  yvec) ♯* (p  Ψ')"
      by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with distinctPerm p have "yvec ♯* (p  Ψ')" by simp
    ultimately obtain P'' P' where PTrans: "Ψ : Q  P (p  M)⦇ν*xvec⦈⟨N  P''"
                               and PChain: "Ψ  (p  Ψ')  P'' ^τ P'"
                               and P'RelQ': "(Ψ  (p  Ψ'), P', Q')  Rel"
      by(drule_tac rAct) auto
    from PTrans have "(p  Ψ) : (p  Q)  (p  P) (p  ((p  M)⦇ν*xvec⦈⟨N))  (p  P'')" 
      by(rule eqvts)
    with S yvec ♯* Ψ (p  yvec) ♯* Ψ yvec ♯* P (p  yvec) ♯* P yvec ♯* Q (p  yvec) ♯* Q yvec ♯* xvec (p  yvec) ♯* xvec 
      yvec ♯* N (p  yvec) ♯* N distinctPerm p have "Ψ : Q  P M⦇ν*xvec⦈⟨N  (p  P'')"
      by(simp add: eqvts)
    moreover from PChain have "(p  (Ψ  (p  Ψ')))  (p  P'') ^τ (p  P')" by(rule eqvts)
    with S yvec ♯* Ψ (p  yvec) ♯* Ψ distinctPerm p have "Ψ  Ψ'  (p  P'') ^τ (p  P')" by(simp add: eqvts)
    moreover from P'RelQ' eqvt Rel have "p  (Ψ  (p  Ψ'), P', Q')  Rel"
      by(simp add: eqvt_def) auto
    with yvec ♯* Ψ (p  yvec) ♯* Ψyvec ♯* Q' (p  yvec) ♯* Q' S distinctPerm p 
    have "(Ψ  Ψ', p  P', Q')  Rel" by(simp add: eqvts)
    ultimately show ?thesis using α=M⦇ν*xvec⦈⟨N by blast
  next
    case cTau
    from α = τ α  τ have "False" by simp
    thus ?thesis by simp
  qed
next
  case(cTau Q')
  from Ψ  Q τ  Q' yvec ♯* Q have "yvec ♯* Q'"
    by(force dest: tauFreshChainDerivative)
  with Ψ  Q τ  Q' show ?case
    by(rule rTau)
qed

lemma weakSimIFresh[consumes 4, case_names cAct cTau]:
  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 α ♯* Ψ; bn α ♯* P; bn α ♯* Q; α  τ;
                       bn α ♯* subject α; bn α ♯* C; x  α; x  Q'; x  Ψ' 
                       P''. Ψ : Q  P α  P''  (P'. Ψ  Ψ'  P'' ^τ P'  (Ψ  Ψ', P', Q')  Rel)"
  and     "Q'. Ψ  Q τ  Q'; x  Q'  P'. Ψ  P ^τ P'  (Ψ, P', Q')  Rel"

  shows "Ψ  P ↝<Rel> Q"
using assms
by(rule_tac yvec="[x]" and C=C in weakSimIChainFresh) auto

lemma weakSimE:
  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''. Ψ : Q  P α  P''  (P'. Ψ  Ψ'  P'' ^τ P'  (Ψ  Ψ', P', Q')  Rel)"
  and   "Q'. Ψ  Q τ  Q'  P'. Ψ  P ^τ P'  (Ψ, P', Q')  Rel"
using assms
by(auto simp add: weakSimulation_def)

lemma weakSimClosedAux:
  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: weakSimI[of _ _ _ _ "(Ψ, P, p)"])
  case(cAct Ψ' α 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+
  moreover from α  τ have "(rev p  α)  τ"
    by(cases rule: actionCases[where α=α]) auto
  ultimately obtain P'' P' where PTrans: "Ψ : Q  P (rev p  α)  P''"
                          and P''Chain: "Ψ  (rev p  Ψ')  P'' ^τ P'" and P'RelQ': "(Ψ  (rev p  Ψ'), P', rev p  Q')  Rel"
    using α  τ PSimQ
    by(drule_tac Ψ'="rev p  Ψ'" in weakSimE(1)) (auto simp add: freshChainPermSimp bnEqvt[symmetric])

  from PTrans have "(p  Ψ) : (p  Q)  (p  P) (p  (rev p  α))  (p  P'')"
    by(rule eqvts)
  hence "(p  Ψ) : (p  Q)  (p  P) α  (p  P'')" by(simp add: eqvts freshChainPermSimp)
  moreover from P''Chain have  "(p  (Ψ  (rev p  Ψ')))  (p  P'') ^τ (p  P')" by(rule eqvts)
  hence "(p  Ψ)  Ψ'  (p  P'') ^τ (p  P')" by(simp add: eqvts)
  moreover from P'RelQ' EqvtRel have "(p  ((Ψ  (rev p  Ψ')), P', rev p  Q'))  Rel"
    by(simp only: eqvt_def)
  hence "((p  Ψ)  Ψ', p  P', Q')  Rel" by(simp add: eqvts)
  ultimately show ?case by blast
next
  case(cTau 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  Q')" by(simp add: eqvts)
  with PSimQ obtain P' where PChain: "Ψ  P ^τ P'" and P'RelQ': "(Ψ, P', rev p  Q')  Rel"
    by(blast dest: weakSimE)
  from PChain have "(p  Ψ)  (p  P) ^τ (p  P')" by(rule tauChainEqvt)
  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 add: eqvts)
  ultimately show ?case
    by blast
qed

lemma weakSimClosed:
  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: weakSimClosedAux simp add: permBottom)+

lemma weakSimReflexive:
  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: weakSimulation_def weakTransition_def dest: rtrancl_into_rtrancl) force+

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

  assumes "Ψ  Q ^τ Q'"
  and     "(Ψ, P, Q)  Rel"
  and     Sim: "Ψ' R S. (Ψ', R, S)  Rel  Ψ'  R ↝<Rel> S"
  
  obtains P' where "Ψ  P ^τ P'" and "(Ψ, P', Q')  Rel"
proof -
  assume A: "P'. Ψ  P ^τ P'; (Ψ, P', Q')  Rel  thesis"
  from Ψ  Q ^τ Q' (Ψ, P, Q)  Rel A show ?thesis
  proof(induct arbitrary: P thesis rule: tauChainInduct)
    case(TauBase Q P)
    moreover have "Ψ  P ^τ P" by simp
    ultimately show ?case by blast
  next
    case(TauStep Q Q' Q'' P)
    from (Ψ, P, Q)  Rel obtain P' where PChain: "Ψ  P ^τ P'" and "(Ψ, P', Q')  Rel"
      by(rule TauStep)
    from (Ψ, P', Q')  Rel have "Ψ  P' ↝<Rel> Q'" by(rule Sim)
    then obtain P'' where P'Chain: "Ψ  P' ^τ P''" and "(Ψ, P'', Q'')  Rel"
      using Ψ  Q' τ  Q'' by(blast dest: weakSimE)
    from PChain P'Chain have "Ψ  P ^τ P''" by simp
    thus ?case using (Ψ, P'', Q'')  Rel by(rule TauStep)
  qed
qed

lemma weakSimE2:
  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"

  assumes PRelQ: "(Ψ, P, Q)  Rel"
  and     Sim: "Ψ' R S. (Ψ', R, S)  Rel  Ψ'  R ↝<Rel> S"
  and     QTrans: "Ψ : R  Q α  Q'"
  and     "bn α ♯* Ψ"
  and     "bn α ♯* P"
  and     "α  τ"

  obtains P'' P' where "Ψ : R  P α  P''" and "Ψ  Ψ'  P'' ^τ P'" and "(Ψ  Ψ', P', Q')  Rel"
proof -
  assume A: "P'' P'. Ψ : R  P α  P''; Ψ  Ψ'  P'' ^τ P'; (Ψ  Ψ', P', Q')  Rel  thesis"
  from QTrans obtain Q'' 
    where QChain: "Ψ  Q ^τ Q''" 
      and ReqQ'': "insertAssertion (extractFrame R) Ψ F insertAssertion (extractFrame Q'') Ψ"
      and Q''Trans: "Ψ  Q'' α  Q'"
    by(rule weakTransitionE)

  from QChain PRelQ Sim
  obtain P'' where PChain: "Ψ  P ^τ P''" and P''RelQ'': "(Ψ, P'', Q'')  Rel" by(rule weakSimTauChain)

  from PChain bn α ♯* P have "bn α ♯* P''" by(rule tauChainFreshChain)
  from P''RelQ'' have "Ψ  P'' ↝<Rel> Q''" by(rule Sim)
  with Q''Trans bn α ♯* Ψ bn α ♯* P'' α  τ
  obtain P''' P' where P''Trans: "Ψ : Q''  P'' α  P'''" and P'''Chain: "Ψ  Ψ'  P''' ^τ P'"
                   and P'RelQ': "(Ψ  Ψ', P', Q')  Rel"
    by(blast dest: weakSimE)
  
  from P''Trans obtain P'''' where P''Chain: "Ψ  P'' ^τ P''''"
                               and Q''eqP'''': "insertAssertion (extractFrame Q'') Ψ F insertAssertion (extractFrame P'''') Ψ"
                               and P''''Trans: "Ψ  P'''' α  P'''"
    by(rule weakTransitionE)
  from PChain P''Chain have "Ψ  P ^τ P''''" by simp
  moreover from ReqQ'' Q''eqP'''' have "insertAssertion (extractFrame R) Ψ F insertAssertion (extractFrame P'''') Ψ"
    by(rule FrameStatImpTrans)
  ultimately have "Ψ : R  P α  P'''" using P''''Trans by(rule weakTransitionI)
  with P'''Chain P'RelQ' A show ?thesis by blast
qed

lemma weakSimTransitive:
  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   T     :: "('a, 'b, 'c) psi"
  and   Rel'' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes PRelQ: "(Ψ, P, Q)  Rel"
  and     QSimR: "Ψ  Q ↝<Rel'> R"
  and     Eqvt: "eqvt Rel''"
  and     Set: "{(Ψ, P, R) | Ψ P R. Q. (Ψ, P, Q)  Rel  (Ψ, Q, R)  Rel'}  Rel''"
  and     Sim: "Ψ' R S. (Ψ', R, S)  Rel  Ψ'  R ↝<Rel> S"

  shows "Ψ  P ↝<Rel''> R"
using eqvt Rel''
proof(induct rule: weakSimI[of _ _ _ _ Q])
  case(cAct Ψ' α R')
  from QSimR Ψ  R α  R' bn α ♯* Ψ bn α ♯* Q α  τ
  obtain Q'' Q' where QTrans: "Ψ : R  Q α  Q''" and Q''Chain: "Ψ  Ψ'  Q'' ^τ Q'"
                  and Q'RelR': "(Ψ  Ψ', Q', R')  Rel'"
    by(blast dest: weakSimE)
  with PRelQ Sim QTrans bn α ♯* Ψ bn α ♯* P α  τ
  obtain P''' P'' where PTrans: "Ψ : R  P α  P'''" 
                and P'''Chain: "Ψ  Ψ'  P''' ^τ P''" and P''RelQ'': "(Ψ  Ψ', P'', Q'')  Rel"
    by(drule_tac weakSimE2) auto

  note PTrans
  moreover from Q''Chain P''RelQ'' Sim obtain P' where P''Chain: "Ψ  Ψ'  P'' ^τ P'" and P'RelQ': "(Ψ  Ψ', P', Q')  Rel"
    by(rule weakSimTauChain)
  from P'''Chain P''Chain have "Ψ  Ψ'  P''' ^τ P'" by simp
  moreover from P'RelQ' Q'RelR' Set have "(Ψ  Ψ', P', R')  Rel''" by blast
  ultimately show ?case by blast
next
  case(cTau R')
  from QSimR Ψ  R τ  R' obtain Q' where QChain: "Ψ  Q ^τ Q'" and Q'RelR': "(Ψ, Q', R')  Rel'" 
    by(blast dest: weakSimE)
  from QChain PRelQ Sim obtain P' where PChain: "Ψ  P ^τ P'" and P'RelQ': "(Ψ, P', Q')  Rel"
    by(rule weakSimTauChain)
  note PChain
  moreover from P'RelQ' Q'RelR' Set have "(Ψ, P', R')  Rel''" by blast
  ultimately show ?case by blast
qed

lemma weakSimStatEq:
  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: weakSimI[of _ _ _ _ Ψ])
  case(cAct Ψ'' α Q')
  from Ψ'  Q α  Q' Ψ  Ψ'
  have "Ψ  Q α  Q'" by(metis statEqTransition AssertionStatEqSym)
  with PSimQ bn α ♯* Ψ bn α ♯* P α  τ
  obtain P'' P' where PTrans: "Ψ : Q  P α  P''" and P''Chain: "Ψ  Ψ''  P'' ^τ P'" 
                  and P'RelQ': "(Ψ  Ψ'', P', Q')  Rel"
    by(blast dest: weakSimE)

  from PTrans Ψ  Ψ' have "Ψ' : Q  P α  P''" by(rule weakTransitionStatEq)
  moreover from P''Chain Ψ  Ψ' have "Ψ'  Ψ''  P'' ^τ P'" by(metis tauChainStatEq Composition)
  moreover from P'RelQ' Ψ  Ψ' have "(Ψ'  Ψ'', P', Q')  Rel'"
    by(metis C1 Composition)
  ultimately show ?case
    by blast
next
  case(cTau Q')
  from Ψ'  Q τ  Q' Ψ  Ψ'
  have "Ψ  Q τ  Q'" by(metis statEqTransition AssertionStatEqSym)
  with PSimQ obtain P' where PChain: "Ψ  P ^τ P'" and P'RelQ': "(Ψ, P', Q')  Rel"
    by(blast dest: weakSimE)
  
  from PChain Ψ  Ψ' have "Ψ'  P ^τ P'" by(rule tauChainStatEq)
  moreover from (Ψ, P', Q')  Rel Ψ  Ψ' have "(Ψ', P', Q')  Rel'"
    by(rule C1)
  ultimately show ?case by blast
qed

lemma weakSimMonotonic: 
  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: weakSimulation_def) (blast dest: weakSimE)+

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

  assumes PRelQ: "(Ψ, P, Q)  Rel"
  and     StatImp: "Ψ' R S. (Ψ', R, S)  Rel  insertAssertion(extractFrame S) Ψ' F insertAssertion(extractFrame R) Ψ'"
  and     Sim:     "Ψ' R S. (Ψ', R, S)  Rel  Ψ'  R ↝[Rel] S"
  and     Ext:     "Ψ' R S Ψ''. (Ψ', R, S)  Rel  (Ψ'  Ψ'', R, S)  Rel"

  shows "Ψ  P ↝<Rel> Q"
proof(induct rule: weakSimI2)
  case(cAct Ψ' α Q')
  from PRelQ have "Ψ  P ↝[Rel] Q" by(rule Sim)
  with Ψ  Q α  Q' bn α ♯* Ψ bn α ♯* P
  obtain P' where PTrans: "Ψ  P α  P'" and P'RelQ': "(Ψ, P', Q')  Rel"
    by(blast dest: simE)
  
  from PRelQ have "insertAssertion(extractFrame Q) Ψ F insertAssertion(extractFrame P) Ψ" by(rule StatImp)
  with PTrans have "Ψ : Q  P α  P'" by(rule transitionWeakTransition)
  moreover from P'RelQ' have "Ψ'. P''. Ψ  Ψ'  P' ^τ P''  (Ψ  Ψ', P'', Q')  Rel"
    by(force intro: Ext)
  ultimately show ?case by blast
next
  case(cTau Q')
  from PRelQ have "Ψ  P ↝[Rel] Q" by(rule Sim)
  with Ψ  Q τ  Q' obtain P' where PTrans: "Ψ  P τ  P'" and P'RelQ': "(Ψ, P', Q')  Rel"
    by(force dest: simE)
  with PTrans have "Ψ  P ^τ P'" by auto
  thus ?case using P'RelQ' by blast
qed

lemma strongAppend:
  fixes Ψ    :: 'b
  and   P     :: "('a, 'b, 'c) psi"
  and   Q     :: "('a, 'b, 'c) psi"
  and   R     :: "('a, 'b, 'c) psi"
  and   Rel   :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Rel'  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  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     RimpQ: "insertAssertion (extractFrame R) Ψ F insertAssertion (extractFrame Q) Ψ"
  and     Set: "{(Ψ, P, R) | Ψ P R. Q. (Ψ, P, Q)  Rel  (Ψ, Q, R)  Rel'}  Rel''"
  and     C1: "Ψ P Q Ψ'. (Ψ, P, Q)  Rel'  (Ψ  Ψ', P, Q)  Rel'"

  shows "Ψ  P ↝<Rel''> R"
proof -
  from Eqvt'' show ?thesis
  proof(induct rule: weakSimI[of _ _ _ _ Q])
    case(cAct Ψ' α R')
    from Ψ  Q ↝[Rel'] R Ψ  R α  R' bn α ♯* Ψ bn α ♯* Q
    obtain Q' where QTrans: "Ψ  Q α  Q'" and "(Ψ, Q', R')  Rel'"
      by(blast dest: simE)

    from (Ψ, Q', R')  Rel' have Q'RelR': "(Ψ  Ψ', Q', R')  Rel'" by(rule C1)

    from Ψ  P ↝<Rel> Q QTrans bn α ♯* Ψ bn α ♯* P α  τ 
    obtain P'' P' where PTrans: "Ψ : Q  P α  P''" and P''Chain: "Ψ  Ψ'  P'' ^τ P'"
                    and P'RelQ': "(Ψ  Ψ', P', Q')  Rel"
      by(blast dest: weakSimE)

    from PTrans RimpQ have "Ψ : R  P α  P''" by(rule weakTransitionFrameImp)
    moreover note P''Chain
    moreover from P'RelQ' Q'RelR' Set have "(Ψ  Ψ', P', R')  Rel''" by blast
    ultimately show ?case by blast
  next
    case(cTau R')
    from Ψ  Q ↝[Rel'] R Ψ  R τ  R'
    obtain Q' where QTrans: "Ψ  Q τ  Q'" and Q'RelR': "(Ψ, Q', R')  Rel'"
      by(force dest: simE)

    from Ψ  P ↝<Rel> Q QTrans
    obtain P' where PTrans: "Ψ  P ^τ P'" and P'RelQ': "(Ψ, P', Q')  Rel"
      by(blast dest: weakSimE)

    note PTrans
    moreover from P'RelQ' Q'RelR' Set have "(Ψ, P', R')  Rel''" by blast
    ultimately show ?case by blast
  qed
qed

lemma quietSim:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"

  assumes "quiet P"
  and     "eqvt Rel"
  and     cQuiet: "P. quiet P  (Ψ, 𝟬, P)  Rel"

  shows "Ψ  𝟬 ↝<Rel> P"
using eqvt Rel
proof(induct rule: weakSimI[of _ _ _ _ "()"])
  case(cAct Ψ' α P')
  from Ψ  P α  P' α  τ have False using quiet P 
    by(cases rule: actionCases[where α=α]) (auto intro: quietOutput quietInput)
  thus ?case by simp
next
  case(cTau P')
  from Ψ  P τ  P' quiet P have "quiet P'"
    by(erule_tac quiet.cases) (force simp add: residualInject)
  have "Ψ  P ^τ P" by simp
  moreover from quiet P' have "(Ψ, 𝟬, P')  Rel" by(rule cQuiet)
  ultimately show ?case by blast
qed


end

end