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.thy 3.54 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
section \<open>Fixed Point Algorithm for Coupled Similarity\<close>

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

context lts_tau
begin

definition fp_step :: 
benkeks committed
15
  \<open>'s rel \<Rightarrow> 's rel\<close>
16
  where
benkeks committed
17 18 19 20
  \<open>fp_step R1 \<equiv> { (p,q)\<in>R1.
    (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow> 
       (\<exists> q'. ((p',q')\<in>R1) \<and> (q \<Rightarrow>^a q')))
  \<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }\<close>
21 22

lemma mono_fp_step:
benkeks committed
23
  \<open>mono fp_step\<close>
24
proof (rule, safe)
benkeks committed
25
  fix x y::\<open>'s rel\<close> and p q
26
  assume
benkeks committed
27 28 29
    \<open>x \<subseteq> y\<close>
    \<open>(p, q) \<in> fp_step x\<close>
  thus  \<open>(p, q) \<in> fp_step y\<close>
30 31 32 33 34 35
    unfolding fp_step_def
    by (auto, blast)
qed

lemma fp_fp_step:
  assumes
benkeks committed
36
    \<open>R = fp_step R\<close>
37
  shows
benkeks committed
38
    \<open>coupled_simulation (\<lambda> p q. (p, q) \<in> R)\<close>
39 40 41 42
  using assms unfolding fp_step_def coupled_simulation_def
  by fastforce

lemma gfp_fp_step_subset_gcs:
benkeks committed
43
  shows \<open>(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }\<close>
44 45 46 47
  unfolding gcs_eq_coupled_sim_by[symmetric]
proof clarify
  fix a b
  assume
benkeks committed
48 49
    \<open>(a, b) \<in> gfp fp_step\<close>
  thus \<open>a \<sqsubseteq>cs  b\<close>
50 51 52 53 54
    using fp_fp_step mono_fp_step gfp_unfold by auto
qed

lemma fp_fp_step_gcs:
  assumes
benkeks committed
55
    \<open>R = { (p,q) . greatest_coupled_simulation p q }\<close>
56
  shows
benkeks committed
57
    \<open>fp_step R = R\<close>
58 59 60 61
  unfolding assms
proof safe
  fix p q
  assume
benkeks committed
62 63 64
    \<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
  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>
65
    unfolding fp_step_def by auto
benkeks committed
66 67 68
  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>
69 70 71 72
    using lts_tau.gcs by metis
next
  fix p q
  assume
benkeks committed
73 74 75 76
    \<open>greatest_coupled_simulation p q\<close>
  hence \<open>(p, q) \<in> {(x, y). greatest_coupled_simulation x y} \<and> (\<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>
77
    using gcs_is_coupled_simulation unfolding coupled_simulation_def by blast
benkeks committed
78
  thus \<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
79 80 81
    unfolding fp_step_def by blast
qed

benkeks committed
82
lemma gfp_fp_step_gcs: \<open>gfp fp_step = { (p,q) . greatest_coupled_simulation p q }\<close>
83 84 85 86 87 88 89 90 91
  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
92
    \<open>gfp fp_step = while (\<lambda>R. fp_step R \<noteq> R) fp_step top\<close>
93 94 95
  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
96
  shows \<open>while (\<lambda>R. fp_step R \<noteq> R) fp_step top = { (p,q) . greatest_coupled_simulation p q }\<close>
97 98 99 100 101 102
  using gfp_fp_step_while gfp_fp_step_gcs by blast

end


end