Theory Tau_Laws_No_Weak

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

context tauSum
begin

lemma tauLaw2:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  
  shows "Ψ ⊳ P ⊕ τ.(P) ≈ τ.(P)"
proof -
  let ?X = "{(Ψ, P ⊕ τ.(P), τ.(P)) | Ψ P. True}"
  let ?Y = "{(Ψ, τ.(P), P ⊕ τ.(P)) | Ψ P. True}"

  have "(Ψ, P ⊕ τ.(P), τ.(P)) ∈ ?X ∪ ?Y" by auto
  moreover have "eqvt(?X ∪ ?Y)" by(auto simp add: eqvt_def eqvts)
  ultimately show ?thesis
  proof(coinduct rule: weakTransitiveCoinduct)
    case(cStatImp Ψ P Q)
    show ?case
    proof(cases "(Ψ, P, Q) ∈ ?X")
      case True
      note ‹(Ψ, P, Q) ∈ ?X›
      moreover {
        fix Ψ P
        have "⋀Ψ'. (Ψ ⊗ Ψ', P ⊕ τ.(P), τ.(P)) ∈ ?X ∪ ?Y ∪ weakBisim" by auto
        hence "Ψ ⊳ P ⊕ τ.(P) ⪅<(?X ∪ ?Y ∪ weakBisim)> τ.(P)" by(rule tauLaw2StatImpLeft)
      }
      ultimately show ?thesis by blast
    next
      case False
      from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by auto
      moreover {
        fix Ψ P
        have "⋀Ψ'. (Ψ ⊗ Ψ', τ.(P), P ⊕ τ.(P)) ∈ ?X ∪ ?Y ∪ weakBisim" by auto
        hence "Ψ ⊳ τ.(P) ⪅<(?X ∪ ?Y ∪ weakBisim)> P ⊕ τ.(P)" by(rule tauLaw2StatImpRight)
      }
      ultimately show ?thesis by blast
    qed
  next
    case(cSim Ψ P Q)
    let ?Z = "{(Ψ, P, S) | Ψ P S. ∃Q R. Ψ ⊳ P ∼ Q ∧ (Ψ, Q, R) ∈ ?X ∪ ?Y ∪ weakBisim ∧ Ψ ⊳ R ∼ S}"
    show ?case
      
    proof(cases "(Ψ, P, Q) ∈ ?X")
      case True
      note ‹(Ψ, P, Q) ∈ ?X›
      moreover {
        fix Ψ P
        have "⋀Ψ P. (Ψ, P, P) ∈ ?Z" 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 dest: bisimE(4))
        ultimately have "Ψ ⊳ P ⊕ τ.(P) ↝<?Z> τ.(P)" by(rule tauLaw2SimLeft)
      }
      ultimately show ?thesis by blast
    next
      case False
      from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by auto
      moreover {
        fix Ψ P
        have "⋀Ψ P Q. Ψ ⊳ P ∼ Q ⟹ (Ψ, P, Q) ∈ ?Z" by(blast intro: weakBisimReflexive bisimReflexive)
        hence "Ψ ⊳ τ.(P) ↝<?Z> P ⊕ τ.(P)" by(rule tauLaw2SimRight)
      }
      ultimately show ?thesis by blast
    qed
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by auto
  next
    case(cSym Ψ P Q)
    thus ?case by auto
  qed
qed

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

  shows "Ψ ⊳ P ⊕ τ.(P) ≐ τ.(P)"
proof(induct rule: weakPsiCongI)
  case cWeakBisim
  thus ?case by(rule tauLaw2)
next
  case cSimLeft
  note weakBisimReflexive
  moreover have "⋀Ψ P Q R S. ⟦Ψ ⊳ P ∼ Q; Ψ ⊳ Q ≈ R; Ψ ⊳ R ∼ S⟧ ⟹ Ψ ⊳ P ≈ S"
    by(metis weakBisimTransitive strongBisimWeakBisim)
  ultimately show ?case by(rule tauLaw2CongSimLeft)
next
  case cSimRight
  from strongBisimWeakBisim show ?case by(rule tauLaw2CongSimRight)
qed

lemma tauLawCong2:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  
  shows "P ⊕ τ.(P) ≐⇩c τ.(P)"
using tauLawPsiCong2
by(rule_tac weakCongI) auto

lemma tauLaw4:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   α :: "'a prefix"
  
  shows "Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ≈ α⋅(τ.(P) ⊕ Q)"
proof -
  let ?X = "{(Ψ, α⋅P ⊕ α⋅(τ.(P) ⊕ Q), α⋅(τ.(P) ⊕ Q)) | Ψ P α Q. True}"
  let ?Y = "{(Ψ, α⋅(τ.(P) ⊕ Q), α⋅P ⊕ α⋅(τ.(P) ⊕ Q)) | Ψ P α Q. True}"
  have "(Ψ, α⋅P ⊕ α⋅(τ.(P) ⊕ Q), α⋅(τ.(P) ⊕ Q)) ∈ ?X ∪ ?Y" by auto
  moreover have "eqvt(?X ∪ ?Y)" by(fastforce simp add: eqvt_def eqvts)
  ultimately show ?thesis
  proof(coinduct rule: weakTransitiveCoinduct)
    case(cStatImp Ψ P Q)
    show ?case
    proof(cases "(Ψ, P, Q) ∈ ?X")
      case True
      note ‹(Ψ, P, Q) ∈ ?X›
      moreover {
        fix Ψ α P Q
        have "⋀Ψ'. (Ψ ⊗ Ψ', α⋅P ⊕ α⋅(τ.(P) ⊕ Q), α⋅(τ.(P) ⊕ Q)) ∈ ?X ∪ ?Y ∪ weakBisim" by blast
        hence "Ψ ⊳  α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ⪅<(?X ∪ ?Y ∪ weakBisim)>  α⋅(τ.(P) ⊕ Q)" by(rule tauLaw4StatImpLeft)
      }
      ultimately show ?thesis by blast
    next
      case False
      from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by blast
      moreover {
        fix Ψ α P Q
        have "⋀Ψ'. (Ψ ⊗ Ψ', α⋅(τ.(P) ⊕ Q), α⋅P ⊕ α⋅(τ.(P) ⊕ Q)) ∈ ?X ∪ ?Y ∪ weakBisim" by auto
        hence "Ψ ⊳  α⋅(τ.(P) ⊕ Q) ⪅<(?X ∪ ?Y ∪ weakBisim)> α⋅P ⊕ α⋅(τ.(P) ⊕ Q)" by(rule tauLaw4StatImpRight)
      }
      ultimately show ?thesis by blast
    qed
  next      
    case(cSim Ψ P Q)
    let ?Z = "{(Ψ, P, S) | Ψ P S. ∃Q R. Ψ ⊳ P ∼ Q ∧ (Ψ, Q, R) ∈ ?X ∪ ?Y ∪ weakBisim ∧ Ψ ⊳ R ∼ S}"
    show ?case
    proof(cases "(Ψ, P, Q) ∈ ?X")
      case True
      note ‹(Ψ, P, Q) ∈ ?X›
      moreover {
        fix Ψ P α Q
        have "⋀Ψ P. (Ψ, P, P) ∈ ?Z" by(blast intro: weakBisimReflexive bisimReflexive)
        moreover have "⋀Ψ P Q. Ψ ⊳ P ∼ Q ⟹ (Ψ, P, Q) ∈ ?Z" by(blast intro: weakBisimReflexive bisimReflexive)
        ultimately have "Ψ ⊳  α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ↝<?Z>  α⋅(τ.(P) ⊕ Q)" by(rule tauLaw4SimLeft)
      }
      ultimately show ?thesis by blast
    next
      case False
      from ‹(Ψ, P, Q) ∉ ?X› ‹(Ψ, P, Q) ∈ ?X ∪ ?Y› have "(Ψ, P, Q) ∈ ?Y" by blast
      moreover {
        fix Ψ P α Q
        have "⋀Ψ P Q. Ψ ⊳ P ∼ Q ⟹ (Ψ, P, Q) ∈ ?Z" by(blast intro: weakBisimReflexive bisimReflexive)
        moreover have "⋀Ψ P. (Ψ, P, P) ∈ ?Z" by(blast intro: weakBisimReflexive bisimReflexive)
        ultimately have "Ψ ⊳ α⋅(τ.(P) ⊕ Q) ↝<?Z> α⋅P ⊕ α⋅(τ.(P) ⊕ Q)" by(rule tauLaw4SimRight)
      }
      ultimately show ?thesis by blast
    qed
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by auto
  next
    case(cSym Ψ P Q)
    thus ?case by blast
  qed
qed

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

  shows "Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ≐ α⋅(τ.(P) ⊕ Q)"
proof(induct rule: weakPsiCongI)
  case cWeakBisim
  show ?case by(rule tauLaw4)
next
  case cSimLeft
  from weakBisimReflexive strongBisimWeakBisim show ?case by(rule tauLaw4CongSimLeft)
next
  case cSimRight
  from strongBisimWeakBisim show ?case by(rule tauLaw4CongSimRight)
qed

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

  shows "α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ≐⇩c α⋅(τ.(P) ⊕ Q)"
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) ♯* Q" and "(p ∙ yvec) ♯* σ"
      by(rule_tac xvec=yvec and c="(N, P, Q, σ)" in name_list_avoiding) auto
    thus ?case using ‹wellFormedSubst σ› tauLaw4PsiCong[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 σ› tauLaw4PsiCong[where α="pOutput (substTerm.seqSubst M σ) (substTerm.seqSubst N σ)"]
      by simp
  next
    case pTau
    thus ?case using  ‹wellFormedSubst σ› tauLaw4PsiCong[where α="pTau"]
      by simp
  qed
qed

end

end