Theory Tau_Laws_Weak

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Tau_Laws_Weak
  imports Weaken_Bisimulation Weak_Congruence Tau_Sim Tau_Stat_Imp
begin

context weakTauLaws begin

lemma tauLaw1:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  
  shows "Ψ ⊳ τ.(P) ≈ P"
proof - 
  let ?X = "{(Ψ, τ.(P), P) | Ψ P. True}" let ?Y = "{(Ψ, P, τ.(P)) | Ψ P. True}"
  have "(Ψ, τ.(P), P) ∈ ?X ∪ ?Y" by auto
  moreover have "eqvt(?X ∪ ?Y)" by(auto simp add: eqvt_def simp add: eqvts)
  ultimately have "Ψ ⊳ τ.(P) ≈⇩w P"
  proof(coinduct rule: weakenTransitiveCoinduct)
    case(cStatImp Ψ P Q)
    show ?case
    proof(cases "(Ψ, P, Q) ∈ ?X")
      case True
      {
        fix Ψ P
        have "Ψ ⊳ P ⪅⇩w<(?X ∪ ?Y ∪ weakBisim)> P" by(auto simp add: weakenStatImp_def intro: weakBisimReflexive)
        moreover have "(Ψ, τ.(P), P) ∈ ?X ∪ ?Y ∪ weakBisim" by auto
        ultimately have "Ψ ⊳ τ.(P) ⪅⇩w<(?X ∪ ?Y ∪ weakBisim)> P"
          by(rule tauLaw1StatImpLeft)
      }
      with ‹(Ψ, P, Q) ∈ ?X› show ?thesis by auto 
    next
      case False
      from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by auto
      {
        fix Ψ P
        have "Ψ ⊳ P ⪅<weakBisim> P" using weakBisimReflexive
          by(rule weakBisimE)
        moreover have "⋀Ψ P Q R. ⟦Ψ ⊳ P ≈ Q; Ψ ⊳ Q ∼ R⟧ ⟹ (Ψ, P, R) ∈ ?X ∪ ?Y ∪ weakBisim"
          by(fastforce intro: weakBisimTransitive strongBisimWeakBisim)
        ultimately have  "Ψ ⊳ P ⪅<( ?X ∪ ?Y ∪ weakBisim)> τ.(P)" by(rule tauLaw1StatImpRight)
        moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?X ∪ ?Y ∪ weakBisim; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?X ∪ ?Y ∪ weakBisim"
          by(auto dest: statEqWeakBisim)
        ultimately have "Ψ ⊳ P ⪅⇩w<( ?X ∪ ?Y ∪ weakBisim)> τ.(P)" by(rule weakStatImpWeakenStatImp)
      }
      with ‹(Ψ, P, Q) ∈ ?Y› show ?thesis by auto
    qed
  next
    case(cSim Ψ P Q)
    let ?Z = "{(Ψ, P, Q) | Ψ P Q. ∃P' Q'. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ ?X ∪ ?Y ∪ weakenBisim ∧ Ψ ⊳ Q' ∼ Q}"
    have "eqvt ?Z" 
      apply auto
      apply(auto simp add: eqvt_def eqvts)
      apply(rule_tac x="(p ∙ (τ.(Q')))" in exI)
      apply(auto intro: bisimClosed)
      apply(simp add: eqvts)
      apply(blast intro: bisimClosed weakBisimClosed)
      apply(rule_tac x="(p ∙ P')" in exI)
      apply(auto intro: bisimClosed)
      apply(rule_tac x="τ.(p ∙ P')" in exI)
      apply auto
      apply(drule_tac p=p and Q=b in bisimClosed)
      apply(simp add: eqvts)
      apply(rule_tac x="(p ∙ P')" in exI)
      apply(auto intro: bisimClosed)
      apply(rule_tac x="p ∙ Q'" in exI)
      apply auto
      by(blast intro: bisimClosed dest: weakBisimClosed)+
    show ?case
    proof(cases "(Ψ, P, Q) ∈ ?X")
      case True
      {
        fix P
        have "Ψ ⊳ P ↝<?Z> P" using weakenBisimEqWeakBisim by(blast intro: weakSimReflexive weakBisimReflexive bisimReflexive)
        moreover note ‹eqvt ?Z›
        moreover have "⋀Ψ P Q R. ⟦Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ ?Z⟧ ⟹ (Ψ, P, R) ∈ ?Z"
          by(blast intro: bisimTransitive)
        ultimately have "Ψ ⊳ τ.(P) ↝<?Z> P"
          by(rule tauLaw1SimLeft)
        moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?Z"
          by simp (blast intro: statEqWeakBisim statEqBisim)
        ultimately have "Ψ ⊳ τ.(P) ↝⇩w<?Z> P" by(rule weakSimWeakenSim)
      }
      with ‹(Ψ, P, Q) ∈ ?X› show ?thesis by auto
    next
      case False
      from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by auto
      moreover {
        fix P
        note ‹eqvt ?Z›  
        moreover have "(Ψ, P, P) ∈ ?Z" by simp (blast intro: weakBisimReflexive bisimReflexive)
        moreover have "⋀Ψ P Q R. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ⊳ Q ∼ R⟧ ⟹ (Ψ, P, R) ∈ ?Z"
          by(blast intro: bisimTransitive)
        ultimately have "Ψ ⊳ P ↝<?Z> τ.(P)" by(rule tauLaw1SimRight)
        moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?Z"
          by simp (blast intro: statEqWeakBisim statEqBisim)
        ultimately have "Ψ ⊳ P ↝⇩w<?Z> τ.(P)" by(rule weakSimWeakenSim)
      }
      ultimately show ?thesis by auto
    qed
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by auto
  next
    case(cSym Ψ P Q)
    thus ?case by auto
  qed
  thus ?thesis by simp
qed

lemma tauLaw3:
  fixes Ψ :: 'b
  and   α :: "'a prefix"
  and   P :: "('a, 'b, 'c) psi"

  shows "Ψ ⊳ α⋅(τ.(P)) ≈ α⋅P"
proof -
  let ?X = "({(Ψ, α⋅(τ.(P)), α⋅P) | Ψ α P. True})"
  let ?Y = "({(Ψ, α⋅P, α⋅(τ.(P))) | Ψ α P. True})"

  have "(Ψ, α⋅(τ.(P)), α⋅P) ∈ ?X ∪ ?Y" by blast
  moreover have "eqvt(?X ∪ ?Y)" by(fastforce simp add: eqvt_def simp add: eqvts)
  ultimately have "Ψ ⊳ α⋅(τ.(P)) ≈⇩w α⋅P"
  proof(coinduct rule: weakenTransitiveCoinduct)
    case(cStatImp Ψ P Q)
    show ?case
    proof(cases "(Ψ, P, Q) ∈ ?X")
      case True
      {
        fix Ψ α P
        have "⋀Ψ'. (Ψ ⊗ Ψ', α⋅(τ.(P)), α⋅P) ∈ ?X ∪ ?Y ∪ weakenBisim" by auto
        hence "Ψ ⊳ α⋅(τ.(P)) ⪅<(?X ∪ ?Y ∪ weakenBisim)> α⋅P" by(rule tauLaw3StatImpLeft)
        moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?X ∪ ?Y ∪ weakenBisim; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?X ∪ ?Y ∪ weakenBisim"
          by(fastforce intro: statEqWeakBisim)
        ultimately have "Ψ ⊳ α⋅(τ.(P)) ⪅⇩w<(?X ∪ ?Y ∪ weakenBisim)> α⋅P" by(rule weakStatImpWeakenStatImp)
      }
      with ‹(Ψ, P, Q) ∈ ?X› show ?thesis by blast
    next
      case False
      {
        fix Ψ α P
        have "⋀Ψ'. (Ψ ⊗ Ψ', α⋅P, α⋅(τ.(P))) ∈ ?X ∪ ?Y ∪ weakenBisim" by auto
        hence "Ψ ⊳ α⋅P ⪅<(?X ∪ ?Y ∪ weakenBisim)> α⋅(τ.(P))" by(rule tauLaw3StatImpRight)
        moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?X ∪ ?Y ∪ weakenBisim; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?X ∪ ?Y ∪ weakenBisim"
          by(fastforce intro: statEqWeakBisim)
        ultimately have "Ψ ⊳ α⋅P ⪅⇩w<(?X ∪ ?Y ∪ weakenBisim)> α⋅(τ.(P))" by(rule weakStatImpWeakenStatImp)
      }
      moreover from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by blast
      ultimately show ?thesis by auto
    qed
  next
    case(cSim Ψ P Q)
    let ?Z = "{(Ψ, P, Q) | Ψ P Q. ∃P' Q'. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ ?X ∪ ?Y ∪ weakenBisim ∧ Ψ ⊳ Q' ∼ Q}"
    have "eqvt ?Z" 
      apply(clarsimp simp add: eqvt_def)
      apply(elim disjE)
      apply(rule_tac x="p ∙ P'" in exI)
      apply(clarsimp simp add: bisimClosed eqvts)
      apply(blast intro: bisimClosed eqvts)
      apply(rule_tac x="p ∙ P'" in exI)
      apply(clarsimp simp add: bisimClosed eqvts)
      apply(rule_tac x="p ∙ (α⋅(τ.(P)))" in exI)
      apply(clarsimp simp add: eqvts)
      apply(rule conjI)
      apply(rule disjI2)
      apply(blast intro: bisimClosed eqvts)
      apply(drule_tac p=p in bisimClosed)
      apply(drule_tac p=p in bisimClosed)
      apply(simp add: eqvts)
      by(blast dest: bisimClosed weakBisimClosed)
    show ?case
    proof(cases "(Ψ, P, Q) ∈ ?X")
      case True
      note ‹(Ψ, P, Q) ∈ ?X›
      moreover {
        fix Ψ P α
        note ‹eqvt ?Z›
        moreover have "(Ψ, P, P) ∈ ?Z" using weakenBisimEqWeakBisim by(blast intro: weakBisimReflexive bisimReflexive)
        moreover have "⋀xvec Tvec. length xvec = length Tvec ⟹ (Ψ, P[xvec::=Tvec], P[xvec::=Tvec]) ∈ ?Z"
           using weakenBisimEqWeakBisim by(blast intro: weakBisimReflexive bisimReflexive)
        moreover have "⋀Ψ P Q R S. ⟦Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ ?Z; Ψ ⊳ R ∼ S⟧ ⟹ (Ψ, P, S) ∈ ?Z" by(blast intro: bisimTransitive)
        moreover have "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ ?Z ⟹ (Ψ ⊗ Ψ', P, Q) ∈ ?Z" by(blast dest: weakenBisimE(3) bisimE(3))
        ultimately have "Ψ ⊳ α⋅(τ.(P)) ↝<?Z> α⋅P" by(rule tauLaw3SimLeft)
        moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?Z" by simp (blast dest: statEqWeakBisim statEqBisim)
        ultimately have "Ψ ⊳ α⋅(τ.(P)) ↝⇩w<?Z> α⋅P" by(rule weakSimWeakenSim)
      }
      ultimately show ?thesis by auto
    next
      case False
      from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by blast
      moreover {
        fix Ψ P α
        note ‹eqvt ?Z›
        moreover have "⋀Ψ xvec Tvec. length xvec=length Tvec ⟹ (Ψ, P[xvec::=Tvec], τ.(P[xvec::=Tvec])) ∈ ?Z"
          by simp (blast intro: weakBisimE(4) bisimReflexive tauLaw1)
        moreover have "⋀Ψ P Q R S. ⟦Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ ?Z; Ψ ⊳ R ∼ S⟧ ⟹ (Ψ, P, S) ∈ ?Z" by(blast intro: bisimTransitive)
        moreover have "⋀Ψ. (Ψ, P, τ.(P)) ∈ ?Z" by simp (blast intro: weakBisimE(4) bisimReflexive tauLaw1)
        ultimately have "Ψ ⊳ α⋅P ↝<?Z> α⋅(τ.(P))" by(rule tauLaw3SimRight)
        moreover have "⋀Ψ P Q Ψ'. ⟦(Ψ, P, Q) ∈ ?Z; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?Z" by simp (blast dest: statEqWeakBisim statEqBisim)
        ultimately have "Ψ ⊳ α⋅P ↝⇩w<?Z> α⋅(τ.(P))" by(rule weakSimWeakenSim)
      }
      ultimately show ?thesis by auto
    qed
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by auto
  next
    case(cSym Ψ P Q)
    thus ?case by blast 
  qed
  thus ?thesis by simp
qed
  
lemma tauLaw3PsiCong:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"

  shows "Ψ ⊳ α⋅(τ.(P)) ≐ α⋅P"
proof(induct rule: weakPsiCongI)
  case cWeakBisim
  show ?case by(rule tauLaw3)
next
  case cSimLeft
  have "Ψ ⊳ P ≈ P" by(rule weakBisimReflexive)
  moreover have "⋀Ψ P Q R S. ⟦Ψ ⊳ P ∼ Q; Ψ ⊳ Q ≈ R; Ψ ⊳ R ∼ S⟧ ⟹ Ψ ⊳ P ≈ S"
    by(blast intro: weakBisimTransitive strongBisimWeakBisim)
  ultimately show ?case using weakBisimE(3) by(rule tauLaw3CongSimLeft)
next
  case cSimRight
  have "Ψ ⊳  P ≈ P" by(rule weakBisimReflexive)
  moreover have "⋀Ψ P Q R S. ⟦Ψ ⊳ P ∼ Q; Ψ ⊳ Q ≈ R; Ψ ⊳ R ∼ S⟧ ⟹ Ψ ⊳ P ≈ S"
    by(blast intro: weakBisimTransitive strongBisimWeakBisim)
  ultimately show ?case using tauLaw1[THEN weakBisimE(4)]
    by(rule tauLaw3CongSimRight)
qed
  
lemma tauLaw3Cong:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"

  shows "α⋅(τ.(P)) ≐⇩c α⋅P"
proof(induct rule: weakCongI)
  case(cWeakPsiCong Ψ σ)
  show ?case
  proof(nominal_induct α rule: prefix.strong_inducts)
  next
    case(pInput M yvec N)
    obtain p where "set p ⊆ set yvec × set(p ∙ yvec)" and "(p ∙ yvec) ♯* N" and "(p ∙ yvec) ♯* P" and "(p ∙ yvec) ♯* σ"
      by(rule_tac xvec=yvec and c="(N, P, σ)" in name_list_avoiding) auto
    thus ?case using ‹wellFormedSubst σ› tauLaw3PsiCong[where α="pInput (substTerm.seqSubst M σ) (p ∙ yvec) (substTerm.seqSubst (p ∙ N) σ)"]
      by(simp add: inputChainAlpha' eqvts)
  next
    case(pOutput M N)
    thus ?case using  ‹wellFormedSubst σ› tauLaw3PsiCong[where α="pOutput (substTerm.seqSubst M σ) (substTerm.seqSubst N σ)"]
      by simp
  next
    case pTau
    thus ?case using  ‹wellFormedSubst σ› tauLaw3PsiCong[where α="pTau"]
      by simp
  qed
qed

end

end