Theory Strong_Late_Sim

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Strong_Late_Sim
  imports Late_Semantics1 Rel
begin

definition derivative :: "pi ⇒ pi ⇒ subject ⇒ name ⇒ (pi × pi) set ⇒ bool" where
  "derivative P Q a x Rel ≡ case a of InputS b ⇒ (∀u. (P[x::=u], Q[x::=u]) ∈ Rel)
                                    | BoundOutputS b ⇒ (P, Q) ∈ Rel"

definition simulation :: "pi ⇒ (pi × pi) set ⇒ pi ⇒ bool" ("_ ↝[_] _" [80, 80, 80] 80) where
  "P ↝[Rel] Q ≡ (∀a x Q'. Q ⟼a«x» ≺ Q' ∧ x ♯ P ⟶ (∃P'. P ⟼a«x» ≺ P' ∧ derivative P' Q' a x Rel)) ∧
                 (∀α Q'. Q ⟼α ≺ Q' ⟶ (∃P'. P ⟼α ≺ P' ∧ (P', Q') ∈ Rel))"

lemma monotonic: 
  fixes A  :: "(pi × pi) set"
  and   B  :: "(pi × pi) set"
  and   P  :: pi
  and   P' :: pi

  assumes "P ↝[A] P'"
  and     "A ⊆ B"

  shows "P ↝[B] P'"
using assms
apply(auto simp add: simulation_def derivative_def)
by(case_tac a) fastforce+

lemma derivativeMonotonic:
  fixes A :: "(pi × pi) set"
  and   B :: "(pi × pi) set"
  and   P :: pi
  and   Q :: pi
  and   a :: subject
  and   x :: name

  assumes "derivative P Q a x A"
  and     "A ⊆ B"
  
  shows "derivative P Q a x B"
using assms
by(case_tac a, auto simp add: derivative_def)

lemma derivativeEqvtI:
  fixes P    :: pi
  and   Q    :: pi
  and   a    :: subject
  and   x    :: name
  and   Rel  :: "(pi × pi) set"
  and   perm :: "name prm"

  assumes Der: "derivative P Q a x Rel"
  and     Eqvt: "eqvt Rel"
  
  shows "derivative (perm ∙ P) (perm ∙ Q) (perm ∙ a) (perm ∙ x) Rel"
using assms
apply(case_tac a, auto simp add: derivative_def)
apply(erule_tac x="rev perm ∙ u" in allE)
apply(drule_tac perm=perm in eqvtRelI)
apply(blast)
apply(force simp add: eqvt_subs name_per_rev)
by(force simp add: eqvt_def)

lemma derivativeEqvtI2:
  fixes P    :: pi
  and   Q    :: pi
  and   a    :: subject
  and   x    :: name
  and   Rel  :: "(pi × pi) set"
  and   perm :: "name prm"

  assumes Der: "derivative P Q a x Rel"
  and     Eqvt: "eqvt Rel"
  
  shows "derivative (perm ∙ P) (perm ∙ Q) a (perm ∙ x) Rel"
using assms
apply(case_tac a, auto simp add: derivative_def)
apply(erule_tac x="rev perm ∙ u" in allE)
apply(drule_tac perm=perm in eqvtRelI)
apply(blast)
apply(force simp add: eqvt_subs name_per_rev)
by(force simp add: eqvt_def)

lemma freshUnit[simp]:
  fixes y :: name

  shows "y ♯ ()"
by(auto simp add: fresh_def supp_unit)

lemma simCasesCont[consumes 1, case_names Bound Free]:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi × pi) set"
  and   C   :: "'a::fs_name"

  assumes Eqvt:  "eqvt Rel"
  and     Bound: "⋀a x Q'. ⟦Q ⟼ a«x» ≺ Q'; x ♯ P; x ♯ Q; x ♯ a; x ♯ C⟧ ⟹ ∃P'. P ⟼ a«x» ≺ P' ∧ derivative P' Q' a x Rel"
  and     Free:  "⋀α Q'. Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel"

  shows "P ↝[Rel] Q"
using Free
proof(auto simp add: simulation_def)
  fix a x Q'
  assume "(x::name) ♯ P"
  assume Trans: "Q ⟼ a«x» ≺ Q'"
  
  obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ a" and "y ♯ C" and "y ♯ Q'" and "y ≠ x"
    by(generate_fresh "name") auto

  from Trans ‹y ♯ Q'› have "Q ⟼ a«y» ≺ [(x, y)] ∙ Q'" by(simp add: alphaBoundResidual)
  hence "∃P'. P ⟼ a«y» ≺ P' ∧ derivative P' ([(x, y)] ∙ Q') a y Rel" 
    using ‹y ♯ P› ‹y ♯ Q› ‹y ♯ a› ‹y ♯ C›
    by(rule Bound)
  then obtain P' where PTrans: "P ⟼ a«y» ≺ P'" and PDer: "derivative P' ([(x, y)] ∙ Q') a y Rel"
    by blast
  
  from PTrans ‹x ♯ P› ‹y ≠ x› have "x ♯ P'" by(force intro: freshBoundDerivative)
  with PTrans have "P ⟼ a«x» ≺ [(x, y)] ∙ P'" by(simp add: alphaBoundResidual name_swap)
  moreover have "derivative ([(x, y)] ∙ P') Q' a x Rel"
  proof -
    from PDer Eqvt have "derivative ([(x, y)] ∙ P') ([(x, y)] ∙ [(x, y)] ∙ Q') a ([(x, y)] ∙ y) Rel"
      by(rule derivativeEqvtI2)
    with ‹y ≠ x› show ?thesis by(simp add: name_calc)
  qed
  ultimately show "∃P'. P ⟼a«x» ≺ P' ∧ derivative P' Q' a x Rel" by blast
qed

lemma simCases[case_names Bound Free]:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Bound: "⋀a y Q'. ⟦Q ⟼ a«y» ≺ Q'; y ♯ P⟧ ⟹ ∃P'. P ⟼ a«y» ≺ P' ∧ derivative P' Q' a y Rel"
  and     Free:  "⋀α Q'. Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel"

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

lemma resSimCases[consumes 1, case_names BoundOutput BoundR FreeR]:
  fixes x   :: name
  and   P   :: pi
  and   Rel :: "(pi × pi) set"
  and   Q   :: pi
  and   C   :: "'a::fs_name"

  assumes Eqvt:    "eqvt Rel"
  and     BoundO:  "⋀Q' a. ⟦Q ⟼a[x] ≺ Q'; a ≠ x⟧ ⟹ ∃P'. P ⟼a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
  and     BR:      "⋀Q' a y. ⟦Q ⟼a«y» ≺ Q'; x ♯ a; x ≠ y; y ♯ C⟧ ⟹ ∃P'. P ⟼a«y» ≺ P' ∧ derivative P' (<νx>Q') a y Rel"
  and     BF:      "⋀Q' α. ⟦Q ⟼α ≺ Q'; x ♯ α⟧ ⟹ ∃P'. P ⟼α ≺ P' ∧ (P', <νx>Q') ∈ Rel"

  shows "P ↝[Rel] <νx>Q"
using Eqvt
proof(induct rule: simCasesCont[where C="(C, x, Q)"])
  case(Bound a y Q')
  have "y ♯ (C, x, Q)" by fact
  hence yFreshC: "y ♯ C" and yineqx: "y ≠ x" and "y ♯ Q"
    by(simp add: fresh_prod)+
  have "<νx>Q ⟼a«y» ≺ Q'" by fact
  thus ?case using yineqx ‹y ♯ Q›
  proof(induct rule: resCasesB)
    case(cOpen a' Q')
    have "Q ⟼a'[x] ≺ Q'" and "a' ≠ x" by fact+
    then obtain P' where PTrans: "P ⟼a'<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(force dest: BoundO)
    
    from PTrans ‹y ♯ P› yineqx have "y ♯ P'" by(force dest: freshBoundDerivative)
    with PTrans have "P ⟼a'<νy> ≺ ([(x, y)] ∙ P')" by(simp add: alphaBoundResidual)
    moreover from P'RelQ' Eqvt have "([(x, y)] ∙ P', [(x, y)] ∙ Q') ∈ Rel" by(auto simp add: eqvt_def)
    ultimately show ?case by(force simp add: derivative_def name_swap) 
  next
    case(cRes Q')
    have "Q ⟼a«y» ≺ Q'" and "x ♯ a" by fact+
    with yineqx yFreshC show ?case by(force dest: BR)
  qed
next
  case(Free α Q')
  have "<νx>Q ⟼α ≺ Q'" by fact
  thus ?case
  proof(induct rule: resCasesF)
    case(cRes Q')
    have "Q ⟼α ≺ Q'" and "x ♯ α" by fact+
    thus ?case by(rule BF)
  qed
qed

lemma simE:
  fixes P   :: pi
  and   Rel :: "(pi × pi) set"
  and   Q   :: pi
  and   a   :: subject
  and   x   :: name
  and   Q'  :: pi

  assumes "P ↝[Rel] Q"

  shows "Q ⟼ a«x» ≺ Q' ⟹ x ♯ P ⟹ ∃P'. P ⟼ a«x» ≺ P' ∧ (derivative P' Q' a x Rel)"
  and   "Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel"
using assms by(simp add: simulation_def)+

lemma eqvtI:
  fixes P    :: pi
  and   Q    :: pi
  and   Rel  :: "(pi × pi) set"
  and   perm :: "name prm"

  assumes Sim: "P ↝[Rel] Q"
  and     RelRel': "Rel ⊆ Rel'"
  and     EqvtRel': "eqvt Rel'"

  shows "(perm ∙ P) ↝[Rel'] (perm ∙ Q)"
proof(induct rule: simCases)
  case(Bound a y Q')
  have QTrans: "(perm ∙ Q) ⟼ a«y» ≺ Q'" and yFreshP: "y ♯ perm ∙ P" by fact+
  
  from QTrans have "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (a«y» ≺ Q')"
    by(rule transitions.eqvt)
  hence "Q ⟼ (rev perm ∙ a)«(rev perm ∙ y)» ≺ (rev perm ∙ Q')" 
    by(simp add: name_rev_per)
  moreover from yFreshP have "(rev perm ∙ y) ♯ P" by(simp add: name_fresh_left)
  ultimately have "∃P'. P ⟼ (rev perm ∙ a)«rev perm ∙ y» ≺ P' ∧ derivative P' (rev perm ∙ Q') (rev perm ∙ a) (rev perm ∙ y) Rel" using Sim
    by(force intro: simE)
  then obtain P' where PTrans: "P ⟼ (rev perm ∙ a)«rev perm ∙ y» ≺ P'" and Pderivative: "derivative P' (rev perm ∙ Q') (rev perm ∙ a) (rev perm ∙ y) Rel" by blast
  
  from PTrans have "(perm ∙ P) ⟼ perm ∙ ((rev perm ∙ a)«rev perm ∙ y» ≺ P')" by(rule transitions.eqvt)
  hence L1: "(perm ∙ P) ⟼ a«y» ≺ (perm ∙ P')" by(simp add: name_per_rev)
  from Pderivative RelRel' have "derivative P' (rev perm ∙ Q') (rev perm ∙ a) (rev perm ∙ y) Rel'"
    by(rule derivativeMonotonic)
  hence "derivative (perm ∙ P') (perm ∙ (rev perm ∙ Q')) (perm ∙ (rev perm ∙ a)) (perm ∙ (rev perm ∙ y)) Rel'" using EqvtRel'
    by(rule derivativeEqvtI)
  hence "derivative (perm ∙ P') Q' a y Rel'" by(simp add: name_per_rev)
  with L1 show ?case by blast
next
  case(Free α Q')
  have "(perm ∙ Q) ⟼ α ≺ Q'" by fact

  hence "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (α ≺ Q')"
    by(rule transitions.eqvt)
  hence "Q ⟼ (rev perm ∙ α) ≺ (rev perm ∙ Q')" 
    by(simp add: name_rev_per)
  with Sim have "∃P'. P ⟼ (rev perm ∙ α) ≺ P' ∧ (P', (rev perm ∙ Q')) ∈ Rel"
    by(force intro: simE)
  then obtain P' where PTrans: "P ⟼ (rev perm ∙ α) ≺ P'" and PRel: "(P', (rev perm ∙ Q')) ∈ Rel"
    by blast
    
  from PTrans have "(perm ∙ P) ⟼ perm ∙ ((rev perm ∙ α)≺ P')" by(rule transitions.eqvt)
  hence L1: "(perm ∙ P) ⟼ α ≺ (perm ∙ P')" by(simp add: name_per_rev)
  from PRel EqvtRel' RelRel'  have "((perm ∙ P'), (perm ∙ (rev perm ∙ Q'))) ∈ Rel'"
    by(force intro: eqvtRelI)
  hence "((perm ∙ P'), Q') ∈ Rel'" by(simp add: name_per_rev)
  with L1 show "∃P'. (perm ∙ P) ⟼α ≺ P' ∧ (P', Q') ∈ Rel'" by blast
qed

lemma derivativeReflexive:
  fixes P   :: pi
  and   a   :: subject
  and   x   :: name
  and   Rel :: "(pi × pi) set"
  
  assumes "Id ⊆ Rel"

  shows "derivative P P a x Rel"
using assms
apply(cases a)
by(auto simp add: derivative_def)
(*
lemma simActFreeCases[consumes 0, case_names Der]:
  fixes P   :: pi
  and   α   :: freeRes
  and   Q'  :: pi
  and   Rel :: "(pi × pi) set"

  assumes "∃P'. P ⟼α ≺ P' ∧ (P', Q') ∈ Rel"

  shows "simAct P (α ≺ Q') P Rel"
using assms
by(simp add: simAct_def residualInject)
*)
(*****************Reflexivity and transitivity*********************)

lemma reflexive:
  fixes P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes "Id ⊆ Rel"

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

lemma transitive:
  fixes P     :: pi
  and   Q     :: pi
  and   R     :: pi
  and   Rel   :: "(pi × pi) set"
  and   Rel'  :: "(pi × pi) set"
  and   Rel'' :: "(pi × pi) set"

  assumes PSimQ: "P ↝[Rel] Q"
  and     QSimR: "Q ↝[Rel'] R"
  and     Eqvt': "eqvt Rel''"
  and     Trans: "Rel O Rel' ⊆ Rel''"

  shows "P ↝[Rel''] R"
using Eqvt'
proof(induct rule: simCasesCont[where C=Q])
  case(Bound a x R')
  have RTrans: "R ⟼ a«x» ≺ R'" by fact

  from ‹x ♯ Q› QSimR RTrans obtain Q' where QTrans: "Q ⟼ a«x» ≺ Q'"
                                        and QDer: "derivative Q' R' a x Rel'" 
    by(blast dest: simE)
  with QTrans ‹x ♯ P› PSimQ obtain P' where PTrans: "P ⟼ a«x» ≺ P'"
                                        and PDer: "derivative P' Q' a x Rel"
    by(blast dest: simE)
  moreover from PDer QDer Trans have "derivative P' R' a x Rel''"
    by(cases a) (auto simp add: derivative_def)
  ultimately show ?case by blast
next
  case(Free α R')
  have RTrans: "R ⟼ α ≺ R'" by fact
  with QSimR obtain Q' where QTrans: "Q ⟼ α ≺ Q'" 
                         and Q'RelR': "(Q', R') ∈ Rel'"
    by(blast dest: simE)
  from QTrans PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'"
                                and P'RelQ': "(P', Q') ∈ Rel"
    by(blast dest: simE)
  from P'RelQ' Q'RelR' Trans have "(P', R') ∈ Rel''" by blast
  with PTrans show ?case by blast
qed

end