subsection ‹Weak Simulation›
theory Weak_Relations
imports
Weak_Transition_Systems
Strong_Relations
begin
context lts_tau
begin
definition weak_simulation ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹weak_simulation R ≡ ∀ p q. R p q ⟶
(∀ p' a. p ⟼a p' ⟶ (∃ q'. R p' q'
∧ (q ⇒^a q')))›
text ‹Note: Isabelle won't finish the proofs needed for the introduction of the following
coinductive predicate if it unfolds the abbreviation of @{text ‹⇒^›}. Therefore we use
@{text ‹⇒^^›} as a barrier. There is no mathematical purpose in this.›
definition weak_step_tau2 :: ‹'s ⇒ 'a ⇒ 's ⇒ bool›
("_ ⇒^^ _ _" [70, 70, 70] 80)
where [simp]:
‹(p ⇒^^ a q) ≡ p ⇒^a q›
coinductive greatest_weak_simulation ::
‹'s ⇒ 's ⇒ bool›
where
‹(∀ p' a. p ⟼a p' ⟶ (∃ q'. greatest_weak_simulation p' q' ∧ (q ⇒^^ a q')))
⟹ greatest_weak_simulation p q›
lemma weak_sim_ruleformat:
assumes ‹weak_simulation R›
and ‹R p q›
shows
‹p ⟼a p' ⟹ ¬tau a ⟹ (∃ q'. R p' q' ∧ (q ⇒a q'))›
‹p ⟼a p' ⟹ tau a ⟹ (∃ q'. R p' q' ∧ (q ⟼* tau q'))›
using assms unfolding weak_simulation_def by (blast+)
abbreviation weakly_simulated_by :: ‹'s ⇒ 's ⇒ bool› ("_ ⊑ws _" [60, 60] 65)
where ‹weakly_simulated_by p q ≡ ∃ R . weak_simulation R ∧ R p q›
lemma weaksim_greatest:
shows ‹weak_simulation (λ p q . p ⊑ws q)›
unfolding weak_simulation_def
by (metis (no_types, lifting))
lemma gws_is_weak_simulation:
shows ‹weak_simulation greatest_weak_simulation›
unfolding weak_simulation_def
proof safe
fix p q p' a
assume ih:
‹greatest_weak_simulation p q›
‹p ⟼a p'›
hence ‹(∀x xa. p ⟼x xa ⟶ (∃q'. q ⇒^^ x q' ∧ greatest_weak_simulation xa q'))›
by (meson greatest_weak_simulation.simps)
then obtain q' where ‹q ⇒^^ a q' ∧ greatest_weak_simulation p' q'› using ih by blast
thus ‹∃q'. greatest_weak_simulation p' q' ∧ q ⇒^a q'›
unfolding weak_step_tau2_def by blast
qed
lemma weakly_sim_by_implies_gws:
assumes ‹p ⊑ws q›
shows ‹greatest_weak_simulation p q›
using assms
proof (coinduct, simp del: weak_step_tau2_def, safe)
fix x1 x2 R a xa
assume ih: ‹weak_simulation R› ‹R x1 x2› ‹x1 ⟼a xa›
then obtain q' where ‹x2 ⇒^^ a q'› ‹R xa q'›
unfolding weak_simulation_def weak_step_tau2_def by blast
thus ‹∃q'. (xa ⊑ws q' ∨ greatest_weak_simulation xa q') ∧ x2 ⇒^^ a q'›
using ih by blast
qed
lemma gws_eq_weakly_sim_by:
shows ‹p ⊑ws q = greatest_weak_simulation p q›
using weakly_sim_by_implies_gws gws_is_weak_simulation by blast
lemma steps_retain_weak_sim:
assumes
‹weak_simulation R›
‹R p q›
‹p ⟼*A p'›
‹⋀ a . tau a ⟹ A a›
shows ‹∃q'. R p' q' ∧ q ⟼*A q'›
using assms(3,2,4) proof (induct)
case (refl p' A)
hence ‹R p' q ∧ q ⟼* A q› using assms(2) steps.refl by simp
then show ?case by blast
next
case (step p A p' a p'')
then obtain q' where q': ‹R p' q'› ‹q ⟼* A q'› by blast
obtain q'' where q'':
‹R p'' q''› ‹(¬ tau a ⟶ q' ⇒a q'') ∧ (tau a ⟶ q' ⟼* tau q'')›
using `weak_simulation R` q'(1) step(3) unfolding weak_simulation_def by blast
have ‹q' ⟼* A q''›
using q''(2) steps_spec[of q'] step(4) step(6) weak_steps[of q' a q''] by blast
hence ‹q ⟼* A q''› using steps_concat[OF _ q'(2)] by blast
thus ?case using q''(1) by blast
qed
lemma weak_sim_weak_premise:
‹weak_simulation R =
(∀ p q . R p q ⟶
(∀ p' a. p ⇒^a p' ⟶ (∃ q'. R p' q' ∧ q ⇒^a q')))›
proof
assume ‹∀ p q . R p q ⟶ (∀p' a. p ⇒^a p' ⟶ (∃q'. R p' q' ∧ q ⇒^a q'))›
thus ‹weak_simulation R›
unfolding weak_simulation_def using step_weak_step_tau by simp
next
assume ws: ‹weak_simulation R›
show ‹∀p q. R p q ⟶ (∀p' a. p ⇒^a p' ⟶ (∃q'. R p' q' ∧ q ⇒^a q'))›
proof safe
fix p q p' a pq1 pq2
assume case_assms:
‹R p q›
‹p ⟼* tau pq1›
‹pq1 ⟼a pq2›
‹pq2 ⟼* tau p'›
then obtain q' where q'_def: ‹q ⟼* tau q'› ‹R pq1 q'›
using steps_retain_weak_sim[OF ws] by blast
then moreover obtain q'' where q''_def: ‹R pq2 q''› ‹q' ⇒^a q''›
using ws case_assms(3) unfolding weak_simulation_def by blast
then moreover obtain q''' where q''_def: ‹R p' q'''› ‹q'' ⟼* tau q'''›
using case_assms(4) steps_retain_weak_sim[OF ws] by blast
ultimately show ‹∃ q'''. R p' q''' ∧ q ⇒^a q'''› using weak_step_extend by blast
next
fix p q p' a
assume
‹R p q›
‹p ⟼* tau p'›
‹∄q'. R p' q' ∧ q ⇒^a q'›
‹tau a›
thus ‹False›
using steps_retain_weak_sim[OF ws] by blast
next
fix p q p' a pq1 pq2
assume case_assms:
‹R p q›
‹p ⟼* tau pq1›
‹pq1 ⟼a pq2›
‹pq2 ⟼* tau p'›
then obtain q' where q'_def: ‹q ⟼* tau q'› ‹R pq1 q'›
using steps_retain_weak_sim[OF ws] by blast
then moreover obtain q'' where q''_def: ‹R pq2 q''› ‹q' ⇒^a q''›
using ws case_assms(3) unfolding weak_simulation_def by blast
then moreover obtain q''' where q''_def: ‹R p' q'''› ‹q'' ⟼* tau q'''›
using case_assms(4) steps_retain_weak_sim[OF ws] by blast
ultimately show ‹∃ q'''. R p' q''' ∧ q ⇒^a q'''› using weak_step_extend by blast
qed
qed
lemma weak_sim_enabled_subs:
assumes
‹p ⊑ws q›
‹weak_enabled p a›
‹¬ tau a›
shows ‹weak_enabled q a›
proof-
obtain p' where p'_spec: ‹p ⇒a p'›
using ‹weak_enabled p a› weak_enabled_step by blast
obtain R where ‹R p q› ‹weak_simulation R› using assms(1) by blast
then obtain q' where ‹q ⇒^a q'›
unfolding weak_sim_weak_premise using weak_step_impl_weak_tau[OF p'_spec] by blast
thus ?thesis using weak_enabled_step assms(3) by blast
qed
lemma weak_sim_union_cl:
assumes
‹weak_simulation RA›
‹weak_simulation RB›
shows
‹weak_simulation (λ p q. RA p q ∨ RB p q)›
using assms unfolding weak_simulation_def by blast
lemma weak_sim_remove_dead_state:
assumes
‹weak_simulation R›
‹⋀ a p . ¬ step d a p ∧ ¬ step p a d›
shows
‹weak_simulation (λ p q . R p q ∧ q ≠ d)›
unfolding weak_simulation_def
proof safe
fix p q p' a
assume
‹R p q›
‹q ≠ d›
‹p ⟼a p'›
then obtain q' where ‹R p' q'› ‹q ⇒^a q'›
using assms(1) unfolding weak_simulation_def by blast
moreover hence ‹q' ≠ d›
using assms(2) `q ≠ d` by (metis steps.cases)
ultimately show ‹∃q'. (R p' q' ∧ q' ≠ d) ∧ q ⇒^a q'› by blast
qed
lemma weak_sim_tau_step:
‹weak_simulation (λ p1 q1 . q1 ⟼* tau p1)›
unfolding weak_simulation_def
using lts.steps.simps by metis
lemma weak_sim_trans_constructive:
fixes R1 R2
defines
‹R ≡ λ p q . ∃ pq . (R1 p pq ∧ R2 pq q) ∨ (R2 p pq ∧ R1 pq q)›
assumes
R1_def: ‹weak_simulation R1› ‹R1 p pq› and
R2_def: ‹weak_simulation R2› ‹R2 pq q›
shows
‹R p q› ‹weak_simulation R›
proof-
show ‹R p q› unfolding R_def using R1_def(2) R2_def(2) by blast
next
show ‹weak_simulation R›
unfolding weak_sim_weak_premise R_def
proof (safe)
fix p q pq p' a pq1 pq2
assume
‹R1 p pq›
‹R2 pq q›
‹¬ tau a›
‹p ⟼* tau pq1›
‹pq1 ⟼a pq2›
‹pq2 ⟼* tau p'›
thus ‹∃q'. (∃pq. R1 p' pq ∧ R2 pq q' ∨ R2 p' pq ∧ R1 pq q') ∧ q ⇒^a q'›
using R1_def(1) R2_def(1) unfolding weak_sim_weak_premise by blast
next
fix p q pq p' a
assume
‹R1 p pq›
‹R2 pq q›
‹p ⟼* tau p'›
‹∄q'.(∃pq. R1 p' pq ∧ R2 pq q' ∨ R2 p' pq ∧ R1 pq q')∧ q ⇒^a q'›
‹tau a›
thus ‹False›
using R1_def(1) R2_def(1) unfolding weak_sim_weak_premise by blast
next
fix p q pq p' a pq1 pq2
assume
‹R1 p pq›
‹R2 pq q›
‹p ⟼* tau p'›
‹p ⟼* tau pq1›
‹pq1 ⟼a pq2›
‹pq2 ⟼* tau p'›
then obtain pq' q' where ‹R1 p' pq'› ‹pq ⇒^a pq'› ‹R2 pq' q'› ‹q ⇒^a q'›
using R1_def(1) R2_def(1) assms(3) unfolding weak_sim_weak_premise by blast
thus ‹∃q'. (∃pq. R1 p' pq ∧ R2 pq q' ∨ R2 p' pq ∧ R1 pq q') ∧ q ⇒^a q'›
by blast
next
fix p q pq p' a pq1 pq2
assume sa:
‹R2 p pq›
‹R1 pq q›
‹¬ tau a›
‹p ⟼* tau pq1›
‹pq1 ⟼a pq2›
‹pq2 ⟼* tau p'›
then obtain pq' q' where ‹R2 p' pq'› ‹pq ⇒^a pq'› ‹R1 pq' q'› ‹q ⇒^a q'›
using R2_def(1) R1_def(1) unfolding weak_sim_weak_premise by blast
thus ‹∃q'. (∃pq. R1 p' pq ∧ R2 pq q' ∨ R2 p' pq ∧ R1 pq q') ∧ q ⇒^a q'›
by blast
next
fix p q pq p' a
assume
‹R2 p pq›
‹R1 pq q›
‹p ⟼* tau p'›
‹∄q'.(∃pq. R1 p' pq ∧ R2 pq q' ∨ R2 p' pq ∧ R1 pq q')∧ q ⇒^a q'›
‹tau a›
thus ‹False›
using R1_def(1) R2_def(1) weak_step_tau_tau[OF `p ⟼* tau p'` tau_tau]
unfolding weak_sim_weak_premise by (metis (no_types, lifting))
next
fix p q pq p' a pq1 pq2
assume sa:
‹R2 p pq›
‹R1 pq q›
‹p ⟼* tau p'›
‹p ⟼* tau pq1›
‹pq1 ⟼a pq2›
‹pq2 ⟼* tau p'›
then obtain pq' where ‹R2 p' pq'› ‹pq ⇒^a pq'›
using R1_def(1) R2_def(1) weak_step_impl_weak_tau[of p a p']
unfolding weak_sim_weak_premise by blast
moreover then obtain q' where ‹R1 pq' q'› ‹q ⇒^a q'›
using R1_def(1) sa(2) unfolding weak_sim_weak_premise by blast
ultimately show ‹∃q'. (∃pq. R1 p' pq ∧ R2 pq q' ∨ R2 p' pq ∧ R1 pq q') ∧ q ⇒^a q'›
by blast
qed
qed
lemma weak_sim_trans:
assumes
‹p ⊑ws pq›
‹pq ⊑ws q›
shows
‹p ⊑ws q›
using assms(1,2)
proof -
obtain R1 R2 where ‹weak_simulation R1› ‹R1 p pq› ‹weak_simulation R2› ‹R2 pq q›
using assms(1,2) by blast
thus ?thesis
using weak_sim_trans_constructive tau_tau
by blast
qed
subsection ‹Weak Bisimulation›
definition weak_bisimulation ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹weak_bisimulation R ≡ ∀ p q. R p q ⟶
(∀ p' a. p ⟼a p' ⟶ (∃ q'. R p' q'
∧ (q ⇒^a q'))) ∧
(∀ q' a. q ⟼a q' ⟶ (∃ p'. R p' q'
∧ ( p ⇒^a p')))›
lemma weak_bisim_ruleformat:
assumes ‹weak_bisimulation R›
and ‹R p q›
shows
‹p ⟼a p' ⟹ ¬tau a ⟹ (∃ q'. R p' q' ∧ (q ⇒a q'))›
‹p ⟼a p' ⟹ tau a ⟹ (∃ q'. R p' q' ∧ (q ⟼* tau q'))›
‹q ⟼a q' ⟹ ¬tau a ⟹ (∃ p'. R p' q' ∧ (p ⇒a p'))›
‹q ⟼a q' ⟹ tau a ⟹ (∃ p'. R p' q' ∧ (p ⟼* tau p'))›
using assms unfolding weak_bisimulation_def by (blast+)
definition tau_weak_bisimulation ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹tau_weak_bisimulation R ≡ ∀ p q. R p q ⟶
(∀ p' a. p ⟼a p' ⟶
(∃ q'. R p' q' ∧ (q ⇒a q'))) ∧
(∀ q' a. q ⟼a q' ⟶
(∃ p'. R p' q' ∧ (p ⇒a p')))›
lemma weak_bisim_implies_tau_weak_bisim:
assumes
‹tau_weak_bisimulation R›
shows
‹weak_bisimulation R›
unfolding weak_bisimulation_def proof (safe)
fix p q p' a
assume ‹R p q› ‹p ⟼a p'›
thus ‹∃q'. R p' q' ∧ (q ⇒^a q')›
using assms weak_steps[of q a _ tau] unfolding tau_weak_bisimulation_def by blast
next
fix p q q' a
assume ‹R p q› ‹q ⟼a q'›
thus ‹∃p'. R p' q' ∧ (p ⇒^a p')›
using assms weak_steps[of p a _ tau] unfolding tau_weak_bisimulation_def by blast
qed
lemma weak_bisim_invert:
assumes
‹weak_bisimulation R›
shows
‹weak_bisimulation (λ p q. R q p)›
using assms unfolding weak_bisimulation_def by auto
lemma bisim_weak_bisim:
assumes ‹bisimulation R›
shows ‹weak_bisimulation R›
unfolding weak_bisimulation_def
proof (clarify, rule)
fix p q
assume R: ‹R p q›
show ‹∀p' a. p ⟼a p' ⟶ (∃q'. R p' q' ∧ (q ⇒^a q'))›
proof (clarify)
fix p' a
assume p'a: ‹p ⟼a p'›
have
‹¬ tau a ⟶ (∃q'. R p' q' ∧ q ⇒a q')›
‹(tau a ⟶ (∃q'. R p' q' ∧ q ⟼* tau q'))›
using bisim_ruleformat(1)[OF assms R p'a] step_weak_step step_weak_step_tau by auto
thus ‹∃q'. R p' q' ∧ (q ⇒^a q')› by blast
qed
next
fix p q
assume R: ‹R p q›
have ‹∀q' a. q ⟼a q' ⟶ (¬ tau a ⟶ (∃p'. R p' q' ∧ p ⇒a p'))
∧ (tau a ⟶ (∃p'. R p' q' ∧ p ⟼* tau p'))›
proof (clarify)
fix q' a
assume q'a: ‹q ⟼a q'›
show
‹(¬ tau a ⟶ (∃p'. R p' q' ∧ p ⇒a p')) ∧
(tau a ⟶ (∃p'. R p' q' ∧ p ⟼* tau p'))›
using bisim_ruleformat(2)[OF assms R q'a] step_weak_step
step_weak_step_tau steps_one_step by auto
qed
thus ‹∀q' a. q ⟼a q' ⟶ (∃p'. R p' q' ∧ (p ⇒^a p'))› by blast
qed
lemma weak_bisim_weak_sim:
shows
‹weak_bisimulation R = (weak_simulation R ∧ weak_simulation (λ p q . R q p))›
unfolding weak_bisimulation_def weak_simulation_def by auto
lemma steps_retain_weak_bisim:
assumes
‹weak_bisimulation R›
‹R p q›
‹p ⟼*A p'›
‹⋀ a . tau a ⟹ A a›
shows ‹∃q'. R p' q' ∧ q ⟼*A q'›
using assms weak_bisim_weak_sim steps_retain_weak_sim
by auto
lemma weak_bisim_union:
assumes
‹weak_bisimulation R1›
‹weak_bisimulation R2›
shows
‹weak_bisimulation (λ p q . R1 p q ∨ R2 p q)›
using assms unfolding weak_bisimulation_def by blast
subsection ‹Delay Simulation›
definition delay_simulation ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹delay_simulation R ≡ ∀ p q. R p q ⟶
(∀ p' a. p ⟼a p' ⟶
(tau a ⟶ R p' q) ∧
(¬tau a ⟶ (∃ q'. R p' q'∧ (q =⊳a q'))))›
lemma delay_simulation_implies_weak_simulation:
assumes
‹delay_simulation R›
shows
‹weak_simulation R›
using assms weak_step_delay_implies_weak_tau steps.refl
unfolding delay_simulation_def weak_simulation_def by blast
subsection ‹Contrasimulation›
definition contrasim ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹contrasim R ≡ ∀ p q p' A .
R p q ∧ (p ⇒$ A p') ⟶
(∃ q'. (q ⇒$ A q')
∧ R q' p')›
definition contrasim_step ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹contrasim_step R ≡ ∀ p q p' a .
R p q ∧ (p ⇒^a p') ⟶
(∃ q'. (q ⇒^a q')
∧ R q' p')›
lemma contrasim_step_weaker_than_seq:
assumes
‹contrasim R›
shows
‹contrasim_step R›
unfolding contrasim_step_def
proof ((rule allI impI)+)
fix p q p' a
assume
‹R p q ∧ p ⇒^a p'›
hence
‹R p q› ‹p ⇒^a p'› by safe
hence ‹p ⇒$ [a] p'› by safe
then obtain q' where ‹R q' p'› ‹q ⇒$ [a] q'›
using assms `R p q` unfolding contrasim_def by blast
hence ‹q ⇒^a q'› by blast
thus ‹∃q'. q ⇒^a q' ∧ R q' p'› using `R q' p'` by blast
qed
lemma contrasim_step_seq_coincide_for_sims:
assumes
‹contrasim_step R›
‹weak_simulation R›
shows
‹contrasim R›
unfolding contrasim_def
proof (clarify)
fix p q p' A
assume
‹R p q›
‹p ⇒$ A p'›
thus ‹∃q'. q ⇒$ A q' ∧ R q' p'›
proof (induct A arbitrary: p p' q)
case Nil
then show ?case using assms(1) unfolding contrasim_step_def
using tau_tau weak_step_seq.simps(1) by blast
next
case (Cons a A)
then obtain p1 where p1_def: ‹p ⇒^a p1› ‹p1 ⇒$ (A) p'› by auto
then obtain q1 where q1_def: ‹q ⇒^a q1› ‹R p1 q1›
using assms(2) `R p q` unfolding weak_sim_weak_premise by blast
then obtain q' where ‹q1 ⇒$ (A) q'› ‹R q' p'› using p1_def(2) Cons(1) by blast
then show ?case using q1_def(1) by auto
qed
qed
definition contrasim_strong_step ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹contrasim_strong_step R ≡ ∀ p q p' a .
R p q ∧ (p ⟼a p') ⟶
(∃ q'. (q ⇒^a q')
∧ R q' p')›
lemma contrasim_challenge_strength_step_impl_strong_step:
assumes
‹contrasim_step R›
shows
‹contrasim_strong_step R›
using assms step_weak_step_tau
unfolding contrasim_step_def contrasim_strong_step_def by fastforce
lemma contrasim_reflexive:
shows
‹contrasim (λ p q . p = q)›
unfolding contrasim_def using step_weak_step_tau by blast
lemma contrasim_union:
assumes
‹contrasim R1›
‹contrasim R2›
shows
‹contrasim (λ p q . R1 p q ∨ R2 p q)›
using assms unfolding contrasim_def by (blast)
abbreviation coupling ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where ‹coupling R ≡ ∀ p q . R p q ⟶ (∃ q'. q ⟼*tau q' ∧ R q' p)›
lemma contrasim_implies_coupling:
assumes
‹contrasim R›
‹R p q›
shows
‹∃ q'. q ⟼*tau q' ∧ R q' p›
proof -
have ‹p ⟼* tau p› using steps.refl by blast
hence ‹p ⇒^τ p› using tau_tau by blast
then obtain q' where ‹q ⇒^τ q'› ‹R q' p›
using `R p q` `contrasim R` unfolding contrasim_def by blast
then moreover have ‹q ⟼* tau q'› using tau_tau by blast
ultimately show ?thesis by blast
qed
lemma symm_contrasim_implies_weak_bisim:
assumes
‹contrasim_strong_step R›
‹⋀ p q . R p q ⟹ R q p›
shows
‹weak_bisimulation R›
unfolding weak_bisimulation_def
proof safe
fix p q p' a
assume ‹R p q› ‹p ⟼a p'›
then obtain q' where q'_def: ‹q ⇒^a q'› ‹R q' p'›
using assms(1) unfolding contrasim_strong_step_def by blast
thus ‹∃q'. R p' q' ∧ q ⇒^a q'› using assms(2) by blast
next
fix p q q' a
assume ‹R p q› ‹q ⟼a q'›
hence ‹R q p› using assms(2) by blast
then obtain p' where p'_def: ‹p ⇒^a p'› ‹R p' q'›
using `q ⟼a q'` assms(1) unfolding contrasim_strong_step_def by blast
thus ‹∃p'. R p' q' ∧ p ⇒^a p'› using assms(2) by blast
qed
lemma coupling_tau_max_symm:
assumes
‹R p q ⟶ (∃ q'. q ⟼*tau q' ∧ R q' p)›
‹tau_max q›
‹R p q›
shows
‹R q p›
using assms steps_no_step_pos[of q tau] by blast
corollary coupling_stability_symm:
assumes
‹R p q ⟶ (∃ q'. q ⟼*tau q' ∧ R q' p)›
‹stable_state q›
‹R p q›
shows
‹R q p›
using coupling_tau_max_symm stable_tauclosure_only_loop assms by metis
lemma taufree_contrasim_symm:
assumes
‹⋀ p1 a p2 . (p1 ⟼a p2 ⟹ ¬ tau a)›
‹contrasim R›
‹R p q›
shows ‹R q p›
using assms contrasim_implies_coupling
by (metis steps.cases)
lemma taufree_contrasim_implies_weak_bisim:
assumes
‹⋀ p1 a p2 . (p1 ⟼a p2 ⟹ ¬ tau a)›
‹contrasim R›
shows
‹weak_bisimulation R›
using assms symm_contrasim_implies_weak_bisim taufree_contrasim_symm
contrasim_step_weaker_than_seq[OF assms(2)]
contrasim_challenge_strength_step_impl_strong_step by blast
lemma contrasim_challenge_strength_does_not_imply:
fixes p1 q1
defines
‹R ≡ λ p q . p = p1 ∧ q = q1›
assumes
‹p1 ≠ q1›
‹trans = (λ p a p' . False)›
shows
‹contrasim_strong_step R› ‹¬contrasim R›
using taufree_contrasim_symm[of R p1 q1] assms
unfolding contrasim_strong_step_def by (blast+)
end
subsection ‹Similarity ignores ‹τ›-sinks›
lemma simulation_tau_sink_1:
fixes
step sink τ R
defines
‹step2 ≡ λ p1 a p2 . (p1 ≠ sink ∧ a = τ ∧ p2 = sink) ∨ step p1 a p2›
assumes
‹⋀ a p . ¬ step sink a p›
‹lts_tau.weak_simulation step τ R›
shows
‹lts_tau.weak_simulation step2 τ (λ p q. p = sink ∨ R p q)›
proof -
let ?tau = ‹(lts_tau.tau τ)›
let ?tauEx = ‹τ›
show ?thesis unfolding lts_tau.weak_simulation_def
proof safe
fix p q p' a
assume ‹step2 sink a p'›
hence ‹p' = sink› ‹a = τ›
using assms(2) unfolding step2_def by auto
thus ‹∃q'. (p' = sink ∨ R p' q') ∧
(?tau a ⟶ lts.steps step2 q ?tau q') ∧
(¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1 ∧ step2 pq1 a pq2
∧ lts.steps step2 pq2 ?tau q'))›
using lts_tau.step_tau_refl[of τ step2 q] lts.steps.refl[of step2 q ?tau] by auto
next
fix p q p' a
assume ‹step2 p a p'› ‹R p q›
have step_impl_step2: ‹⋀ p1 a p2 . step p1 a p2 ⟹ step2 p1 a p2›
unfolding step2_def by blast
have ‹(p ≠ sink ∧ a = ?tauEx ∧ p' = sink) ∨ step p a p'›
using `step2 p a p'` unfolding step2_def .
thus ‹∃q'. (p' = sink ∨ R p' q') ∧
(?tau a ⟶ lts.steps step2 q ?tau q') ∧
(¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1 ∧ step2 pq1 a pq2
∧ lts.steps step2 pq2 ?tau q'))›
proof safe
show ‹∃q'. (sink = sink ∨ R sink q') ∧
(?tau ?tauEx ⟶ lts.steps step2 q ?tau q') ∧
(¬ ?tau ?tauEx ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1
∧ step2 pq1 ?tauEx pq2 ∧ lts.steps step2 pq2 ?tau q'))›
using lts.steps.refl[of step2 q ?tau] assms(1) by (meson lts_tau.tau_tau)
next
assume ‹step p a p'›
then obtain q' where q'_def:
‹R p' q' ∧
(?tau a ⟶ lts.steps step q ?tau q') ∧
(¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step q ?tau pq1 ∧ step pq1 a pq2
∧ lts.steps step pq2 ?tau q'))›
using assms(3) `R p q` unfolding lts_tau.weak_simulation_def by blast
hence ‹(p' = sink ∨ R p' q') ∧
(?tau a ⟶ lts.steps step2 q ?tau q') ∧
(¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1 ∧ step2 pq1 a pq2
∧ lts.steps step2 pq2 ?tau q'))›
using lts_impl_steps[of step _ _ _ step2] step_impl_step2 by blast
thus ‹∃q'. (p' = sink ∨ R p' q') ∧
(?tau a ⟶ lts.steps step2 q ?tau q') ∧
(¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1 ∧ step2 pq1 a pq2
∧ lts.steps step2 pq2 ?tau q'))›
by blast
qed
qed
qed
lemma simulation_tau_sink_2:
fixes
step sink R τ
defines
‹step2 ≡ λ p1 a p2 . (p1 ≠ sink ∧ a = τ ∧ p2 = sink) ∨ step p1 a p2›
assumes
‹⋀ a p . ¬ step sink a p ∧ ¬ step p a sink›
‹lts_tau.weak_simulation step2 τ (λ p q. p = sink ∨ R p q)›
‹⋀ p' q' q . (p' = sink ∨ R p' q')
∧ lts.steps step2 q (lts_tau.tau τ) q' ⟶ (p' = sink ∨ R p' q)›
shows
‹lts_tau.weak_simulation step τ (λ p q. p = sink ∨ R p q)›
proof -
let ?tau = ‹(lts_tau.tau τ)›
let ?tauEx = ‹τ›
let ?steps = ‹lts.steps›
show ?thesis
unfolding lts_tau.weak_simulation_def
proof safe
fix p q p' a
assume
‹step sink a p'›
hence False using assms(2) by blast
thus ‹∃q'. (p' = sink ∨ R p' q') ∧
(?tau a ⟶ ?steps step q ?tau q') ∧
(¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
∧ ?steps step pq2 ?tau q'))› ..
next
fix p q p' a
assume ‹R p q› ‹step p a p'›
hence not_sink: ‹p ≠ sink› ‹p' ≠ sink›
using assms(2)[of a p] assms(2)[of a p'] by auto
have ‹step2 p a p'› using `step p a p'` unfolding step2_def by blast
then obtain q' where q'_def:
‹p' = sink ∨ R p' q'›
‹?tau a ⟶ ?steps step2 q ?tau q'›
‹¬ ?tau a ⟶ (∃pq1 pq2. ?steps step2 q ?tau pq1 ∧ step2 pq1 a pq2
∧ ?steps step2 pq2 ?tau q')›
using assms(3) `R p q` unfolding lts_tau.weak_simulation_def by blast
hence outer_goal_a: ‹R p' q'› using not_sink by blast
show ‹∃q'. (p' = sink ∨ R p' q') ∧
(?tau a ⟶ ?steps step q ?tau q') ∧
(¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
∧ ?steps step pq2 ?tau q'))›
proof (cases ‹q' = sink›)
assume ‹q' = sink›
then obtain q'' where q''_def:
‹?tau a ⟶ (?steps step q ?tau q'' ∧ ?steps step2 q'' ?tau q')›
‹¬ ?tau a ⟶ (∃pq1. ?steps step2 q ?tau pq1 ∧ step pq1 a q''
∧ ?steps step2 q'' ?tau q')›
using q'_def(2,3) assms(1) step2_def lts_tau.step_tau_refl[of τ]
lts_tau.tau_tau[of τ] by metis
hence ‹q'' = sink ⟶ q = sink›
using assms(2) unfolding step2_def by (metis lts.steps.cases)
have ‹?steps step2 q'' ?tau q'› using q''_def by auto
hence ‹p' = sink ∨ R p' q''› using q'_def(1) assms(4)[of p' q' q''] by blast
moreover have ‹¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
∧ ?steps step pq2 ?tau q'')›
proof
assume ‹¬ ?tau a›
hence ‹q ≠ sink› using q'_def by (metis assms(2) lts.steps_left step2_def)
hence ‹q'' ≠ sink› using `q'' = sink ⟶ q = sink` by simp
obtain pq1 where pq1_def:
‹?steps step2 q ?tau pq1› ‹step pq1 a q''› ‹?steps step2 q'' ?tau q'›
using q''_def(2) `¬ ?tau a` by blast
hence ‹pq1 ≠ sink› using `q'' ≠ sink` assms(2) by blast
hence ‹?steps step q ?tau pq1› using `q ≠ sink` `?steps step2 q ?tau pq1`
proof (induct rule: lts.steps.induct[OF `?steps step2 q ?tau pq1`])
case (1 p af)
then show ?case using lts.steps.refl[of step p af] by blast
next
case (2 p af q1 a q)
hence ‹q1 ≠ sink› ‹step q1 a q› using assms(2) unfolding step2_def by auto
moreover hence ‹?steps step p af q1› using 2 by blast
ultimately show ?case using 2(4) by (meson lts.step)
qed
thus
‹∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2 ∧ ?steps step pq2 ?tau q''›
using pq1_def(2) lts.steps.refl[of step q'' ?tau] by blast
qed
ultimately show ‹∃q''. (p' = sink ∨ R p' q'') ∧
(?tau a ⟶ ?steps step q ?tau q'') ∧
(¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
∧ ?steps step pq2 ?tau q''))›
using q''_def(1) q'_def(1) by auto
next
assume not_sink_q': ‹q' ≠ sink›
have outer_goal_b: ‹?tau a ⟶ ?steps step q ?tau q'›
using q'_def(2) not_sink_q' unfolding step2_def
proof (safe)
assume i:
‹q' ≠ sink› ‹?tau a›
‹?steps (λp1 a p2. p1 ≠ sink ∧ a = ?tauEx ∧ p2 = sink ∨ step p1 a p2) q ?tau q'›
thus ‹?steps step q ?tau q'›
proof (induct rule: lts.steps.induct[OF i(3)])
case (1 p af)
then show ?case using lts.steps.refl[of _ p af] by auto
next
case (2 p af q1 a q)
hence ‹step q1 a q› by blast
moreover have ‹?steps step p af q1› using 2 assms(2) by blast
ultimately show ?case using `af a` lts.step[of step p af q1 a q] by blast
qed
qed
have outer_goal_c:
‹¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
∧ ?steps step pq2 ?tau q')›
using q'_def(3)
proof safe
fix pq1 pq2
assume subassms:
‹¬ ?tau a›
‹?steps step2 q ?tau pq1›
‹step2 pq1 a pq2›
‹?steps step2 pq2 ?tau q'›
have ‹pq2 ≠ sink›
using subassms(4) assms(2) not_sink_q' lts.steps_loop
unfolding step2_def by (metis (mono_tags, lifting))
have goal_c: ‹?steps step pq2 ?tau q'›
using subassms(4) not_sink_q' unfolding step2_def
proof (induct rule:lts.steps.induct[OF subassms(4)])
case (1 p af) show ?case using lts.steps.refl by assumption
next
case (2 p af q1 a q)
hence ‹step q1 a q› unfolding step2_def by simp
moreover hence ‹q1 ≠ sink› using assms(2) by blast
ultimately have ‹?steps step p af q1› using 2 unfolding step2_def by auto
thus ?case using `step q1 a q` 2(4) lts.step[of step p af q1 a q] by blast
qed
have goal_b: ‹step pq1 a pq2›
using `pq2 ≠ sink` subassms(3) unfolding step2_def by blast
hence ‹pq1 ≠ sink› using assms(2) by blast
hence goal_a: ‹?steps step q ?tau pq1›
using subassms(4) unfolding step2_def
proof (induct rule:lts.steps.induct[OF subassms(2)])
case (1 p af) show ?case using lts.steps.refl by assumption
next
case (2 p af q1 a q)
hence ‹step q1 a q› unfolding step2_def by simp
moreover hence ‹q1 ≠ sink› using assms(2) by blast
ultimately have ‹?steps step p af q1› using 2 unfolding step2_def by auto
thus ?case using `step q1 a q` 2(4) lts.step[of step p af q1 a q] by blast
qed
thus
‹∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2 ∧ ?steps step pq2 ?tau q'›
using goal_b goal_c by auto
qed
thus ‹∃q'. (p' = sink ∨ R p' q') ∧ (?tau a ⟶ ?steps step q ?tau q') ∧
(¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
∧ ?steps step pq2 ?tau q'))›
using outer_goal_a outer_goal_b by auto
qed
qed
qed
lemma simulation_sink_invariant:
fixes
step sink τ R
defines
‹step2 ≡ λ p1 a p2 . (p1 ≠ sink ∧ a = τ ∧ p2 = sink) ∨ step p1 a p2›
assumes
‹⋀ a p . ¬ step sink a p ∧ ¬ step p a sink›
shows ‹lts_tau.weakly_simulated_by step2 τ p q = lts_tau.weakly_simulated_by step τ p q›
proof (rule)
have sink_sim_min: ‹lts_tau.weak_simulation step2 τ (λ p q. p = sink)›
unfolding lts_tau.weak_simulation_def step2_def using assms(2)
by (meson lts.steps.simps)
define R where ‹R ≡ lts_tau.weakly_simulated_by step2 τ›
have weak_sim_R: ‹lts_tau.weak_simulation step2 τ R›
using lts_tau.weaksim_greatest[of step2 τ] unfolding R_def by blast
have R_contains_inv_tau_closure:
‹R = (λp1 q1. R p1 q1 ∨ lts.steps step2 q1 (lts_tau.tau τ) p1)› unfolding R_def
proof (rule, rule, rule, simp)
fix p q
assume
‹(∃R. lts_tau.weak_simulation step2 τ R ∧ R p q) ∨
(lts.steps step2 q (lts_tau.tau τ) p)›
thus ‹∃R. lts_tau.weak_simulation step2 τ R ∧ R p q›
using weak_sim_R
lts_tau.weak_sim_tau_step[of step2 ‹τ›]
lts_tau.weak_sim_union_cl[of step2 ‹τ›] by blast
qed
assume Rpq: ‹R p q›
have ‹⋀ p' q' q . R p' q' ∧ lts.steps step2 q (lts_tau.tau τ) q' ⟶ R p' q›
using R_contains_inv_tau_closure lts_tau.weak_sim_trans[of step2 ‹τ› _ _ _] R_def assms(2)
by meson
hence closed_R:
‹⋀ p' q' q . (p' = sink ∨ R p' q') ∧ lts.steps step2 q (lts_tau.tau τ) q'
⟶ (p' = sink ∨ R p' q)›
using weak_sim_R sink_sim_min lts_tau.weak_sim_union_cl by blast
have ‹lts_tau.weak_simulation step2 τ (λp q. p = sink ∨ R p q)›
using weak_sim_R sink_sim_min lts_tau.weak_sim_union_cl[of step2 τ] by blast
hence ‹lts_tau.weak_simulation step τ (λp q. p = sink ∨ R p q)›
using simulation_tau_sink_2[of step sink τ R] assms(2) closed_R
unfolding step2_def by blast
thus ‹∃R. lts_tau.weak_simulation step τ R ∧ R p q›
using Rpq weak_sim_R by blast
next
show ‹∃R. lts_tau.weak_simulation step τ R ∧ R p q ⟹
∃R. lts_tau.weak_simulation step2 τ R ∧ R p q›
proof clarify
fix R
assume
‹lts_tau.weak_simulation step τ R›
‹R p q›
hence ‹lts_tau.weak_simulation
(λp1 a p2. p1 ≠ sink ∧ a = τ ∧ p2 = sink ∨ step p1 a p2) τ (λp q. p = sink ∨ R p q)›
using simulation_tau_sink_1[of step sink τ R] assms(2) unfolding step2_def by auto
thus ‹∃R. lts_tau.weak_simulation step2 τ R ∧ R p q›
using `R p q` unfolding step2_def by blast
qed
qed
end