Theory Weak_Stat_Imp_Pres

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

context env begin

lemma weakStatImpInputPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a

  assumes PRelQ: "Ψ'. (Ψ  Ψ', M⦇λ*xvec N⦈.P, M⦇λ*xvec N⦈.Q)  Rel"

  shows "Ψ  M⦇λ*xvec N⦈.P ⪅<Rel> M⦇λ*xvec N⦈.Q"
using assms
by(fastforce simp add: weakStatImp_def)

lemma weakStatImpOutputPres:
  fixes Ψ   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   M   :: 'a
  and   N   :: 'a

  assumes PRelQ: "Ψ'. (Ψ  Ψ', MN⟩.P, MN⟩.Q)  Rel"

  shows "Ψ  MN⟩.P ⪅<Rel> MN⟩.Q"
using assms
by(fastforce simp add: weakStatImp_def)
(*
lemma weakStatImpCasePres:
  fixes Ψ    :: 'b
  and   CsP  :: "('c × ('a, 'b, 'c) psi) list"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   CsQ  :: "('c × ('a, 'b, 'c) psi) list"
  and   M    :: 'a
  and   N    :: 'a

  assumes PRelQ: "⋀φ Q. (φ, Q) mem CsQ ⟹ ∃P. (φ, P) mem CsP ∧ guarded P ∧ Eq P Q"
  and     Sim:   "⋀Ψ P Q. (Ψ, P, Q) ∈ Rel ⟹ Ψ ⊳ P ⪅<Rel> Q"
  and     EqRel: "⋀Ψ P Q. Eq P Q ⟹ (Ψ, P, Q) ∈ Rel"

  shows "Ψ ⊳ Cases CsP ⪅<Rel> Cases CsQ"
using assms
apply(auto simp add: weakStatImp_def)
apply(rule_tac x="Cases CsQ" in exI)
apply auto
apply(rule_tac x="Cases CsQ" in exI)
apply auto
apply blast
proof(induct rule: weakSimI2)
  case(cAct Ψ' α Q')
  from `bn α ♯* (Cases CsP)` have "bn α ♯* CsP" by auto
  from `Ψ ⊳ Cases CsQ ⟼α ≺ Q'`
  show ?case
  proof(induct rule: caseCases)
    case(cCase φ Q)
    from `(φ, Q) mem CsQ` obtain P where "(φ, P) mem CsP" and "guarded P" and "Eq P Q"
      by(metis PRelQ)
    from `Eq P Q` have "Ψ ⊳ P ↝<Rel> Q" by(metis EqRel Sim)
    moreover note `Ψ ⊳ Q ⟼α ≺ Q'` `bn α ♯* Ψ`
    moreover from `bn α ♯* CsP` `(φ, P) mem CsP` have "bn α ♯* P" by(auto dest: memFreshChain)
    ultimately obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹α ≺ P''"
                               and P''Chain: "Ψ ⊗ Ψ' ⊳ P'' ⟹^τ P'" and P'RelQ': "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
      using `α ≠ τ`
      by(blast dest: weakSimE)
    note PTrans `(φ, P) mem CsP` `Ψ ⊢ φ` `guarded P`
    moreover from `guarded Q` have "insertAssertion (extractFrame Q) Ψ ≃F ⟨ε, Ψ ⊗ 𝟭⟩"
      by(rule insertGuardedAssertion)
    hence "insertAssertion (extractFrame(Cases CsQ)) Ψ ↪F insertAssertion (extractFrame Q) Ψ"
      by(auto simp add: FrameStatEq_def)
    moreover from Identity have "insertAssertion (extractFrame(Cases CsQ)) Ψ ↪F ⟨ε, Ψ⟩"
      by(auto simp add: AssertionStatEq_def)
    ultimately have "Ψ : (Cases CsQ) ⊳ Cases CsP ⟹α ≺ P''"
      by(rule weakCase)
    with P''Chain P'RelQ' show ?case by blast
  qed
next
  case(cTau Q')
  from `Ψ ⊳ Cases CsQ ⟼τ ≺ Q'` show ?case
  proof(induct rule: caseCases)
    case(cCase φ Q)
    from `(φ, Q) mem CsQ` obtain P where "(φ, P) mem CsP" and "guarded P" and "Eq P Q"
      by(metis PRelQ)
    from `Eq P Q` `Ψ ⊳ Q ⟼τ ≺ Q'`
    obtain P' where PChain: "Ψ ⊳ P ⟹τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
      by(blast dest: EqSim weakCongSimE)
    from PChain `(φ, P) mem CsP` `Ψ ⊢ φ` `guarded P` have "Ψ ⊳ Cases CsP ⟹τ P'"
      by(rule tauStepChainCase)
    hence "Ψ ⊳ Cases CsP ⟹^τ P'" by(simp add: trancl_into_rtrancl)
    with P'RelQ' show ?case by blast
  qed
qed
*)
lemma weakStatImpResPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   x    :: name
  and   Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes PSimQ: "Ψ  P ⪅<Rel> Q"
  and     "eqvt Rel"
  and     "x  Ψ"
  and     C1: "Ψ' R S y. (Ψ', R, S)  Rel; y  Ψ'  (Ψ', ⦇νyR, ⦇νyS)  Rel'"

  shows   "Ψ  ⦇νxP ⪅<Rel'> ⦇νxQ"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  obtain y::name where "y  Ψ" and "y  Ψ'" and "y  P" and "y  Q" by(generate_fresh "name") auto
  from eqvt Rel Ψ  P ⪅<Rel> Q  have "([(x, y)]  Ψ)  ([(x, y)]  P) ⪅<Rel> ([(x, y)]  Q)" by(rule weakStatImpClosed)
  with x  Ψ y  Ψ have "Ψ  ([(x, y)]  P) ⪅<Rel> ([(x, y)]  Q)" by simp
  then obtain Q' Q'' where QChain: "Ψ  ([(x, y)]  Q) ^τ Q'"
                       and PimpQ': "insertAssertion (extractFrame ([(x, y)]  P)) Ψ F insertAssertion (extractFrame Q') Ψ"
                       and Q'Chain: "Ψ  Ψ'  Q' ^τ Q''" and "(Ψ  Ψ', ([(x, y)]  P), Q'')  Rel"
    by(rule weakStatImpE)
  from QChain y  Ψ have "Ψ  ⦇νy([(x, y)]  Q) ^τ ⦇νyQ'" by(rule tauChainResPres)
  with y  Q have "Ψ  ⦇νxQ ^τ ⦇νyQ'" by(simp add: alphaRes)
  moreover from PimpQ' y  Ψ have "insertAssertion (extractFrame(⦇νy([(x, y)]  P))) Ψ F insertAssertion (extractFrame(⦇νyQ')) Ψ"
    by(force intro: frameImpResPres)
  with y  P have "insertAssertion (extractFrame(⦇νxP)) Ψ F insertAssertion (extractFrame(⦇νyQ')) Ψ"
    by(simp add: alphaRes)
  moreover from Q'Chain y  Ψ y  Ψ' have "Ψ  Ψ'  ⦇νyQ' ^τ ⦇νyQ''" by(rule_tac tauChainResPres) auto
  moreover from (Ψ  Ψ', ([(x, y)]  P), Q'')  Rel y  Ψ y  Ψ' have "(Ψ  Ψ', ⦇νy([(x, y)]  P), ⦇νyQ'')  Rel'" 
    by(blast intro: C1)
  with y  P have "(Ψ  Ψ', ⦇νxP, ⦇νyQ'')  Rel'" by(simp add: alphaRes)
  ultimately show ?case
    by blast
qed

lemma weakStatImpParPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"
  and   Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  
  assumes PStatImpQ: "AR ΨR. extractFrame R = AR, ΨR; AR ♯* Ψ; AR ♯* P; AR ♯* Q  Ψ  ΨR  P ⪅<Rel> Q"
  and     "xvec ♯* Ψ"
  and     Eqvt:  "eqvt Rel"

  and     C1: "Ψ' S T AU ΨU U. (Ψ'  ΨU, S, T)  Rel; extractFrame U = AU, ΨU; AU ♯* Ψ'; AU ♯* S; AU ♯* T  (Ψ', S  U, T  U)  Rel'"
  and     C2: "Ψ' S T yvec. (Ψ', S, T)  Rel'; yvec ♯* Ψ'  (Ψ', ⦇ν*yvecS, ⦇ν*yvecT)  Rel'"
  and     C3: "Ψ' S T Ψ''. (Ψ', S, T)  Rel; Ψ'  Ψ''  (Ψ'', S, T)  Rel"

  shows "Ψ  ⦇ν*xvec(P  R) ⪅<Rel'> ⦇ν*xvec(Q  R)"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  obtain AR ΨR where FrR: "extractFrame R = AR, ΨR" and "AR ♯* Ψ" and "AR ♯* Ψ'" and "AR ♯* P" and "AR ♯* Q" and "AR ♯* R" and "AR ♯* xvec"
    by(rule_tac F="extractFrame R" and C="(xvec, Ψ, Ψ', P, Q, R, xvec)" in freshFrame) auto

  hence "Ψ  ΨR  P ⪅<Rel> Q" by(rule_tac PStatImpQ)
    
  obtain p::"name prm" where "(p  xvec) ♯* P" and "(p  xvec) ♯* Q" and "(p  xvec) ♯* Ψ" and "(p  xvec) ♯* Ψ'" and  "(p  xvec) ♯* ΨR" 
                         and  "(p  xvec) ♯* AR" and "(p  xvec) ♯* R" and "(p  xvec) ♯* P"
                         and "distinctPerm p" and S: "set p  set xvec × set (p  xvec)"
    by(rule_tac c="(P, Q, R, Ψ, Ψ', AR, ΨR, P)" in name_list_avoiding) auto
    
  from FrR have "(p  extractFrame R) = (p  AR, ΨR)" by(rule pt_bij3)
  with AR ♯* xvec (p  xvec) ♯* AR S have FrpR: "extractFrame(p  R) = AR, p  ΨR" by(simp add: eqvts)
  from eqvt Rel Ψ  ΨR  P ⪅<Rel> Q have "(p  (Ψ  ΨR))  (p  P) ⪅<Rel> (p  Q)" by(rule weakStatImpClosed)
  with xvec ♯* Ψ (p  xvec) ♯* Ψ S have "Ψ  (p  ΨR)  (p  P) ⪅<Rel> (p  Q)" by(simp add: eqvts)
  then obtain Q' Q'' where QChain: "Ψ  (p  ΨR)  (p  Q) ^τ Q'"
                       and PimpQ': "insertAssertion (extractFrame (p  P)) (Ψ  (p  ΨR)) F insertAssertion (extractFrame Q') (Ψ  (p  ΨR))"
                       and Q'Chain: "(Ψ  (p  ΨR))  Ψ'  Q' ^τ Q''" and "((Ψ  (p  ΨR))  Ψ', (p  P), Q'')  Rel"
    by(rule weakStatImpE)
    
  from AR ♯* xvec (p  xvec) ♯* AR AR ♯* Q S have "AR ♯* (p  Q)" by(simp add: freshChainSimps)
  moreover from (p  xvec) ♯* Q have "(p  p  xvec) ♯* (p  Q)"
    by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  hence "xvec ♯* (p  Q)" using distinctPerm p by simp
  ultimately have "AR ♯* Q'" and "AR ♯* Q''" and "xvec ♯* Q'" and "xvec ♯* Q''" using QChain Q'Chain
    by(metis tauChainFreshChain)+

  obtain AP ΨP where FrP: "extractFrame(p  P) = AP, ΨP" and "AP ♯* Ψ" "AP ♯* Ψ'" and "AP ♯* AR" and "AP ♯* (p  ΨR)"
    by(rule_tac C="(Ψ, Ψ', AR, p  ΨR)" in freshFrame) auto
  obtain AQ' ΨQ' where FrQ': "extractFrame Q' = AQ', ΨQ'" and "AQ' ♯* Ψ"and "AQ' ♯* Ψ'" and "AQ' ♯* AR" and "AQ' ♯* (p  ΨR)"
    by(rule_tac C="(Ψ, Ψ', AR, p  ΨR)" in freshFrame) auto
  from AR ♯* xvec (p  xvec) ♯* AR AR ♯* P S have "AR ♯* (p  P)" by(simp add: freshChainSimps)
  with AR ♯* Q' AP ♯* AR AQ' ♯* AR FrP FrQ' have "AR ♯* ΨP" and  "AR ♯* ΨQ'"
    by(force dest: extractFrameFreshChain)+

  from QChain FrpR AR ♯* Ψ AR ♯* (p  Q) have "Ψ  (p  Q)  (p  R) ^τ Q'  (p  R)" by(rule tauChainPar1)
  hence "(p  Ψ)  (p  ((p  Q)  (p  R))) ^τ p  (Q'  (p  R))" by(rule eqvts)
  with xvec ♯* Ψ (p  xvec) ♯* Ψ S distinctPerm p have "Ψ  Q  R ^τ (p  Q')  R" by(simp add: eqvts)
  hence "Ψ  ⦇ν*xvec(Q  R) ^τ ⦇ν*xvec((p  Q')  R)" using xvec ♯* Ψ by(rule tauChainResChainPres)
  moreover have "(AP@AR), Ψ  ΨP  (p  ΨR) F (AQ'@AR), Ψ  ΨQ'  (p  ΨR)"
  proof -
    have "AP, Ψ  ΨP  (p  ΨR) F AP, (Ψ  (p  ΨR))  ΨP"
      by(metis frameResChainPres frameNilStatEq Associativity Commutativity AssertionStatEqTrans Composition)
    moreover with FrP FrQ' PimpQ' AP ♯* Ψ AP ♯* (p  ΨR) AQ' ♯* Ψ AQ' ♯* (p  ΨR)
    have "AP, (Ψ  (p  ΨR))  ΨP F AQ', (Ψ  (p  ΨR))  ΨQ'"  using freshCompChain
      by simp
    moreover have "AQ', (Ψ  (p  ΨR))  ΨQ' F AQ', Ψ  ΨQ'  (p  ΨR)"
      by(metis frameResChainPres frameNilStatEq Associativity Commutativity AssertionStatEqTrans Composition)
    ultimately have "AP, Ψ  ΨP  (p  ΨR) F AQ', Ψ  ΨQ'  (p  ΨR)"
      by(rule FrameStatEqImpCompose)
    hence "(AR@AP), Ψ  ΨP  (p  ΨR) F (AR@AQ'), Ψ  ΨQ'  (p  ΨR)"
      by(drule_tac frameImpResChainPres) (simp add: frameChainAppend)
    thus ?thesis
      apply(simp add: frameChainAppend)
      by(metis frameImpChainComm FrameStatImpTrans)
  qed
  with FrP FrpR FrQ' AP ♯* AR AP ♯* (p  ΨR) AQ' ♯* AR AQ' ♯* (p  ΨR) AR ♯* ΨP AR ♯* ΨQ'
      AP ♯* Ψ AQ' ♯* Ψ AR ♯* Ψ
  have "insertAssertion(extractFrame((p  P)  (p  R))) Ψ F insertAssertion(extractFrame(Q'  (p  R))) Ψ"
    by simp
  hence "(p  insertAssertion(extractFrame((p  P)  (p  R))) Ψ) F (p  insertAssertion(extractFrame(Q'  (p  R))) Ψ)"
    by(rule FrameStatImpClosed)
  with xvec ♯* Ψ (p  xvec) ♯* Ψ S distinctPerm p
  have "insertAssertion(extractFrame(P  R)) Ψ F insertAssertion(extractFrame((p  Q')  R)) Ψ"
    by(simp add: eqvts)
  with xvec ♯* Ψ have "insertAssertion(extractFrame(⦇ν*xvec(P  R))) Ψ F insertAssertion(extractFrame(⦇ν*xvec((p  Q')  R))) Ψ"
    by(force intro: frameImpResChainPres)
  moreover from Q'Chain have "(Ψ  Ψ')  (p  ΨR)  Q' ^τ Q''"
    by(rule tauChainStatEq) (metis Associativity AssertionStatEqTrans Commutativity Composition)
  hence "Ψ  Ψ'  Q'  (p  R) ^τ Q''  (p  R)" using FrpR AR ♯* Ψ AR ♯* Ψ' AR ♯* Q' AR ♯* xvec (p  xvec) ♯* AR S
    by(force intro: tauChainPar1 simp add: freshChainSimps)
  hence "Ψ  Ψ'  ⦇ν*(p  xvec)(Q'  (p  R)) ^τ ⦇ν*(p  xvec)(Q''  (p  R))" using (p  xvec) ♯* Ψ (p  xvec) ♯* Ψ'
    by(rule_tac tauChainResChainPres) auto
  hence "Ψ  Ψ'  ⦇ν*xvec((p  Q')  R) ^τ ⦇ν*xvec((p  Q'')  R)" using xvec ♯* Q' xvec ♯* Q'' (p  xvec) ♯* R S distinctPerm p
    apply(subst resChainAlpha) apply(auto simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    by(subst resChainAlpha[of _ xvec]) (auto simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  moreover from ((Ψ  (p  ΨR))  Ψ', (p  P), Q'')  Rel have "((Ψ  Ψ')  (p  ΨR), (p  P),  Q'')  Rel"
    by(rule C3) (metis Associativity AssertionStatEqTrans Commutativity Composition)
  hence "(Ψ  Ψ', (p  P)  (p  R), Q''  (p  R))  Rel'" 
    using FrpR AR ♯* Ψ AR ♯* Ψ' AR ♯* Q'' AR ♯* P AR ♯* xvec (p  xvec) ♯* AR S
    by(rule_tac C1) (auto simp add: freshChainSimps)
  hence "(Ψ  Ψ', ⦇ν*(p  xvec)((p  P)  (p  R)), ⦇ν*(p  xvec)(Q''  (p  R)))  Rel'"  using (p  xvec) ♯* Ψ (p  xvec) ♯* Ψ'
    by(rule_tac C2) auto
  hence "(Ψ  Ψ', ⦇ν*xvec(P  R), ⦇ν*xvec((p  Q'')  R))  Rel'" using (p  xvec) ♯* P xvec ♯* Q'' (p  xvec) ♯* R S distinctPerm p
    apply(subst resChainAlpha[where p=p]) 
    apply simp
    apply simp
    apply(subst resChainAlpha[where xvec=xvec and p=p]) 
    by(auto simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  ultimately show ?case 
    by blast
qed

end

end