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 to import your old projects to the new GitLab platform 📥

Commit 3a99aa3e by benkeks

Improve Isabelle proofs

parent a6d32189
......@@ -12,74 +12,74 @@ context lts_tau
begin
definition fp_step ::
"'s rel \<Rightarrow> 's rel"
\<open>'s rel \<Rightarrow> 's rel\<close>
where
"fp_step R1 \<equiv> { (p,q)\<in>R1.
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow>
(\<exists> q'. ((p',q')\<in>R1) \<and> (q \<longmapsto>^ a q')))
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }"
\<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>
lemma mono_fp_step:
"mono fp_step"
\<open>mono fp_step\<close>
proof (rule, safe)
fix x y::"'s rel" and p q
fix x y::\<open>'s rel\<close> and p q
assume
"x \<subseteq> y"
"(p, q) \<in> fp_step x"
thus "(p, q) \<in> fp_step y"
\<open>x \<subseteq> y\<close>
\<open>(p, q) \<in> fp_step x\<close>
thus \<open>(p, q) \<in> fp_step y\<close>
unfolding fp_step_def
by (auto, blast)
qed
lemma fp_fp_step:
assumes
"R = fp_step R"
\<open>R = fp_step R\<close>
shows
"coupled_simulation (\<lambda> p q. (p, q) \<in> R)"
\<open>coupled_simulation (\<lambda> p q. (p, q) \<in> R)\<close>
using assms unfolding fp_step_def coupled_simulation_def
by fastforce
lemma gfp_fp_step_subset_gcs:
shows "(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }"
shows \<open>(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }\<close>
unfolding gcs_eq_coupled_sim_by[symmetric]
proof clarify
fix a b
assume
"(a, b) \<in> gfp fp_step"
thus "a \<sqsubseteq>cs b"
\<open>(a, b) \<in> gfp fp_step\<close>
thus \<open>a \<sqsubseteq>cs b\<close>
using fp_fp_step mono_fp_step gfp_unfold by auto
qed
lemma fp_fp_step_gcs:
assumes
"R = { (p,q) . greatest_coupled_simulation p q }"
\<open>R = { (p,q) . greatest_coupled_simulation p q }\<close>
shows
"fp_step R = R"
\<open>fp_step R = R\<close>
unfolding assms
proof safe
fix p q
assume
"(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}"
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)"
\<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>
unfolding fp_step_def by auto
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^^ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)" using weak_step_tau2_def by simp
thus "greatest_coupled_simulation p q"
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>
using lts_tau.gcs by metis
next
fix p q
assume
"greatest_coupled_simulation p q"
hence "(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 \<longmapsto>^ a q')))
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> (greatest_coupled_simulation q' p))"
\<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>
using gcs_is_coupled_simulation unfolding coupled_simulation_def by blast
thus "(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}"
thus \<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
unfolding fp_step_def by blast
qed
lemma gfp_fp_step_gcs: "gfp fp_step = { (p,q) . greatest_coupled_simulation p q }"
lemma gfp_fp_step_gcs: \<open>gfp fp_step = { (p,q) . greatest_coupled_simulation p q }\<close>
using fp_fp_step_gcs gfp_fp_step_subset_gcs
by (simp add: equalityI gfp_upperbound)
......@@ -89,11 +89,11 @@ context lts_tau_finite
begin
lemma gfp_fp_step_while:
shows
"gfp fp_step = while (\<lambda>R. fp_step R \<noteq> R) fp_step top"
\<open>gfp fp_step = while (\<lambda>R. fp_step R \<noteq> R) fp_step top\<close>
using gfp_while_lattice[OF mono_fp_step] finite_state_rel Finite_Set.finite_set by blast
theorem coupled_sim_fp_step_while:
shows "while (\<lambda>R. fp_step R \<noteq> R) fp_step top = { (p,q) . greatest_coupled_simulation p q }"
shows \<open>while (\<lambda>R. fp_step R \<noteq> R) fp_step top = { (p,q) . greatest_coupled_simulation p q }\<close>
using gfp_fp_step_while gfp_fp_step_gcs by blast
end
......
section \<open>Fixed Point Algorithm for Coupled Similarity\<close>
subsection \<open>The Algorithm\<close>
theory CS_Fixpoint_Algo_Delay
imports
Coupled_Simulation
Finite_Weak_Transition_Systems
"~~/src/HOL/Library/While_Combinator"
"~~/src/HOL/Library/Finite_Lattice"
begin
......@@ -12,83 +14,99 @@ context lts_tau
begin
definition fp_step ::
"'s rel \<Rightarrow> 's rel"
where
"fp_step R1 \<equiv> { (p,q)\<in>R1.
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow>
(\<exists> q'. ((p',q')\<in>R1) \<and> (q \<longmapsto>^~ a q')))
\<and> (\<exists> q'. q \<longmapsto>*tau q' \<and> ((q',p)\<in>R1)) }"
\<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>
lemma mono_fp_step:
"mono fp_step"
\<open>mono fp_step\<close>
proof (rule, safe)
fix x y::"'s rel" and p q
fix x y::\<open>'s rel\<close> and p q
assume
"x \<subseteq> y"
"(p, q) \<in> fp_step x"
thus "(p, q) \<in> fp_step y"
\<open>x \<subseteq> y\<close>
\<open>(p, q) \<in> fp_step x\<close>
thus \<open>(p, q) \<in> fp_step y\<close>
unfolding fp_step_def
by (auto, blast)
qed
thm prod.simps(2)
lemma fp_fp_step:
assumes
"R = fp_step R"
\<open>R = fp_step R\<close>
shows
"coupled_delay_simulation (\<lambda> p q. (p, q) \<in> R)"
using assms unfolding fp_step_def coupled_delay_simulation_def delay_simulation_def
by fastforce
\<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+)
lemma gfp_fp_step_subset_gcs:
shows "(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }"
shows \<open>(gfp fp_step) \<subseteq> { (p,q) . greatest_coupled_simulation p q }\<close>
unfolding gcs_eq_coupled_sim_by[symmetric]
proof clarify
fix a b
assume
"(a, b) \<in> gfp fp_step"
thus "a \<sqsubseteq>cs b"
unfolding coupled_sim_by_eq_delay_coupled_simulation
\<open>(a, b) \<in> gfp fp_step\<close>
thus \<open>a \<sqsubseteq>cs b\<close>
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 }"
\<open>R = { (p,q) . greatest_coupled_simulation p q }\<close>
shows
"fp_step R = R"
\<open>fp_step R = R\<close>
unfolding assms
proof safe
fix p q
assume
"(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}"
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^~ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)"
\<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>
unfolding fp_step_def by auto
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)"
unfolding fp_step_def using weak_step_delay_implies_weak_tau by blast
hence "(\<forall>p' a. p \<longmapsto>a p' \<longrightarrow> (\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<longmapsto>^^ a q')) \<and>
(\<exists>q'. q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p)" using weak_step_tau2_def by simp
thus "greatest_coupled_simulation p q"
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>
using lts_tau.gcs by metis
next
fix p q
assume asm:
"greatest_coupled_simulation p q"
then have "(p, q) \<in> {(x, y). greatest_coupled_simulation x y}" by blast
\<open>greatest_coupled_simulation p q\<close>
then have \<open>(p, q) \<in> {(x, y). greatest_coupled_simulation x y}\<close> by blast
moreover from asm have \<open>\<exists> R. R p q \<and> coupled_delay_simulation R\<close>
unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_delay_coupled_simulation .
moreover from asm have "(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow> (\<exists> q'. (greatest_coupled_simulation p' q') \<and> (q \<longmapsto>^~ a q')))"
unfolding gcs_eq_coupled_sim_by[symmetric] coupled_sim_by_eq_delay_coupled_simulation
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
by (metis coupled_delay_simulation_def delay_simulation_def)
moreover have "(\<exists> q'. q \<longmapsto>*tau q' \<and> (greatest_coupled_simulation q' p))"
moreover have \<open>(\<exists> q'. q \<longmapsto>*tau q' \<and> (greatest_coupled_simulation q' p))\<close>
using asm gcs_is_coupled_simulation coupled_simulation_implies_coupling by blast
ultimately show "(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}"
ultimately show \<open>(p, q) \<in> fp_step {(x, y). greatest_coupled_simulation x y}\<close>
unfolding fp_step_def by blast
qed
lemma gfp_fp_step_gcs: "gfp fp_step = { (p,q) . greatest_coupled_simulation p q }"
lemma gfp_fp_step_gcs: \<open>gfp fp_step = { (p,q) . greatest_coupled_simulation p q }\<close>
using fp_fp_step_gcs gfp_fp_step_subset_gcs
by (simp add: equalityI gfp_upperbound)
......@@ -98,14 +116,14 @@ context lts_tau_finite
begin
lemma gfp_fp_step_while:
shows
"gfp fp_step = while (\<lambda>R. fp_step R \<noteq> R) fp_step top"
\<open>gfp fp_step = fp_compute_cs\<close>
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 "while (\<lambda>R. fp_step R \<noteq> R) fp_step top = { (p,q) . greatest_coupled_simulation p q }"
shows \<open>fp_compute_cs = { (p,q) . greatest_coupled_simulation p q }\<close>
using gfp_fp_step_while gfp_fp_step_gcs by blast
end
end
This source diff could not be displayed because it is too large. You can view the blob instead.
section \<open>Preliminaries\<close>
subsection \<open>Some Utilities for Finite Partial Orders\<close>
text \<open>For some reason there seems to be no Isaeblle support for maximal elements in finite regions
of incomplete partial orders (such as the transitive step relation in cycle-compressed transition
systems ;).)\<close>
theory Finite_Partial_Order
imports Main
begin
context preorder
begin
lemma foldl_max_inflation:
\<open>foldl max x0 xs \<le> foldl max x0 (xs @ [x])\<close>
unfolding foldl_append foldl.simps
by (simp add: ord.max_def)
lemma foldl_max_soundness:
shows
\<open>foldl max x0 (x0 # xs) \<in> set (x0 # xs)\<close>
proof (induct xs rule: rev_induct)
case Nil
then show ?case by (auto simp add: max_def)
next
case (snoc x xs)
then show ?case unfolding foldl_append max_def by auto
qed
lemma foldl_max_maximal:
shows
\<open>\<forall> y \<in> set (x0 # xs). foldl max x0 (x0 # xs) \<le> y \<longrightarrow> y \<le> foldl max x0 (x0 # xs)\<close>
proof (induct xs rule: rev_induct)
case Nil
then show ?case by (auto simp add: max_def)
next
case (snoc x xs)
then show ?case unfolding foldl.simps foldl_append
by (metis Un_insert_right append_Nil2 foldl_Cons insert_iff list.simps(15) local.order_refl
local.order_trans ord.max_def set_append snoc.hyps)
qed
end
context order \<comment>\<open>that is: partial order\<close>
begin
lemma finite_max:
fixes q
defines \<open>above_q \<equiv> {q'. q \<le> q'}\<close>
assumes
\<open>finite above_q\<close>
shows
\<open>\<exists> q_max. q_max \<in> above_q \<and> (\<forall> q''\<in> above_q. q_max \<le> q'' \<longrightarrow> q'' = q_max)\<close>
proof -
have \<open>q \<in> above_q\<close> unfolding above_q_def by blast
then obtain above_list where above_list_spec: \<open>set (q#above_list) = above_q\<close>
using \<open>finite above_q\<close> finite_list by auto
define q_max where \<open>q_max \<equiv> foldl max q (q#above_list)\<close>
have \<open>q_max \<in> above_q\<close>
unfolding q_max_def above_list_spec[symmetric] using foldl_max_soundness .
moreover have \<open>\<forall> q'' \<in> above_q. q_max \<le> q'' \<longrightarrow> q'' = q_max\<close>
unfolding q_max_def above_list_spec[symmetric] using foldl_max_maximal antisym by blast
ultimately show ?thesis by blast
qed
end
end
\ No newline at end of file
......@@ -3,11 +3,10 @@ session "Coupled_Simulation" = "HOL" +
theories [quick_and_dirty, document = false]
"~~/src/HOL/Library/While_Combinator"
"~~/src/HOL/Library/Finite_Lattice"
theories [quick_and_dirty]
CS_Fixpoint_Algo
CS_Game
theories
CS_Fixpoint_Algo_Delay
CS_Game_Delay
document_files
"root.tex"
(*"root.bib"*)
"root.bib"
"splncs04.bst"
......@@ -8,53 +8,65 @@ begin
text \<open>Simple games are games where player0 wins all infinite plays.\<close>
locale simple_game =
fixes
game_move :: "'s \<Rightarrow> 's \<Rightarrow> bool" ("_ \<longmapsto>\<heartsuit> _" [70, 70] 80) and
player0_position :: "'s \<Rightarrow> bool" and
game_move :: \<open>'s \<Rightarrow> 's \<Rightarrow> bool\<close> ("_ \<longmapsto>\<heartsuit> _" [70, 70] 80) and
player0_position :: \<open>'s \<Rightarrow> bool\<close> and
initial :: 's
begin
definition player1_position :: "'s \<Rightarrow> bool"
where "player1_position s \<equiv> \<not> player0_position s"
definition player1_position :: \<open>'s \<Rightarrow> bool\<close>
where \<open>player1_position s \<equiv> \<not> player0_position s\<close>
\<comment>\<open>plays (to be precise: play p refixes) are lists. we model them
with the most recent move at the beginning. (for our purpose it's enough to consider finite plays)\<close>
type_synonym ('s2) play = "'s2 list"
type_synonym ('s2) strategy = "'s2 play \<Rightarrow> 's2"
type_synonym ('s2) play = \<open>'s2 list\<close>
type_synonym ('s2) strategy = \<open>'s2 play \<Rightarrow> 's2\<close>
inductive_set plays :: "'s play set" where
"[initial] \<in> plays" |
"p#play \<in> plays \<Longrightarrow> p \<longmapsto>\<heartsuit> p' \<Longrightarrow> p'#p#play \<in> plays"
inductive_set plays :: \<open>'s play set\<close> where
\<open>[initial] \<in> plays\<close> |
\<open>p#play \<in> plays \<Longrightarrow> p \<longmapsto>\<heartsuit> p' \<Longrightarrow> p'#p#play \<in> plays\<close>
\<comment>\<open>plays for a given player 0 strategy\<close>
inductive_set plays_for_strategy :: "'s strategy \<Rightarrow> 's play set" for f where
init: "[initial] \<in> plays_for_strategy f" |
p0move: "n0#play \<in> plays_for_strategy f \<Longrightarrow> player0_position n0 \<Longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play)
\<Longrightarrow> (f (n0#play))#n0#play \<in> plays_for_strategy f" |
p1move: "n1#play \<in> plays_for_strategy f \<Longrightarrow> player1_position n1 \<Longrightarrow> n1 \<longmapsto>\<heartsuit> n1'
\<Longrightarrow> n1'#n1#play \<in> plays_for_strategy f"
inductive_set plays_for_strategy :: \<open>'s strategy \<Rightarrow> 's play set\<close> for f where
init: \<open>[initial] \<in> plays_for_strategy f\<close> |
p0move: \<open>n0#play \<in> plays_for_strategy f \<Longrightarrow> player0_position n0 \<Longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play)
\<Longrightarrow> (f (n0#play))#n0#play \<in> plays_for_strategy f\<close> |
p1move: \<open>n1#play \<in> plays_for_strategy f \<Longrightarrow> player1_position n1 \<Longrightarrow> n1 \<longmapsto>\<heartsuit> n1'
\<Longrightarrow> n1'#n1#play \<in> plays_for_strategy f\<close>
lemma strategy_step:
assumes
\<open>n0 # n1 # rest \<in> plays_for_strategy f\<close>
\<open>player0_position n1\<close>
shows
\<open>f (n1 # rest) = n0\<close>
using assms
by (induct rule: plays_for_strategy.cases, auto simp add: simple_game.player1_position_def)
definition positional_strategy :: \<open>'s strategy \<Rightarrow> bool\<close> where
\<open>positional_strategy f \<equiv> \<forall>r1 r2 n. f (n # r1) = f (n # r2)\<close>
text \<open>a strategy is sound if it only decides on enabled transitions.\<close>
definition sound_strategy :: "'s strategy \<Rightarrow> bool" where
"sound_strategy f \<equiv>
\<forall> n0 play . n0#play \<in> plays_for_strategy f \<and> player0_position n0 \<longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play)"
definition sound_strategy :: \<open>'s strategy \<Rightarrow> bool\<close> where
\<open>sound_strategy f \<equiv>
\<forall> n0 play . n0#play \<in> plays_for_strategy f \<and> player0_position n0 \<longrightarrow> n0 \<longmapsto>\<heartsuit> f (n0#play)\<close>
lemma strategy_plays_subset:
assumes "play \<in> plays_for_strategy f"
shows "play \<in> plays"
assumes \<open>play \<in> plays_for_strategy f\<close>
shows \<open>play \<in> plays\<close>
using assms by (induct rule: plays_for_strategy.induct, auto simp add: plays.intros)
lemma no_empty_plays:
assumes "[] \<in> plays"
shows "False"
assumes \<open>[] \<in> plays\<close>
shows \<open>False\<close>
using assms plays.cases by blast
text \<open>player1 wins a play if the play has reached a deadlock where it's player0's turn\<close>
text"player1 wins a play if the play has reached a deadlock where it's player0's turn"
definition player1_wins :: "'s play \<Rightarrow> bool" where
"player1_wins play \<equiv> player0_position (hd play) \<and> (\<nexists> p' . (hd play) \<longmapsto>\<heartsuit> p')"
definition player1_wins :: \<open>'s play \<Rightarrow> bool\<close> where
\<open>player1_wins play \<equiv> player0_position (hd play) \<and> (\<nexists> p' . (hd play) \<longmapsto>\<heartsuit> p')\<close>
definition player0_winning_strategy :: "'s strategy \<Rightarrow> bool" where
"player0_winning_strategy f \<equiv> (\<forall> play \<in> plays_for_strategy f . \<not> player1_wins play)"
definition player0_winning_strategy :: \<open>'s strategy \<Rightarrow> bool\<close> where
\<open>player0_winning_strategy f \<equiv> (\<forall> play \<in> plays_for_strategy f . \<not> player1_wins play)\<close>
end
......
section \<open>Strong Simulation and Bisimulation\<close>
section \<open>Notions of Equivalence\<close>
subsection \<open>Strong Simulation and Bisimulation\<close>
theory Strong_Relations
imports Transition_Systems
......@@ -8,37 +10,29 @@ context lts
begin
definition simulation ::
"('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
where
"simulation R \<equiv> \<forall> p q. R p q \<longrightarrow>
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow>
(\<exists> q'. R p' q' \<and> (q \<longmapsto> a q')))"
definition simulation_on ::
"('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's set \<Rightarrow> 's set \<Rightarrow> bool"
\<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where
"simulation_on R S1 S2 \<equiv> \<forall> p \<in> S1. \<forall> q \<in> S2. R p q \<longrightarrow>
(\<forall> p' \<in> S1 . \<forall> a . p \<longmapsto> a p' \<longrightarrow>
(\<exists> q' \<in> S2 . R p' q' \<and> (q \<longmapsto> a q')))"
\<open>simulation R \<equiv> \<forall> p q. R p q \<longrightarrow>
(\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
(\<exists> q'. R p' q' \<and> (q \<longmapsto>a q')))\<close>
definition bisimulation ::
"('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
\<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where
"bisimulation R \<equiv> \<forall> p q. R p q \<longrightarrow>
(\<forall> p' a. p \<longmapsto> a p' \<longrightarrow>
(\<exists> q'. R p' q' \<and> (q \<longmapsto> a q'))) \<and>
(\<forall> q' a. q \<longmapsto> a q' \<longrightarrow>
(\<exists> p'. R p' q' \<and> (p \<longmapsto> a p')))"
\<open>bisimulation R \<equiv> \<forall> p q. R p q \<longrightarrow>
(\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
(\<exists> q'. R p' q' \<and> (q \<longmapsto>a q'))) \<and>
(\<forall> q' a. q \<longmapsto>a q' \<longrightarrow>
(\<exists> p'. R p' q' \<and> (p \<longmapsto>a p')))\<close>
lemma bisim_ruleformat:
assumes "bisimulation R"
and "R p q"
shows
"p \<longmapsto> a p' \<Longrightarrow> (\<exists> q'. R p' q' \<and> (q \<longmapsto> a q'))"
"q \<longmapsto> a q' \<Longrightarrow> (\<exists> p'. R p' q' \<and> (p \<longmapsto> a p'))"
assumes \<open>bisimulation R\<close>
and \<open>R p q\<close>
shows
\<open>p \<longmapsto>a p' \<Longrightarrow> (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q'))\<close>
\<open>q \<longmapsto>a q' \<Longrightarrow> (\<exists> p'. R p' q' \<and> (p \<longmapsto>a p'))\<close>
using assms unfolding bisimulation_def by auto
end \<comment>\<open>context lts\<close>
end
section \<open>Transition Systems\<close>
subsection \<open>Labeled Transition Systems\<close>
theory Transition_Systems
imports Main
imports Finite_Partial_Order
begin
locale lts =
fixes
trans :: "'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
trans :: \<open>'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool\<close>
begin
abbreviation step_pred :: "'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool" where
"step_pred p af q \<equiv> \<exists> a. af a \<and> trans p a q"
abbreviation step_pred :: \<open>'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool\<close>
where
\<open>step_pred p af q \<equiv> \<exists> a. af a \<and> trans p a q\<close>
abbreviation step ::
"'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
("_ \<longmapsto>_ _" [70, 70, 70] 80)
\<open>'s \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool\<close>
("_ \<longmapsto>_ _" [70, 70, 70] 80)
where
"p \<longmapsto>a q \<equiv> trans p a q"
inductive steps :: "'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool"
("_ \<longmapsto>* _ _" [70, 70, 70] 80)
\<open>p \<longmapsto>a q \<equiv> trans p a q\<close>
inductive steps :: \<open>'s \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> bool\<close>
("_ \<longmapsto>* _ _" [70, 70, 70] 80)
where
refl: "p \<longmapsto>* af p"
| step: "p \<longmapsto>* af q1 \<Longrightarrow> q1 \<longmapsto> a q \<Longrightarrow> af a \<Longrightarrow> (p \<longmapsto>* af q)"
refl: \<open>p \<longmapsto>* A p\<close> | step: \<open>p \<longmapsto>* A q1 \<Longrightarrow> q1 \<longmapsto>a q \<Longrightarrow> A a \<Longrightarrow> (p \<longmapsto>* A q)\<close>
lemma steps_one_step:
assumes
"p \<longmapsto> a p'"
"A a"
shows
"p \<longmapsto>* A p'"
using steps.step[of p A p a p'] steps.refl[of p A] assms .
\<open>p \<longmapsto>a p'\<close>
\<open>A a\<close>
shows
\<open>p \<longmapsto>* A p'\<close> using steps.step[of p A p a p'] steps.refl[of p A] assms .
lemma steps_concat:
assumes
\<open>p' \<longmapsto>* A p''\<close>
\<open>p \<longmapsto>* A p'\<close>
shows
\<open>p \<longmapsto>* A p''\<close> using assms
proof (induct arbitrary: p)
case (refl p'' A p')
then show ?case by auto
next
case (step p' A p'' a pp p)
hence \<open>p \<longmapsto>* A p''\<close> by simp
show ?case using steps.step[OF `p \<longmapsto>* A p''` step(3,4)] .
qed
lemma steps_left:
assumes
"p \<noteq> p'"
"p \<longmapsto>* A p'"
shows
"\<exists>p'' a . p \<longmapsto> a p'' \<and> A a"
using assms(2,1) by (induct, auto)
\<open>p \<noteq> p'\<close>
\<open>p \<longmapsto>* A p'\<close>
shows
\<open>\<exists>p'' a . p \<longmapsto>a p'' \<and> A a \<and> p'' \<longmapsto>* A p'\<close>
using assms(1)
by (induct rule:steps.induct[OF assms(2)], blast, metis refl steps_concat steps_one_step)
lemma steps_no_step:
assumes
"\<And> a p' . p \<longmapsto> a p' \<Longrightarrow> \<not>A a"
"p \<noteq> p''"
"p \<longmapsto>* A p''"
shows
"False"
using steps_left[OF assms(2,3)] assms(1) by blast
\<open>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> \<not>A a\<close>
\<open>p \<noteq> p''\<close>
\<open>p \<longmapsto>* A p''\<close>
shows
\<open>False\<close>
using steps_left[OF assms(2,3)] assms(1) by blast
lemma steps_no_step_pos:
assumes
"\<And> a p' . p \<longmapsto> a p' \<Longrightarrow> \<not>A a"
"p \<longmapsto>* A p'"
shows
"p = p'"
using assms steps_no_step by blast
\<open>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> \<not>A a\<close>
\<open>p \<longmapsto>* A p'\<close>
shows
\<open>p = p'\<close>
using assms steps_no_step by blast
lemma steps_loop:
assumes
"\<And> a p' . p \<longmapsto> a p' \<Longrightarrow> p = p'"
"p \<noteq> p''"
"p \<longmapsto>* A p''"
shows
"False"
using assms(3,1,2) by (induct, auto)
\<open>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> p = p'\<close>
\<open>p \<noteq> p''\<close>
\<open>p \<longmapsto>* A p''\<close>
shows
\<open>False\<close>
using assms(3,1,2) by (induct, auto)
lemma steps_concat:
assumes
"p' \<longmapsto>* A p''"
"p \<longmapsto>* A p'"
shows
"p \<longmapsto>* A p''"
using assms proof (induct arbitrary: p)
case (refl p'' A p')
then show ?case by auto
next
case (step p' A p'' a pp p)
hence "p \<longmapsto>* A p''" by simp
show ?case using steps.step[OF `p \<longmapsto>* A p''` step(3,4)] .
qed
corollary steps_transp:
\<open>transp (\<lambda> p p'. p \<longmapsto>* A p')\<close>
using steps_concat unfolding transp_def by blast
lemma steps_spec:
assumes
"p \<longmapsto>* A' p'"
"\<And> a . A' a \<Longrightarrow> A a"
shows
"p \<longmapsto>* A p'"
using assms(1,2) proof induct
\<open>p \<longmapsto>* A' p'\<close>
\<open>\<And> a . A' a \<Longrightarrow> A a\<close>
shows
\<open>p \<longmapsto>* A p'\<close> using assms(1,2)
proof induct
case (refl p)
show ?case using steps.refl .
next
case (step p A' pp a pp')
hence "p \<longmapsto>* A pp" by simp
hence \<open>p \<longmapsto>* A pp\<close> by simp
then show ?case using step(3,4,5) steps.step by auto
qed
text\<open>If one can reach only a finite portion of the graph following @{text "\<longmapsto>* A"},
interpretation preorder \<open>(\<lambda> p p'. p \<longmapsto>* A p')\<close> \<open>\<lambda> p p'. p \<longmapsto>* A p' \<and> \<not>(p' \<longmapsto>* A p)\<close>
by (standard, simp, simp add: steps.refl, metis steps_concat)
text\<open>If one can reach only a finite portion of the graph following @{text \<open>\<longmapsto>* A\<close>},
and all cycles are loops, then there must be nodes which are maximal wrt. \<open>\<longmapsto>* A\<close>.\<close>
lemma step_max_deadlock:
fixes A q
assumes
"\<And> r1 r2. r1 \<longmapsto>* A r2 \<and> r2 \<longmapsto>* A r1 \<Longrightarrow> r1 = r2" \<comment>\<open>contracted cycles (anti-symmetry)\<close>
"finite {q'. q \<longmapsto>* A q'}"
"\<forall> q'. q \<longmapsto>* A q' \<longrightarrow> (\<exists>q''. q' \<longmapsto>* A q'' \<and> q' \<noteq> q'')"
shows
antiysmm: \<open>\<And> r1 r2. r1 \<longmapsto>* A r2 \<and> r2 \<longmapsto>* A r1 \<Longrightarrow> r1 = r2\<close> and
finite: \<open>finite {q'. q \<longmapsto>* A q'}\<close> and
no_max: \<open>\<forall> q'. q \<longmapsto>* A q' \<longrightarrow> (\<exists>q''. q' \<longmapsto>* A q'' \<and> q' \<noteq> q'')\<close>
shows
False
using assms
sorry \<comment>\<open>this should be easy to prove if i understood anything about \<open>finite\<close> in isabelle..\<close>
proof -
interpret order \<open>(\<lambda> p p'. p \<longmapsto>* A p')\<close> \<open>\<lambda> p p'. p \<longmapsto>* A p' \<and> \<not>(p' \<longmapsto>* A p)\<close>
by (standard, simp add: assms(1))
show ?thesis using local.finite_max assms local.order_trans mem_Collect_eq by metis
qed
end \<comment>\<open>end of lts\<close>
lemma lts_impl_steps2:
assumes
"lts.steps step1 p1 ap p2"
"\<And> p1 a p2 . step1 p1 a p2 \<and> P p1 a p2 \<Longrightarrow> step2 p1 a p2"
"\<And> p1 a p2 . P p1 a p2"
shows
"lts.steps step2 p1 ap p2"
\<open>lts.steps step1 p1 ap p2\<close>
\<open>\<And> p1 a p2 . step1 p1 a p2 \<and> P p1 a p2 \<Longrightarrow> step2 p1 a p2\<close>
\<open>\<And> p1 a p2 . P p1 a p2\<close>
shows
\<open>lts.steps step2 p1 ap p2\<close>
proof (induct rule: lts.steps.induct[OF assms(1)])
case (1 p af)
show ?case using lts.steps.refl[of step2 p af] by blast
next
case (2 p af q1 a q)
hence "step2 q1 a q" using assms(2,3) by blast
hence \<open>step2 q1 a q\<close> using assms(2,3) by blast
thus ?case using lts.step[OF 2(2) _ 2(4)] by blast
qed
lemma lts_impl_steps:
assumes
"lts.steps step1 p1 ap p2"
"\<And> p1 a p2 . step1 p1 a p2 \<Longrightarrow> step2 p1 a p2"