Theory SimulationRelations

(* Kirstin Peters, TU Berlin, 2015 concerning the reduction semantics and
   Kirstin Peters, University of Augsburg, 2026 for the labelled semantics *)

theory SimulationRelations
  imports ProcessCalculi
begin

section ‹Simulation Relations›

text ‹Simulation relations are a special kind of property on relations on processes. They usually
      require that steps are (strongly or weakly) preserved and/or reflected modulo the relation.
      We consider different kinds of simulation relations.›

subsection ‹Simulation›

text ‹A weak (reduction) simulation is relation R such that if (P, Q) in R and P evolves to some P'
      then there exists some Q' such that Q evolves to Q' and (P', Q') in R.›

abbreviation weak_reduction_simulation :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool"
  where
  "weak_reduction_simulation Rel Cal ≡
   ∀P Q P'. (P, Q) ∈ Rel ∧ P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel)"

text ‹A weak barbed simulation is weak reduction simulation that weakly preserves barbs.›

abbreviation weak_barbed_simulation
  :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool" where
  "weak_barbed_simulation Rel CWB ≡
   weak_reduction_simulation Rel (Calculus CWB) ∧ rel_weakly_preserves_barbs Rel CWB"

text ‹A weak labelled simulation is relation R such that if (P, Q) in R and P evolves to some P'
      using label a then there exists some Q' such that Q evolves to Q' using a and (P', Q') in R.›

abbreviation weak_labelled_simulation
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "weak_labelled_simulation Rel Cal ≡
   ∀P Q α P'. (P, Q) ∈ Rel ∧ P ─⁀α→Cal* P' ⟶ (∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel)"

text ‹A weak labelled simulation also simulates words of labels including the empty word.›

lemma weak_labelled_simulation_internal:
  fixes Rel    :: "('proc × 'proc) set"
    and Cal    :: "('proc, 'lab) labelledProcessCalculus"
    and P Q P' :: "'proc"
  assumes simulation: "weak_labelled_simulation Rel Cal"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P →Cal* P'"
    shows "∃Q'. Q →Cal* Q' ∧ (P', Q') ∈ Rel"
proof -
  from execution have "P ─⁀τ-Cal→Cal* P'"
    unfolding weakLabelledStep_def
    by simp
  with simulation relation obtain Q' where A1: "Q ─⁀τ-Cal→Cal* Q'" and A2: "(P', Q') ∈ Rel"
    by blast
  from A1 have "Q →Cal* Q'"
    unfolding weakLabelledStep_def
    by simp
  with A2 show "∃Q'. Q →Cal* Q' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma weak_labelled_simulation_word:
  fixes Rel    :: "('proc × 'proc) set"
    and Cal    :: "('proc, 'lab) labelledProcessCalculus"
    and P Q P' :: "'proc"
    and w      :: "'lab list"
  assumes simulation: "weak_labelled_simulation Rel Cal"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P ─⌢w→Cal* P'"
    shows "∃Q'. Q ─⌢w→Cal* Q' ∧ (P', Q') ∈ Rel"
  using execution simulation relation
proof induct
  case (WLS_Nil P Cal P')
  assume "P →Cal* P'" and "weak_labelled_simulation Rel Cal" and "(P, Q) ∈ Rel"
  then obtain Q' where A1: "Q →Cal* Q'" and A2: "(P', Q') ∈ Rel"
    using weak_labelled_simulation_internal[of Rel Cal P Q P']
    by blast
  from A1 have "Q ─⌢[]→Cal* Q'"
    using weakLabelledSequence.WLS_Nil[of Q Cal Q']
    by simp
  with A2 show "∃Q'. Q ─⌢[]→Cal* Q' ∧ (P', Q') ∈ Rel"
    by blast
next
  case (WLS_Cons P w Cal P' α P'')
  from WLS_Cons(2) have IH: "weak_labelled_simulation Rel Cal ∧ (P, Q) ∈ Rel ⟹
                             ∃Q'. Q ─⌢w→Cal* Q' ∧ (P', Q') ∈ Rel"
    by simp
  assume A1: "weak_labelled_simulation Rel Cal" and "(P, Q) ∈ Rel"
  with IH obtain Q' where A2: "Q ─⌢w→Cal* Q'" and A3: "(P', Q') ∈ Rel"
    by blast
  assume "P' ─⁀α→Cal* P''"
  with A1 A2 A3 obtain Q'' where A4: "Q' ─⁀α→Cal* Q''" and A5: "(P'', Q'') ∈ Rel"
    by blast
  from A2 A4 have "Q ─⌢(w@[α])→Cal* Q''"
    using weakLabelledSequence.WLS_Cons[of Q w Cal Q' α Q'']
    by simp
  with A5 show "∃Q''. Q ─⌢(w@[α])→Cal* Q'' ∧ (P'', Q'') ∈ Rel"
    by blast
qed

text ‹The reflexive and/or transitive closure of a weak simulation is a weak simulation.›

lemma weak_reduction_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes simulation: "weak_reduction_simulation Rel Cal"
  shows "weak_reduction_simulation (Rel⇧=) Cal"
    and "weak_reduction_simulation (Rel⇧+) Cal"
    and "weak_reduction_simulation (Rel⇧*) Cal"
proof -
  from simulation show A: "weak_reduction_simulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast)
  have B: "⋀Rel. weak_reduction_simulation Rel Cal ⟹ weak_reduction_simulation (Rel⇧+) Cal"
  proof clarify
    fix Rel P Q P'
    assume B1: "weak_reduction_simulation Rel Cal"
    assume "(P, Q) ∈ Rel⇧+" and "P ⟼Cal* P'"
    thus "∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel⇧+"
    proof (induct arbitrary: P')
      fix Q P'
      assume "(P, Q) ∈ Rel" and "P ⟼Cal* P'"
      with B1 obtain Q' where "Q ⟼Cal* Q'" and "(P', Q') ∈ Rel"
        by blast
      thus "∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel⇧+"
        by auto
    next
      case (step Q R P')
      assume "⋀P'. P ⟼Cal* P' ⟹ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel⇧+)"
         and "P ⟼Cal* P'"
      from this obtain Q' where B2: "Q ⟼Cal* Q'" and B3: "(P', Q') ∈ Rel⇧+"
        by blast
      assume "(Q, R) ∈ Rel"
      with B1 B2 obtain R' where B4: "R ⟼Cal* R'" and B5: "(Q', R') ∈ Rel⇧+"
        by blast
      from B3 B5 have "(P', R') ∈ Rel⇧+"
        by simp
      from B4 this show "∃R'. R ⟼Cal* R' ∧ (P', R') ∈ Rel⇧+"
        by blast
    qed
  qed
  with simulation show "weak_reduction_simulation (Rel⇧+) Cal"
    by blast
  from simulation A B[where Rel="Rel⇧="]
  show "weak_reduction_simulation (Rel⇧*) Cal"
      using trancl_reflcl[of Rel]
    by fast
qed

lemma weak_barbed_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes simulation: "weak_barbed_simulation Rel CWB"
  shows "weak_barbed_simulation (Rel⇧=) CWB"
    and "weak_barbed_simulation (Rel⇧+) CWB"
    and "weak_barbed_simulation (Rel⇧*) CWB"
proof -
  from simulation show "weak_barbed_simulation (Rel⇧=) CWB"
      using weak_reduction_simulation_and_closures(1)[where Rel="Rel" and Cal="Calculus CWB"]
            weak_preservation_of_barbs_and_closures(1)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from simulation show "weak_barbed_simulation (Rel⇧+) CWB"
      using weak_reduction_simulation_and_closures(2)[where Rel="Rel" and Cal="Calculus CWB"]
            weak_preservation_of_barbs_and_closures(2)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from simulation show "weak_barbed_simulation (Rel⇧*) CWB"
      using weak_reduction_simulation_and_closures(3)[where Rel="Rel" and Cal="Calculus CWB"]
            weak_preservation_of_barbs_and_closures(3)[where Rel="Rel" and CWB="CWB"]
    by blast
qed

lemma weak_labelled_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes simulation: "weak_labelled_simulation Rel Cal"
  shows "weak_labelled_simulation (Rel⇧=) Cal"
    and "weak_labelled_simulation (Rel⇧+) Cal"
    and "weak_labelled_simulation (Rel⇧*) Cal"
proof -
  from simulation show A: "weak_labelled_simulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast)
  have B: "⋀Rel. weak_labelled_simulation Rel Cal ⟹ weak_labelled_simulation (Rel⇧+) Cal"
  proof clarify
    fix Rel P Q α P'
    assume B1: "weak_labelled_simulation Rel Cal"
    assume "(P, Q) ∈ Rel⇧+" and "P ─⁀α→Cal* P'"
    thus "∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel⇧+"
    proof (induct arbitrary: P')
      fix Q P'
      assume "(P, Q) ∈ Rel" and "P ─⁀α→Cal* P'"
      with B1 obtain Q' where "Q ─⁀α→Cal* Q'" and "(P', Q') ∈ Rel"
        by blast
      thus "∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel⇧+"
        by auto
    next
      case (step Q R P')
      assume "⋀P'. P ─⁀α→Cal* P' ⟹ (∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel⇧+)"
         and "P ─⁀α→Cal* P'"
      from this obtain Q' where B2: "Q ─⁀α→Cal* Q'" and B3: "(P', Q') ∈ Rel⇧+"
        by blast
      assume "(Q, R) ∈ Rel"
      with B1 B2 obtain R' where B4: "R ─⁀α→Cal* R'" and B5: "(Q', R') ∈ Rel⇧+"
        by blast
      from B3 B5 have "(P', R') ∈ Rel⇧+"
        by simp
      from B4 this show "∃R'. R ─⁀α→Cal* R' ∧ (P', R') ∈ Rel⇧+"
        by blast
    qed
  qed
  with simulation show "weak_labelled_simulation (Rel⇧+) Cal"
    by blast
  from simulation A B[where Rel="Rel⇧="]
  show "weak_labelled_simulation (Rel⇧*) Cal"
      using trancl_reflcl[of Rel]
    by fast
qed

text ‹In the case of a simulation weak preservation of barbs can be replaced by the weaker
      condition that whenever (P, Q) in the relation and P has a barb then Q have to be able to
      reach this barb.›

abbreviation weak_barbed_preservation_cond
  :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool" where
  "weak_barbed_preservation_cond Rel CWB ≡ ∀P Q a. (P, Q) ∈ Rel ∧ P↓<CWB>a ⟶ Q⇓<CWB>a"

lemma weak_preservation_of_barbs:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes preservation: "rel_weakly_preserves_barbs Rel CWB"
  shows "weak_barbed_preservation_cond Rel CWB"
proof clarify
  fix P Q a
  have "P ⟼(Calculus CWB)* P"
    by (simp add: steps_refl)
  moreover assume "P↓<CWB>a"
  ultimately have "P⇓<CWB>a"
    by blast
  moreover assume "(P, Q) ∈ Rel"
  ultimately show "Q⇓<CWB>a"
    using preservation
    by blast
qed

lemma simulation_impl_equality_of_preservation_of_barbs_conditions:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes simulation: "weak_reduction_simulation Rel (Calculus CWB)"
  shows "rel_weakly_preserves_barbs Rel CWB = weak_barbed_preservation_cond Rel CWB"
proof
  assume "rel_weakly_preserves_barbs Rel CWB"
  thus "weak_barbed_preservation_cond Rel CWB"
    using weak_preservation_of_barbs[where Rel="Rel" and CWB="CWB"]
    by blast
next
  assume condition: "weak_barbed_preservation_cond Rel CWB"
  show "rel_weakly_preserves_barbs Rel CWB"
  proof clarify
    fix P Q a P'
    assume "(P, Q) ∈ Rel" and "P ⟼(Calculus CWB)* P'"
    with simulation obtain Q' where A1: "Q ⟼(Calculus CWB)* Q'" and A2: "(P', Q') ∈ Rel"
      by blast
    assume "P'↓<CWB>a"
    with A2 condition obtain Q'' where A3: "Q' ⟼(Calculus CWB)* Q''" and A4: "Q''↓<CWB>a"
      by blast
    from A1 A3 have "Q ⟼(Calculus CWB)* Q''"
      by (rule steps_add)
    with A4 show "Q⇓<CWB>a"
      by blast
  qed
qed

text ‹A strong reduction simulation is relation R such that for each pair (P, Q) in R and each
      step of P to some P' there exists some Q' such that there is a step of Q to Q' and (P', Q')
      in R.›

abbreviation strong_reduction_simulation :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool"
  where
  "strong_reduction_simulation Rel Cal ≡
   ∀P Q P'. (P, Q) ∈ Rel ∧ P ⟼Cal P' ⟶ (∃Q'. Q ⟼Cal Q' ∧ (P', Q') ∈ Rel)"

text ‹A strong barbed simulation is strong reduction simulation that preserves barbs.›

abbreviation strong_barbed_simulation
  :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool" where
  "strong_barbed_simulation Rel CWB ≡
   strong_reduction_simulation Rel (Calculus CWB) ∧ rel_preserves_barbs Rel CWB"

text ‹A strong labelled simulation is relation R such that for each pair (P, Q) in R and each
      step of P to some P' there exists some Q' such that there is a step of Q to Q' and (P', Q')
      in R.›

abbreviation strong_labelled_simulation
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "strong_labelled_simulation Rel Cal ≡
   ∀P Q α P'. (P, Q) ∈ Rel ∧ P ─α→Cal P' ⟶ (∃Q'. Q ─α→Cal Q' ∧ (P', Q') ∈ Rel)"

text ‹A strong strong simulation is also a weak simulation.›

lemma strong_impl_weak_reduction_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes simulation: "strong_reduction_simulation Rel Cal"
  shows "weak_reduction_simulation Rel Cal"
proof clarify
  fix P Q P'
  assume A1: "(P, Q) ∈ Rel"
  assume "P ⟼Cal* P'"
  from this obtain n where "P ⟼Cal⇗n⇖ P'"
    by (auto simp add: steps_def)
  thus "∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel"
  proof (induct n arbitrary: P')
    case 0
    assume "P ⟼Cal⇗0⇖ P'"
    hence "P = P'"
      by (simp add: steps_refl)
    moreover have "Q ⟼Cal* Q"
      by (rule steps_refl)
    ultimately show "∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel"
      using A1
      by blast
  next
    case (Suc n P'')
    assume "P ⟼Cal⇗Suc n⇖ P''"
    from this obtain P' where A2: "P ⟼Cal⇗n⇖P'" and A3: "P' ⟼Cal P''"
      by auto
    assume "⋀P'. P ⟼Cal⇗n⇖ P' ⟹ ∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel"
    with A2 obtain Q' where A4: "Q ⟼Cal* Q'" and A5: "(P', Q') ∈ Rel"
      by blast
    from simulation A5 A3 obtain Q'' where A6: "Q' ⟼Cal Q''" and A7: "(P'', Q'') ∈ Rel"
      by blast
    from A4 A6 have "Q ⟼Cal* Q''"
      using steps_add[where P="Q" and Q="Q'" and R="Q''"]
      by (simp add: step_to_steps)
    with A7 show "∃Q'. Q ⟼Cal* Q' ∧ (P'', Q') ∈ Rel"
      by blast
  qed
qed

lemma strong_barbed_simulation_impl_weak_preservation_of_barbs:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes simulation: "strong_barbed_simulation Rel CWB"
  shows "rel_weakly_preserves_barbs Rel CWB"
proof clarify
  fix P Q a P'
  assume "(P, Q) ∈ Rel" and "P ⟼(Calculus CWB)* P'"
  with simulation obtain Q' where A1: "Q ⟼(Calculus CWB)* Q'" and A2: "(P', Q') ∈ Rel"
    using strong_impl_weak_reduction_simulation[where Rel="Rel" and Cal="Calculus CWB"]
    by blast
  assume "P'↓<CWB>a"
  with simulation A2 have "Q'↓<CWB>a"
    by blast
  with A1 show "Q⇓<CWB>a"
    by blast
qed

lemma strong_impl_weak_barbed_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes simulation: "strong_barbed_simulation Rel CWB"
  shows "weak_barbed_simulation Rel CWB"
  using simulation
        strong_impl_weak_reduction_simulation[where Rel="Rel" and Cal="Calculus CWB"]
        strong_barbed_simulation_impl_weak_preservation_of_barbs[where Rel="Rel" and CWB="CWB"]
  by blast

lemma strong_simulation_impl_preservation_weak_internal_steps:
  fixes Rel    :: "('proc × 'proc) set"
    and Cal    :: "('proc, 'lab) labelledProcessCalculus"
    and P Q P' :: "'proc"
  assumes simulation: "strong_labelled_simulation Rel Cal"
      and relation:   "(P, Q) ∈ Rel"
      and steps:      "P →Cal* P'"
    shows "∃Q'. Q →Cal* Q' ∧ (P', Q') ∈ Rel"
  using steps simulation relation
proof (induct)
  case (WTS_refl P Cal)
  assume "(P, Q) ∈ Rel"
  moreover have "Q →Cal* Q"
    using weakTauStep.WTS_refl[of Q Cal] .
  ultimately show "∃Q'. Q →Cal* Q' ∧ (P, Q') ∈ Rel"
    by blast
next
  case (WTS_trans P Cal P' P'')
  from WTS_trans(2) have IH: "strong_labelled_simulation Rel Cal ∧ (P, Q) ∈ Rel ⟹
                              ∃Q'. Q →Cal* Q' ∧ (P', Q') ∈ Rel"
    by simp
  assume A1: "strong_labelled_simulation Rel Cal" and "(P, Q) ∈ Rel"
  with IH obtain Q' where A2: "Q →Cal* Q'" and A3: "(P', Q') ∈ Rel"
    by blast
  assume "P' ─τ-Cal→Cal P''"
  with A1 A3 obtain Q'' where A4: "Q' ─τ-Cal→Cal Q''" and A5: "(P'', Q'') ∈ Rel"
    by blast
  from A2 A4 have "Q →Cal* Q''"
    using weakTauStep.WTS_trans[of Q Cal Q' Q'']
    by simp
  with A5 show "∃Q''. Q →Cal* Q'' ∧ (P'', Q'') ∈ Rel"
    by blast
qed

lemma strong_impl_weak_labelled_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes simulation: "strong_labelled_simulation Rel Cal"
  shows "weak_labelled_simulation Rel Cal"
proof clarify
  fix P Q α P'
  assume A1: "(P, Q) ∈ Rel"
  assume "P ─⁀α→Cal* P'"
  thus "∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel"
    unfolding weakLabelledStep_def
  proof (cases "α = τ-Cal", simp_all)
    assume "α = τ-Cal"
    assume "P →Cal* P'"
    with simulation A1 show "∃Q'. Q →Cal* Q' ∧ (P', Q') ∈ Rel"
      using strong_simulation_impl_preservation_weak_internal_steps[of Rel Cal P Q P']
      by simp
  next
    assume A2: "α ≠ τ-Cal" and "P ─α→Cal* P'"
    then obtain R S where A3: "P →Cal* R" and A4: "R ─α→Cal S" and A5: "S →Cal* P'"
      unfolding weakLabelledActionStep_def
      by blast
    from simulation A1 A3 obtain R' where A6: "Q →Cal* R'" and A7: "(R, R') ∈ Rel"
      using strong_simulation_impl_preservation_weak_internal_steps[of Rel Cal P Q R]
      by blast
    from simulation A4 A7 obtain S' where A8: "R' ─α→Cal S'" and A9: "(S, S') ∈ Rel"
      by blast
    from simulation A5 A9 obtain Q' where A10: "S' →Cal* Q'" and A11: "(P', Q') ∈ Rel"
      using strong_simulation_impl_preservation_weak_internal_steps[of Rel Cal S S' P']
      by blast
    from A2 A6 A8 A10 have "Q ─α→Cal* Q'"
      unfolding weakLabelledActionStep_def
      by blast
    with A11 show "∃Q'. Q ─α→Cal* Q' ∧ (P', Q') ∈ Rel"
      by blast
  qed
qed

text ‹The reflexive and/or transitive closure of a strong simulation is a strong simulation.›

lemma strong_reduction_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes simulation: "strong_reduction_simulation Rel Cal"
  shows "strong_reduction_simulation (Rel⇧=) Cal"
    and "strong_reduction_simulation (Rel⇧+) Cal"
    and "strong_reduction_simulation (Rel⇧*) Cal"
proof -
  from simulation show A: "strong_reduction_simulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast)
  have B: "⋀Rel. strong_reduction_simulation Rel Cal ⟹ strong_reduction_simulation (Rel⇧+) Cal"
  proof clarify
    fix Rel P Q P'
    assume B1: "strong_reduction_simulation Rel Cal"
    assume "(P, Q) ∈ Rel⇧+" and "P ⟼Cal P'"
    thus "∃Q'. Q ⟼Cal Q' ∧ (P', Q') ∈ Rel⇧+"
    proof (induct arbitrary: P')
      fix Q P'
      assume "(P, Q) ∈ Rel" and "P ⟼Cal P'"
      with B1 obtain Q' where "Q ⟼Cal Q'" and "(P', Q') ∈ Rel"
        by blast
      thus "∃Q'. Q ⟼Cal Q' ∧ (P', Q') ∈ Rel⇧+"
        by auto
    next
      case (step Q R P')
      assume "⋀P'. P ⟼Cal P' ⟹ (∃Q'. Q ⟼Cal Q' ∧ (P', Q') ∈ Rel⇧+)"
         and "P ⟼Cal P'"
      from this obtain Q' where B2: "Q ⟼Cal Q'" and B3: "(P', Q') ∈ Rel⇧+"
        by blast
      assume "(Q, R) ∈ Rel"
      with B1 B2 obtain R' where B4: "R ⟼Cal R'" and B5: "(Q', R') ∈ Rel⇧+"
        by blast
      from B3 B5 have "(P', R') ∈ Rel⇧+"
        by simp
      with B4 show "∃R'. R ⟼Cal R' ∧ (P', R') ∈ Rel⇧+"
        by blast
    qed
  qed
  with simulation show "strong_reduction_simulation (Rel⇧+) Cal"
    by blast
  from simulation A B[where Rel="Rel⇧="]
  show "strong_reduction_simulation (Rel⇧*) Cal"
    using trancl_reflcl[of Rel]
    by fast
qed

lemma strong_barbed_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes simulation: "strong_barbed_simulation Rel CWB"
  shows "strong_barbed_simulation (Rel⇧=) CWB"
    and "strong_barbed_simulation (Rel⇧+) CWB"
    and "strong_barbed_simulation (Rel⇧*) CWB"
proof -
  from simulation show "strong_barbed_simulation (Rel⇧=) CWB"
      using strong_reduction_simulation_and_closures(1)[where Rel="Rel" and Cal="Calculus CWB"]
            preservation_of_barbs_and_closures(1)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from simulation show "strong_barbed_simulation (Rel⇧+) CWB"
      using strong_reduction_simulation_and_closures(2)[where Rel="Rel" and Cal="Calculus CWB"]
            preservation_of_barbs_and_closures(2)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from simulation show "strong_barbed_simulation (Rel⇧*) CWB"
      using strong_reduction_simulation_and_closures(3)[where Rel="Rel" and Cal="Calculus CWB"]
            preservation_of_barbs_and_closures(3)[where Rel="Rel" and CWB="CWB"]
    by blast
qed

lemma strong_labelled_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes simulation: "strong_labelled_simulation Rel Cal"
  shows "strong_labelled_simulation (Rel⇧=) Cal"
    and "strong_labelled_simulation (Rel⇧+) Cal"
    and "strong_labelled_simulation (Rel⇧*) Cal"
proof -
  from simulation show A: "strong_labelled_simulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast)
  have B: "⋀Rel. strong_labelled_simulation Rel Cal ⟹ strong_labelled_simulation (Rel⇧+) Cal"
  proof clarify
    fix Rel P Q α P'
    assume B1: "strong_labelled_simulation Rel Cal"
    assume "(P, Q) ∈ Rel⇧+" and "P ─α→Cal P'"
    thus "∃Q'. Q ─α→Cal Q' ∧ (P', Q') ∈ Rel⇧+"
    proof (induct arbitrary: P')
      fix Q P'
      assume "(P, Q) ∈ Rel" and "P ─α→Cal P'"
      with B1 obtain Q' where "Q ─α→Cal Q'" and "(P', Q') ∈ Rel"
        by blast
      thus "∃Q'. Q ─α→Cal Q' ∧ (P', Q') ∈ Rel⇧+"
        by auto
    next
      case (step Q R P')
      assume "⋀P'. P ─α→Cal P' ⟹ (∃Q'. Q ─α→Cal Q' ∧ (P', Q') ∈ Rel⇧+)"
         and "P ─α→Cal P'"
      from this obtain Q' where B2: "Q ─α→Cal Q'" and B3: "(P', Q') ∈ Rel⇧+"
        by blast
      assume "(Q, R) ∈ Rel"
      with B1 B2 obtain R' where B4: "R ─α→Cal R'" and B5: "(Q', R') ∈ Rel⇧+"
        by blast
      from B3 B5 have "(P', R') ∈ Rel⇧+"
        by simp
      with B4 show "∃R'. R ─α→Cal R' ∧ (P', R') ∈ Rel⇧+"
        by blast
    qed
  qed
  with simulation show "strong_labelled_simulation (Rel⇧+) Cal"
    by blast
  from simulation A B[where Rel="Rel⇧="]
  show "strong_labelled_simulation (Rel⇧*) Cal"
    using trancl_reflcl[of Rel]
    by fast
qed

subsection ‹Contrasimulation›

text ‹A weak (reduction) contrasimulation is relation R such that if (P, Q) in R and P evolves to
      some P' then there exists some Q' such that Q evolves to Q' and (Q', P') in R.›

abbreviation weak_reduction_contrasimulation
  :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool" where
  "weak_reduction_contrasimulation Rel Cal ≡
   ∀P Q P'. (P, Q) ∈ Rel ∧ P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel)"

text ‹A weak barbed contrasimulation is weak reduction contrasimulation that weakly preserves
      barbs.›

abbreviation weak_barbed_contrasimulation
  :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool" where
  "weak_barbed_contrasimulation Rel CWB ≡
   weak_reduction_contrasimulation Rel (Calculus CWB) ∧ rel_weakly_preserves_barbs Rel CWB"

text ‹A weak labelled contrasimulation is relation R such that if (P, Q) in R and P evolves to
      some P' using word w of labels then there exists some Q' such that Q evolves to Q' using w
      and (Q', P') in R.›

abbreviation weak_labelled_contrasimulation
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "weak_labelled_contrasimulation Rel Cal ≡
   ∀P Q w P'. (P, Q) ∈ Rel ∧ P ─⌢w→Cal* P' ⟶ (∃Q'. Q ─⌢w→Cal* Q' ∧ (Q', P') ∈ Rel)"

text ‹The reflexive and/or transitive closure of a weak contrasimulation is a weak
      contrasimulation.›

lemma weak_reduction_contrasimulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes contrasimulation: "weak_reduction_contrasimulation Rel Cal"
  shows "weak_reduction_contrasimulation (Rel⇧=) Cal"
    and "weak_reduction_contrasimulation (Rel⇧+) Cal"
    and "weak_reduction_contrasimulation (Rel⇧*) Cal"
proof -
  from contrasimulation show A: "weak_reduction_contrasimulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast)
  have B: "⋀Rel. weak_reduction_contrasimulation Rel Cal
           ⟹ weak_reduction_contrasimulation (Rel⇧+) Cal"
  proof clarify
    fix Rel P Q P'
    assume B1: "weak_reduction_contrasimulation Rel Cal"
    assume "(P, Q) ∈ Rel⇧+" and "P ⟼Cal* P'"
    thus "∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel⇧+"
    proof (induct arbitrary: P')
      fix Q P'
      assume "(P, Q) ∈ Rel" and "P ⟼Cal* P'"
      with B1 obtain Q' where "Q ⟼Cal* Q'" and "(Q', P') ∈ Rel"
        by blast
      thus "∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel⇧+"
        by auto
    next
      case (step Q R P')
      assume "⋀P'. P ⟼Cal* P' ⟹ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel⇧+)"
         and "P ⟼Cal* P'"
      from this obtain Q' where B2: "Q ⟼Cal* Q'" and B3: "(Q', P') ∈ Rel⇧+"
        by blast
      assume "(Q, R) ∈ Rel"
      with B1 B2 obtain R' where B4: "R ⟼Cal* R'" and B5: "(R', Q') ∈ Rel⇧+"
        by blast
      from B5 B3 have "(R', P') ∈ Rel⇧+"
        by simp
      with B4 show "∃R'. R ⟼Cal* R' ∧ (R', P') ∈ Rel⇧+"
        by blast
    qed
  qed
  with contrasimulation show "weak_reduction_contrasimulation (Rel⇧+) Cal"
    by blast
  from contrasimulation A B[where Rel="Rel⇧="]
  show "weak_reduction_contrasimulation (Rel⇧*) Cal"
    using trancl_reflcl[of Rel]
    by fast
qed

lemma weak_barbed_contrasimulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes contrasimulation: "weak_barbed_contrasimulation Rel CWB"
  shows "weak_barbed_contrasimulation (Rel⇧=) CWB"
    and "weak_barbed_contrasimulation (Rel⇧+) CWB"
    and "weak_barbed_contrasimulation (Rel⇧*) CWB"
proof -
  from contrasimulation show "weak_barbed_contrasimulation (Rel⇧=) CWB"
    using weak_reduction_contrasimulation_and_closures(1)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_preservation_of_barbs_and_closures(1)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from contrasimulation show "weak_barbed_contrasimulation (Rel⇧+) CWB"
    using weak_reduction_contrasimulation_and_closures(2)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_preservation_of_barbs_and_closures(2)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from contrasimulation show "weak_barbed_contrasimulation (Rel⇧*) CWB"
    using weak_reduction_contrasimulation_and_closures(3)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_preservation_of_barbs_and_closures(3)[where Rel="Rel" and CWB="CWB"]
    by blast
qed

lemma weak_labelled_contrasimulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes contrasimulation: "weak_labelled_contrasimulation Rel Cal"
  shows "weak_labelled_contrasimulation (Rel⇧=) Cal"
    and "weak_labelled_contrasimulation (Rel⇧+) Cal"
    and "weak_labelled_contrasimulation (Rel⇧*) Cal"
proof -
  from contrasimulation show A: "weak_labelled_contrasimulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast)
  have B: "⋀Rel. weak_labelled_contrasimulation Rel Cal
           ⟹ weak_labelled_contrasimulation (Rel⇧+) Cal"
  proof clarify
    fix Rel P Q w P'
    assume B1: "weak_labelled_contrasimulation Rel Cal"
    assume "(P, Q) ∈ Rel⇧+" and "P ─⌢w→Cal* P'"
    thus "∃Q'. Q ─⌢w→Cal* Q' ∧ (Q', P') ∈ Rel⇧+"
    proof (induct arbitrary: P')
      fix Q P'
      assume "(P, Q) ∈ Rel" and "P ─⌢w→Cal* P'"
      with B1 obtain Q' where "Q ─⌢w→Cal* Q'" and "(Q', P') ∈ Rel"
        by blast
      thus "∃Q'. Q ─⌢w→Cal* Q' ∧ (Q', P') ∈ Rel⇧+"
        by auto
    next
      case (step Q R P')
      assume "⋀P'. P ─⌢w→Cal* P' ⟹ (∃Q'. Q ─⌢w→Cal* Q' ∧ (Q', P') ∈ Rel⇧+)"
         and "P ─⌢w→Cal* P'"
      from this obtain Q' where B2: "Q ─⌢w→Cal* Q'" and B3: "(Q', P') ∈ Rel⇧+"
        by blast
      assume "(Q, R) ∈ Rel"
      with B1 B2 obtain R' where B4: "R ─⌢w→Cal* R'" and B5: "(R', Q') ∈ Rel⇧+"
        by blast
      from B5 B3 have "(R', P') ∈ Rel⇧+"
        by simp
      with B4 show "∃R'. R ─⌢w→Cal* R' ∧ (R', P') ∈ Rel⇧+"
        by blast
    qed
  qed
  with contrasimulation show "weak_labelled_contrasimulation (Rel⇧+) Cal"
    by blast
  from contrasimulation A B[where Rel="Rel⇧="]
  show "weak_labelled_contrasimulation (Rel⇧*) Cal"
    using trancl_reflcl[of Rel]
    by fast
qed

subsection ‹Coupled Simulation›

text ‹A weak (reduction) coupled simulation is relation R such that if (P, Q) in R and P evolves to
      some P' then there exists some Q' such that Q evolves to Q' and (P', Q') in R and there exits
      some Q' such that Q evolves to Q' and (Q', P') in R.›

abbreviation weak_reduction_coupled_simulation
  :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool" where
  "weak_reduction_coupled_simulation Rel Cal ≡
   ∀P Q P'. (P, Q) ∈ Rel ∧ P ⟼Cal* P'
   ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel) ∧ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel)"

text ‹A weak barbed coupled simulation is weak reduction coupled simulation that weakly preserves
      barbs.›

abbreviation weak_barbed_coupled_simulation
  :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool" where
  "weak_barbed_coupled_simulation Rel CWB ≡
   weak_reduction_coupled_simulation Rel (Calculus CWB) ∧ rel_weakly_preserves_barbs Rel CWB"

text ‹A weak labelled coupled simulation is relation R such that if (P, Q) in R and P evolves to
      some P' using label a then there exists some Q' such that Q evolves to Q' using a and
      (P', Q') in R (simulation) and there exits some Q' such that Q evolves to Q' and (Q', P) in
      R (coupling).›

abbreviation weak_labelled_coupled_simulation
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "weak_labelled_coupled_simulation Rel Cal ≡
   ∀P Q. (P, Q) ∈ Rel ⟶ (∀α P'. P ─⁀α→Cal* P' ⟶ (∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel))
                          ∧ (∃Q'. Q →Cal* Q' ∧ (Q', P) ∈ Rel)"

text ‹A weak labelled coupled simulation also simulates words of labels including the empty word.›

lemma weak_labelled_coupled_simulation_internal:
  fixes Rel    :: "('proc × 'proc) set"
    and Cal    :: "('proc, 'lab) labelledProcessCalculus"
    and P Q P' :: "'proc"
  assumes simulation: "weak_labelled_coupled_simulation Rel Cal"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P →Cal* P'"
    shows "∃Q'. Q →Cal* Q' ∧ (P', Q') ∈ Rel"
proof -
  from execution have "P ─⁀τ-Cal→Cal* P'"
    unfolding weakLabelledStep_def
    by simp
  with simulation relation obtain Q' where A1: "Q ─⁀τ-Cal→Cal* Q'" and A2: "(P', Q') ∈ Rel"
    by blast
  from A1 have "Q →Cal* Q'"
    unfolding weakLabelledStep_def
    by simp
  with A2 show "∃Q'. Q →Cal* Q' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma weak_labelled_coupled_simulation_word:
  fixes Rel    :: "('proc × 'proc) set"
    and Cal    :: "('proc, 'lab) labelledProcessCalculus"
    and P Q P' :: "'proc"
    and w      :: "'lab list"
  assumes simulation: "weak_labelled_coupled_simulation Rel Cal"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P ─⌢w→Cal* P'"
    shows "∃Q'. Q ─⌢w→Cal* Q' ∧ (P', Q') ∈ Rel"
  using execution simulation relation
proof induct
  case (WLS_Nil P Cal P')
  assume "P →Cal* P'" and "weak_labelled_coupled_simulation Rel Cal" and "(P, Q) ∈ Rel"
  then obtain Q' where A1: "Q →Cal* Q'" and A2: "(P', Q') ∈ Rel"
    using weak_labelled_coupled_simulation_internal[of Rel Cal P Q P']
    by blast
  from A1 have "Q ─⌢[]→Cal* Q'"
    using weakLabelledSequence.WLS_Nil[of Q Cal Q']
    by simp
  with A2 show "∃Q'. Q ─⌢[]→Cal* Q' ∧ (P', Q') ∈ Rel"
    by blast
next
  case (WLS_Cons P w Cal P' α P'')
  from WLS_Cons(2) have IH: "weak_labelled_coupled_simulation Rel Cal ∧ (P, Q) ∈ Rel ⟹
                             ∃Q'. Q ─⌢w→Cal* Q' ∧ (P', Q') ∈ Rel"
    by simp
  assume A1: "weak_labelled_coupled_simulation Rel Cal" and "(P, Q) ∈ Rel"
  with IH obtain Q' where A2: "Q ─⌢w→Cal* Q'" and A3: "(P', Q') ∈ Rel"
    by blast
  assume "P' ─⁀α→Cal* P''"
  with A1 A2 A3 obtain Q'' where A4: "Q' ─⁀α→Cal* Q''" and A5: "(P'', Q'') ∈ Rel"
    by blast
  from A2 A4 have "Q ─⌢(w@[α])→Cal* Q''"
    using weakLabelledSequence.WLS_Cons[of Q w Cal Q' α Q'']
    by simp
  with A5 show "∃Q''. Q ─⌢(w@[α])→Cal* Q'' ∧ (P'', Q'') ∈ Rel"
    by blast
qed

text ‹A weak coupled simulation combines the conditions on a weak simulation and a weak
      contrasimulation.›

lemma weak_reduction_coupled_simulation_versus_simulation_and_contrasimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  shows "weak_reduction_coupled_simulation Rel Cal
         = (weak_reduction_simulation Rel Cal ∧ weak_reduction_contrasimulation Rel Cal)"
  by blast

lemma weak_barbed_coupled_simulation_versus_simulation_and_contrasimulation:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "weak_barbed_coupled_simulation Rel CWB
         = (weak_barbed_simulation Rel CWB ∧ weak_barbed_contrasimulation Rel CWB)"
  by blast

lemma weak_labelled_coupled_simulation_versus_simulation_and_contrasimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  shows "weak_labelled_coupled_simulation Rel Cal
         = (weak_labelled_simulation Rel Cal ∧ weak_labelled_contrasimulation Rel Cal)"
proof auto
  fix P Q w P'
  assume A1: "weak_labelled_coupled_simulation Rel Cal" and "(P, Q) ∈ Rel" and "P ─⌢w→Cal* P'"
  then obtain Q' where A2: "Q ─⌢w→Cal* Q'" and A3: "(P', Q') ∈ Rel"
    using weak_labelled_coupled_simulation_word[of Rel Cal P Q w P']
    by blast
  from A1 A3 obtain Q'' where A4: "Q' →Cal* Q''" and A5: "(Q'', P') ∈ Rel"
    by blast
  from A2 A4 have "Q ─⌢w→Cal* Q''"
    using weakLabelledSequence_extend_by_internal[of Q w Cal Q' Q'']
    by simp
  with A5 show "∃Q''. Q ─⌢w→Cal* Q'' ∧ (Q'', P') ∈ Rel"
    by blast
next
  fix P Q
  assume "weak_labelled_contrasimulation Rel Cal" and "(P, Q) ∈ Rel"
  moreover have "P ─⌢[]→Cal* P"
    using WTS_refl[of P Cal ] WLS_Nil[of P Cal P]
    by simp
  ultimately obtain Q' where A1: "Q ─⌢[]→Cal* Q'" and A2: "(Q', P) ∈ Rel"
    by blast
  hence "Q →Cal* Q'"
    using internal_weakLabelledSequence[of Q Cal Q']
    by simp
  with A2 show "∃Q'. Q →Cal* Q' ∧ (Q', P) ∈ Rel"
    by blast
qed

text ‹The reflexive and/or transitive closure of a weak coupled simulation is a weak coupled
      simulation.›

lemma weak_reduction_coupled_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes coupledSimulation: "weak_reduction_coupled_simulation Rel Cal"
  shows "weak_reduction_coupled_simulation (Rel⇧=) Cal"
    and "weak_reduction_coupled_simulation (Rel⇧+) Cal"
    and "weak_reduction_coupled_simulation (Rel⇧*) Cal"
  using weak_reduction_simulation_and_closures[where Rel="Rel" and Cal="Cal"]
        weak_reduction_contrasimulation_and_closures[where Rel="Rel" and Cal="Cal"]
        weak_reduction_coupled_simulation_versus_simulation_and_contrasimulation[where Rel="Rel"
          and Cal="Cal"]
        coupledSimulation
  by auto

lemma weak_barbed_coupled_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes coupledSimulation: "weak_barbed_coupled_simulation Rel CWB"
  shows "weak_barbed_coupled_simulation (Rel⇧=) CWB"
    and "weak_barbed_coupled_simulation (Rel⇧+) CWB"
    and "weak_barbed_coupled_simulation (Rel⇧*) CWB"
proof -
  from coupledSimulation show "weak_barbed_coupled_simulation (Rel⇧=) CWB"
    using weak_reduction_coupled_simulation_and_closures(1)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_preservation_of_barbs_and_closures(1)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from coupledSimulation show "weak_barbed_coupled_simulation (Rel⇧+) CWB"
    using weak_reduction_coupled_simulation_and_closures(2)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_preservation_of_barbs_and_closures(2)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from coupledSimulation show "weak_barbed_coupled_simulation (Rel⇧*) CWB"
    using weak_reduction_coupled_simulation_and_closures(3)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_preservation_of_barbs_and_closures(3)[where Rel="Rel" and CWB="CWB"]
    by blast
qed

lemma weak_labelled_coupled_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes coupledSimulation: "weak_labelled_coupled_simulation Rel Cal"
  shows "weak_labelled_coupled_simulation (Rel⇧=) Cal"
    and "weak_labelled_coupled_simulation (Rel⇧+) Cal"
    and "weak_labelled_coupled_simulation (Rel⇧*) Cal"
proof -
  from coupledSimulation have A1: "weak_labelled_simulation Rel Cal"
                          and A2: "weak_labelled_contrasimulation Rel Cal"
    using weak_labelled_coupled_simulation_versus_simulation_and_contrasimulation[where Rel="Rel"
            and Cal="Cal"]
    by simp_all
  from A1 have A3: "weak_labelled_simulation (Rel⇧=) Cal"
           and A4: "weak_labelled_simulation (Rel⇧+) Cal"
           and A5: "weak_labelled_simulation (Rel⇧*) Cal"
    using weak_labelled_simulation_and_closures[where Rel="Rel" and Cal="Cal"]
    by simp_all
  from A2 have A6: "weak_labelled_contrasimulation (Rel⇧=) Cal"
           and A7: "weak_labelled_contrasimulation (Rel⇧+) Cal"
           and A8: "weak_labelled_contrasimulation (Rel⇧*) Cal"
    using weak_labelled_contrasimulation_and_closures[where Rel="Rel" and Cal="Cal"]
    by simp_all
  from A3 A6 show "weak_labelled_coupled_simulation (Rel⇧=) Cal"
    using weak_labelled_coupled_simulation_versus_simulation_and_contrasimulation[where Rel="Rel⇧="
            and Cal="Cal"]
    by simp
  from A4 A7 show "weak_labelled_coupled_simulation (Rel⇧+) Cal"
    using weak_labelled_coupled_simulation_versus_simulation_and_contrasimulation[where Rel="Rel⇧+"
            and Cal="Cal"]
    by simp
  from A5 A8 show "weak_labelled_coupled_simulation (Rel⇧*) Cal"
    using weak_labelled_coupled_simulation_versus_simulation_and_contrasimulation[where Rel="Rel⇧*"
            and Cal="Cal"]
    by simp
qed

subsection ‹Correspondence Simulation›

text ‹A weak (reduction) correspondence simulation is relation R such that
      (1) if (P, Q) in R and P evolves to some P' then there exists some Q' such that Q evolves to
          Q' and (P', Q') in R, and
      (2) if (P, Q) in R and Q evolves to some Q' then there exists some P'' and Q'' such that P
          evolves to P'' and Q' evolves to Q'' and (P'', Q'') in R.›

abbreviation weak_reduction_correspondence_simulation
  :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool" where
  "weak_reduction_correspondence_simulation Rel Cal ≡
   (∀P Q P'. (P, Q) ∈ Rel ∧ P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel))
   ∧ (∀P Q Q'. (P, Q) ∈ Rel ∧ Q ⟼Cal* Q'
      ⟶ (∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel))"

text ‹A weak barbed correspondence simulation is weak reduction correspondence simulation that
      weakly respects barbs.›

abbreviation weak_barbed_correspondence_simulation
  :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool" where
  "weak_barbed_correspondence_simulation Rel CWB ≡
   weak_reduction_correspondence_simulation Rel (Calculus CWB)
   ∧ rel_weakly_respects_barbs Rel CWB"

text ‹A weak labelled correspondence simulation is relation R such that
      (1) if (P, Q) in R and P evolves to some P' using label a then there exists some Q' such that
          Q evolves to Q' using a and (P', Q') in R, and
      (2) if (P, Q) in R and Q evolves to some Q' using label a then there exists some P'' and Q''
          such that P evolves to P'' using a and Q' evolves to Q'' using only internal steps and
          (P'', Q'') in R.›

abbreviation weak_labelled_correspondence_simulation
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "weak_labelled_correspondence_simulation Rel Cal ≡
   (∀P Q α P'. (P, Q) ∈ Rel ∧ P ─⁀α→Cal* P' ⟶ (∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel))
   ∧ (∀P Q α Q'. (P, Q) ∈ Rel ∧ Q ─⁀α→Cal* Q'
      ⟶ (∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel))"

text ‹For each weak correspondence simulation R there exists a weak coupled simulation that
      contains all pairs of R in both directions.›

inductive_set cSim_cs :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ ('proc × 'proc) set"
    for Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  where
  left:  "⟦Q ⟼Cal* Q'; (P', Q') ∈ Rel⟧ ⟹ (P', Q) ∈ cSim_cs Rel Cal"
| right: "⟦P ⟼Cal* P'; (Q, P) ∈ Rel⟧ ⟹ (P', Q) ∈ cSim_cs Rel Cal"
| trans: "⟦(P, Q) ∈ cSim_cs Rel Cal; (Q, R) ∈ cSim_cs Rel Cal⟧ ⟹ (P, R) ∈ cSim_cs Rel Cal"

lemma weak_reduction_correspondence_simulation_impl_coupled_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes corrSim: "weak_reduction_correspondence_simulation Rel Cal"
  shows "weak_reduction_coupled_simulation (cSim_cs Rel Cal) Cal"
    and "∀P Q. (P, Q) ∈ Rel ⟶ (P, Q) ∈ cSim_cs Rel Cal ∧ (Q, P) ∈ cSim_cs Rel Cal"
proof -
  show "weak_reduction_coupled_simulation (cSim_cs Rel Cal) Cal"
  proof (rule allI, rule allI, rule allI, rule impI, erule conjE)
    fix P Q P'
    assume "(P, Q) ∈ cSim_cs Rel Cal" and "P ⟼Cal* P'"
    thus "(∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ cSim_cs Rel Cal)
          ∧ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ cSim_cs Rel Cal)"
    proof (induct arbitrary: P')
      case (left Q Q' P)
      assume "(P, Q') ∈ Rel" and "P ⟼Cal* P'"
      with corrSim obtain Q'' where A1: "Q' ⟼Cal* Q''" and A2: "(P', Q'') ∈ Rel"
        by blast
      assume A3: "Q ⟼Cal* Q'"
      from this A1 have A4: "Q ⟼Cal* Q''"
        by (rule steps_add[where P="Q" and Q="Q'" and R="Q''"])
      have "Q'' ⟼Cal* Q''"
        by (rule steps_refl)
      with A2 have A5: "(Q'', P') ∈ cSim_cs Rel Cal"
        by (simp add: cSim_cs.right)
      from A1 A2 have "(P', Q') ∈ cSim_cs Rel Cal"
        by (rule cSim_cs.left)
      with A4 A5 A3 show ?case
        by blast
    next
      case (right P P' Q P'')
      assume "P ⟼Cal* P'" and "P' ⟼Cal* P''"
      hence B1: "P ⟼Cal* P''"
        by (rule steps_add[where P="P" and Q="P'" and R="P''"])
      assume B2: "(Q, P) ∈ Rel"
      with corrSim B1 obtain Q''' P''' where B3: "Q ⟼Cal* Q'''" and B4: "P'' ⟼Cal* P'''"
                                       and B5: "(Q''', P''') ∈ Rel"
        by blast
      from B4 B5 have B6: "(Q''', P'') ∈ cSim_cs Rel Cal"
        by (rule cSim_cs.left)
      have B7: "Q ⟼Cal* Q"
        by (rule steps_refl)
      from B1 B2 have "(P'', Q) ∈ cSim_cs Rel Cal"
        by (rule cSim_cs.right)
      with B3 B6 B7 show ?case
        by blast
    next
      case (trans P Q R P')
      assume "P ⟼Cal* P'"
         and "⋀P'. P ⟼Cal* P' ⟹ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ cSim_cs Rel Cal)
                                     ∧ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ cSim_cs Rel Cal)"
      from this obtain Q1 Q2 where C1: "Q ⟼Cal* Q1" and C2: "(Q1, P') ∈ cSim_cs Rel Cal"
                             and C3: "Q ⟼Cal* Q2" and C4: "(P', Q2) ∈ cSim_cs Rel Cal"
        by blast
      assume C5: "⋀Q'. Q ⟼Cal* Q' ⟹ (∃R'. R ⟼Cal* R' ∧ (Q', R') ∈ cSim_cs Rel Cal)
                                         ∧ (∃R'. R ⟼Cal* R' ∧ (R', Q') ∈ cSim_cs Rel Cal)"
      with C1 obtain R1 where C6: "R ⟼Cal* R1" and C7: "(R1, Q1) ∈ cSim_cs Rel Cal"
        by blast
      from C7 C2 have C8: "(R1, P') ∈ cSim_cs Rel Cal"
        by (rule cSim_cs.trans)
      from C3 C5 obtain R2 where C9: "R ⟼Cal* R2" and C10: "(Q2, R2) ∈ cSim_cs Rel Cal"
        by blast
      from C4 C10 have "(P', R2) ∈ cSim_cs Rel Cal"
        by (rule cSim_cs.trans)
      with C6 C8 C9 show ?case
        by blast
    qed
  qed
next
  show "∀P Q. (P, Q) ∈ Rel ⟶ (P, Q) ∈ cSim_cs Rel Cal ∧ (Q, P) ∈ cSim_cs Rel Cal"
  proof clarify
    fix P Q
    have "Q ⟼Cal* Q"
      by (rule steps_refl)
    moreover assume "(P, Q) ∈ Rel"
    ultimately show "(P, Q) ∈ cSim_cs Rel Cal ∧ (Q, P) ∈ cSim_cs Rel Cal"
      by (simp add: cSim_cs.left cSim_cs.right)
  qed
qed

lemma weak_barbed_correspondence_simulation_impl_coupled_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes corrSim: "weak_barbed_correspondence_simulation Rel CWB"
  shows "weak_barbed_coupled_simulation (cSim_cs Rel (Calculus CWB)) CWB"
    and "∀P Q. (P, Q) ∈ Rel ⟶ (P, Q) ∈ cSim_cs Rel (Calculus CWB)
                                ∧ (Q, P) ∈ cSim_cs Rel (Calculus CWB)"
proof -
  show "weak_barbed_coupled_simulation (cSim_cs Rel (Calculus CWB)) CWB"
  proof
    from corrSim
    show "weak_reduction_coupled_simulation (cSim_cs Rel (Calculus CWB)) (Calculus CWB)"
      using weak_reduction_correspondence_simulation_impl_coupled_simulation(1)[where Rel="Rel"
            and Cal="Calculus CWB"]
      by blast
  next
    show "rel_weakly_preserves_barbs (cSim_cs Rel (Calculus CWB)) CWB"
    proof clarify
      fix P Q a P'
      assume "(P, Q) ∈ cSim_cs Rel (Calculus CWB)" and "P ⟼(Calculus CWB)* P'" and "P'↓<CWB>a"
      thus "Q⇓<CWB>a"
      proof (induct arbitrary: P')
        case (left Q Q' P P')
        assume "(P, Q') ∈ Rel" and "P ⟼(Calculus CWB)* P'" and "P'↓<CWB>a"
        with corrSim obtain Q'' where A1: "Q' ⟼(Calculus CWB)* Q''" and A2: "Q''↓<CWB>a"
          by blast
        assume "Q ⟼(Calculus CWB)* Q'"
        from this A1 have "Q ⟼(Calculus CWB)* Q''"
          by (rule steps_add)
        with A2 show "Q⇓<CWB>a"
          by blast
      next
        case (right P P' Q P'')
        assume "(Q, P) ∈ Rel"
        moreover assume "P ⟼(Calculus CWB)* P'" and "P' ⟼(Calculus CWB)* P''"
        hence "P ⟼(Calculus CWB)* P''"
          by (rule steps_add)
        moreover assume "P''↓<CWB>a"
        ultimately show "Q⇓<CWB>a"
          using corrSim
          by blast
      next
        case (trans P Q R P')
        assume "⋀P'. P ⟼(Calculus CWB)* P' ⟹ P'↓<CWB>a ⟹ Q⇓<CWB>a"
           and "P ⟼(Calculus CWB)* P'" and "P'↓<CWB>a"
           and "⋀Q'. Q ⟼(Calculus CWB)* Q' ⟹ Q'↓<CWB>a ⟹ R⇓<CWB>a"
        thus "R⇓<CWB>a"
          by blast
      qed
    qed
  qed
next
  from corrSim show "∀P Q. (P, Q) ∈ Rel ⟶ (P, Q) ∈ cSim_cs Rel (Calculus CWB)
                                            ∧ (Q, P) ∈ cSim_cs Rel (Calculus CWB)"
    using weak_reduction_correspondence_simulation_impl_coupled_simulation(2)[where Rel="Rel"
          and Cal="Calculus CWB"]
    by blast
qed

text ‹The reflexive and/or transitive closure of a weak correspondence simulation is a weak
      correspondence simulation.›

lemma reduction_correspondence_simulation_condition_trans:
  fixes Cal   :: "'proc processCalculus"
    and P Q R :: "'proc"
    and Rel   :: "('proc × 'proc) set"
  assumes A1: "∀Q'. Q ⟼Cal* Q' ⟶ (∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel)"
      and A2: "∀R'. R ⟼Cal* R' ⟶ (∃Q'' R''. Q ⟼Cal* Q'' ∧ R' ⟼Cal* R'' ∧ (Q'', R'') ∈ Rel)"
      and A3: "weak_reduction_simulation Rel Cal"
      and A4: "trans Rel"
  shows "∀R'. R ⟼Cal* R' ⟶ (∃P'' R''. P ⟼Cal* P'' ∧ R' ⟼Cal* R'' ∧ (P'', R'') ∈ Rel)"
proof clarify
  fix R'
  assume "R ⟼Cal* R'"
  with A2 obtain Q'' R'' where A5: "Q ⟼Cal* Q''" and A6: "R' ⟼Cal* R''"
                           and A7: "(Q'', R'') ∈ Rel"
    by blast
  from A1 A5 obtain P''' Q''' where A8: "P ⟼Cal* P'''" and A9: "Q'' ⟼Cal* Q'''"
                               and A10: "(P''', Q''') ∈ Rel"
    by blast
  from A3 A7 A9 obtain R''' where A11: "R'' ⟼Cal* R'''" and A12: "(Q''', R''') ∈ Rel"
    by blast
  from A6 A11 have A13: "R' ⟼Cal* R'''"
    by (rule steps_add[where P="R'" and Q="R''" and R="R'''"])
  from A4 A10 A12 have "(P''', R''') ∈ Rel"
    unfolding trans_def
    by blast
  with A8 A13 show "∃P'' R''. P ⟼Cal* P'' ∧ R' ⟼Cal* R'' ∧ (P'', R'') ∈ Rel"
    by blast
qed

lemma weak_reduction_correspondence_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes corrSim: "weak_reduction_correspondence_simulation Rel Cal"
  shows "weak_reduction_correspondence_simulation (Rel⇧=) Cal"
    and "weak_reduction_correspondence_simulation (Rel⇧+) Cal"
    and "weak_reduction_correspondence_simulation (Rel⇧*) Cal"
proof -
  show A: "weak_reduction_correspondence_simulation (Rel⇧=) Cal"
  proof
    from corrSim show "weak_reduction_simulation (Rel⇧=) Cal"
      using weak_reduction_simulation_and_closures(1)[where Rel="Rel" and Cal="Cal"]
      by blast
  next
    show "∀P Q Q'. (P, Q) ∈ Rel⇧= ∧ Q ⟼Cal* Q'
          ⟶ (∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧=)"
    proof clarify
      fix P Q Q'
      assume "(P, Q) ∈ Rel⇧=" and A1: "Q ⟼Cal* Q'"
      moreover have "P = Q ⟹ ∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
      proof -
        assume "P = Q"
        moreover have "Q' ⟼Cal* Q'"
          by (rule steps_refl)
        ultimately show "∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
          using A1
          by blast
      qed
      moreover
      have "(P, Q) ∈ Rel ⟹ ∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
      proof -
        assume "(P, Q) ∈ Rel"
        with corrSim A1 obtain P'' Q'' where "P ⟼Cal* P''" and "Q' ⟼Cal* Q''"
                                         and "(P'', Q'') ∈ Rel"
          by blast
        thus "∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
          by auto
      qed
      ultimately show "∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
        by auto
    qed
  qed
  have B: "⋀Rel. weak_reduction_correspondence_simulation Rel Cal
           ⟹ weak_reduction_correspondence_simulation (Rel⇧+) Cal"
  proof
    fix Rel
    assume "weak_reduction_correspondence_simulation Rel Cal"
    thus "weak_reduction_simulation (Rel⇧+) Cal"
      using weak_reduction_simulation_and_closures(2)[where Rel="Rel" and Cal="Cal"]
      by blast
  next
    fix Rel
    assume B1: "weak_reduction_correspondence_simulation Rel Cal"
    show "∀P Q Q'. (P, Q) ∈ Rel⇧+ ∧ Q ⟼Cal* Q'
          ⟶ (∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧+)"
    proof clarify
      fix P Q Q'
      assume "(P, Q) ∈ Rel⇧+" and "Q ⟼Cal* Q'"
      thus "∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧+"
      proof (induct arbitrary: Q')
        fix Q Q'
        assume "(P, Q) ∈ Rel" and "Q ⟼Cal* Q'"
        with B1 obtain P'' Q'' where B2: "P ⟼Cal* P''" and B3: "Q' ⟼Cal* Q''"
                                 and B4: "(P'', Q'') ∈ Rel"
          by blast
        from B4 have "(P'', Q'') ∈ Rel⇧+"
          by simp
        with B2 B3 show "∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧+"
          by blast
      next
        case (step Q R R')
        assume "⋀Q'. Q ⟼Cal* Q'
                ⟹ ∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧+"
        moreover assume "(Q, R) ∈ Rel"
        with B1
        have "⋀R'. R ⟼Cal* R' ⟹ ∃Q'' R''. Q ⟼Cal* Q'' ∧ R' ⟼Cal* R'' ∧ (Q'', R'') ∈ Rel⇧+"
          by blast
        moreover from B1 have "weak_reduction_simulation (Rel⇧+) Cal"
          using weak_reduction_simulation_and_closures(2)[where Rel="Rel" and Cal="Cal"]
          by blast
        moreover have "trans (Rel⇧+)"
          using trans_trancl[of Rel]
          by blast
        moreover assume "R ⟼Cal* R'"
        ultimately show "∃P'' R''. P ⟼Cal* P'' ∧ R' ⟼Cal* R'' ∧ (P'', R'') ∈ Rel⇧+"
          using reduction_correspondence_simulation_condition_trans[where Rel="Rel⇧+"]
          by blast
      qed
    qed
  qed
  from corrSim B[where Rel="Rel"] show "weak_reduction_correspondence_simulation (Rel⇧+) Cal"
    by blast
  from A B[where Rel="Rel⇧="]
  show "weak_reduction_correspondence_simulation (Rel⇧*) Cal"
    using trancl_reflcl[of Rel]
    by auto
qed

lemma weak_barbed_correspondence_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes corrSim: "weak_barbed_correspondence_simulation Rel CWB"
  shows "weak_barbed_correspondence_simulation (Rel⇧=) CWB"
    and "weak_barbed_correspondence_simulation (Rel⇧+) CWB"
    and "weak_barbed_correspondence_simulation (Rel⇧*) CWB"
proof -
  from corrSim show "weak_barbed_correspondence_simulation (Rel⇧=) CWB"
    using weak_reduction_correspondence_simulation_and_closures(1)[where Rel="Rel"
            and Cal="Calculus CWB"]
          weak_respection_of_barbs_and_closures(1)[where Rel="Rel" and CWB="CWB"]
    by fast
next
  from corrSim show "weak_barbed_correspondence_simulation (Rel⇧+) CWB"
    using weak_reduction_correspondence_simulation_and_closures(2)[where Rel="Rel"
            and Cal="Calculus CWB"]
          weak_respection_of_barbs_and_closures(3)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from corrSim show "weak_barbed_correspondence_simulation (Rel⇧*) CWB"
    using weak_reduction_correspondence_simulation_and_closures(3)[where Rel="Rel"
            and Cal="Calculus CWB"]
          weak_respection_of_barbs_and_closures(5)[where Rel="Rel" and CWB="CWB"]
    by blast
qed

lemma labelled_correspondence_simulation_condition_trans:
  fixes Cal   :: "('proc, 'lab) labelledProcessCalculus"
    and P Q R :: "'proc"
    and α     :: "'lab"
    and Rel   :: "('proc × 'proc) set"
  assumes A1: "∀Q'. Q ─⁀α→Cal* Q' ⟶
               (∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel)"
      and A2: "∀R'. R ─⁀α→Cal* R' ⟶
               (∃Q'' R''. Q ─⁀α→Cal* Q'' ∧ R' →Cal* R'' ∧ (Q'', R'') ∈ Rel)"
      and A3: "weak_labelled_simulation Rel Cal"
      and A4: "trans Rel"
  shows "∀R'. R ─⁀α→Cal* R' ⟶ (∃P'' R''. P ─⁀α→Cal* P'' ∧ R' →Cal* R'' ∧ (P'', R'') ∈ Rel)"
proof clarify
  fix R'
  assume "R ─⁀α→Cal* R'"
  with A2 obtain Q'' R'' where A5: "Q ─⁀α→Cal* Q''" and A6: "R' →Cal* R''"
                           and A7: "(Q'', R'') ∈ Rel"
    by blast
  from A1 A5 obtain P''' Q''' where A8: "P ─⁀α→Cal* P'''" and A9: "Q'' →Cal* Q'''"
                                and A10: "(P''', Q''') ∈ Rel"
    by blast
  from A9 have "Q'' ─⁀τ-Cal→Cal* Q'''"
    unfolding weakLabelledStep_def
    by simp
  with A3 A7 obtain R''' where A11: "R'' ─⁀τ-Cal→Cal* R'''" and A12: "(Q''', R''') ∈ Rel"
    by blast
  from A6 A11 have A13: "R' →Cal* R'''"
    unfolding weakLabelledStep_def
    using weakTauSteps_trans[of R' Cal R'' R''']
    by simp
  from A4 A10 A12 have "(P''', R''') ∈ Rel"
    unfolding trans_def
    by blast
  with A8 A13 show "∃P'' R''. P ─⁀α→Cal* P'' ∧ R' →Cal* R'' ∧ (P'', R'') ∈ Rel"
    by blast
qed

lemma weak_labelled_correspondence_simulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes corrSim: "weak_labelled_correspondence_simulation Rel Cal"
  shows "weak_labelled_correspondence_simulation (Rel⇧=) Cal"
    and "weak_labelled_correspondence_simulation (Rel⇧+) Cal"
    and "weak_labelled_correspondence_simulation (Rel⇧*) Cal"
proof -
  show A: "weak_labelled_correspondence_simulation (Rel⇧=) Cal"
  proof
    from corrSim show "weak_labelled_simulation (Rel⇧=) Cal"
      using weak_labelled_simulation_and_closures(1)[where Rel="Rel" and Cal="Cal"]
      by blast
  next
    show "∀P Q α Q'. (P, Q) ∈ Rel⇧= ∧ Q ─⁀α→Cal* Q'
          ⟶ (∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧=)"
    proof clarify
      fix P Q α Q'
      assume "(P, Q) ∈ Rel⇧=" and A1: "Q ─⁀α→Cal* Q'"
      moreover have "P = Q ⟹ ∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
      proof -
        assume "P = Q"
        moreover have "Q' →Cal* Q'"
          using WTS_refl[of Q' Cal]
          by simp
        ultimately show "∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
          using A1
          by blast
      qed
      moreover
      have "(P, Q) ∈ Rel ⟹ ∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
      proof -
        assume "(P, Q) ∈ Rel"
        with corrSim A1 obtain P'' Q'' where "P ─⁀α→Cal* P''" and "Q' →Cal* Q''"
                                         and "(P'', Q'') ∈ Rel"
          by blast
        thus "∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
          by auto
      qed
      ultimately show "∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧="
        by auto
    qed
  qed
  have B: "⋀Rel. weak_labelled_correspondence_simulation Rel Cal
           ⟹ weak_labelled_correspondence_simulation (Rel⇧+) Cal"
  proof
    fix Rel
    assume "weak_labelled_correspondence_simulation Rel Cal"
    thus "weak_labelled_simulation (Rel⇧+) Cal"
      using weak_labelled_simulation_and_closures(2)[where Rel="Rel" and Cal="Cal"]
      by blast
  next
    fix Rel
    assume B1: "weak_labelled_correspondence_simulation Rel Cal"
    show "∀P Q α Q'. (P, Q) ∈ Rel⇧+ ∧ Q ─⁀α→Cal* Q'
          ⟶ (∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧+)"
    proof clarify
      fix P Q α Q'
      assume "(P, Q) ∈ Rel⇧+" and "Q ─⁀α→Cal* Q'"
      thus "∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧+"
      proof (induct arbitrary: Q')
        fix Q Q'
        assume "(P, Q) ∈ Rel" and "Q ─⁀α→Cal* Q'"
        with B1 obtain P'' Q'' where B2: "P ─⁀α→Cal* P''" and B3: "Q' →Cal* Q''"
                                 and B4: "(P'', Q'') ∈ Rel"
          by blast
        from B4 have "(P'', Q'') ∈ Rel⇧+"
          by simp
        with B2 B3 show "∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧+"
          by blast
      next
        case (step Q R R')
        assume "⋀Q'. Q ─⁀α→Cal* Q'
                ⟹ ∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel⇧+"
        moreover assume "(Q, R) ∈ Rel"
        with B1 have "⋀R'. R ─⁀α→Cal* R' ⟹
                      ∃Q'' R''. Q ─⁀α→Cal* Q'' ∧ R' →Cal* R'' ∧ (Q'', R'') ∈ Rel⇧+"
          by blast
        moreover from B1 have "weak_labelled_simulation (Rel⇧+) Cal"
          using weak_labelled_simulation_and_closures(2)[where Rel="Rel" and Cal="Cal"]
          by blast
        moreover have "trans (Rel⇧+)"
          using trans_trancl[of Rel]
          by blast
        moreover assume "R ─⁀α→Cal* R'"
        ultimately show "∃P'' R''. P ─⁀α→Cal* P'' ∧ R' →Cal* R'' ∧ (P'', R'') ∈ Rel⇧+"
            using labelled_correspondence_simulation_condition_trans[of Q α Cal P "Rel⇧+" R]
          by blast
      qed
    qed
  qed
  from corrSim B[where Rel="Rel"] show "weak_labelled_correspondence_simulation (Rel⇧+) Cal"
    by blast
  from A B[where Rel="Rel⇧="]
  show "weak_labelled_correspondence_simulation (Rel⇧*) Cal"
      using trancl_reflcl[of Rel]
    by auto
qed

subsection ‹Bisimulation›

text ‹A weak (reduction) bisimulation is a relation R such that
      (1) if (P, Q) in R and P evolves to some P' then there exists some Q' such that Q evolves to
          Q' and (P', Q') in R, and
      (2) if (P, Q) in R and Q evolves to some Q' then there exists some P' such that P evolves to
          P' and (P', Q') in R.›

abbreviation weak_reduction_bisimulation :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool"
  where
  "weak_reduction_bisimulation Rel Cal ≡
   (∀P Q P'. (P, Q) ∈ Rel ∧ P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel))
   ∧ (∀P Q Q'. (P, Q) ∈ Rel ∧ Q ⟼Cal* Q' ⟶ (∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel))"

text ‹A weak barbed bisimulation is weak reduction bisimulation that weakly respects barbs.›

abbreviation weak_barbed_bisimulation
  :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool" where
  "weak_barbed_bisimulation Rel CWB ≡
   weak_reduction_bisimulation Rel (Calculus CWB) ∧ rel_weakly_respects_barbs Rel CWB"

text ‹A weak labelled bisimulation is a relation R such that
      (1) if (P, Q) in R and P evolves to some P' using a then there exists some Q' such that Q
          evolves to Q' using a and (P', Q') in R, and
      (2) if (P, Q) in R and Q evolves to some Q' using a then there exists some P' such that P
          evolves to P' using a and (P', Q') in R.›

abbreviation weak_labelled_bisimulation
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "weak_labelled_bisimulation Rel Cal ≡
   (∀P Q α P'. (P, Q) ∈ Rel ∧ P ─⁀α→Cal* P' ⟶ (∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel))
   ∧ (∀P Q α Q'. (P, Q) ∈ Rel ∧ Q ─⁀α→Cal* Q' ⟶ (∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel))"

text ‹A symetric weak simulation is a weak bisimulation.›

lemma symm_weak_reduction_simulation_is_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes "sym Rel"
      and "weak_reduction_simulation Rel Cal"
  shows "weak_reduction_bisimulation Rel Cal"
  using assms symD[of Rel]
  by blast

lemma symm_weak_barbed_simulation_is_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes "sym Rel"
      and "weak_barbed_simulation Rel Cal"
    shows "weak_barbed_bisimulation Rel Cal"
  using assms symD[of Rel]
  by blast

lemma symm_weak_labelled_simulation_is_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes "sym Rel"
      and "weak_labelled_simulation Rel Cal"
    shows "weak_labelled_bisimulation Rel Cal"
  using assms symD[of Rel]
  by blast

text ‹If a relation as well as its inverse are weak simulations, then this relation is a weak
      bisimulation.›

lemma weak_reduction_simulations_impl_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes sim:    "weak_reduction_simulation Rel Cal"
      and simInv: "weak_reduction_simulation (Rel¯) Cal"
    shows "weak_reduction_bisimulation Rel Cal"
proof auto
  fix P Q P'
  assume "(P, Q) ∈ Rel" and "P ⟼Cal* P'"
  with sim show "∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel"
    by simp
next
  fix P Q Q'
  assume "(P, Q) ∈ Rel"
  hence "(Q, P) ∈ Rel¯"
    by simp
  moreover assume "Q ⟼Cal* Q'"
  ultimately obtain P' where A1: "P ⟼Cal* P'" and A2: "(Q', P') ∈ Rel¯"
    using simInv
    by blast
  from A2 have "(P', Q') ∈ Rel"
    by induct
  with A1 show "∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma weak_labelled_simulations_impl_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes sim:    "weak_labelled_simulation Rel Cal"
      and simInv: "weak_labelled_simulation (Rel¯) Cal"
    shows "weak_labelled_bisimulation Rel Cal"
proof auto
  fix P Q α P'
  assume "(P, Q) ∈ Rel" and "P ─⁀α→Cal* P'"
  with sim show "∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel"
    by simp
next
  fix P Q α Q'
  assume "(P, Q) ∈ Rel"
  hence "(Q, P) ∈ Rel¯"
    by simp
  moreover assume "Q ─⁀α→Cal* Q'"
  ultimately obtain P' where A1: "P ─⁀α→Cal* P'" and A2: "(Q', P') ∈ Rel¯"
    using simInv
    by blast
  from A2 have "(P', Q') ∈ Rel"
    by induct
  with A1 show "∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma weak_reduction_bisimulations_impl_inverse_is_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes bisim: "weak_reduction_bisimulation Rel Cal"
  shows "weak_reduction_simulation (Rel¯) Cal"
proof clarify
  fix P Q P'
  assume "(Q, P) ∈ Rel"
  moreover assume "P ⟼Cal* P'"
  ultimately obtain Q' where A1: "Q ⟼Cal* Q'" and A2: "(Q', P') ∈ Rel"
    using bisim
    by blast
  from A2 have "(P', Q') ∈ Rel¯"
    by simp
  with A1 show "∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel¯"
    by blast
qed

lemma weak_labelled_bisimulations_impl_inverse_is_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes bisim: "weak_labelled_bisimulation Rel Cal"
  shows "weak_labelled_simulation (Rel¯) Cal"
proof clarify
  fix P Q α P'
  assume "(Q, P) ∈ Rel"
  moreover assume "P ─⁀α→Cal* P'"
  ultimately obtain Q' where A1: "Q ─⁀α→Cal* Q'" and A2: "(Q', P') ∈ Rel"
    using bisim
    by blast
  from A2 have "(P', Q') ∈ Rel¯"
    by simp
  with A1 show "∃Q'. Q ─⁀α→Cal* Q' ∧ (P', Q') ∈ Rel¯"
    by blast
qed

lemma weak_reduction_simulations_iff_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  shows "(weak_reduction_simulation Rel Cal ∧ weak_reduction_simulation (Rel¯) Cal)
         = weak_reduction_bisimulation Rel Cal"
  using weak_reduction_simulations_impl_bisimulation[where Rel="Rel" and Cal="Cal"]
        weak_reduction_bisimulations_impl_inverse_is_simulation[where Rel="Rel" and Cal="Cal"]
  by blast

lemma weak_barbed_simulations_iff_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "(weak_barbed_simulation Rel CWB ∧ weak_barbed_simulation (Rel¯) CWB)
         = weak_barbed_bisimulation Rel CWB"
proof (rule iffI, erule conjE)
  assume sim: "weak_barbed_simulation Rel CWB"
     and rev: "weak_barbed_simulation (Rel¯) CWB"
  hence "weak_reduction_bisimulation Rel (Calculus CWB)"
    using weak_reduction_simulations_impl_bisimulation[where Rel="Rel" and Cal="Calculus CWB"]
    by blast
  moreover from sim have "rel_weakly_preserves_barbs Rel CWB"
    by simp
  moreover from rev have "rel_weakly_reflects_barbs Rel CWB"
    by simp
  ultimately show "weak_barbed_bisimulation Rel CWB"
    by blast
next
  assume bisim: "weak_barbed_bisimulation Rel CWB"
  hence "weak_barbed_simulation Rel CWB"
    by blast
  moreover from bisim have "weak_reduction_simulation (Rel¯) (Calculus CWB)"
    using weak_reduction_bisimulations_impl_inverse_is_simulation[where Rel="Rel"]
    by simp
  moreover from bisim have "rel_weakly_reflects_barbs Rel CWB"
    by blast
  hence "rel_weakly_preserves_barbs (Rel¯) CWB"
    by simp
  ultimately show "weak_barbed_simulation Rel CWB ∧ weak_barbed_simulation (Rel¯) CWB"
    by blast
qed

lemma weak_labelled_simulations_iff_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  shows "(weak_labelled_simulation Rel Cal ∧ weak_labelled_simulation (Rel¯) Cal)
         = weak_labelled_bisimulation Rel Cal"
  using weak_labelled_simulations_impl_bisimulation[where Rel="Rel" and Cal="Cal"]
        weak_labelled_bisimulations_impl_inverse_is_simulation[where Rel="Rel" and Cal="Cal"]
  by blast

text ‹A weak bisimulation is a weak correspondence simulation.›

lemma weak_reduction_bisimulation_is_correspondence_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes bisim: "weak_reduction_bisimulation Rel Cal"
  shows "weak_reduction_correspondence_simulation Rel Cal"
proof
  from bisim show "weak_reduction_simulation Rel Cal"
    by blast
next
  show "∀P Q Q'. (P, Q) ∈ Rel ∧ Q ⟼Cal* Q'
        ⟶ (∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel)"
  proof clarify
    fix P Q Q'
    assume "(P, Q) ∈ Rel" and "Q ⟼Cal* Q'"
    with bisim obtain P' where "P ⟼Cal* P'" and "(P', Q') ∈ Rel"
      by blast
    moreover have "Q' ⟼Cal* Q'"
      by (rule steps_refl)
    ultimately show "(∃P'' Q''. P ⟼Cal* P'' ∧ Q' ⟼Cal* Q'' ∧ (P'', Q'') ∈ Rel)"
      by blast
  qed
qed

lemma weak_barbed_bisimulation_is_correspondence_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes bisim: "weak_barbed_bisimulation Rel CWB"
  shows "weak_barbed_correspondence_simulation Rel CWB"
  using bisim weak_reduction_bisimulation_is_correspondence_simulation[where Rel="Rel"
              and Cal="Calculus CWB"]
  by blast

lemma weak_labelled_bisimulation_is_correspondence_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes bisim: "weak_labelled_bisimulation Rel Cal"
  shows "weak_labelled_correspondence_simulation Rel Cal"
proof
  from bisim show "weak_labelled_simulation Rel Cal"
    by blast
next
  show "∀P Q α Q'. (P, Q) ∈ Rel ∧ Q ─⁀α→Cal* Q'
        ⟶ (∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel)"
  proof clarify
    fix P Q α Q'
    assume "(P, Q) ∈ Rel" and "Q ─⁀α→Cal* Q'"
    with bisim obtain P' where "P ─⁀α→Cal* P'" and "(P', Q') ∈ Rel"
      by blast
    moreover have "Q' →Cal* Q'"
      using WTS_refl[of Q' Cal]
      by simp
    ultimately show "(∃P'' Q''. P ─⁀α→Cal* P'' ∧ Q' →Cal* Q'' ∧ (P'', Q'') ∈ Rel)"
      by blast
  qed
qed

text ‹The reflexive, symmetric, and/or transitive closure of a weak bisimulation is a weak
      bisimulation.›

lemma weak_reduction_bisimulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes bisim: "weak_reduction_bisimulation Rel Cal"
  shows "weak_reduction_bisimulation (Rel⇧=) Cal"
    and "weak_reduction_bisimulation (symcl Rel) Cal"
    and "weak_reduction_bisimulation (Rel⇧+) Cal"
    and "weak_reduction_bisimulation (symcl (Rel⇧=)) Cal"
    and "weak_reduction_bisimulation (Rel⇧*) Cal"
    and "weak_reduction_bisimulation ((symcl (Rel⇧=))⇧+) Cal"
proof -
  from bisim show A: "weak_reduction_bisimulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast+)
  have B: "⋀Rel. weak_reduction_bisimulation Rel Cal
           ⟹ weak_reduction_bisimulation (symcl Rel) Cal"
    by (auto simp add: symcl_def, blast+)
  from bisim B[where Rel="Rel"] show "weak_reduction_bisimulation (symcl Rel) Cal"
    by blast
  have C: "⋀Rel. weak_reduction_bisimulation Rel Cal
           ⟹ weak_reduction_bisimulation (Rel⇧+) Cal"
  proof
    fix Rel
    assume "weak_reduction_bisimulation Rel Cal"
    thus "weak_reduction_simulation (Rel⇧+) Cal"
      using weak_reduction_simulation_and_closures(2)[where Rel="Rel" and Cal="Cal"]
      by blast
  next
    fix Rel
    assume C1: "weak_reduction_bisimulation Rel Cal"
    show "∀P Q Q'. (P, Q) ∈ Rel⇧+ ∧ Q ⟼Cal* Q'
          ⟶ (∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel⇧+)"
    proof clarify
      fix P Q Q'
      assume "(P, Q) ∈ Rel⇧+" and "Q ⟼Cal* Q'"
      thus "∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel⇧+"
      proof (induct arbitrary: Q')
        fix Q Q'
        assume "(P, Q) ∈ Rel" and "Q ⟼Cal* Q'"
        with C1 obtain P' where "P ⟼Cal* P'" and "(P', Q') ∈ Rel"
          by blast
        thus "∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel⇧+"
          by auto
      next
        case (step Q R R')
        assume "(Q, R) ∈ Rel" and "R ⟼Cal* R'"
        with C1 obtain Q' where C2: "Q ⟼Cal* Q'" and C3: "(Q', R') ∈ Rel⇧+"
          by blast
        assume "⋀Q'. Q ⟼Cal* Q' ⟹ ∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel⇧+"
        with C2 obtain P' where C4: "P ⟼Cal* P'" and C5: "(P', Q') ∈ Rel⇧+"
          by blast
        from C5 C3 have "(P', R') ∈ Rel⇧+"
          by simp
        with C4 show "∃P'. P ⟼Cal* P' ∧ (P', R') ∈ Rel⇧+"
          by blast
      qed
    qed
  qed
  from bisim C[where Rel="Rel"] show "weak_reduction_bisimulation (Rel⇧+) Cal"
    by blast
  from A B[where Rel="Rel⇧="] show "weak_reduction_bisimulation (symcl (Rel⇧=)) Cal"
    by blast
  from A C[where Rel="Rel⇧="] show "weak_reduction_bisimulation (Rel⇧*) Cal"
    using trancl_reflcl[of Rel]
    by auto
  from A B[where Rel="Rel⇧="] C[where Rel="symcl (Rel⇧=)"]
  show "weak_reduction_bisimulation ((symcl (Rel⇧=))⇧+) Cal"
    by blast
qed

lemma weak_barbed_bisimulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes bisim: "weak_barbed_bisimulation Rel CWB"
  shows "weak_barbed_bisimulation (Rel⇧=) CWB"
    and "weak_barbed_bisimulation (symcl Rel) CWB"
    and "weak_barbed_bisimulation (Rel⇧+) CWB"
    and "weak_barbed_bisimulation (symcl (Rel⇧=)) CWB"
    and "weak_barbed_bisimulation (Rel⇧*) CWB"
    and "weak_barbed_bisimulation ((symcl (Rel⇧=))⇧+) CWB"
proof -
  from bisim show "weak_barbed_bisimulation (Rel⇧=) CWB"
    using weak_reduction_bisimulation_and_closures(1)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_respection_of_barbs_and_closures(1)[where Rel="Rel" and CWB="CWB"]
    by fast
next
  from bisim show "weak_barbed_bisimulation (symcl Rel) CWB"
    using weak_reduction_bisimulation_and_closures(2)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_respection_of_barbs_and_closures(2)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from bisim show "weak_barbed_bisimulation (Rel⇧+) CWB"
    using weak_reduction_bisimulation_and_closures(3)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_respection_of_barbs_and_closures(3)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from bisim show "weak_barbed_bisimulation (symcl (Rel⇧=)) CWB"
    using weak_reduction_bisimulation_and_closures(4)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_respection_of_barbs_and_closures(4)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from bisim show "weak_barbed_bisimulation (Rel⇧*) CWB"
    using weak_reduction_bisimulation_and_closures(5)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_respection_of_barbs_and_closures(5)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from bisim show "weak_barbed_bisimulation ((symcl (Rel⇧=))⇧+) CWB"
    using weak_reduction_bisimulation_and_closures(6)[where Rel="Rel" and Cal="Calculus CWB"]
          weak_respection_of_barbs_and_closures(6)[where Rel="Rel" and CWB="CWB"]
    by blast
qed

lemma weak_labelled_bisimulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes bisim: "weak_labelled_bisimulation Rel Cal"
  shows "weak_labelled_bisimulation (Rel⇧=) Cal"
    and "weak_labelled_bisimulation (symcl Rel) Cal"
    and "weak_labelled_bisimulation (Rel⇧+) Cal"
    and "weak_labelled_bisimulation (symcl (Rel⇧=)) Cal"
    and "weak_labelled_bisimulation (Rel⇧*) Cal"
    and "weak_labelled_bisimulation ((symcl (Rel⇧=))⇧+) Cal"
proof -
  from bisim show A: "weak_labelled_bisimulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast+)
  have B: "⋀Rel. weak_labelled_bisimulation Rel Cal
           ⟹ weak_labelled_bisimulation (symcl Rel) Cal"
    by (auto simp add: symcl_def, blast+)
  from bisim B[where Rel="Rel"] show "weak_labelled_bisimulation (symcl Rel) Cal"
    by blast
  have C: "⋀Rel. weak_labelled_bisimulation Rel Cal
           ⟹ weak_labelled_bisimulation (Rel⇧+) Cal"
  proof
    fix Rel
    assume "weak_labelled_bisimulation Rel Cal"
    thus "weak_labelled_simulation (Rel⇧+) Cal"
      using weak_labelled_simulation_and_closures(2)[where Rel="Rel" and Cal="Cal"]
      by blast
  next
    fix Rel
    assume C1: "weak_labelled_bisimulation Rel Cal"
    show "∀P Q α Q'. (P, Q) ∈ Rel⇧+ ∧ Q ─⁀α→Cal* Q'
          ⟶ (∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel⇧+)"
    proof clarify
      fix P Q α Q'
      assume "(P, Q) ∈ Rel⇧+" and "Q ─⁀α→Cal* Q'"
      thus "∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel⇧+"
      proof (induct arbitrary: Q')
        fix Q Q'
        assume "(P, Q) ∈ Rel" and "Q ─⁀α→Cal* Q'"
        with C1 obtain P' where "P ─⁀α→Cal* P'" and "(P', Q') ∈ Rel"
          by blast
        thus "∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel⇧+"
          by auto
      next
        case (step Q R R')
        assume "(Q, R) ∈ Rel" and "R ─⁀α→Cal* R'"
        with C1 obtain Q' where C2: "Q ─⁀α→Cal* Q'" and C3: "(Q', R') ∈ Rel⇧+"
          by blast
        assume "⋀Q'. Q ─⁀α→Cal* Q' ⟹ ∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel⇧+"
        with C2 obtain P' where C4: "P ─⁀α→Cal* P'" and C5: "(P', Q') ∈ Rel⇧+"
          by blast
        from C5 C3 have "(P', R') ∈ Rel⇧+"
          by simp
        with C4 show "∃P'. P ─⁀α→Cal* P' ∧ (P', R') ∈ Rel⇧+"
          by blast
      qed
    qed
  qed
  from bisim C[where Rel="Rel"] show "weak_labelled_bisimulation (Rel⇧+) Cal"
    by blast
  from A B[where Rel="Rel⇧="] show "weak_labelled_bisimulation (symcl (Rel⇧=)) Cal"
    by blast
  from A C[where Rel="Rel⇧="] show "weak_labelled_bisimulation (Rel⇧*) Cal"
    using trancl_reflcl[of Rel]
    by auto
  from A B[where Rel="Rel⇧="] C[where Rel="symcl (Rel⇧=)"]
  show "weak_labelled_bisimulation ((symcl (Rel⇧=))⇧+) Cal"
    by blast
qed

text ‹A strong (reduction) bisimulation is a relation R such that
      (1) if (P, Q) in R and P' is a derivative of P then there exists some Q' such that Q' is a
          derivative of Q and (P', Q') in R, and
      (2) if (P, Q) in R and Q' is a derivative of Q then there exists some P' such that P' is a
          derivative of P and (P', Q') in R.›

abbreviation strong_reduction_bisimulation
  :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool" where
  "strong_reduction_bisimulation Rel Cal ≡
   (∀P Q P'. (P, Q) ∈ Rel ∧ P ⟼Cal P' ⟶ (∃Q'. Q ⟼Cal Q' ∧ (P', Q') ∈ Rel))
   ∧ (∀P Q Q'. (P, Q) ∈ Rel ∧ Q ⟼Cal Q' ⟶ (∃P'. P ⟼Cal P' ∧ (P', Q') ∈ Rel))"

text ‹A strong barbed bisimulation is strong reduction bisimulation that respects barbs.›

abbreviation strong_barbed_bisimulation
  :: "('proc × 'proc) set ⇒ ('proc, 'barbs) calculusWithBarbs ⇒ bool" where
  "strong_barbed_bisimulation Rel CWB ≡
   strong_reduction_bisimulation Rel (Calculus CWB) ∧ rel_respects_barbs Rel CWB"

text ‹A strong labelled bisimulation is a relation R such that
      (1) if (P, Q) in R and P' is a derivative of P using a then there exists some Q' such that
          Q' is a derivative of Q using a and (P', Q') in R, and
      (2) if (P, Q) in R and Q' is a derivative of Q using a then there exists some P' such that
          P' is a derivative of P using a and (P', Q') in R.›

abbreviation strong_labelled_bisimulation
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "strong_labelled_bisimulation Rel Cal ≡
   (∀P Q α P'. (P, Q) ∈ Rel ∧ P ─α→Cal P' ⟶ (∃Q'. Q ─α→Cal Q' ∧ (P', Q') ∈ Rel))
   ∧ (∀P Q α Q'. (P, Q) ∈ Rel ∧ Q ─α→Cal Q' ⟶ (∃P'. P ─α→Cal P' ∧ (P', Q') ∈ Rel))"

text ‹A symetric strong simulation is a strong bisimulation.›

lemma symm_strong_reduction_simulation_is_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes "sym Rel"
      and "strong_reduction_simulation Rel Cal"
    shows "strong_reduction_bisimulation Rel Cal"
  using assms symD[of Rel]
  by blast

lemma symm_strong_barbed_simulation_is_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes "sym Rel"
      and "strong_barbed_simulation Rel CWB"
    shows "strong_barbed_bisimulation Rel CWB"
  using assms symD[of Rel]
  by blast

lemma symm_strong_labelled_simulation_is_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes "sym Rel"
      and "strong_labelled_simulation Rel Cal"
    shows "strong_labelled_bisimulation Rel Cal"
  using assms symD[of Rel]
  by blast

text ‹If a relation as well as its inverse are strong simulations, then this relation is a strong
      bisimulation.›

lemma strong_reduction_simulations_impl_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes sim:    "strong_reduction_simulation Rel Cal"
      and simInv: "strong_reduction_simulation (Rel¯) Cal"
    shows "strong_reduction_bisimulation Rel Cal"
proof auto
  fix P Q P'
  assume "(P, Q) ∈ Rel" and "P ⟼Cal P'"
  with sim show "∃Q'. Q ⟼Cal Q' ∧ (P', Q') ∈ Rel"
    by simp
next
  fix P Q Q'
  assume "(P, Q) ∈ Rel"
  hence "(Q, P) ∈ Rel¯"
    by simp
  moreover assume "Q ⟼Cal Q'"
  ultimately obtain P' where A1: "P ⟼Cal P'" and A2: "(Q', P') ∈ Rel¯"
    using simInv
    by blast
  from A2 have "(P', Q') ∈ Rel"
    by induct
  with A1 show "∃P'. P ⟼Cal P' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma strong_labelled_simulations_impl_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes sim:    "strong_labelled_simulation Rel Cal"
      and simInv: "strong_labelled_simulation (Rel¯) Cal"
    shows "strong_labelled_bisimulation Rel Cal"
proof auto
  fix P Q α P'
  assume "(P, Q) ∈ Rel" and "P ─α→Cal P'"
  with sim show "∃Q'. Q ─α→Cal Q' ∧ (P', Q') ∈ Rel"
    by simp
next
  fix P Q α Q'
  assume "(P, Q) ∈ Rel"
  hence "(Q, P) ∈ Rel¯"
    by simp
  moreover assume "Q ─α→Cal Q'"
  ultimately obtain P' where A1: "P ─α→Cal P'" and A2: "(Q', P') ∈ Rel¯"
    using simInv
    by blast
  from A2 have "(P', Q') ∈ Rel"
    by induct
  with A1 show "∃P'. P ─α→Cal P' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma strong_reduction_bisimulations_impl_inverse_is_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes bisim: "strong_reduction_bisimulation Rel Cal"
  shows "strong_reduction_simulation (Rel¯) Cal"
proof clarify
  fix P Q P'
  assume "(Q, P) ∈ Rel"
  moreover assume "P ⟼Cal P'"
  ultimately obtain Q' where A1: "Q ⟼Cal Q'" and A2: "(Q', P') ∈ Rel"
    using bisim
    by blast
  from A2 have "(P', Q') ∈ Rel¯"
    by simp
  with A1 show "∃Q'. Q ⟼Cal Q' ∧ (P', Q') ∈ Rel¯"
    by blast
qed

lemma strong_labelled_bisimulations_impl_inverse_is_simulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes bisim: "strong_labelled_bisimulation Rel Cal"
  shows "strong_labelled_simulation (Rel¯) Cal"
proof clarify
  fix P Q α P'
  assume "(Q, P) ∈ Rel"
  moreover assume "P ─α→Cal P'"
  ultimately obtain Q' where A1: "Q ─α→Cal Q'" and A2: "(Q', P') ∈ Rel"
    using bisim
    by blast
  from A2 have "(P', Q') ∈ Rel¯"
    by simp
  with A1 show "∃Q'. Q ─α→Cal Q' ∧ (P', Q') ∈ Rel¯"
    by blast
qed

lemma strong_reduction_simulations_iff_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  shows "(strong_reduction_simulation Rel Cal ∧ strong_reduction_simulation (Rel¯) Cal)
         = strong_reduction_bisimulation Rel Cal"
  using strong_reduction_simulations_impl_bisimulation[where Rel="Rel" and Cal="Cal"]
        strong_reduction_bisimulations_impl_inverse_is_simulation[where Rel="Rel"]
  by blast

lemma strong_barbed_simulations_iff_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "(strong_barbed_simulation Rel CWB ∧ strong_barbed_simulation (Rel¯) CWB)
         = strong_barbed_bisimulation Rel CWB"
proof (rule iffI, erule conjE)
  assume sim: "strong_barbed_simulation Rel CWB"
     and rev: "strong_barbed_simulation (Rel¯) CWB"
  hence "strong_reduction_bisimulation Rel (Calculus CWB)"
    using strong_reduction_simulations_impl_bisimulation[where Rel="Rel" and Cal="Calculus CWB"]
    by blast
  moreover from sim have "rel_preserves_barbs Rel CWB"
    by simp
  moreover from rev have "rel_reflects_barbs Rel CWB"
    by simp
  ultimately show "strong_barbed_bisimulation Rel CWB"
    by blast
next
  assume bisim: "strong_barbed_bisimulation Rel CWB"
  hence "strong_barbed_simulation Rel CWB"
    by blast
  moreover from bisim have "strong_reduction_simulation (Rel¯) (Calculus CWB)"
    using strong_reduction_bisimulations_impl_inverse_is_simulation[where Rel="Rel"]
    by simp
  moreover from bisim have "rel_reflects_barbs Rel CWB"
    by blast
  hence "rel_preserves_barbs (Rel¯) CWB"
    by simp
  ultimately
  show "strong_barbed_simulation Rel CWB ∧ strong_barbed_simulation (Rel¯) CWB"
    by blast
qed

lemma strong_labelled_simulations_iff_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  shows "(strong_labelled_simulation Rel Cal ∧ strong_labelled_simulation (Rel¯) Cal)
         = strong_labelled_bisimulation Rel Cal"
  using strong_labelled_simulations_impl_bisimulation[where Rel="Rel" and Cal="Cal"]
        strong_labelled_bisimulations_impl_inverse_is_simulation[where Rel="Rel"]
  by blast

text ‹A strong bisimulation is a weak bisimulation.›

lemma strong_impl_weak_reduction_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes bisim: "strong_reduction_bisimulation Rel Cal"
  shows "weak_reduction_bisimulation Rel Cal"
proof
  from bisim show "weak_reduction_simulation Rel Cal"
    using strong_impl_weak_reduction_simulation[where Rel="Rel" and Cal="Cal"]
    by blast
next
  show "∀P Q Q'. (P, Q) ∈ Rel ∧ Q ⟼Cal* Q' ⟶ (∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel)"
  proof clarify
    fix P Q Q'
    assume A1: "(P, Q) ∈ Rel"
    assume "Q ⟼Cal* Q'"
    from this obtain n where "Q ⟼Cal⇗n⇖ Q'"
      by (auto simp add: steps_def)
    thus "∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel"
    proof (induct n arbitrary: Q')
      case 0
      assume "Q ⟼Cal⇗0⇖ Q'"
      hence "Q = Q'"
        by (simp add: steps_refl)
      moreover have "P ⟼Cal* P"
        by (rule steps_refl)
      ultimately show "∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel"
        using A1
        by blast
    next
      case (Suc n Q'')
      assume "Q ⟼Cal⇗Suc n⇖ Q''"
      from this obtain Q' where A2: "Q ⟼Cal⇗n⇖Q'" and A3: "Q' ⟼Cal Q''"
        by auto
      assume "⋀Q'. Q ⟼Cal⇗n⇖ Q' ⟹ ∃P'. P ⟼Cal* P' ∧ (P', Q') ∈ Rel"
      with A2 obtain P' where A4: "P ⟼Cal* P'" and A5: "(P', Q') ∈ Rel"
        by blast
      from bisim A5 A3 obtain P'' where A6: "P' ⟼Cal P''" and A7: "(P'', Q'') ∈ Rel"
        by blast
      from A4 A6 have "P ⟼Cal* P''"
        using steps_add[where P="P" and Q="P'" and R="P''"]
        by (simp add: step_to_steps)
      with A7 show "∃P'. P ⟼Cal* P' ∧ (P', Q'') ∈ Rel"
        by blast
    qed
  qed
qed

lemma strong_barbed_bisimulation_impl_weak_respection_of_barbs:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes bisim: "strong_barbed_bisimulation Rel CWB"
  shows "rel_weakly_respects_barbs Rel CWB"
proof
  from bisim show "rel_weakly_preserves_barbs Rel CWB"
    using strong_barbed_simulation_impl_weak_preservation_of_barbs[where Rel="Rel" and CWB="CWB"]
    by blast
next
  show "rel_weakly_reflects_barbs Rel CWB"
  proof clarify
    fix P Q a Q'
    assume "(P, Q) ∈ Rel" and "Q ⟼(Calculus CWB)* Q'"
    with bisim obtain P' where A1: "P ⟼(Calculus CWB)* P'" and A2: "(P', Q') ∈ Rel"
      using strong_impl_weak_reduction_bisimulation[where Rel="Rel" and Cal="Calculus CWB"]
      by blast
    assume "Q'↓<CWB>a"
    with bisim A2 have "P'↓<CWB>a"
      by blast
    with A1 show "P⇓<CWB>a"
      by blast
  qed
qed

lemma strong_impl_weak_barbed_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes bisim: "strong_barbed_bisimulation Rel CWB"
  shows "weak_barbed_bisimulation Rel CWB"
  using bisim strong_impl_weak_reduction_bisimulation[where Rel="Rel" and Cal="Calculus CWB"]
        strong_barbed_bisimulation_impl_weak_respection_of_barbs[where Rel="Rel" and CWB="CWB"]
  by blast

lemma strong_labelled_bisimulation_impl_weak_simulation_of_internal:
  fixes Rel    :: "('proc × 'proc) set"
    and Cal    :: "('proc, 'lab) labelledProcessCalculus"
    and P Q Q' :: "'proc"
  assumes bisim:    "strong_labelled_bisimulation Rel Cal"
      and relation: "(P, Q) ∈ Rel"
      and internal: "Q →Cal* Q'"
    shows "∃P'. P →Cal* P' ∧ (P', Q') ∈ Rel"
  using internal bisim relation
proof induct
  case (WTS_refl Q Cal)
  have "P →Cal* P"
    using weakTauStep.WTS_refl[of P Cal]
    by simp
  moreover assume "(P, Q) ∈ Rel"
  ultimately show "∃P'. P →Cal* P' ∧ (P', Q) ∈ Rel"
    by blast
next
  case (WTS_trans Q Cal Q' Q'')
  from WTS_trans(2) have IH: "(strong_labelled_simulation Rel Cal ∧ (∀P Q α Q'. (P, Q) ∈ Rel ∧
    Q ─α→Cal Q' ⟶ (∃P'. P ─α→Cal P' ∧ (P', Q') ∈ Rel))) ∧ (P, Q) ∈ Rel ⟹
    ∃P'. P →Cal* P' ∧ (P', Q') ∈ Rel"
    by simp
  assume A1: "strong_labelled_simulation Rel Cal ∧
    (∀P Q α Q'. (P, Q) ∈ Rel ∧ Q ─α→Cal Q' ⟶ (∃P'. P ─α→Cal P' ∧ (P', Q') ∈ Rel))"
    and "(P, Q) ∈ Rel"
  with IH obtain P' where A2: "P →Cal* P'" and A3: "(P', Q') ∈ Rel"
    by blast
  assume "Q' ─τ-Cal→Cal Q''"
  with A1 A3 obtain P'' where A4: "P' ─τ-Cal→Cal P''" and A5: "(P'', Q'') ∈ Rel"
    by blast
  from A4 have "P' →Cal* P''"
    using WTS_refl[of P' Cal] weakTauStep.WTS_trans[of P' Cal P' P'']
    by simp
  with A2 have "P →Cal* P''"
    using weakTauSteps_trans[of P Cal P' P'']
    by simp
  with A5 show "∃P''. P →Cal* P'' ∧ (P'', Q'') ∈ Rel"
    by blast
qed

lemma strong_impl_weak_labelled_bisimulation:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes bisim: "strong_labelled_bisimulation Rel Cal"
  shows "weak_labelled_bisimulation Rel Cal"
proof
  from bisim show "weak_labelled_simulation Rel Cal"
    using strong_impl_weak_labelled_simulation[where Rel="Rel" and Cal="Cal"]
    by blast
next
  show "∀P Q α Q'. (P, Q) ∈ Rel ∧ Q ─⁀α→Cal* Q' ⟶ (∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel)"
  proof clarify
    fix P Q α Q'
    assume A1: "(P, Q) ∈ Rel" and A2: "Q ─⁀α→Cal* Q'"
    thus "∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel"
    proof (cases "α = τ-Cal")
      assume B1: "α = τ-Cal"
      with A2 have "Q →Cal* Q'"
        unfolding weakLabelledStep_def
        by simp
      with bisim A1 obtain P' where B2: "P →Cal* P'" and B3: "(P', Q') ∈ Rel"
        using strong_labelled_bisimulation_impl_weak_simulation_of_internal[of Rel Cal P Q Q']
        by blast
      from B1 B2 have "P ─⁀α→Cal* P'"
        unfolding weakLabelledStep_def
        by simp
      with B3 show "∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel"
        by blast
    next
      assume B1: "α ≠ τ-Cal" and "Q ─⁀α→Cal* Q'"
      then obtain R S where B2: "Q →Cal* R" and B3: "R ─α→Cal S" and B4: "S →Cal* Q'"
        unfolding weakLabelledStep_def weakLabelledActionStep_def
        by auto
      from bisim A1 B2 obtain T where B5: "P →Cal* T" and B6: "(T, R) ∈ Rel"
        using strong_labelled_bisimulation_impl_weak_simulation_of_internal[of Rel Cal P Q R]
        by blast
      from bisim B3 B6 obtain U where B7: "T ─α→Cal U" and B8: "(U, S) ∈ Rel"
        by blast
      from bisim B4 B8 obtain P' where B9: "U →Cal* P'" and B10: "(P', Q') ∈ Rel"
        using strong_labelled_bisimulation_impl_weak_simulation_of_internal[of Rel Cal U S Q']
        by blast
      from B1 B5 B7 B9 have "P ─⁀α→Cal* P'"
        unfolding weakLabelledStep_def weakLabelledActionStep_def
        by auto
      with B10 show "∃P'. P ─⁀α→Cal* P' ∧ (P', Q') ∈ Rel"
        by blast
    qed
  qed
qed

text ‹The reflexive, symmetric, and/or transitive closure of a strong bisimulation is a strong
      bisimulation.›

lemma strong_reduction_bisimulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "'proc processCalculus"
  assumes bisim: "strong_reduction_bisimulation Rel Cal"
  shows "strong_reduction_bisimulation (Rel⇧=) Cal"
    and "strong_reduction_bisimulation (symcl Rel) Cal"
    and "strong_reduction_bisimulation (Rel⇧+) Cal"
    and "strong_reduction_bisimulation (symcl (Rel⇧=)) Cal"
    and "strong_reduction_bisimulation (Rel⇧*) Cal"
    and "strong_reduction_bisimulation ((symcl (Rel⇧=))⇧+) Cal"
proof -
  from bisim show A: "strong_reduction_bisimulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast+)
  have B: "⋀Rel. strong_reduction_bisimulation Rel Cal
           ⟹ strong_reduction_bisimulation (symcl Rel) Cal"
    by (auto simp add: symcl_def, blast+)
  from bisim B[where Rel="Rel"] show "strong_reduction_bisimulation (symcl Rel) Cal"
    by blast
  have C: "⋀Rel. strong_reduction_bisimulation Rel Cal
           ⟹ strong_reduction_bisimulation (Rel⇧+) Cal"
  proof
    fix Rel
    assume "strong_reduction_bisimulation Rel Cal"
    thus "strong_reduction_simulation (Rel⇧+) Cal"
      using strong_reduction_simulation_and_closures(2)[where Rel="Rel" and Cal="Cal"]
      by blast
  next
    fix Rel
    assume C1: "strong_reduction_bisimulation Rel Cal"
    show "∀P Q Q'. (P, Q) ∈ Rel⇧+ ∧ Q ⟼Cal Q' ⟶ (∃P'. P ⟼Cal P' ∧ (P', Q') ∈ Rel⇧+)"
    proof clarify
      fix P Q Q'
      assume "(P, Q) ∈ Rel⇧+" and "Q ⟼Cal Q'"
      thus "∃P'. P ⟼Cal P' ∧ (P', Q') ∈ Rel⇧+"
      proof (induct arbitrary: Q')
        fix Q Q'
        assume "(P, Q) ∈ Rel" and "Q ⟼Cal Q'"
        with C1 obtain P' where "P ⟼Cal P'" and "(P', Q') ∈ Rel"
          by blast
        thus "∃P'. P ⟼Cal P' ∧ (P', Q') ∈ Rel⇧+"
          by auto
      next
        case (step Q R R')
        assume "(Q, R) ∈ Rel" and "R ⟼Cal R'"
        with C1 obtain Q' where C2: "Q ⟼Cal Q'" and C3: "(Q', R') ∈ Rel⇧+"
          by blast
        assume "⋀Q'. Q ⟼Cal Q' ⟹ ∃P'. P ⟼Cal P' ∧ (P', Q') ∈ Rel⇧+"
        with C2 obtain P' where C4: "P ⟼Cal P'" and C5: "(P', Q') ∈ Rel⇧+"
          by blast
        from C5 C3 have "(P', R') ∈ Rel⇧+"
          by simp
        with C4 show "∃P'. P ⟼Cal P' ∧ (P', R') ∈ Rel⇧+"
          by blast
      qed
    qed
  qed
  from bisim C[where Rel="Rel"] show "strong_reduction_bisimulation (Rel⇧+) Cal"
    by blast
  from A B[where Rel="Rel⇧="]
  show "strong_reduction_bisimulation (symcl (Rel⇧=)) Cal"
    by blast
  from A C[where Rel="Rel⇧="]
  show "strong_reduction_bisimulation (Rel⇧*) Cal"
    using trancl_reflcl[of Rel]
    by auto
  from A B[where Rel="Rel⇧="] C[where Rel="symcl (Rel⇧=)"]
  show "strong_reduction_bisimulation ((symcl (Rel⇧=))⇧+) Cal"
    by blast
qed

lemma strong_barbed_bisimulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  assumes bisim: "strong_barbed_bisimulation Rel CWB"
  shows "strong_barbed_bisimulation (Rel⇧=) CWB"
    and "strong_barbed_bisimulation (symcl Rel) CWB"
    and "strong_barbed_bisimulation (Rel⇧+) CWB"
    and "strong_barbed_bisimulation (symcl (Rel⇧=)) CWB"
    and "strong_barbed_bisimulation (Rel⇧*) CWB"
    and "strong_barbed_bisimulation ((symcl (Rel⇧=))⇧+) CWB"
proof -
  from bisim show "strong_barbed_bisimulation (Rel⇧=) CWB"
    using strong_reduction_bisimulation_and_closures(1)[where Rel="Rel" and Cal="Calculus CWB"]
          respection_of_barbs_and_closures(1)[where Rel="Rel" and CWB="CWB"]
    by fast
next
  from bisim show "strong_barbed_bisimulation (symcl Rel) CWB"
    using strong_reduction_bisimulation_and_closures(2)[where Rel="Rel" and Cal="Calculus CWB"]
          respection_of_barbs_and_closures(2)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from bisim show "strong_barbed_bisimulation (Rel⇧+) CWB"
    using strong_reduction_bisimulation_and_closures(3)[where Rel="Rel" and Cal="Calculus CWB"]
          respection_of_barbs_and_closures(3)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from bisim show "strong_barbed_bisimulation (symcl (Rel⇧=)) CWB"
    using strong_reduction_bisimulation_and_closures(4)[where Rel="Rel" and Cal="Calculus CWB"]
          respection_of_barbs_and_closures(4)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from bisim show "strong_barbed_bisimulation (Rel⇧*) CWB"
    using strong_reduction_bisimulation_and_closures(5)[where Rel="Rel" and Cal="Calculus CWB"]
          respection_of_barbs_and_closures(5)[where Rel="Rel" and CWB="CWB"]
    by blast
next
  from bisim show "strong_barbed_bisimulation ((symcl (Rel⇧=))⇧+) CWB"
    using strong_reduction_bisimulation_and_closures(6)[where Rel="Rel" and Cal="Calculus CWB"]
          respection_of_barbs_and_closures(6)[where Rel="Rel" and CWB="CWB"]
    by blast
qed

lemma strong_labelled_bisimulation_and_closures:
  fixes Rel :: "('proc × 'proc) set"
    and Cal :: "('proc, 'lab) labelledProcessCalculus"
  assumes bisim: "strong_labelled_bisimulation Rel Cal"
  shows "strong_labelled_bisimulation (Rel⇧=) Cal"
    and "strong_labelled_bisimulation (symcl Rel) Cal"
    and "strong_labelled_bisimulation (Rel⇧+) Cal"
    and "strong_labelled_bisimulation (symcl (Rel⇧=)) Cal"
    and "strong_labelled_bisimulation (Rel⇧*) Cal"
    and "strong_labelled_bisimulation ((symcl (Rel⇧=))⇧+) Cal"
proof -
  from bisim show A: "strong_labelled_bisimulation (Rel⇧=) Cal"
    by (auto simp add: refl, blast+)
  have B: "⋀Rel. strong_labelled_bisimulation Rel Cal
           ⟹ strong_labelled_bisimulation (symcl Rel) Cal"
    by (auto simp add: symcl_def, blast+)
  from bisim B[where Rel="Rel"] show "strong_labelled_bisimulation (symcl Rel) Cal"
    by blast
  have C: "⋀Rel. strong_labelled_bisimulation Rel Cal ⟹ strong_labelled_bisimulation (Rel⇧+) Cal"
  proof
    fix Rel
    assume "strong_labelled_bisimulation Rel Cal"
    thus "strong_labelled_simulation (Rel⇧+) Cal"
      using strong_labelled_simulation_and_closures(2)[where Rel="Rel" and Cal="Cal"]
      by blast
  next
    fix Rel
    assume C1: "strong_labelled_bisimulation Rel Cal"
    show "∀P Q α Q'. (P, Q) ∈ Rel⇧+ ∧ Q ─α→Cal Q' ⟶ (∃P'. P ─α→Cal P' ∧ (P', Q') ∈ Rel⇧+)"
    proof clarify
      fix P Q α Q'
      assume "(P, Q) ∈ Rel⇧+" and "Q ─α→Cal Q'"
      thus "∃P'. P ─α→Cal P' ∧ (P', Q') ∈ Rel⇧+"
      proof (induct arbitrary: Q')
        fix Q Q'
        assume "(P, Q) ∈ Rel" and "Q ─α→Cal Q'"
        with C1 obtain P' where "P ─α→Cal P'" and "(P', Q') ∈ Rel"
          by blast
        thus "∃P'. P ─α→Cal P' ∧ (P', Q') ∈ Rel⇧+"
          by auto
      next
        case (step Q R R')
        assume "(Q, R) ∈ Rel" and "R ─α→Cal R'"
        with C1 obtain Q' where C2: "Q ─α→Cal Q'" and C3: "(Q', R') ∈ Rel⇧+"
          by blast
        assume "⋀Q'. Q ─α→Cal Q' ⟹ ∃P'. P ─α→Cal P' ∧ (P', Q') ∈ Rel⇧+"
        with C2 obtain P' where C4: "P ─α→Cal P'" and C5: "(P', Q') ∈ Rel⇧+"
          by blast
        from C5 C3 have "(P', R') ∈ Rel⇧+"
          by simp
        with C4 show "∃P'. P ─α→Cal P' ∧ (P', R') ∈ Rel⇧+"
          by blast
      qed
    qed
  qed
  from bisim C[where Rel="Rel"] show "strong_labelled_bisimulation (Rel⇧+) Cal"
    by blast
  from A B[where Rel="Rel⇧="]
  show "strong_labelled_bisimulation (symcl (Rel⇧=)) Cal"
    by blast
  from A C[where Rel="Rel⇧="]
  show "strong_labelled_bisimulation (Rel⇧*) Cal"
    using trancl_reflcl[of Rel]
    by auto
  from A B[where Rel="Rel⇧="] C[where Rel="symcl (Rel⇧=)"]
  show "strong_labelled_bisimulation ((symcl (Rel⇧=))⇧+) Cal"
    by blast
qed

subsection ‹Step Closure of Relations›

text ‹The step closure of a relation on process terms is the transitive closure of the union of
      the relation and the inverse of the reduction relation of the respective calculus.›

inductive_set stepsClosure :: "('a × 'a) set ⇒ 'a processCalculus ⇒ ('a × 'a) set"
    for Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
  where
  rel:   "(P, Q) ∈ Rel ⟹ (P, Q) ∈ stepsClosure Rel Cal" |
  steps: "P ⟼Cal* P' ⟹ (P', P) ∈ stepsClosure Rel Cal" |
  trans: "⟦(P, Q) ∈ stepsClosure Rel Cal; (Q, R) ∈ stepsClosure Rel Cal⟧
          ⟹ (P, R) ∈ stepsClosure Rel Cal"

abbreviation stepsClosureInfix ::
    "'a ⇒ ('a × 'a) set ⇒ 'a processCalculus ⇒ 'a ⇒ bool" (‹_ ℛ↦<_,_> _› [75, 75, 75, 75] 80)
  where
  "P ℛ↦<Rel,Cal> Q ≡ (P, Q) ∈ stepsClosure Rel Cal"

inductive_set stepsClosureLS
  :: "('a × 'a) set ⇒ ('a, 'b) labelledProcessCalculus ⇒ ('a × 'a) set"
    for Rel :: "('a × 'a) set"
    and Cal :: "('a, 'b) labelledProcessCalculus"
  where
  rel:   "(P, Q) ∈ Rel ⟹ (P, Q) ∈ stepsClosureLS Rel Cal" |
  steps: "P →Cal* P' ⟹ (P', P) ∈ stepsClosureLS Rel Cal" |
  trans: "⟦(P, Q) ∈ stepsClosureLS Rel Cal; (Q, R) ∈ stepsClosureLS Rel Cal⟧
          ⟹ (P, R) ∈ stepsClosureLS Rel Cal"

abbreviation stepsClosureLSInfix
  :: "'a ⇒ ('a × 'a) set ⇒ ('a, 'b) labelledProcessCalculus ⇒ 'a ⇒ bool"
  (‹_ ℛ→<_,_> _› [75, 75, 75, 75] 80) where
  "P ℛ→<Rel,Cal> Q ≡ (P, Q) ∈ stepsClosureLS Rel Cal"

text ‹Applying the steps closure twice does not change the relation.›

lemma steps_closure_of_steps_closure:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
  shows "stepsClosure (stepsClosure Rel Cal) Cal = stepsClosure Rel Cal"
proof auto
  fix P Q
  assume "P ℛ↦<stepsClosure Rel Cal,Cal> Q"
  thus "P ℛ↦<Rel,Cal> Q"
  proof induct
    case (rel P Q)
    assume "P ℛ↦<Rel,Cal> Q"
    thus "P ℛ↦<Rel,Cal> Q"
      by simp
  next
    case (steps P P')
    assume "P ⟼Cal* P'"
    thus "P' ℛ↦<Rel,Cal> P"
      by (rule stepsClosure.steps)
  next
    case (trans P Q R)
    assume "P ℛ↦<Rel,Cal> Q" and "Q ℛ↦<Rel,Cal> R"
    thus "P ℛ↦<Rel,Cal> R"
      by (rule stepsClosure.trans)
  qed
next
  fix P Q
  assume "P ℛ↦<Rel,Cal> Q"
  thus "P ℛ↦<stepsClosure Rel Cal,Cal> Q"
    by (rule stepsClosure.rel)
qed

lemma steps_closure_LS_of_steps_closure_LS:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "('a, 'b) labelledProcessCalculus"
  shows "stepsClosureLS (stepsClosureLS Rel Cal) Cal = stepsClosureLS Rel Cal"
proof auto
  fix P Q
  assume "P ℛ→<stepsClosureLS Rel Cal,Cal> Q"
  thus "P ℛ→<Rel,Cal> Q"
  proof induct
    case (rel P Q)
    assume "P ℛ→<Rel,Cal> Q"
    thus "P ℛ→<Rel,Cal> Q"
      by simp
  next
    case (steps P P')
    assume "P →Cal* P'"
    thus "P' ℛ→<Rel,Cal> P"
      by (rule stepsClosureLS.steps)
  next
    case (trans P Q R)
    assume "P ℛ→<Rel,Cal> Q" and "Q ℛ→<Rel,Cal> R"
    thus "P ℛ→<Rel,Cal> R"
      by (rule stepsClosureLS.trans)
  qed
next
  fix P Q
  assume "P ℛ→<Rel,Cal> Q"
  thus "P ℛ→<stepsClosureLS Rel Cal,Cal> Q"
    by (rule stepsClosureLS.rel)
qed

text ‹The steps closure is a preorder.›

lemma stepsClosure_refl:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
  shows "refl (stepsClosure Rel Cal)"
  unfolding refl_on_def
proof auto
  fix P
  have "P ⟼Cal* P"
    by (rule steps_refl)
  thus "P ℛ↦<Rel,Cal> P"
    by (rule stepsClosure.steps)
qed

lemma stepsClosureLS_refl:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "('a, 'b) labelledProcessCalculus"
  shows "refl (stepsClosureLS Rel Cal)"
  unfolding refl_on_def
proof auto
  fix P
  have "P →Cal* P"
    by (rule WTS_refl)
  thus "P ℛ→<Rel,Cal> P"
    by (rule stepsClosureLS.steps)
qed

lemma refl_trans_closure_of_rel_impl_steps_closure:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
    and P Q :: "'a"
  assumes "(P, Q) ∈ Rel⇧*"
  shows "P ℛ↦<Rel,Cal> Q"
  using assms
proof induct
  show "P ℛ↦<Rel,Cal> P"
    using stepsClosure_refl[of Rel Cal]
    unfolding refl_on_def
    by simp
next
  case (step Q R)
  assume "(Q, R) ∈ Rel" and "P ℛ↦<Rel,Cal> Q"
  thus "P ℛ↦<Rel,Cal> R"
    using stepsClosure.rel[of Q R Rel Cal] stepsClosure.trans[of P Q Rel Cal R]
    by blast
qed

lemma refl_trans_closure_of_rel_impl_steps_closure_LS:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "('a, 'b) labelledProcessCalculus"
    and P Q :: "'a"
  assumes "(P, Q) ∈ Rel⇧*"
  shows "P ℛ→<Rel,Cal> Q"
  using assms
proof induct
  show "P ℛ→<Rel,Cal> P"
    using stepsClosureLS_refl[of Rel Cal]
    unfolding refl_on_def
    by simp
next
  case (step Q R)
  assume "(Q, R) ∈ Rel" and "P ℛ→<Rel,Cal> Q"
  thus "P ℛ→<Rel,Cal> R"
    using stepsClosureLS.rel[of Q R Rel Cal] stepsClosureLS.trans[of P Q Rel Cal R]
    by blast
qed

text ‹The steps closure of a relation is always a weak reduction simulation.›

lemma steps_closure_is_weak_reduction_simulation:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
  shows "weak_reduction_simulation (stepsClosure Rel Cal) Cal"
proof clarify
  fix P Q P'
  assume "P ℛ↦<Rel,Cal> Q" and "P ⟼Cal* P'"
  thus "∃Q'. Q ⟼Cal* Q' ∧ P' ℛ↦<Rel,Cal> Q'"
  proof (induct arbitrary: P')
    case (rel P Q)
    assume "P ⟼Cal* P'"
    hence "P' ℛ↦<Rel,Cal> P"
      by (rule stepsClosure.steps)
    moreover assume "(P, Q) ∈ Rel"
    hence "P ℛ↦<Rel,Cal> Q"
      by (simp add: stepsClosure.rel)
    ultimately have "P' ℛ↦<Rel,Cal> Q"
      by (rule stepsClosure.trans)
    thus "∃Q'. Q ⟼Cal* Q' ∧ P' ℛ↦<Rel,Cal> Q'"
      using steps_refl[where Cal="Cal" and P="Q"]
      by blast
  next
    case (steps P P' P'')
    assume "P ⟼Cal* P'" and "P' ⟼Cal* P''"
    hence "P ⟼Cal* P''"
      by (rule steps_add)
    moreover have "P'' ℛ↦<Rel,Cal> P''"
      using stepsClosure_refl[where Rel="Rel" and Cal="Cal"]
      unfolding refl_on_def
      by simp
    ultimately show "∃Q'. P ⟼Cal* Q' ∧ P'' ℛ↦<Rel,Cal> Q'"
      by blast
  next
    case (trans P Q R)
    assume "P ⟼Cal* P'"
       and "⋀P'. P ⟼Cal* P' ⟹ ∃Q'. Q ⟼Cal* Q' ∧ P' ℛ↦<Rel,Cal> Q'"
    from this obtain Q' where A1: "Q ⟼Cal* Q'" and A2: "P' ℛ↦<Rel,Cal> Q'"
      by blast
    assume "⋀Q'. Q ⟼Cal* Q' ⟹ ∃R'. R ⟼Cal* R' ∧ Q' ℛ↦<Rel,Cal> R'"
    with A1 obtain R' where A3: "R ⟼Cal* R'" and A4: "Q' ℛ↦<Rel,Cal> R'"
      by blast
    from A2 A4 have "P' ℛ↦<Rel,Cal> R'"
      by (rule stepsClosure.trans)
    with A3 show "∃R'. R ⟼Cal* R' ∧ P' ℛ↦<Rel,Cal> R'"
      by blast
  qed
qed

text ‹If Rel is a weak simulation and its inverse is a weak contrasimulation, then the steps
      closure of Rel is a contrasimulation.›

lemma inverse_contrasimulation_impl_reverse_pair_in_steps_closure:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
    and P Q :: "'a"
  assumes con:  "weak_reduction_contrasimulation (Rel¯) Cal"
      and pair: "(P, Q) ∈ Rel"
  shows "Q ℛ↦<Rel,Cal> P"
proof -
  from pair have "(Q, P) ∈ Rel¯"
    by simp
  moreover have "Q ⟼Cal* Q"
    by (rule steps_refl)
  ultimately obtain P' where A1: "P ⟼Cal* P'" and A2: "(P', Q) ∈ Rel¯"
    using con
    by blast
  from A2 have "Q ℛ↦<Rel,Cal> P'"
    by (simp add: stepsClosure.rel)
  moreover from A1 have "P' ℛ↦<Rel,Cal> P"
    by (rule stepsClosure.steps)
  ultimately show "Q ℛ↦<Rel,Cal> P"
    by (rule stepsClosure.trans)
qed

lemma simulation_and_inverse_contrasimulation_impl_steps_closure_is_contrasimulation:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
  assumes sim: "weak_reduction_simulation Rel Cal"
      and con: "weak_reduction_contrasimulation (Rel¯) Cal"
    shows "weak_reduction_contrasimulation (stepsClosure Rel Cal) Cal"
proof clarify
  fix P Q P'
  assume "P ℛ↦<Rel,Cal> Q" and "P ⟼Cal* P'"
  thus "∃Q'. Q ⟼Cal* Q' ∧ Q' ℛ↦<Rel,Cal> P'"
  proof (induct arbitrary: P')
    case (rel P Q)
    assume "(P, Q) ∈ Rel" and "P ⟼Cal* P'"
    with sim obtain Q' where A1: "Q ⟼Cal* Q'" and A2: "(P', Q') ∈ Rel"
      by blast
    from A2 con have "Q' ℛ↦<Rel,Cal> P'"
      using inverse_contrasimulation_impl_reverse_pair_in_steps_closure[where Rel="Rel"]
      by blast
    with A1 show "∃Q'. Q ⟼Cal* Q' ∧ Q' ℛ↦<Rel,Cal> P'"
      by blast
  next
    case (steps P P' P'')
    assume "P ⟼Cal* P'" and "P' ⟼Cal* P''"
    hence "P ⟼Cal* P''"
      by (rule steps_add)
    thus "∃Q'. P ⟼Cal* Q' ∧ Q' ℛ↦<Rel,Cal> P''"
      using stepsClosure_refl[where Rel="Rel" and Cal="Cal"]
      unfolding refl_on_def
      by blast
  next
    case (trans P Q R)
    assume "⋀P'. P ⟼Cal* P' ⟹ ∃Q'. Q ⟼Cal* Q' ∧ Q' ℛ↦<Rel,Cal> P'"
       and "P ⟼Cal* P'"
    from this obtain Q' where A1: "Q ⟼Cal* Q'" and A2: "Q' ℛ↦<Rel,Cal> P'"
      by blast
    assume "⋀Q'. Q ⟼Cal* Q' ⟹ ∃R'. R ⟼Cal* R' ∧ R' ℛ↦<Rel,Cal> Q'"
    with A1 obtain R' where A3: "R ⟼Cal* R'" and A4: "R' ℛ↦<Rel,Cal> Q'"
      by blast
    from A4 A2 have "R' ℛ↦<Rel,Cal> P'"
      by (rule stepsClosure.trans)
    with A3 show "∃R'. R ⟼Cal* R' ∧ R' ℛ↦<Rel,Cal> P'"
      by blast
  qed
qed

text ‹Accordingly, if Rel is a weak simulation and its inverse is a weak contrasimulation, then the
      steps closure of Rel is a coupled simulation.›

lemma simulation_and_inverse_contrasimulation_impl_steps_closure_is_coupled_simulation:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
  assumes sim: "weak_reduction_simulation Rel Cal"
      and con: "weak_reduction_contrasimulation (Rel¯) Cal"
    shows "weak_reduction_coupled_simulation (stepsClosure Rel Cal) Cal"
  using sim con simulation_and_inverse_contrasimulation_impl_steps_closure_is_contrasimulation
        steps_closure_is_weak_reduction_simulation[where Rel="Rel" and Cal="Cal"]
  by simp

text ‹If the relation that is closed under steps is a (contra)simulation, then we can conclude from
      a pair in the closure on a pair in the original relation.›

lemma stepsClosure_simulation_impl_refl_trans_closure_of_Rel:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
    and P Q :: "'a"
  assumes A1: "P ℛ↦<Rel,Cal> Q"
      and A2: "weak_reduction_simulation Rel Cal"
    shows "∃Q'. Q ⟼Cal* Q' ∧ (P, Q') ∈ Rel⇧*"
proof -
  have "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel⇧*)"
    using A1
  proof induct
    case (rel P Q)
    assume "(P, Q) ∈ Rel"
    with A2 have "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel)"
      by blast
    thus "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel⇧*)"
      by blast
  next
    case (steps P P')
    assume A: "P ⟼Cal* P'"
    show "∀P''. P' ⟼Cal* P'' ⟶ (∃Q'. P ⟼Cal* Q' ∧ (P'', Q') ∈ Rel⇧*)"
    proof clarify
      fix P''
      assume "P' ⟼Cal* P''"
      with A have "P ⟼Cal* P''"
        by (rule steps_add)
      moreover have "(P'', P'') ∈ Rel⇧*"
        by simp
      ultimately show "∃Q'. P ⟼Cal* Q' ∧ (P'', Q') ∈ Rel⇧*"
        by blast
    qed
  next
    case (trans P Q R)
    assume A1: "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel⇧*)"
       and A2: "∀Q'. Q ⟼Cal* Q' ⟶ (∃R'. R ⟼Cal* R' ∧ (Q', R') ∈ Rel⇧*)"
    show "∀P'. P ⟼Cal* P' ⟶ (∃R'. R ⟼Cal* R' ∧ (P', R') ∈ Rel⇧*)"
    proof clarify
      fix P'
      assume "P ⟼Cal* P'"
      with A1 obtain Q' where A3: "Q ⟼Cal* Q'" and A4: "(P', Q') ∈ Rel⇧*"
        by blast
      from A2 A3 obtain R' where A5: "R ⟼Cal* R'" and A6: "(Q', R') ∈ Rel⇧*"
        by blast
      from A4 A6 have "(P', R') ∈ Rel⇧*"
        by simp
      with A5 show "∃R'. R ⟼Cal* R' ∧ (P', R') ∈ Rel⇧*"
        by blast
    qed
  qed
  moreover have "P ⟼Cal* P"
    by (rule steps_refl)
  ultimately show ?thesis
    by blast
qed

lemma stepsClosure_contrasimulation_impl_refl_trans_closure_of_Rel:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
    and P Q :: "'a"
  assumes A1: "P ℛ↦<Rel,Cal> Q"
      and A2: "weak_reduction_contrasimulation Rel Cal"
    shows "∃Q'. Q ⟼Cal* Q' ∧ (Q', P) ∈ Rel⇧*"
proof -
  have "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel⇧*)"
    using A1
  proof induct
    case (rel P Q)
    assume "(P, Q) ∈ Rel"
    with A2 have "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel)"
      by blast
    thus "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel⇧*)"
      by blast
  next
    case (steps P P')
    assume A: "P ⟼Cal* P'"
    show "∀P''. P' ⟼Cal* P'' ⟶ (∃Q'. P ⟼Cal* Q' ∧ (Q', P'') ∈ Rel⇧*)"
    proof clarify
      fix P''
      assume "P' ⟼Cal* P''"
      with A have "P ⟼Cal* P''"
        by (rule steps_add)
      moreover have "(P'', P'') ∈ Rel⇧*"
        by simp
      ultimately show "∃Q'. P ⟼Cal* Q' ∧ (Q', P'') ∈ Rel⇧*"
        by blast
    qed
  next
    case (trans P Q R)
    assume A1: "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel⇧*)"
       and A2: "∀Q'. Q ⟼Cal* Q' ⟶ (∃R'. R ⟼Cal* R' ∧ (R', Q') ∈ Rel⇧*)"
    show "∀P'. P ⟼Cal* P' ⟶ (∃R'. R ⟼Cal* R' ∧ (R', P') ∈ Rel⇧*)"
    proof clarify
      fix P'
      assume "P ⟼Cal* P'"
      with A1 obtain Q' where A3: "Q ⟼Cal* Q'" and A4: "(Q', P') ∈ Rel⇧*"
        by blast
      from A2 A3 obtain R' where A5: "R ⟼Cal* R'" and A6: "(R', Q') ∈ Rel⇧*"
        by blast
      from A4 A6 have "(R', P') ∈ Rel⇧*"
        by simp
      with A5 show "∃R'. R ⟼Cal* R' ∧ (R', P') ∈ Rel⇧*"
        by blast
    qed
  qed
  moreover have "P ⟼Cal* P"
    by (rule steps_refl)
  ultimately show ?thesis
    by blast
qed

lemma stepsClosure_contrasimulation_of_inverse_impl_refl_trans_closure_of_Rel:
  fixes Rel :: "('a × 'a) set"
    and Cal :: "'a processCalculus"
    and P Q :: "'a"
  assumes A1: "P ℛ↦<Rel¯,Cal> Q"
      and A2: "weak_reduction_contrasimulation (Rel¯) Cal"
    shows "∃Q'. Q ⟼Cal* Q' ∧ (P, Q') ∈ Rel⇧*"
proof -
  have "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel⇧*)"
    using A1
  proof induct
    case (rel P Q)
    assume "(P, Q) ∈ Rel¯"
    with A2 have "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (Q', P') ∈ Rel¯)"
      by blast
    thus "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel⇧*)"
      by blast
  next
    case (steps P P')
    assume A: "P ⟼Cal* P'"
    show "∀P''. P' ⟼Cal* P'' ⟶ (∃Q'. P ⟼Cal* Q' ∧ (P'', Q') ∈ Rel⇧*)"
    proof clarify
      fix P''
      assume "P' ⟼Cal* P''"
      with A have "P ⟼Cal* P''"
        by (rule steps_add)
      moreover have "(P'', P'') ∈ Rel⇧*"
        by simp
      ultimately show "∃Q'. P ⟼Cal* Q' ∧ (P'', Q') ∈ Rel⇧*"
        by blast
    qed
  next
    case (trans P Q R)
    assume A1: "∀P'. P ⟼Cal* P' ⟶ (∃Q'. Q ⟼Cal* Q' ∧ (P', Q') ∈ Rel⇧*)"
       and A2: "∀Q'. Q ⟼Cal* Q' ⟶ (∃R'. R ⟼Cal* R' ∧ (Q', R') ∈ Rel⇧*)"
    show "∀P'. P ⟼Cal* P' ⟶ (∃R'. R ⟼Cal* R' ∧ (P', R') ∈ Rel⇧*)"
    proof clarify
      fix P'
      assume "P ⟼Cal* P'"
      with A1 obtain Q' where A3: "Q ⟼Cal* Q'" and A4: "(P', Q') ∈ Rel⇧*"
        by blast
      from A3 A2 obtain R' where A5: "R ⟼Cal* R'" and A6: "(Q', R') ∈ Rel⇧*"
        by blast
      from A4 A6 have "(P', R') ∈ Rel⇧*"
        by simp
      with A5 show "∃R'. R ⟼Cal* R' ∧ (P', R') ∈ Rel⇧*"
        by blast
    qed
  qed
  moreover have "P ⟼Cal* P"
    by (rule steps_refl)
  ultimately show ?thesis
    by blast
qed

end