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