Theory Weaken_Transition

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

context weak
begin

definition weakenTransition :: "'b ⇒ ('a, 'b, 'c) psi ⇒ 'a action ⇒ ('a, 'b, 'c) psi ⇒ bool" (‹_ ⊳ _ ⟹_ ≺ _› [80, 80, 80, 80] 80)
where
  "Ψ ⊳ P ⟹α ≺ P' ≡ (∃P''' P''. Ψ ⊳ P ⟹⇧^⇩τ P''' ∧ Ψ ⊳ P''' ⟼α ≺ P'' ∧ Ψ ⊳ P'' ⟹⇧^⇩τ P') ∨ (P = P' ∧ α = τ)"

lemma weakenTransitionCases[consumes 1, case_names cBase cStep]:
  assumes "Ψ ⊳ P ⟹α ≺ P'"
  and "Prop (τ) P"
  and "⋀P''' P''. ⟦Ψ ⊳ P ⟹⇧^⇩τ P'''; Ψ ⊳ P''' ⟼α ≺ P''; Ψ ⊳ P'' ⟹⇧^⇩τ P'⟧ ⟹ Prop α P'"

  shows "Prop α P'"
using assms
by(auto simp add: weakenTransition_def)

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

  assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"

  shows "insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame P') Ψ"
using assms
by(induct rule: tauChainInduct) (auto intro: statImpTauDerivative dest: FrameStatImpTrans)

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

  assumes "Ψ ⊳ P ⟹⇧^⇩τ P'"
  shows "Ψ ⊗ Ψ' ⊳ P ⟹⇧^⇩τ P'"
using assms
proof(induct rule: tauChainInduct)
  case(TauBase P)
  thus ?case by simp
next
  case(TauStep P P' P'')
  note ‹Ψ ⊗ Ψ' ⊳ P ⟹⇧^⇩τ P'›
  moreover from ‹Ψ ⊳ P' ⟼τ ≺ P''› have "Ψ ⊗ Ψ' ⊳ P' ⟼τ ≺ P''" by(rule weakenTransition)
  ultimately show ?case by(auto dest: tauActTauChain)
qed

end

end