Theory SimulationRelations

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 ‹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

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 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 CalnP'"
    by (auto simp add: steps_def)
  thus "Q'. Q Cal* Q'  (P', Q')  Rel"
  proof (induct n arbitrary: P')
    case 0
    assume "P Cal0P'"
    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 CalSuc nP''"
    from this obtain P' where A2: "P CalnP'" and A3: "P' Cal P''"
      by auto
    assume "P'. P CalnP'  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

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

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 ‹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

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 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

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

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 P evolves to some P' then there exists some P'' and Q'' such that
            P evolves to P'' and Q' evolves to Q'' and (P'', Q'') in Rel.›

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 ‹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

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

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

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 refl
          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

subsection ‹Bisimulation›

text ‹A weak reduction bisimulation 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' 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 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

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_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_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

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

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

text ‹A strong reduction bisimulation is 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 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

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_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_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

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 CalnQ'"
      by (auto simp add: steps_def)
    thus "P'. P Cal* P'  (P', Q')  Rel"
    proof (induct n arbitrary: Q')
      case 0
      assume "Q Cal0Q'"
      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 CalSuc nQ''"
      from this obtain Q' where A2: "Q CalnQ'" and A3: "Q' Cal Q''"
        by auto
      assume "Q'. Q CalnQ'  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

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

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"

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

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 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

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 conlude
        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