Quelle  Res_Pres.thy

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
eqvt Rel
P ↝[Rel] Q

∧
==>

P ∼ Q ≡ P ↝[∼] Q ∧ Q ↝[∼] P




lemma resPres:
  fixes P :: pi
  and   Q :: pi
  and   x :: name
  
  assumes PBiSimQ: "P ∼ Q"

  shows "<νx>P ∼ <νx>Q"
proof -
  let ?X = "{x. ∃P Q. P ∼ Q ∧ (∃a. x = (<νa>P, <νa>Q))}"
  from PBiSimQ have "(<νx>P, <νx>Q) ∈ ?X" by blast
  moreover have "∧P Q a. P ↝[bisim] Q ==> <νa>P ↝[(?X ∪ bisim)] <νa>Q"
  proof -
    fix P Q a
    assume PSimQ: "P ↝[bisim] Q"
    moreover have "∧P Q a. P ∼ Q ==> (<νa>P, <νa>Q) ∈ ?X ∪ bisim" by blast
    moreover have "bisim ⊆ ?X ∪ bisim" by blast
    moreover have "eqvt bisim" by(rule eqvt)
    moreover have "eqvt (?X ∪ bisim)"
      by(auto simp add: eqvt_def dest: eqvtI)+
    ultimately show "<νa>P ↝[(?X ∪ bisim)] <νa>Q"
      by(rule Strong_Late_Sim_Pres.resPres)
  qed
    
  ultimately show ?thesis using PBiSimQ
    by(coinduct, blast dest: unfoldE)
qed