Theory Weaken_Bisimulation

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

context weak
begin

lemma weakenMonoCoinduct: "⋀x y xa xb xc P Q Ψ.
                      x ≤ y ⟹
                      (Ψ ⊳ Q ↝⇩w<{(xc, xb, xa). x xc xb xa}> P) ⟶
                     (Ψ ⊳ Q ↝⇩w<{(xb, xa, xc). y xb xa xc}> P)"
apply auto
apply(rule weakenSimMonotonic)
by(auto dest: le_funE)

lemma weakenMonoCoinduct2: "⋀x y xa xb xc P Q Ψ.
                      x ≤ y ⟹
                      (Ψ ⊳ Q ⪅⇩w<{(xc, xb, xa). x xc xb xa}> P) ⟶
                     (Ψ ⊳ Q ⪅⇩w<{(xb, xa, xc). y xb xa xc}> P)"
apply auto
apply(rule weakenStatImpMonotonic)
by(auto dest: le_funE)

coinductive_set weakenBisim :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set" 
where
  step: "⟦Ψ ⊳ P ⪅⇩w<weakenBisim> Q; Ψ ⊳ P ↝⇩w<weakenBisim> Q;
          ∀Ψ'. (Ψ ⊗ Ψ',  P, Q) ∈ weakenBisim; (Ψ, Q, P) ∈ weakenBisim⟧ ⟹ (Ψ, P, Q) ∈ weakenBisim"
monos weakenMonoCoinduct weakenMonoCoinduct2

abbreviation
  weakenBisimJudge ("_ ⊳ _ ≈⇩w _" [70, 70, 70] 65) where "Ψ ⊳ P ≈⇩w Q ≡ (Ψ, P, Q) ∈ weakenBisim"
abbreviation
  weakenBisimNilJudge ("_ ≈⇩w _" [70, 70] 65) where "P ≈⇩w Q ≡ 𝟭 ⊳ P ≈⇩w Q"

lemma weakenBisimCoinductAux[consumes 1]:
  fixes F :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "(Ψ, P, Q) ∈ X"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ (Ψ ⊳ P ⪅⇩w<(X ∪ weakenBisim)> Q) ∧
                                    (Ψ ⊳ P ↝⇩w<(X ∪ weakenBisim)> Q) ∧
                                    (∀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ X ∨ (Ψ ⊗ Ψ', P, Q) ∈ weakenBisim) ∧
                                    ((Ψ, Q, P) ∈ X ∨ (Ψ, Q, P) ∈ weakenBisim)"

  shows "(Ψ, P, Q) ∈ weakenBisim"
proof -
  have "X ∪ weakenBisim = {(Ψ, P, Q). (Ψ, P, Q) ∈ X ∨ (Ψ, P, Q) ∈ weakenBisim}" by auto
  with assms show ?thesis
    by coinduct (simp add: rtrancl_def)
qed

lemma weakenBisimCoinduct[consumes 1, case_names cStatImp cSim cExt cSym]:
  fixes F :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "(Ψ, P, Q) ∈ X"
  and     "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ Ψ' ⊳ R ⪅⇩w<(X ∪ weakenBisim)> S"
  and     "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ Ψ' ⊳ R ↝⇩w<(X ∪ weakenBisim)> S"
  and     "⋀Ψ' R S Ψ''. (Ψ', R, S) ∈ X ⟹ (Ψ' ⊗ Ψ'', R, S) ∈ X ∨ Ψ' ⊗ Ψ'' ⊳ R ≈⇩w S"
  and     "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ (Ψ', S, R) ∈ X ∨ Ψ' ⊳ S ≈⇩w R"

  shows "Ψ ⊳ P ≈⇩w Q"
proof -
  have "X ∪ weakenBisim = {(Ψ, P, Q). (Ψ, P, Q) ∈ X ∨ (Ψ, P, Q) ∈ weakenBisim}" by auto
  with assms show ?thesis
    by coinduct (simp add: rtrancl_def)
qed

lemma weakenBisimWeakCoinductAux[consumes 1]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "(Ψ, P, Q) ∈ X"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ⪅⇩w<X> Q ∧
                                     Ψ ⊳ P ↝⇩w<X> Q ∧ (∀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ X) ∧ 
                                    (Ψ, Q, P) ∈ X" 

  shows "Ψ ⊳ P ≈⇩w Q"
using assms
by(coinduct rule: weakenBisimCoinductAux) (blast intro: weakenSimMonotonic weakenStatImpMonotonic)

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

  assumes "Ψ ⊳ P ≈⇩w Q"

  shows "Ψ ⊳ P ⪅⇩w<weakenBisim> Q"
  and   "Ψ ⊳ P ↝⇩w<weakenBisim> Q"
  and   "Ψ ⊗ Ψ' ⊳ P ≈⇩w Q"
  and   "Ψ ⊳ Q ≈⇩w P"
using assms
by(auto intro: weakenBisim.cases simp add: rtrancl_def)

lemma weakenBisimWeakCoinduct[consumes 1, case_names cStatImp cSim cExt cSym]:
  fixes F :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "(Ψ, P, Q) ∈ X"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ⪅⇩w<X> Q"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝⇩w<X> Q"
  and     "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ X ⟹ (Ψ ⊗ Ψ', P, Q) ∈ X"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ (Ψ, Q, P) ∈ X"

  shows "(Ψ, P, Q) ∈ weakenBisim"
proof -
  have "X ∪ weakenBisim = {(Ψ, P, Q). (Ψ, P, Q) ∈ X ∨ (Ψ, P, Q) ∈ weakenBisim}" by auto
  with assms show ?thesis
    by(coinduct rule: weakenBisimWeakCoinductAux) blast
qed

lemma weakenBisimEqWeakBisim[simp]: "weakenBisim = weakBisim"
proof auto
  fix Ψ P Q
  assume "Ψ ⊳ P ≈⇩w Q" thus "Ψ ⊳ P ≈ Q"
  proof(coinduct rule: weakBisimWeakCoinduct)
    case(cStatImp Ψ P Q)
    from ‹Ψ ⊳ P ≈⇩w Q› have "Ψ ⊳ P ⪅⇩w<weakenBisim> Q" by(rule weakenBisimE)
    thus ?case using weakenBisimE(3) by(rule weakenStatImpWeakStatImp)
  next
    case(cSim Ψ P Q)
    from ‹Ψ ⊳ P ≈⇩w Q› weakenBisimE
    show ?case by(rule weakenSimWeakSim)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(rule weakenBisimE)
  next
    case(cSym Ψ P Q)
    thus ?case by(rule weakenBisimE)
  qed
next
  fix Ψ P Q
  assume "Ψ ⊳ P ≈ Q" thus "Ψ ⊳ P ≈⇩w Q"
  proof(coinduct rule: weakenBisimWeakCoinduct)
    case(cStatImp Ψ P Q)
    from ‹Ψ ⊳ P ≈ Q› have "Ψ ⊳ P ⪅<weakBisim> Q" by(rule weakBisimE)
    thus ?case using statEqWeakBisim by(rule weakStatImpWeakenStatImp)
  next
    case(cSim Ψ P Q)
    from ‹Ψ ⊳ P ≈ Q› have "Ψ ⊳ P ↝<weakBisim> Q" by(rule weakBisimE)
    thus ?case using statEqWeakBisim by(rule weakSimWeakenSim)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(rule weakBisimE)
  next
    case(cSym Ψ P Q)
    thus ?case by(rule weakBisimE)
  qed
qed

lemma weakenTransitiveWeakCoinduct[case_names cStatImp cSim cExt cSym, case_conclusion bisim step, consumes 2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes p: "(Ψ, P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and rStatImp: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ⪅⇩w<X> Q"
  and rSim: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝⇩w<({(Ψ, P, Q) | Ψ P Q. ∃P' Q'. Ψ ⊳ P ∼ P' ∧
                                                                        (Ψ, P', Q') ∈ X ∧
                                                                        Ψ ⊳ Q' ∼ Q})> Q"
  and rExt: "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ X ⟹ (Ψ ⊗ Ψ', P, Q) ∈ X"
  and rSym: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ (Ψ, Q, P) ∈ X"

  shows "Ψ ⊳ P ≈⇩w Q"
proof -
  from p ‹eqvt X› have "Ψ ⊳ P ≈ Q"
  proof(coinduct rule: weakTransitiveWeakCoinduct)
    case(cStatImp Ψ P Q)
    from ‹(Ψ, P, Q) ∈ X› have "Ψ ⊳ P ⪅⇩w<X> Q" by(rule rStatImp)
    thus ?case using rExt by(rule weakenStatImpWeakStatImp)
  next
    case(cSim Ψ P Q)
    let ?Y = "{(Ψ, P, Q) | Ψ P Q. ∃P' Q'. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"
    note ‹(Ψ, P, Q) ∈ X›
    moreover note rStatImp rSim
    moreover have "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ ?Y ⟹ (Ψ ⊗ Ψ', P, Q) ∈ ?Y"
      by(blast dest: bisimE rExt)
    ultimately show ?case using rSym by(rule weakenSimWeakSim)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(rule rExt) 
  next
    case(cSym Ψ P Q)
    thus ?case by(rule rSym)
  qed
  thus ?thesis by(simp add: weakenBisimEqWeakBisim)
qed

lemma weakenTransitiveCoinduct[case_names cStatImp cSim cExt cSym, case_conclusion bisim step, consumes 2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes p: "(Ψ, P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and rStatImp: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ⪅⇩w<(X ∪ weakenBisim)> Q"
  and rSim: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝⇩w<({(Ψ, P, Q) | Ψ P Q. ∃P' Q'. Ψ ⊳ P ∼ P' ∧
                                                                        (Ψ, P', Q') ∈ (X ∪ weakenBisim) ∧
                                                                        Ψ ⊳ Q' ∼ Q})> Q"
  and rExt: "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ X ⟹ (Ψ ⊗ Ψ', P, Q) ∈ X ∪ weakenBisim"
  and rSym: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ (Ψ, Q, P) ∈ X ∪ weakenBisim"

  shows "Ψ ⊳ P ≈⇩w Q"
proof -
  from p have "(Ψ, P, Q) ∈ X ∪ weakenBisim" by auto
  moreover from ‹eqvt X› have "eqvt(X ∪ weakenBisim)" by auto
  ultimately show ?thesis
  proof(coinduct rule: weakenTransitiveWeakCoinduct)
    case(cStatImp Ψ P Q)
    thus ?case by(fastforce intro: rStatImp weakenBisimE(1) weakenStatImpMonotonic)
  next
    case(cSim Ψ P Q)
    thus ?case by(fastforce intro: rSim weakenBisimE(2) weakenSimMonotonic bisimReflexive)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(blast dest: weakenBisimE rExt) 
  next
    case(cSym Ψ P Q)
    thus ?case by(blast dest: weakenBisimE rSym)
  qed
qed

end

end