Theory Tau_Stat_Imp

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

locale weakTauLaws = weak + tau
begin

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

  assumes "Ψ ⊳ P ⪅⇩w<Rel> Q"
  and     "(Ψ, τ.(P), Q) ∈ Rel"
 
  shows "Ψ ⊳ τ.(P) ⪅⇩w<Rel> Q"
proof -
  have "Ψ ⊳ Q ⟹⇧^⇩τ Q" by simp
  moreover have "insertAssertion (extractFrame(τ.(P))) Ψ ≃⇩F ⟨ε, Ψ⟩" by(rule insertTauAssertion)
  hence "insertAssertion (extractFrame(τ.(P))) Ψ ↪⇩F insertAssertion (extractFrame Q) Ψ"
    by(metis FrameStatImpTrans FrameStatEq_def insertAssertionWeaken)
  ultimately show ?thesis using ‹(Ψ, τ.(P), Q) ∈ Rel›
    by(rule weakenStatImpI)
qed

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

  assumes "Ψ ⊳ P ⪅<Rel> Q"
  and     C1: "⋀Ψ P Q R. ⟦(Ψ, P, Q) ∈ Rel; Ψ ⊳ Q ∼ R⟧ ⟹ (Ψ, P, R) ∈ Rel'"

  shows "Ψ ⊳ P ⪅<Rel'> τ.(Q)"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  from ‹Ψ ⊳ P ⪅<Rel> Q› obtain Q' Q'' 
    where QChain: "Ψ ⊳ Q ⟹⇧^⇩τ Q'" and PImpQ': "insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame Q') Ψ" 
      and Q'Chain: "Ψ ⊗ Ψ' ⊳ Q' ⟹⇧^⇩τ Q''" and PRelQ'': "(Ψ ⊗ Ψ', P, Q'') ∈ Rel"
    by(rule weakStatImpE)
    
  obtain Q''' where QTrans: "Ψ ⊳ τ.(Q) ⟼τ ≺ Q'''" and "Ψ ⊳ Q ∼ Q'''" using tauActionI by auto
  
  from ‹Ψ ⊳ Q ∼ Q'''› QChain bisimE(2) obtain Q'''' where Q'''Chain: "Ψ ⊳ Q''' ⟹⇧^⇩τ Q''''" and "Ψ ⊳ Q' ∼ Q''''"
    by(metis bisimE(4) simTauChain)
  
  from QTrans Q'''Chain have "Ψ ⊳ τ.(Q) ⟹⇧^⇩τ Q''''" by(drule_tac tauActTauChain) auto
  moreover from ‹Ψ ⊳ Q' ∼ Q''''› have "insertAssertion (extractFrame Q') Ψ ↪⇩F insertAssertion (extractFrame Q'''') Ψ"
    by(metis bisimE FrameStatEq_def)
  with PImpQ'  have "insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame Q'''') Ψ"
    by(rule FrameStatImpTrans)
  moreover from ‹Ψ ⊳ Q' ∼ Q''''› have "Ψ ⊗ Ψ' ⊳ Q' ∼ Q''''" by(rule bisimE) 
  then obtain Q''''' where Q''''Chain: "Ψ ⊗ Ψ' ⊳ Q'''' ⟹⇧^⇩τ Q'''''" and "Ψ ⊗ Ψ' ⊳ Q'' ∼ Q'''''" using Q'Chain bisimE(2) 
    by(metis bisimE(4) simTauChain)
  note Q''''Chain
  moreover from ‹(Ψ ⊗ Ψ', P, Q'') ∈ Rel› ‹Ψ ⊗ Ψ' ⊳ Q'' ∼ Q'''''› have "(Ψ ⊗ Ψ', P, Q''''') ∈ Rel'"
    by(rule C1)
  ultimately show ?case by blast
qed

end

context tau begin

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

  assumes C1: "⋀Ψ'. (Ψ ⊗ Ψ', α⋅(τ.(P)), α⋅Q) ∈ Rel"

  shows "Ψ ⊳ α⋅(τ.(P)) ⪅<Rel> α⋅Q"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  have "Ψ ⊳ α⋅Q ⟹⇧^⇩τ α⋅Q" by auto
  moreover have "insertAssertion (extractFrame(α⋅(τ.(P)))) Ψ ↪⇩F insertAssertion (extractFrame(α⋅Q)) Ψ" using insertTauAssertion
    by(nominal_induct α rule: prefix.strong_inducts) (auto simp add: FrameStatEq_def intro: FrameStatImpTrans)
  moreover have "Ψ ⊗ Ψ' ⊳ α⋅Q ⟹⇧^⇩τ α⋅Q" by auto
  moreover have "(Ψ ⊗ Ψ', α⋅(τ.(P)), α⋅Q) ∈ Rel" by(rule C1)
  ultimately show ?case by blast
qed

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

  assumes C1: "⋀Ψ'. (Ψ ⊗ Ψ', α⋅P, α⋅(τ.(Q))) ∈ Rel"

  shows "Ψ ⊳ α⋅P ⪅<Rel> α⋅(τ.(Q))"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  have "Ψ ⊳  α⋅(τ.(Q)) ⟹⇧^⇩τ  α⋅(τ.(Q))" by auto
  moreover have "insertAssertion (extractFrame(α⋅P)) Ψ ↪⇩F insertAssertion (extractFrame(α⋅(τ.(Q)))) Ψ" using insertTauAssertion
    by(nominal_induct α rule: prefix.strong_inducts) (auto simp add: FrameStatEq_def intro: FrameStatImpTrans)
  moreover have "Ψ ⊗ Ψ' ⊳  α⋅(τ.(Q)) ⟹⇧^⇩τ  α⋅(τ.(Q))" by auto
  moreover have "(Ψ ⊗ Ψ', α⋅P, α⋅(τ.(Q))) ∈ Rel" by(rule C1)
  ultimately show ?case by blast
qed

end

context tauSum begin

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

  assumes C1: "⋀Ψ'. (Ψ ⊗ Ψ', P ⊕ τ.(P), τ.(P)) ∈ Rel" 

  shows "Ψ ⊳ P ⊕ τ.(P) ⪅<Rel> τ.(P)"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  have "Ψ ⊳ τ.(P) ⟹⇧^⇩τ τ.(P)" by auto
  moreover have "insertAssertion (extractFrame(τ.(P))) Ψ ≃⇩F ⟨ε, Ψ⟩" by(rule insertTauAssertion)
  hence "insertAssertion (extractFrame(P ⊕ τ.(P))) Ψ ↪⇩F insertAssertion (extractFrame(τ.(P))) Ψ" using Identity
    by(rule_tac FrameStatImpTrans) (auto simp add: FrameStatEq_def AssertionStatEq_def)
  moreover have "Ψ ⊗ Ψ' ⊳ τ.(P) ⟹⇧^⇩τ τ.(P)" by auto
  moreover have "(Ψ ⊗ Ψ', P ⊕ τ.(P), τ.(P)) ∈ Rel" by(rule C1)
  ultimately show ?case by blast
qed  

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

  assumes C1: "⋀Ψ'. (Ψ ⊗ Ψ', τ.(P), P ⊕ τ.(P)) ∈ Rel"

  shows "Ψ ⊳ τ.(P) ⪅<Rel> P ⊕ τ.(P)"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  have "Ψ ⊳ P ⊕ τ.(P) ⟹⇧^⇩τ P ⊕ τ.(P)" by auto
  moreover have "insertAssertion (extractFrame(τ.(P))) Ψ ≃⇩F ⟨ε, Ψ⟩" by(rule insertTauAssertion)
  hence "insertAssertion (extractFrame(τ.(P))) Ψ ↪⇩F insertAssertion (extractFrame(P ⊕ τ.(P))) Ψ" using Identity
    by(rule_tac FrameStatImpTrans) (auto simp add: FrameStatEq_def AssertionStatEq_def)
  moreover have "Ψ ⊗ Ψ' ⊳ P ⊕ τ.(P) ⟹⇧^⇩τ P ⊕ τ.(P)" by auto
  moreover have "(Ψ ⊗ Ψ', τ.(P), P ⊕ τ.(P)) ∈ Rel" by(rule C1)
  ultimately show ?case by blast
qed

lemma tauLaw4StatImpLeft:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   M :: 'a
  and   N :: 'a

  assumes C1: "⋀Ψ'. (Ψ ⊗ Ψ', α⋅P ⊕ α⋅(τ.(P) ⊕ Q), α⋅(τ.(P) ⊕ Q)) ∈ Rel"

  shows "Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ⪅<Rel> α⋅(τ.(P) ⊕ Q)"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  have "Ψ ⊳ α⋅(τ.(P) ⊕ Q) ⟹⇧^⇩τ α⋅(τ.(P) ⊕ Q)" by auto
  hence "insertAssertion (extractFrame(α⋅P ⊕ α⋅(τ.(P) ⊕ Q))) Ψ ↪⇩F insertAssertion (extractFrame(α⋅(τ.(P) ⊕ Q))) Ψ" 
    using insertTauAssertion Identity
    by(nominal_induct α rule: prefix.strong_inducts, auto) 
  (rule FrameStatImpTrans[where G="⟨ε, Ψ⟩"], auto simp add: FrameStatEq_def AssertionStatEq_def)
  moreover have "Ψ ⊗ Ψ' ⊳ α⋅(τ.(P) ⊕ Q) ⟹⇧^⇩τ α⋅(τ.(P) ⊕ Q)" by auto
  moreover have "(Ψ ⊗ Ψ', α⋅P ⊕ α⋅(τ.(P) ⊕ Q), α⋅(τ.(P) ⊕ Q)) ∈ Rel" by(rule C1)
  ultimately show ?case by blast
qed

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

  assumes C1: "⋀Ψ'. (Ψ ⊗ Ψ', α⋅(τ.(P) ⊕ Q), α⋅P ⊕ α⋅(τ.(P) ⊕ Q)) ∈ Rel"

  shows "Ψ ⊳ α⋅(τ.(P) ⊕ Q) ⪅<Rel> α⋅P ⊕ α⋅(τ.(P) ⊕ Q)"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  have "Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ⟹⇧^⇩τ α⋅P ⊕ α⋅(τ.(P) ⊕ Q)" by auto
  hence "insertAssertion (extractFrame(α⋅(τ.(P) ⊕ Q))) Ψ ↪⇩F insertAssertion (extractFrame(α⋅P ⊕ α⋅(τ.(P) ⊕ Q))) Ψ"
    using insertTauAssertion Identity
    by(nominal_induct α rule: prefix.strong_inducts, auto) 
  (rule FrameStatImpTrans[where G="⟨ε, Ψ⟩"], auto simp add: FrameStatEq_def AssertionStatEq_def)
  moreover have "Ψ ⊗ Ψ' ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ⟹⇧^⇩τ α⋅P ⊕ α⋅(τ.(P) ⊕ Q)" by auto
  moreover have "(Ψ ⊗ Ψ', α⋅(τ.(P) ⊕ Q), α⋅P ⊕ α⋅(τ.(P) ⊕ Q)) ∈ Rel" by(rule C1)
  ultimately show ?case by blast
qed

end

end