# Theory CS_Fixpoint_Algo_Delay

theory CS_Fixpoint_Algo_Delay
imports Coupled_Simulation While_Combinator Finite_Lattice
```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
```