Theory CS_Fixpoint_Algo_Delay

section ‹Fixed Point Algorithm for Coupled Similarity›


subsection ‹The Algorithm›

theory CS_Fixpoint_Algo_Delay
imports
  Coupled_Simulation
  "~~/src/HOL/Library/While_Combinator"
  "~~/src/HOL/Library/Finite_Lattice"
begin

context lts_tau
begin

definition fp_step :: 
  ‹'s rel ⇒ 's rel›
where
  ‹fp_step R1 ≡ { (p,q)∈R1.
    (∀ p' a. p ⟼a p' ⟶
      (tau a ⟶ (p',q)∈R1) ∧
      (¬tau a ⟶ (∃ q'. ((p',q')∈R1) ∧ (q =⊳a q')))) ∧
    (∃ q'. q ⟼*tau q' ∧ ((q',p)∈R1)) }›

definition fp_compute_cs :: ‹'s rel›
where ‹fp_compute_cs ≡ while (λR. fp_step R ≠ R) fp_step top›

subsection ‹Correctness›

lemma mono_fp_step:
  ‹mono fp_step›
proof (rule, safe)
  fix x y::‹'s rel› and p q
  assume
    ‹x ⊆ y›
    ‹(p, q) ∈ fp_step x›
  thus  ‹(p, q) ∈ fp_step y›
    unfolding fp_step_def
    by (auto, blast)
qed

thm   prod.simps(2)

lemma fp_fp_step:
  assumes
    ‹R = fp_step R›
  shows
    ‹coupled_delay_simulation (λ p q. (p, q) ∈ R)›
  using assms unfolding fp_step_def coupled_delay_simulation_def delay_simulation_def 
  by (auto, blast, fastforce+)

lemma gfp_fp_step_subset_gcs:
  shows ‹(gfp fp_step) ⊆ { (p,q) . greatest_coupled_simulation p q }›
  unfolding  gcs_eq_coupled_sim_by[symmetric] 
proof clarify
  fix a b
  assume
    ‹(a, b) ∈ gfp fp_step›
  thus ‹a ⊑cs  b›
    unfolding coupled_sim_by_eq_coupled_delay_simulation
    using fp_fp_step mono_fp_step gfp_unfold
    by metis
qed

lemma fp_fp_step_gcs:
  assumes
    ‹R = { (p,q) . greatest_coupled_simulation p q }›
  shows
    ‹fp_step R = R›
  unfolding assms
proof safe
  fix p q
  assume
    ‹(p, q) ∈ fp_step {(x, y). greatest_coupled_simulation x y}›
  hence
    ‹(∀p' a. p ⟼a  p' ⟶
      (tau a ⟶ greatest_coupled_simulation p' q) ∧
      (¬tau a ⟶  (∃q'. greatest_coupled_simulation p' q' ∧ q =⊳a  q'))) ∧
    (∃q'. q ⟼* tau  q' ∧ greatest_coupled_simulation q' p)›
    unfolding fp_step_def by auto
  hence ‹(∀p' a. p ⟼a  p' ⟶ (∃q'. greatest_coupled_simulation p' q' ∧ q ⇒^a  q')) ∧
    (∃q'. q ⟼* tau  q' ∧ greatest_coupled_simulation q' p)›
    unfolding fp_step_def using weak_step_delay_implies_weak_tau steps.refl by blast
  hence ‹(∀p' a. p ⟼a  p' ⟶ (∃q'. greatest_coupled_simulation p' q' ∧ q ⇒^^a  q')) ∧
    (∃q'. q ⟼* tau  q' ∧ greatest_coupled_simulation q' p)›
    using weak_step_tau2_def by simp
  thus ‹greatest_coupled_simulation p q›
    using lts_tau.gcs by metis
next
  fix p q
  assume asm:
    ‹greatest_coupled_simulation p q›
  then have ‹(p, q) ∈ {(x, y). greatest_coupled_simulation x y}› by blast
  moreover from asm have ‹∃ R. R p q ∧ coupled_delay_simulation R›
    unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_coupled_delay_simulation .
  moreover from asm have  ‹∀ p' a. p ⟼a p' ∧ ¬tau a ⟶
      (∃ q'. (greatest_coupled_simulation p' q') ∧ (q =⊳a q'))›
    unfolding  gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_coupled_delay_simulation
    by (metis coupled_delay_simulation_def delay_simulation_def)
  moreover from asm have  ‹∀ p' a. p ⟼a p' ∧ tau a ⟶ greatest_coupled_simulation p' q›
    unfolding  gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_coupled_delay_simulation
    by (metis coupled_delay_simulation_def delay_simulation_def)
  moreover have  ‹(∃ q'. q ⟼*tau q' ∧ (greatest_coupled_simulation q' p))›
    using asm gcs_is_coupled_simulation coupled_simulation_implies_coupling by blast
  ultimately show ‹(p, q) ∈ fp_step {(x, y). greatest_coupled_simulation x y}›
    unfolding fp_step_def by blast
qed

lemma gfp_fp_step_gcs: ‹gfp fp_step = { (p,q) . greatest_coupled_simulation p q }›
  using fp_fp_step_gcs gfp_fp_step_subset_gcs
  by (simp add: equalityI gfp_upperbound)

end

context lts_tau_finite
begin
lemma gfp_fp_step_while:
  shows
    ‹gfp fp_step = fp_compute_cs›
  unfolding fp_compute_cs_def
  using gfp_while_lattice[OF mono_fp_step] finite_state_rel Finite_Set.finite_set by blast

theorem coupled_sim_fp_step_while:
  shows ‹fp_compute_cs = { (p,q) . greatest_coupled_simulation p q }›
  using gfp_fp_step_while gfp_fp_step_gcs by blast

end

end