This GitLab instance reached the end of its service life. It won't be possible to create new users or projects.

Please read the deprecation notice for more information concerning the deprecation timeline

Visit migration.git.tu-berlin.de (internal network only) to import your old projects to the new GitLab platform 📥

CS_Fixpoint_Algo_Delay.thy 5.04 KB
Newer Older
1 2
section \<open>Fixed Point Algorithm for Coupled Similarity\<close>

benkeks committed
3 4 5

subsection \<open>The Algorithm\<close>

6 7 8 9 10 11 12 13 14 15 16
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 :: 
benkeks committed
17 18 19 20 21 22 23 24 25 26 27 28
  \<open>'s rel \<Rightarrow> 's rel\<close>
where
  \<open>fp_step R1 \<equiv> { (p,q)\<in>R1.
    (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
      (tau a \<longrightarrow> (p',q)\<in>R1) \<and>
      (\<not>tau a \<longrightarrow> (\<exists> q'. ((p',q')\<in>R1) \<and> (q =\<rhd>a q')))) \<and>
    (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }\<close>

definition fp_compute_cs :: \<open>'s rel\<close>
where \<open>fp_compute_cs \<equiv> while (\<lambda>R. fp_step R \<noteq> R) fp_step top\<close>

subsection \<open>Correctness\<close>
29 30

lemma mono_fp_step:
benkeks committed
31
  \<open>mono fp_step\<close>
32
proof (rule, safe)
benkeks committed
33
  fix x y::\<open>'s rel\<close> and p q
34
  assume
benkeks committed
35 36 37
    \<open>x \<subseteq> y\<close>
    \<open>(p, q) \<in> fp_step x\<close>
  thus  \<open>(p, q) \<in> fp_step y\<close>
38 39 40 41
    unfolding fp_step_def
    by (auto, blast)
qed

benkeks committed
42 43
thm   prod.simps(2)

44 45
lemma fp_fp_step:
  assumes
benkeks committed
46
    \<open>R = fp_step R\<close>
47
  shows
benkeks committed
48 49 50
    \<open>coupled_delay_simulation (\<lambda> p q. (p, q) \<in> R)\<close>
  using assms unfolding fp_step_def coupled_delay_simulation_def delay_simulation_def 
  by (auto, blast, fastforce+)
51 52

lemma gfp_fp_step_subset_gcs:
benkeks committed
53
  shows \<open>(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }\<close>
54 55 56 57
  unfolding  gcs_eq_coupled_sim_by[symmetric] 
proof clarify
  fix a b
  assume
benkeks committed
58 59 60
    \<open>(a, b) \<in> gfp fp_step\<close>
  thus \<open>a \<sqsubseteq>cs  b\<close>
    unfolding coupled_sim_by_eq_coupled_delay_simulation
61 62 63 64 65 66
    using fp_fp_step mono_fp_step gfp_unfold
    by metis
qed

lemma fp_fp_step_gcs:
  assumes
benkeks committed
67
    \<open>R = { (p,q) . greatest_coupled_simulation p q }\<close>
68
  shows
benkeks committed
69
    \<open>fp_step R = R\<close>
70 71 72 73
  unfolding assms
proof safe
  fix p q
  assume
benkeks committed
74 75 76 77 78 79
    \<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
  hence
    \<open>(\<forall>p' a. p \<longmapsto>a  p' \<longrightarrow>
      (tau a \<longrightarrow> greatest_coupled_simulation p' q) \<and>
      (\<not>tau a \<longrightarrow>  (\<exists>q'. greatest_coupled_simulation p' q' \<and> q =\<rhd>a  q'))) \<and>
    (\<exists>q'. q \<longmapsto>* tau  q' \<and> greatest_coupled_simulation q' p)\<close>
80
    unfolding fp_step_def by auto
benkeks committed
81 82 83 84 85 86 87
  hence \<open>(\<forall>p' a. p \<longmapsto>a  p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<Rightarrow>^a  q')) \<and>
    (\<exists>q'. q \<longmapsto>* tau  q' \<and> greatest_coupled_simulation q' p)\<close>
    unfolding fp_step_def using weak_step_delay_implies_weak_tau steps.refl by blast
  hence \<open>(\<forall>p' a. p \<longmapsto>a  p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<Rightarrow>^^a  q')) \<and>
    (\<exists>q'. q \<longmapsto>* tau  q' \<and> greatest_coupled_simulation q' p)\<close>
    using weak_step_tau2_def by simp
  thus \<open>greatest_coupled_simulation p q\<close>
88 89 90 91
    using lts_tau.gcs by metis
next
  fix p q
  assume asm:
benkeks committed
92 93
    \<open>greatest_coupled_simulation p q\<close>
  then have \<open>(p, q) \<in> {(x, y). greatest_coupled_simulation x y}\<close> by blast
94
  moreover from asm have \<open>\<exists> R. R p q \<and> coupled_delay_simulation R\<close>
benkeks committed
95 96 97 98 99 100 101
    unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_coupled_delay_simulation .
  moreover from asm have  \<open>\<forall> p' a. p \<longmapsto>a p' \<and> \<not>tau a \<longrightarrow>
      (\<exists> q'. (greatest_coupled_simulation p' q') \<and> (q =\<rhd>a q'))\<close>
    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  \<open>\<forall> p' a. p \<longmapsto>a p' \<and> tau a \<longrightarrow> greatest_coupled_simulation p' q\<close>
    unfolding  gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_coupled_delay_simulation
102
    by (metis coupled_delay_simulation_def delay_simulation_def)
benkeks committed
103
  moreover have  \<open>(\<exists> q'. q \<longmapsto>*tau q' \<and> (greatest_coupled_simulation q' p))\<close>
104
    using asm gcs_is_coupled_simulation coupled_simulation_implies_coupling by blast
benkeks committed
105
  ultimately show \<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
106 107 108
    unfolding fp_step_def by blast
qed

benkeks committed
109
lemma gfp_fp_step_gcs: \<open>gfp fp_step = { (p,q) . greatest_coupled_simulation p q }\<close>
110 111 112 113 114 115 116 117 118
  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
benkeks committed
119 120
    \<open>gfp fp_step = fp_compute_cs\<close>
  unfolding fp_compute_cs_def
121 122 123
  using gfp_while_lattice[OF mono_fp_step] finite_state_rel Finite_Set.finite_set by blast

theorem coupled_sim_fp_step_while:
benkeks committed
124
  shows \<open>fp_compute_cs = { (p,q) . greatest_coupled_simulation p q }\<close>
125 126 127 128 129
  using gfp_fp_step_while gfp_fp_step_gcs by blast

end

end