Theory Weak_Relations

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
  case (greatest_weak_simulation p q)
  then obtain R where ‹weak_simulation R› ‹R p q›
    unfolding weak_simulation_def by blast
  with weak_sim_ruleformat[OF this] show ?case
    unfolding weak_step_tau2_def
    by metis
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) by (simp add: steps.refl)
  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
    ―‹case identical to first case›
    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 . ¬ d ⟼a p ∧ ¬ 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.simps)
  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

lemma weak_sim_word_impl:
  fixes
    p q p' A
  assumes
    ‹weak_simulation R› ‹R p q› ‹p ⇒$ A  p'›
  shows
    ‹∃q'. R p' q' ∧ q ⇒$ A  q'›
using assms(2,3) proof (induct A arbitrary: p q)
  case Nil
  then show ?case
    using assms(1) steps_retain_weak_sim by auto
next
  case (Cons a A)
  then obtain p'' where p''_spec: ‹p ⇒^a p''› ‹p'' ⇒$ A p'› by auto
  with Cons(2) assms(1) obtain q'' where q''_spec: ‹q ⇒^a q''› ‹R p'' q''›
    unfolding weak_sim_weak_premise by blast
  then show ?case using Cons(1) p''_spec(2)
    using weak_step_seq.simps(2) by blast
qed

lemma weak_sim_word_impl_contra:
  assumes
    ‹∀ p q . R p q ⟶
      (∀ p' A. p ⇒$A p' ⟶ (∃ q'. R p' q' ∧ q ⇒$A q'))›
  shows
    ‹weak_simulation R›
proof -
  from assms have
    ‹∀ p q p' A . R p q ⟶ p ⇒$A p' ⟶ (∃ q'. R p' q' ∧ q ⇒$A q')› by blast
  hence ‹∀ p q p' a . R p q ⟶ p ⇒$[a] p' ⟶ (∃ q'. R p' q' ∧ q ⇒$[a] q')› by blast
  thus ?thesis unfolding weak_single_step weak_sim_weak_premise by blast
qed

lemma weak_sim_word:
  ‹weak_simulation R =
    (∀ p q . R p q ⟶
      (∀ p' A. p ⇒$A p' ⟶ (∃ q'. R p' q' ∧ q ⇒$A q')))›
  using weak_sim_word_impl weak_sim_word_impl_contra by blast

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

lemma weak_bisim_taufree_strong:
  assumes
    ‹weak_bisimulation R›
    ‹⋀ p q a. p ⟼ a q ⟹ ¬ tau a›
  shows
    ‹bisimulation R›
  using assms strong_weak_transition_system
  unfolding weak_bisimulation_def bisimulation_def
  by auto

subsection ‹Trace Inclusion›

definition trace_inclusion ::
  ‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
  ‹trace_inclusion R  ≡ ∀ p q p' A . (∀ a ∈ set(A). a ≠ τ) 
  ∧ R p q ∧ p ⇒$ A p' ⟶ (∃ q'. q ⇒$ A q')›

abbreviation weakly_trace_included_by :: ‹'s ⇒ 's ⇒ bool› ("_ ⊑T  _" [60, 60] 65)
  where ‹weakly_trace_included_by p q ≡ ∃ R . trace_inclusion R ∧ R p q›

lemma weak_trace_inlcusion_greatest:
  shows ‹trace_inclusion (λ p q . p ⊑T q)›
  unfolding trace_inclusion_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 ‹Coupled Equivalences›

abbreviation coupling ::
  ‹('s ⇒ 's ⇒ bool) ⇒ bool›
  where ‹coupling R ≡ ∀ p q . R p q ⟶ (∃ q'. q ⟼*tau q' ∧ R q' p)›

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

end ―‹context @{locale lts_tau}›
end