Theory Sum

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

context env
begin

abbreviation sumAssertJudge ("_ ⊕⇩_ _" [150, 50, 50] 150) 
  where "(P::('a, 'b, 'c) psi) ⊕⇩φ Q ≡ Cases [(φ, P), (φ, Q)]"

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

  assumes "Ψ ⊳ P ⟼ Rs"
  and     "Ψ ⊢ φ"
  and     "guarded P"

  shows "Ψ ⊳ P ⊕⇩φ Q ⟼ Rs"
proof -
  note ‹Ψ ⊳ P ⟼ Rs›
  moreover have "(φ, P) mem [(φ, P), (φ, Q)]" by simp
  ultimately show ?thesis using ‹Ψ ⊢ φ› ‹guarded P›
    by(rule Case)
qed

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

  assumes "Ψ ⊳ Q ⟼ Rs"
  and     "Ψ ⊢ φ"
  and     "guarded Q"

  shows "Ψ ⊳ P ⊕⇩φ Q ⟼ Rs"
proof -
  note ‹Ψ ⊳ Q ⟼ Rs›
  moreover have "(φ, Q) mem [(φ, P), (φ, Q)]" by simp
  ultimately show ?thesis using ‹Ψ ⊢ φ› ‹guarded Q›
    by(rule Case)
qed

lemma sumAssertCases[consumes 2, case_names cSum1 cSum2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   φ :: 'c

  assumes "Ψ ⊳ P ⊕⇩φ Q ⟼ Rs"
  and     "Ψ ⊢ φ"
  and     rSum1: "⟦Ψ ⊳ P ⟼ Rs; guarded P⟧ ⟹ Prop"
  and     rSum2: "⟦Ψ ⊳ Q ⟼ Rs; guarded Q⟧ ⟹ Prop"

  shows Prop
proof -
  from ‹Ψ ⊳ P ⊕⇩φ Q ⟼ Rs› show ?thesis
  proof(induct rule: caseCases)
    case(cCase φ' P')
    from ‹(φ', P') mem [(φ, P), (φ, Q)]›
    have "φ = φ'" and D: "P = P' ∨ Q = P'" by auto
    from D show ?thesis
    proof(rule disjE)
      assume "P = P'"
      with ‹Ψ ⊳ P' ⟼ Rs› ‹guarded P'› show ?case by(rule_tac rSum1) auto
    next
      assume "Q = P'"
      with ‹Ψ ⊳ P' ⟼ Rs› ‹guarded P'› show ?case by(rule_tac rSum2) auto
    qed
  qed
qed

lemma sumElim[dest]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   φ :: 'c

  assumes "Ψ ⊳ P ⊕⇩φ Q ⟼ Rs"
  and     "¬(Ψ ⊢ φ)"

  shows False
using assms
by(induct rule: caseCases) auto

end

locale sum = env +
  fixes T :: 'c

  assumes Top: "Ψ ⊢ T"
  and     TopEqvt[eqvt]: "((p::name prm) ∙ T) = T"
  and     TopSubst[simp]: "substCond T xvec Tvec = T"
begin

abbreviation topJudge ("⊤" 150) where "⊤ ≡ T"
abbreviation sumJudge (infixr "⊕" 80) where "P ⊕ Q ≡ P ⊕⇩⊤ Q"

lemma topSeqSubst[simp]:
  shows "(substCond.seqSubst T σ) = T"
by(induct σ) auto

lemma suppTop:
  shows "((supp(⊤))::name set) = {}"
by(auto simp add: supp_def eqvts)

lemma freshTop[simp]:
  fixes x    :: name
  and   xvec :: "name list"
  and   Xs   :: "name set"

  shows "x ♯ ⊤" and "xvec ♯* ⊤" and "Xs ♯* ⊤"
by(auto simp add: fresh_def fresh_star_def suppTop)

lemma sumSubst[simp]:
  fixes P    :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"
  and   Tvec :: "'a list"

  assumes "length xvec = length Tvec"
  and     "distinct xvec"

  shows "(P ⊕ Q)[xvec::=Tvec] = (P[xvec::=Tvec] ⊕ Q[xvec::=Tvec])"
by auto

lemma sumSeqSubst[simp]:
  fixes P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   σ :: "(name list × 'a list) list"

  assumes "wellFormedSubst σ"

  shows "(P ⊕ Q)[<σ>] = ((P[<σ>]) ⊕ (Q[<σ>]))"
using assms
by(induct σ arbitrary: P Q) auto

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

  assumes "Ψ ⊳ P ⟼ Rs"
  and     "guarded P"

  shows "Ψ ⊳ P ⊕ Q ⟼ Rs"
proof -
  have "Ψ ⊢ ⊤" by(rule Top)
  with ‹Ψ ⊳ P ⟼ Rs› show ?thesis using ‹guarded P›
    by(rule SumAssert1)
qed

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

  assumes "Ψ ⊳ Q ⟼ Rs"
  and     "guarded Q"

  shows "Ψ ⊳ P ⊕ Q ⟼ Rs"
proof -
  have "Ψ ⊢ ⊤" by(rule Top)
  with ‹Ψ ⊳ Q ⟼ Rs› show ?thesis using ‹guarded Q›
    by(rule SumAssert2)
qed

lemma sumCases[consumes 1, case_names cSum1 cSum2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ⊕ Q ⟼ Rs"
  and     rSum1: "⟦Ψ ⊳ P ⟼ Rs; guarded P⟧ ⟹ Prop"
  and     rSum2: "⟦Ψ ⊳ Q ⟼ Rs; guarded Q⟧ ⟹ Prop"

  shows Prop
proof -
  have "Ψ ⊢ ⊤" by(rule Top)
  with ‹Ψ ⊳ P ⊕ Q ⟼ Rs› show ?thesis
  proof(induct rule: sumAssertCases)
    case cSum1
    thus ?case by (rule rSum1)
  next
    case cSum2
    thus ?case by(rule rSum2)
  qed
qed

end

end