Theory MoreCoinductiveList

section ‹Auxiliary Lemmas for Coinductive Lists›

text ‹Some lemmas to allow better reasoning with coinductive lists.›

theory MoreCoinductiveList
imports
Main
Coinductive.Coinductive_List
begin

subsection ‹@{term "lset"}›

lemma lset_lnth: "x ∈ lset xs ⟹ ∃n. lnth xs n = x"
by (induct rule: llist.set_induct, meson lnth_0, meson lnth_Suc_LCons)

lemma lset_lnth_member: "⟦ lset xs ⊆ A; enat n < llength xs ⟧ ⟹ lnth xs n ∈ A"
using contra_subsetD[of "lset xs" A] in_lset_conv_lnth[of _ xs] by blast

lemma lset_nth_member_inf: "⟦ ¬lfinite xs; lset xs ⊆ A ⟧ ⟹ lnth xs n ∈ A"
by (metis contra_subsetD inf_llist_lnth lset_inf_llist rangeI)

lemma lset_intersect_lnth: "lset xs ∩ A ≠ {} ⟹ ∃n. enat n < llength xs ∧ lnth xs n ∈ A"
by (metis disjoint_iff_not_equal in_lset_conv_lnth)

lemma lset_ltake_Suc:
assumes "¬lnull xs" "lnth xs 0 = x" "lset (ltake (enat n) (ltl xs)) ⊆ A"
shows "lset (ltake (enat (Suc n)) xs) ⊆ insert x A"
proof-
have "lset (ltake (eSuc (enat n)) (LCons x (ltl xs))) ⊆ insert x A"
using assms(3) by auto
moreover from assms(1,2) have "LCons x (ltl xs) = xs"
by (metis lnth_0 ltl_simps(2) not_lnull_conv)
ultimately show ?thesis by (simp add: eSuc_enat)
qed

lemma lfinite_lset: "lfinite xs ⟹ ¬lnull xs ⟹ llast xs ∈ lset xs"
proof (induct rule: lfinite_induct)
case (LCons xs)
show ?case proof (cases)
assume *: "¬lnull (ltl xs)"
hence "llast (ltl xs) ∈ lset (ltl xs)" using LCons.hyps(3) by blast
hence "llast (ltl xs) ∈ lset xs" by (simp add: in_lset_ltlD)
thus ?thesis by (metis * LCons.prems lhd_LCons_ltl llast_LCons2)
qed (metis LCons.prems lhd_LCons_ltl llast_LCons llist.set_sel(1))
qed simp

lemma lset_subset: "¬(lset xs ⊆ A) ⟹ ∃n. enat n < llength xs ∧ lnth xs n ∉ A"
by (metis in_lset_conv_lnth subsetI)

subsection ‹@{term "llength"}›

lemma enat_Suc_ltl:
assumes "enat (Suc n) < llength xs"
shows "enat n < llength (ltl xs)"
proof-
from assms have "eSuc (enat n) < llength xs" by (simp add: eSuc_enat)
hence "enat n < epred (llength xs)" using eSuc_le_iff ileI1 by fastforce
thus ?thesis by (simp add: epred_llength)
qed

lemma enat_ltl_Suc: "enat n < llength (ltl xs) ⟹ enat (Suc n) < llength xs"
by (metis eSuc_enat ldrop_ltl leD leI lnull_ldrop)

lemma infinite_small_llength [intro]: "¬lfinite xs ⟹ enat n < llength xs"
using enat_iless lfinite_conv_llength_enat neq_iff by blast

lemma lnull_0_llength: "¬lnull xs ⟹ enat 0 < llength xs"
using zero_enat_def by auto

lemma Suc_llength: "enat (Suc n) < llength xs ⟹ enat n < llength xs"
using dual_order.strict_trans enat_ord_simps(2) by blast

subsection ‹@{term "ltake"}›

lemma ltake_lnth: "ltake n xs = ltake n ys ⟹ enat m < n ⟹ lnth xs m = lnth ys m"
by (metis lnth_ltake)

lemma lset_ltake_prefix [simp]: "n ≤ m ⟹ lset (ltake n xs) ⊆ lset (ltake m xs)"
by (simp add: lprefix_lsetD)

lemma lset_ltake: "(⋀m. m < n ⟹ lnth xs m ∈ A) ⟹ lset (ltake (enat n) xs) ⊆ A"
proof (induct n arbitrary: xs)
case 0
have "ltake (enat 0) xs = LNil" by (simp add: zero_enat_def)
thus ?case by simp
next
case (Suc n)
show ?case proof (cases)
assume "xs ≠ LNil"
then obtain x xs' where xs: "xs = LCons x xs'" by (meson neq_LNil_conv)
{ fix m assume "m < n"
hence "Suc m < Suc n" by simp
hence "lnth xs (Suc m) ∈ A" using Suc.prems by presburger
hence "lnth xs' m ∈ A" using xs by simp
}
hence "lset (ltake (enat n) xs') ⊆ A" using Suc.hyps by blast
moreover have "ltake (enat (Suc n)) xs = LCons x (ltake (enat n) xs')"
using xs ltake_eSuc_LCons[of _ x xs'] by (metis (no_types) eSuc_enat)
moreover have "x ∈ A" using Suc.prems xs by force
ultimately show ?thesis by simp
qed simp
qed

lemma llength_ltake': "enat n < llength xs ⟹ llength (ltake (enat n) xs) = enat n"
by (metis llength_ltake min.strict_order_iff)

lemma llast_ltake:
assumes "enat (Suc n) < llength xs"
shows "llast (ltake (enat (Suc n)) xs) = lnth xs n" (is "llast ?A = _")
unfolding llast_def using llength_ltake'[OF assms] by (auto simp add: lnth_ltake)

lemma lset_ltake_ltl: "lset (ltake (enat n) (ltl xs)) ⊆ lset (ltake (enat (Suc n)) xs)"
proof (cases)
assume "¬lnull xs"
then obtain v0 where "xs = LCons v0 (ltl xs)" by (metis lhd_LCons_ltl)
hence "ltake (eSuc (enat n)) xs = LCons v0 (ltake (enat n) (ltl xs))"
by (metis ltake_eSuc_LCons)
hence "lset (ltake (enat (Suc n)) xs) = lset (LCons v0 (ltake (enat n) (ltl xs)))"
by (simp add: eSuc_enat)
thus ?thesis using lset_LCons[of v0 "ltake (enat n) (ltl xs)"] by blast
qed (simp add: lnull_def)

subsection ‹@{term "ldropn"}›

lemma ltl_ldrop: "⟦ ⋀xs. P xs ⟹ P (ltl xs); P xs ⟧ ⟹ P (ldropn n xs)"
unfolding ldropn_def by (induct n) simp_all

subsection ‹@{term "lfinite"}›

lemma lfinite_drop_set: "lfinite xs ⟹ ∃n. v ∉ lset (ldrop n xs)"
by (metis ldrop_inf lmember_code(1) lset_lmember)

lemma index_infinite_set:
"⟦ ¬lfinite x; lnth x m = y; ⋀i. lnth x i = y ⟹ (∃m > i. lnth x m = y) ⟧ ⟹ y ∈ lset (ldropn n x)"
proof (induct n arbitrary: x m)
case 0 thus ?case using lset_nth_member_inf by auto
next
case (Suc n)
obtain a xs where x: "x = LCons a xs" by (meson Suc.prems(1) lnull_imp_lfinite not_lnull_conv)
obtain j where j: "j > m" "lnth x j = y" using Suc.prems(2,3) by blast
have "lnth xs (j - 1) = y" by (metis lnth_LCons' j(1,2) not_less0 x)
moreover {
fix i assume "lnth xs i = y"
hence "lnth x (Suc i) = y" by (simp add: x)
hence "∃j>i. lnth xs j = y" by (metis Suc.prems(3) Suc_lessE lnth_Suc_LCons x)
}
ultimately show ?case using Suc.hyps Suc.prems(1) x by auto
qed

subsection ‹@{term "lmap"}›

lemma lnth_lmap_ldropn:
"enat n < llength xs ⟹ lnth (lmap f (ldropn n xs)) 0 = lnth (lmap f xs) n"
by (simp add: lhd_ldropn lnth_0_conv_lhd)

lemma lnth_lmap_ldropn_Suc:
"enat (Suc n) < llength xs ⟹ lnth (lmap f (ldropn n xs)) (Suc 0) = lnth (lmap f xs) (Suc n)"
by (metis (no_types, lifting) Suc_llength ldropn_ltl leD llist.map_disc_iff lnth_lmap_ldropn
lnth_ltl lnull_ldropn ltl_ldropn ltl_lmap)

subsection ‹Notation›

text ‹We introduce the notation \$to denote @{term "lnth"}.› notation lnth (infix "$" 61)

end


Theory ParityGame

section ‹Parity Games›

theory ParityGame
imports
Main
MoreCoinductiveList
begin

subsection ‹Basic definitions›

text ‹@{typ "'a"} is the node type.  Edges are pairs of nodes.›
type_synonym 'a Edge = "'a × 'a"

text ‹A path is a possibly infinite list of nodes.›
type_synonym 'a Path = "'a llist"

subsection ‹Graphs›

text ‹
We define graphs as a locale over a record.
The record contains nodes (AKA vertices) and edges.
The locale adds the assumption that the edges are pairs of nodes.
›

record 'a Graph =
verts :: "'a set" ("Vı")
arcs :: "'a Edge set" ("Eı")
abbreviation is_arc :: "('a, 'b) Graph_scheme ⇒ 'a ⇒ 'a ⇒ bool" (infixl "→ı" 60) where
"v →⇘G⇙ w ≡ (v,w) ∈ E⇘G⇙"

locale Digraph =
fixes G (structure)
assumes valid_edge_set: "E ⊆ V × V"
begin
lemma edges_are_in_V [intro]: "v→w ⟹ v ∈ V" "v→w ⟹ w ∈ V" using valid_edge_set by blast+

text ‹A node without successors is a \emph{deadend}.›
abbreviation deadend :: "'a ⇒ bool" where "deadend v ≡ ¬(∃w ∈ V. v → w)"

subsection ‹Valid Paths›

text ‹
We say that a path is \emph{valid} if it is empty or if it starts in @{term V} and walks along edges.
›
coinductive valid_path :: "'a Path ⇒ bool" where
valid_path_base: "valid_path LNil"
| valid_path_base': "v ∈ V ⟹ valid_path (LCons v LNil)"
| valid_path_cons: "⟦ v ∈ V; w ∈ V; v→w; valid_path Ps; ¬lnull Ps; lhd Ps = w ⟧
⟹ valid_path (LCons v Ps)"

inductive_simps valid_path_cons_simp: "valid_path (LCons x xs)"

lemma valid_path_ltl': "valid_path (LCons v Ps) ⟹ valid_path Ps"
using valid_path.simps by blast
lemma valid_path_ltl: "valid_path P ⟹ valid_path (ltl P)"
by (metis llist.exhaust_sel ltl_simps(1) valid_path_ltl')
lemma valid_path_drop: "valid_path P ⟹ valid_path (ldropn n P)"
by (simp add: valid_path_ltl ltl_ldrop)

lemma valid_path_in_V: assumes "valid_path P" shows "lset P ⊆ V" proof
fix x assume "x ∈ lset P" thus "x ∈ V"
using assms by (induct rule: llist.set_induct) (auto intro: valid_path.cases)
qed
lemma valid_path_finite_in_V: "⟦ valid_path P; enat n < llength P ⟧ ⟹ P $n ∈ V" using valid_path_in_V lset_lnth_member by blast lemma valid_path_edges': "valid_path (LCons v (LCons w Ps)) ⟹ v→w" using valid_path.cases by fastforce lemma valid_path_edges: assumes "valid_path P" "enat (Suc n) < llength P" shows "P$ n → P $Suc n" proof- define P' where "P' = ldropn n P" have "enat n < llength P" using assms(2) enat_ord_simps(2) less_trans by blast hence "P'$ 0 = P $n" by (simp add: P'_def) moreover have "P'$ Suc 0 = P $Suc n" by (metis One_nat_def P'_def Suc_eq_plus1 add.commute assms(2) lnth_ldropn) ultimately have "∃Ps. P' = LCons (P$ n) (LCons (P $Suc n) Ps)" by (metis P'_def ‹enat n < llength P› assms(2) ldropn_Suc_conv_ldropn) moreover have "valid_path P'" by (simp add: P'_def assms(1) valid_path_drop) ultimately show ?thesis using valid_path_edges' by blast qed lemma valid_path_coinduct [consumes 1, case_names base step, coinduct pred: valid_path]: assumes major: "Q P" and base: "⋀v P. Q (LCons v LNil) ⟹ v ∈ V" and step: "⋀v w P. Q (LCons v (LCons w P)) ⟹ v→w ∧ (Q (LCons w P) ∨ valid_path (LCons w P))" shows "valid_path P" using major proof (coinduction arbitrary: P) case valid_path { assume "P ≠ LNil" "¬(∃v. P = LCons v LNil ∧ v ∈ V)" then obtain v w P' where "P = LCons v (LCons w P')" using neq_LNil_conv base valid_path by metis hence ?case using step valid_path by auto } thus ?case by blast qed lemma valid_path_no_deadends: "⟦ valid_path P; enat (Suc i) < llength P ⟧ ⟹ ¬deadend (P$ i)"
using valid_path_edges by blast

lemma valid_path_ends_on_deadend:
"⟦ valid_path P; enat i < llength P; deadend (P $i) ⟧ ⟹ enat (Suc i) = llength P" using valid_path_no_deadends by (metis enat_iless enat_ord_simps(2) neq_iff not_less_eq) lemma valid_path_prefix: "⟦ valid_path P; lprefix P' P ⟧ ⟹ valid_path P'" proof (coinduction arbitrary: P' P) case (step v w P'' P' P) then obtain Ps where Ps: "LCons v (LCons w Ps) = P" by (metis LCons_lprefix_conv) hence "valid_path (LCons w Ps)" using valid_path_ltl' step(2) by blast moreover have "lprefix (LCons w P'') (LCons w Ps)" using Ps step(1,3) by auto ultimately show ?case using Ps step(2) valid_path_edges' by blast qed (metis LCons_lprefix_conv valid_path_cons_simp) lemma valid_path_lappend: assumes "valid_path P" "valid_path P'" "⟦ ¬lnull P; ¬lnull P' ⟧ ⟹ llast P→lhd P'" shows "valid_path (lappend P P')" proof (cases, cases) assume "¬lnull P" "¬lnull P'" thus ?thesis using assms proof (coinduction arbitrary: P' P) case (step v w P'' P' P) show ?case proof (cases) assume "lnull (ltl P)" thus ?case using step(1,2,3,5,6) by (metis lhd_LCons lhd_LCons_ltl lhd_lappend llast_singleton llist.collapse(1) ltl_lappend ltl_simps(2)) next assume "¬lnull (ltl P)" moreover have "ltl (lappend P P') = lappend (ltl P) P'" using step(2) by simp ultimately show ?case using step by (metis (no_types, lifting) lhd_LCons lhd_LCons_ltl lhd_lappend llast_LCons ltl_simps(2) valid_path_edges' valid_path_ltl) qed qed (metis llist.disc(1) lnull_lappend ltl_lappend ltl_simps(2)) qed (simp_all add: assms(1,2) lappend_lnull1 lappend_lnull2) text ‹A valid path is still valid in a supergame.› lemma valid_path_supergame: assumes "valid_path P" and G': "Digraph G'" "V ⊆ V⇘G'⇙" "E ⊆ E⇘G'⇙" shows "Digraph.valid_path G' P" using ‹valid_path P› proof (coinduction arbitrary: P rule: Digraph.valid_path_coinduct[OF G'(1), case_names base step]) case base thus ?case using G'(2) valid_path_cons_simp by auto qed (meson G'(3) subset_eq valid_path_edges' valid_path_ltl') subsection ‹Maximal Paths› text ‹ We say that a path is \emph{maximal} if it is empty or if it ends in a deadend. › coinductive maximal_path where maximal_path_base: "maximal_path LNil" | maximal_path_base': "deadend v ⟹ maximal_path (LCons v LNil)" | maximal_path_cons: "¬lnull Ps ⟹ maximal_path Ps ⟹ maximal_path (LCons v Ps)" lemma maximal_no_deadend: "maximal_path (LCons v Ps) ⟹ ¬deadend v ⟹ ¬lnull Ps" by (metis lhd_LCons llist.distinct(1) ltl_simps(2) maximal_path.simps) lemma maximal_ltl: "maximal_path P ⟹ maximal_path (ltl P)" by (metis ltl_simps(1) ltl_simps(2) maximal_path.simps) lemma maximal_drop: "maximal_path P ⟹ maximal_path (ldropn n P)" by (simp add: maximal_ltl ltl_ldrop) lemma maximal_path_lappend: assumes "¬lnull P'" "maximal_path P'" shows "maximal_path (lappend P P')" proof (cases) assume "¬lnull P" thus ?thesis using assms proof (coinduction arbitrary: P' P rule: maximal_path.coinduct) case (maximal_path P' P) let ?P = "lappend P P'" show ?case proof (cases "?P = LNil ∨ (∃v. ?P = LCons v LNil ∧ deadend v)") case False then obtain Ps v where P: "?P = LCons v Ps" by (meson neq_LNil_conv) hence "Ps = lappend (ltl P) P'" by (simp add: lappend_ltl maximal_path(1)) hence "∃Ps1 P'. Ps = lappend Ps1 P' ∧ ¬lnull P' ∧ maximal_path P'" using maximal_path(2) maximal_path(3) by auto thus ?thesis using P lappend_lnull1 by fastforce qed blast qed qed (simp add: assms(2) lappend_lnull1[of P P']) lemma maximal_ends_on_deadend: assumes "maximal_path P" "lfinite P" "¬lnull P" shows "deadend (llast P)" proof- from ‹lfinite P› ‹¬lnull P› obtain n where n: "llength P = enat (Suc n)" by (metis enat_ord_simps(2) gr0_implies_Suc lfinite_llength_enat lnull_0_llength) define P' where "P' = ldropn n P" hence "maximal_path P'" using assms(1) maximal_drop by blast thus ?thesis proof (cases rule: maximal_path.cases) case (maximal_path_base' v) hence "deadend (llast P')" unfolding P'_def by simp thus ?thesis unfolding P'_def using llast_ldropn[of n P] n by (metis P'_def ldropn_eq_LConsD local.maximal_path_base'(1)) next case (maximal_path_cons P'' v) hence "ldropn (Suc n) P = P''" unfolding P'_def by (metis ldrop_eSuc_ltl ltl_ldropn ltl_simps(2)) thus ?thesis using n maximal_path_cons(2) by auto qed (simp add: P'_def n ldropn_eq_LNil) qed lemma maximal_ends_on_deadend': "⟦ lfinite P; deadend (llast P) ⟧ ⟹ maximal_path P" proof (coinduction arbitrary: P rule: maximal_path.coinduct) case (maximal_path P) show ?case proof (cases) assume "P ≠ LNil" then obtain v P' where P': "P = LCons v P'" by (meson neq_LNil_conv) show ?thesis proof (cases) assume "P' = LNil" thus ?thesis using P' maximal_path(2) by auto qed (metis P' lfinite_LCons llast_LCons llist.collapse(1) maximal_path(1,2)) qed simp qed lemma infinite_path_is_maximal: "⟦ valid_path P; ¬lfinite P ⟧ ⟹ maximal_path P" by (coinduction arbitrary: P rule: maximal_path.coinduct) (cases rule: valid_path.cases, auto) end ― ‹locale Digraph› subsection ‹Parity Games› text ‹Parity games are games played by two players, called \Even and \Odd.› datatype Player = Even | Odd abbreviation "other_player p ≡ (if p = Even then Odd else Even)" notation other_player ("(_**)" [1000] 1000) lemma other_other_player [simp]: "p**** = p" using Player.exhaust by auto text ‹ A parity game is tuple$(V,E,V_0,\omega)$, where$(V,E)$is a graph,$V_0 \subseteq V$and @{term ω} is a function from$V \to \mathbb{N}$with finite image. › record 'a ParityGame = "'a Graph" + player0 :: "'a set" ("V0ı") priority :: "'a ⇒ nat" ("ωı") locale ParityGame = Digraph G for G :: "('a, 'b) ParityGame_scheme" (structure) + assumes valid_player0_set: "V0 ⊆ V" and priorities_finite: "finite (ω  V)" begin text ‹‹VV p› is the set of nodes belonging to player @{term p}.› abbreviation VV :: "Player ⇒ 'a set" where "VV p ≡ (if p = Even then V0 else V - V0)" lemma VVp_to_V [intro]: "v ∈ VV p ⟹ v ∈ V" using valid_player0_set by (cases p) auto lemma VV_impl1: "v ∈ VV p ⟹ v ∉ VV p**" by auto lemma VV_impl2: "v ∈ VV p** ⟹ v ∉ VV p" by auto lemma VV_equivalence [iff]: "v ∈ V ⟹ v ∉ VV p ⟷ v ∈ VV p**" by auto lemma VV_cases [consumes 1]: "⟦ v ∈ V ; v ∈ VV p ⟹ P ; v ∈ VV p** ⟹ P ⟧ ⟹ P" by auto subsection ‹Sets of Deadends› definition "deadends p ≡ {v ∈ VV p. deadend v}" lemma deadends_in_V: "deadends p ⊆ V" unfolding deadends_def by blast subsection ‹Subgames› text ‹We define a subgame by restricting the set of nodes to a given subset.› definition subgame where "subgame V' ≡ G⦇ verts := V ∩ V', arcs := E ∩ (V' × V'), player0 := V0 ∩ V' ⦈" lemma subgame_V [simp]: "V⇘subgame V'⇙ ⊆ V" and subgame_E [simp]: "E⇘subgame V'⇙ ⊆ E" and subgame_ω: "ω⇘subgame V'⇙ = ω" unfolding subgame_def by simp_all lemma assumes "V' ⊆ V" shows subgame_V' [simp]: "V⇘subgame V'⇙ = V'" and subgame_E' [simp]: "E⇘subgame V'⇙ = E ∩ (V⇘subgame V'⇙ × V⇘subgame V'⇙)" unfolding subgame_def using assms by auto lemma subgame_VV [simp]: "ParityGame.VV (subgame V') p = V' ∩ VV p" proof- have "ParityGame.VV (subgame V') Even = V' ∩ VV Even" unfolding subgame_def by auto moreover have "ParityGame.VV (subgame V') Odd = V' ∩ VV Odd" proof- have "V' ∩ V - (V0 ∩ V') = V' ∩ V ∩ (V - V0)" by blast thus ?thesis unfolding subgame_def by auto qed ultimately show ?thesis by simp qed corollary subgame_VV_subset [simp]: "ParityGame.VV (subgame V') p ⊆ VV p" by simp lemma subgame_finite [simp]: "finite (ω⇘subgame V'⇙  V⇘subgame V'⇙)" proof- have "finite (ω  V⇘subgame V'⇙)" using subgame_V priorities_finite by (meson finite_subset image_mono) thus ?thesis by (simp add: subgame_def) qed lemma subgame_ω_subset [simp]: "ω⇘subgame V'⇙  V⇘subgame V'⇙ ⊆ ω  V" by (simp add: image_mono subgame_ω) lemma subgame_Digraph: "Digraph (subgame V')" by (unfold_locales) (auto simp add: subgame_def) lemma subgame_ParityGame: shows "ParityGame (subgame V')" proof (unfold_locales) show "E⇘subgame V'⇙ ⊆ V⇘subgame V'⇙ × V⇘subgame V'⇙" using subgame_Digraph[unfolded Digraph_def] . show "V0⇘subgame V'⇙ ⊆ V⇘subgame V'⇙" unfolding subgame_def using valid_player0_set by auto show "finite (ω⇘subgame V'⇙  V⇘subgame V'⇙)" by simp qed lemma subgame_valid_path: assumes P: "valid_path P" "lset P ⊆ V'" shows "Digraph.valid_path (subgame V') P" proof- have "lset P ⊆ V" using P(1) valid_path_in_V by blast hence "lset P ⊆ V⇘subgame V'⇙" unfolding subgame_def using P(2) by auto with P(1) show ?thesis proof (coinduction arbitrary: P rule: Digraph.valid_path.coinduct[OF subgame_Digraph, case_names IH]) case IH thus ?case proof (cases rule: valid_path.cases) case (valid_path_cons v w Ps) moreover hence "v ∈ V⇘subgame V'⇙" "w ∈ V⇘subgame V'⇙" using IH(2) by auto moreover hence "v →⇘subgame V'⇙ w" using local.valid_path_cons(4) subgame_def by auto moreover have "valid_path Ps" using IH(1) valid_path_ltl' local.valid_path_cons(1) by blast ultimately show ?thesis using IH(2) by auto qed auto qed qed lemma subgame_maximal_path: assumes V': "V' ⊆ V" and P: "maximal_path P" "lset P ⊆ V'" shows "Digraph.maximal_path (subgame V') P" proof- have "lset P ⊆ V⇘subgame V'⇙" unfolding subgame_def using P(2) V' by auto with P(1) V' show ?thesis by (coinduction arbitrary: P rule: Digraph.maximal_path.coinduct[OF subgame_Digraph]) (cases rule: maximal_path.cases, auto) qed subsection ‹Priorities Occurring Infinitely Often› text ‹ The set of priorities that occur infinitely often on a given path. We need this to define the winning condition of parity games. › definition path_inf_priorities :: "'a Path ⇒ nat set" where "path_inf_priorities P ≡ {k. ∀n. k ∈ lset (ldropn n (lmap ω P))}" text ‹ Because @{term ω} is image-finite, by the pigeon-hole principle every infinite path has at least one priority that occurs infinitely often. › lemma path_inf_priorities_is_nonempty: assumes P: "valid_path P" "¬lfinite P" shows "∃k. k ∈ path_inf_priorities P" proof- text ‹Define a map from indices to priorities on the path.› define f where "f i = ω (P$ i)" for i
have "range f ⊆ ω  V" unfolding f_def
using valid_path_in_V[OF P(1)] lset_nth_member_inf[OF P(2)]
by blast
hence "finite (range f)"
using priorities_finite finite_subset by blast
then obtain n0 where n0: "¬(finite {n. f n = f n0})"
using pigeonhole_infinite[of UNIV f] by auto
define k where "k = f n0"
text ‹The priority @{term k} occurs infinitely often.›
have "lmap ω P $n0 = k" unfolding f_def k_def using assms(2) by (simp add: infinite_small_llength) moreover { fix n assume "lmap ω P$ n = k"
have "∃n' > n. f n' = k" unfolding k_def using n0 infinite_nat_iff_unbounded by auto
hence "∃n' > n. lmap ω P $n' = k" unfolding f_def using assms(2) by (simp add: infinite_small_llength) } ultimately have "∀n. k ∈ lset (ldropn n (lmap ω P))" using index_infinite_set[of "lmap ω P" n0 k] P(2) lfinite_lmap by blast thus ?thesis unfolding path_inf_priorities_def by blast qed lemma path_inf_priorities_at_least_min_prio: assumes P: "valid_path P" and a: "a ∈ path_inf_priorities P" shows "Min (ω  V) ≤ a" proof- have "a ∈ lset (ldropn 0 (lmap ω P))" using a unfolding path_inf_priorities_def by blast hence "a ∈ ω  lset P" by simp thus ?thesis using P valid_path_in_V priorities_finite Min_le by blast qed lemma path_inf_priorities_LCons: "path_inf_priorities P = path_inf_priorities (LCons v P)" (is "?A = ?B") proof show "?A ⊆ ?B" proof fix a assume "a ∈ ?A" hence "∀n. a ∈ lset (ldropn n (lmap ω (LCons v P)))" unfolding path_inf_priorities_def using in_lset_ltlD[of a] by (simp add: ltl_ldropn) thus "a ∈ ?B" unfolding path_inf_priorities_def by blast qed next show "?B ⊆ ?A" proof fix a assume "a ∈ ?B" hence "∀n. a ∈ lset (ldropn (Suc n) (lmap ω (LCons v P)))" unfolding path_inf_priorities_def by blast thus "a ∈ ?A" unfolding path_inf_priorities_def by simp qed qed corollary path_inf_priorities_ltl: "path_inf_priorities P = path_inf_priorities (ltl P)" by (metis llist.exhaust ltl_simps path_inf_priorities_LCons) subsection ‹Winning Condition› text ‹ Let$G = (V,E,V_0,\omega)$be a parity game. An infinite path$v_0,v_1,\ldots$in$G$is winning for player \Even (\Odd) if the minimum priority occurring infinitely often is even (odd). A finite path is winning for player @{term p} iff the last node on the path belongs to the other player. Empty paths are irrelevant, but it is useful to assign a fixed winner to them in order to get simpler lemmas. › abbreviation "winning_priority p ≡ (if p = Even then even else odd)" definition winning_path :: "Player ⇒ 'a Path ⇒ bool" where "winning_path p P ≡ (¬lfinite P ∧ (∃a ∈ path_inf_priorities P. (∀b ∈ path_inf_priorities P. a ≤ b) ∧ winning_priority p a)) ∨ (¬lnull P ∧ lfinite P ∧ llast P ∈ VV p**) ∨ (lnull P ∧ p = Even)" text ‹Every path has a unique winner.› lemma paths_are_winning_for_one_player: assumes "valid_path P" shows "winning_path p P ⟷ ¬winning_path p** P" proof (cases) assume "¬lnull P" show ?thesis proof (cases) assume "lfinite P" thus ?thesis using assms lfinite_lset valid_path_in_V unfolding winning_path_def by auto next assume "¬lfinite P" then obtain a where "a ∈ path_inf_priorities P" "⋀b. b < a ⟹ b ∉ path_inf_priorities P" using assms ex_least_nat_le[of "λa. a ∈ path_inf_priorities P"] path_inf_priorities_is_nonempty by blast hence "∀q. winning_priority q a ⟷ winning_path q P" unfolding winning_path_def using ‹¬lnull P› ‹¬lfinite P› by (metis le_antisym not_le) moreover have "∀q. winning_priority p q ⟷ ¬winning_priority p** q" by simp ultimately show ?thesis by blast qed qed (simp add: winning_path_def) lemma winning_path_ltl: assumes P: "winning_path p P" "¬lnull P" "¬lnull (ltl P)" shows "winning_path p (ltl P)" proof (cases) assume "lfinite P" moreover have "llast P = llast (ltl P)" using P(2,3) by (metis llast_LCons2 ltl_simps(2) not_lnull_conv) ultimately show ?thesis using P by (simp add: winning_path_def) next assume "¬lfinite P" thus ?thesis using winning_path_def path_inf_priorities_ltl P(1,2) by auto qed corollary winning_path_drop: assumes "winning_path p P" "enat n < llength P" shows "winning_path p (ldropn n P)" using assms proof (induct n) case (Suc n) hence "winning_path p (ldropn n P)" using dual_order.strict_trans enat_ord_simps(2) by blast moreover have "ltl (ldropn n P) = ldropn (Suc n) P" by (simp add: ldrop_eSuc_ltl ltl_ldropn) moreover hence "¬lnull (ldropn n P)" using Suc.prems(2) by (metis leD lnull_ldropn lnull_ltlI) ultimately show ?case using winning_path_ltl[of p "ldropn n P"] Suc.prems(2) by auto qed simp corollary winning_path_drop_add: assumes "valid_path P" "winning_path p (ldropn n P)" "enat n < llength P" shows "winning_path p P" using assms paths_are_winning_for_one_player valid_path_drop winning_path_drop by blast lemma winning_path_LCons: assumes P: "winning_path p P" "¬lnull P" shows "winning_path p (LCons v P)" proof (cases) assume "lfinite P" moreover have "llast P = llast (LCons v P)" using P(2) by (metis llast_LCons2 not_lnull_conv) ultimately show ?thesis using P unfolding winning_path_def by simp next assume "¬lfinite P" thus ?thesis using P path_inf_priorities_LCons unfolding winning_path_def by simp qed lemma winning_path_supergame: assumes "winning_path p P" and G': "ParityGame G'" "VV p** ⊆ ParityGame.VV G' p**" "ω = ω⇘G'⇙" shows "ParityGame.winning_path G' p P" proof- interpret G': ParityGame G' using G'(1) . have "⟦ lfinite P; ¬lnull P ⟧ ⟹ llast P ∈ G'.VV p**" and "lnull P ⟹ p = Even" using assms(1) unfolding winning_path_def using G'(2) by auto thus ?thesis unfolding G'.winning_path_def using lnull_imp_lfinite assms(1) unfolding winning_path_def path_inf_priorities_def G'.path_inf_priorities_def G'(3) by blast qed end ― ‹locale ParityGame› subsection ‹Valid Maximal Paths› text ‹Define a locale for valid maximal paths, because we need them often.› locale vm_path = ParityGame + fixes P v0 assumes P_not_null [simp]: "¬lnull P" and P_valid [simp]: "valid_path P" and P_maximal [simp]: "maximal_path P" and P_v0 [simp]: "lhd P = v0" begin lemma P_LCons: "P = LCons v0 (ltl P)" using lhd_LCons_ltl[OF P_not_null] by simp lemma P_len [simp]: "enat 0 < llength P" by (simp add: lnull_0_llength) lemma P_0 [simp]: "P$ 0 = v0" by (simp add: lnth_0_conv_lhd)
lemma P_lnth_Suc: "P $Suc n = ltl P$ n" by (simp add: lnth_ltl)
lemma P_no_deadends: "enat (Suc n) < llength P ⟹ ¬deadend (P $n)" using valid_path_no_deadends by simp lemma P_no_deadend_v0: "¬lnull (ltl P) ⟹ ¬deadend v0" by (metis P_LCons P_valid edges_are_in_V(2) not_lnull_conv valid_path_edges') lemma P_no_deadend_v0_llength: "enat (Suc n) < llength P ⟹ ¬deadend v0" by (metis P_0 P_len P_valid enat_ord_simps(2) not_less_eq valid_path_ends_on_deadend zero_less_Suc) lemma P_ends_on_deadend: "⟦ enat n < llength P; deadend (P$ n) ⟧ ⟹ enat (Suc n) = llength P"
using P_valid valid_path_ends_on_deadend by blast

lemma P_lnull_ltl_deadend_v0: "lnull (ltl P) ⟹ deadend v0"
using P_LCons maximal_no_deadend by force
lemma P_lnull_ltl_LCons: "lnull (ltl P) ⟹ P = LCons v0 LNil"
using P_LCons lnull_def by metis
lemma P_deadend_v0_LCons: "deadend v0 ⟹ P = LCons v0 LNil"
using P_lnull_ltl_LCons P_no_deadend_v0 by blast

lemma Ptl_valid [simp]: "valid_path (ltl P)" using valid_path_ltl by auto
lemma Ptl_maximal [simp]: "maximal_path (ltl P)" using maximal_ltl by auto

lemma Pdrop_valid [simp]: "valid_path (ldropn n P)" using valid_path_drop by auto
lemma Pdrop_maximal [simp]: "maximal_path (ldropn n P)" using maximal_drop by auto

lemma prefix_valid [simp]: "valid_path (ltake n P)"
using valid_path_prefix[of P] by auto

lemma extension_valid [simp]: "v→v0 ⟹ valid_path (LCons v P)"
using P_not_null P_v0 P_valid valid_path_cons by blast
lemma extension_maximal [simp]: "maximal_path (LCons v P)"
by (simp add: maximal_path_cons)
lemma lappend_maximal [simp]: "maximal_path (lappend P' P)"
by (simp add: maximal_path_lappend)

lemma v0_V [simp]: "v0 ∈ V" by (metis P_LCons P_valid valid_path_cons_simp)
lemma v0_lset_P [simp]: "v0 ∈ lset P" using P_not_null P_v0 llist.set_sel(1) by blast
lemma v0_VV: "v0 ∈ VV p ∨ v0 ∈ VV p**" by simp
lemma lset_P_V [simp]: "lset P ⊆ V" by (simp add: valid_path_in_V)
lemma lset_ltl_P_V [simp]: "lset (ltl P) ⊆ V" by (simp add: valid_path_in_V)

lemma finite_llast_deadend [simp]: "lfinite P ⟹ deadend (llast P)"
using P_maximal P_not_null maximal_ends_on_deadend by blast
lemma finite_llast_V [simp]: "lfinite P ⟹ llast P ∈ V"
using P_not_null lfinite_lset lset_P_V by blast

text ‹If a path visits a deadend, it is winning for the other player.›
lemma visits_deadend:
assumes "lset P ∩ deadends p ≠ {}"
shows "winning_path p** P"
proof-
obtain n where n: "enat n < llength P" "P $n ∈ deadends p" using assms by (meson lset_intersect_lnth) hence *: "enat (Suc n) = llength P" using P_ends_on_deadend unfolding deadends_def by blast hence "llast P = P$ n" by (simp add: eSuc_enat llast_conv_lnth)
hence "llast P ∈ deadends p" using n(2) by simp
moreover have "lfinite P" using * llength_eq_enat_lfiniteD by force
ultimately show ?thesis unfolding winning_path_def deadends_def by auto
qed

end

end


Theory Strategy

section ‹Positional Strategies›

theory Strategy
imports
Main
ParityGame
begin

subsection ‹Definitions›

text ‹
A \emph{strategy} is simply a function from nodes to nodes
We only consider positional strategies.
›
type_synonym 'a Strategy = "'a ⇒ 'a"

text ‹
A \emph{valid} strategy for player @{term p} is a function assigning a successor to each node
in @{term "VV p"}.›
definition (in ParityGame) strategy :: "Player ⇒ 'a Strategy ⇒ bool" where
"strategy p σ ≡ ∀v ∈ VV p. ¬deadend v ⟶ v→σ v"

lemma (in ParityGame) strategyI [intro]:
"(⋀v. ⟦ v ∈ VV p; ¬deadend v ⟧ ⟹ v→σ v) ⟹ strategy p σ"
unfolding strategy_def by blast

subsection ‹Strategy-Conforming Paths›

text ‹
If @{term "path_conforms_with_strategy p P σ"} holds, then we call @{term P} a
\emph{@{term σ}-path}.
This means that @{term P} follows @{term σ} on all nodes of player @{term p}
except maybe the last node on the path.
›
coinductive (in ParityGame) path_conforms_with_strategy
:: "Player ⇒ 'a Path ⇒ 'a Strategy ⇒ bool" where
path_conforms_LNil:  "path_conforms_with_strategy p LNil σ"
| path_conforms_LCons_LNil: "path_conforms_with_strategy p (LCons v LNil) σ"
| path_conforms_VVp: "⟦ v ∈ VV p; w = σ v; path_conforms_with_strategy p (LCons w Ps) σ ⟧
⟹ path_conforms_with_strategy p (LCons v (LCons w Ps)) σ"
| path_conforms_VVpstar: "⟦ v ∉ VV p; path_conforms_with_strategy p Ps σ ⟧
⟹ path_conforms_with_strategy p (LCons v Ps) σ"

text ‹
Define a locale for valid maximal paths that conform to a given strategy, because we need
this concept quite often.  However, we are not yet able to add interesting lemmas to this locale.
We will do this at the end of this section, where we have more lemmas available.
›
locale vmc_path = vm_path +
fixes p σ assumes P_conforms [simp]: "path_conforms_with_strategy p P σ"

text ‹
Similary, define a locale for valid maximal paths that conform to given strategies for both
players.
›
locale vmc2_path = comp?: vmc_path G P v0 "p**" σ' + vmc_path G P v0 p σ
for G P v0 p σ σ'

subsection ‹An Arbitrary Strategy›

context ParityGame begin

text ‹
Define an arbitrary strategy.  This is useful to define other strategies by overriding part of
this strategy.
›
definition "σ_arbitrary ≡ λv. SOME w. v→w"

lemma valid_arbitrary_strategy [simp]: "strategy p σ_arbitrary" proof
fix v assume "¬deadend v"
thus "v → σ_arbitrary v" unfolding σ_arbitrary_def using someI_ex[of "λw. v→w"] by blast
qed

subsection ‹Valid Strategies›

lemma valid_strategy_updates: "⟦ strategy p σ; v0→w0 ⟧ ⟹ strategy p (σ(v0 := w0))"
unfolding strategy_def by auto

lemma valid_strategy_updates_set:
assumes "strategy p σ" "⋀v. ⟦ v ∈ A; v ∈ VV p; ¬deadend v ⟧ ⟹ v→σ' v"
shows "strategy p (override_on σ σ' A)"
unfolding strategy_def by (metis assms override_on_def strategy_def)

lemma valid_strategy_updates_set_strong:
assumes "strategy p σ" "strategy p σ'"
shows "strategy p (override_on σ σ' A)"
using assms(1) assms(2)[unfolded strategy_def] valid_strategy_updates_set by simp

lemma subgame_strategy_stays_in_subgame:
assumes σ: "ParityGame.strategy (subgame V') p σ"
and "v ∈ ParityGame.VV (subgame V') p" "¬Digraph.deadend (subgame V') v"
shows "σ v ∈ V'"
proof-
interpret G': ParityGame "subgame V'" using subgame_ParityGame .
have "σ v ∈ V⇘subgame V'⇙" using assms unfolding G'.strategy_def G'.edges_are_in_V(2) by blast
thus "σ v ∈ V'" by (metis Diff_iff IntE subgame_VV Player.distinct(2))
qed

lemma valid_strategy_supergame:
assumes σ: "strategy p σ"
and σ': "ParityGame.strategy (subgame V') p σ'"
and G'_no_deadends: "⋀v. v ∈ V' ⟹ ¬Digraph.deadend (subgame V') v"
shows "strategy p (override_on σ σ' V')" (is "strategy p ?σ")
proof
interpret G': ParityGame "subgame V'" using subgame_ParityGame .
fix v assume v: "v ∈ VV p" "¬deadend v"
show "v → ?σ v" proof (cases)
assume "v ∈ V'"
hence "v ∈ G'.VV p" using subgame_VV ‹v ∈ VV p› by blast
moreover have "¬G'.deadend v" using G'_no_deadends ‹v ∈ V'› by blast
ultimately have "v →⇘subgame V'⇙ σ' v" using σ' unfolding G'.strategy_def by blast
moreover have "σ' v = ?σ v" using ‹v ∈ V'› by simp
ultimately show ?thesis by (metis subgame_E subsetCE)
next
assume "v ∉ V'"
thus ?thesis using v σ unfolding strategy_def by simp
qed
qed

lemma valid_strategy_in_V: "⟦ strategy p σ; v ∈ VV p; ¬deadend v ⟧ ⟹ σ v ∈ V"
unfolding strategy_def using valid_edge_set by auto

lemma valid_strategy_only_in_V: "⟦ strategy p σ; ⋀v. v ∈ V ⟹ σ v = σ' v ⟧ ⟹ strategy p σ'"
unfolding strategy_def using edges_are_in_V(1) by auto

subsection ‹Conforming Strategies›

lemma path_conforms_with_strategy_ltl [intro]:
"path_conforms_with_strategy p P σ ⟹ path_conforms_with_strategy p (ltl P) σ"
by (drule path_conforms_with_strategy.cases) (simp_all add: path_conforms_with_strategy.intros(1))

lemma path_conforms_with_strategy_drop:
"path_conforms_with_strategy p P σ ⟹ path_conforms_with_strategy p (ldropn n P) σ"
by (simp add: path_conforms_with_strategy_ltl ltl_ldrop[of "λP. path_conforms_with_strategy p P σ"])

lemma path_conforms_with_strategy_prefix:
"path_conforms_with_strategy p P σ ⟹ lprefix P' P ⟹ path_conforms_with_strategy p P' σ"
proof (coinduction arbitrary: P P')
case (path_conforms_with_strategy P P')
thus ?case proof (cases rule: path_conforms_with_strategy.cases)
case path_conforms_LNil
thus ?thesis using path_conforms_with_strategy(2) by auto
next
case path_conforms_LCons_LNil
thus ?thesis by (metis lprefix_LCons_conv lprefix_antisym lprefix_code(1) path_conforms_with_strategy(2))
next
case (path_conforms_VVp v w)
thus ?thesis proof (cases)
assume "P' ≠ LNil ∧ P' ≠ LCons v LNil"
hence "∃Q. P' = LCons v (LCons w Q)"
by (metis local.path_conforms_VVp(1) lprefix_LCons_conv path_conforms_with_strategy(2))
thus ?thesis using local.path_conforms_VVp(1,3,4) path_conforms_with_strategy(2) by force
qed auto
next
case (path_conforms_VVpstar v)
thus ?thesis proof (cases)
assume "P' ≠ LNil"
hence "∃Q. P' = LCons v Q"
using local.path_conforms_VVpstar(1) lprefix_LCons_conv path_conforms_with_strategy(2) by fastforce
thus ?thesis using local.path_conforms_VVpstar path_conforms_with_strategy(2) by auto
qed simp
qed
qed

lemma path_conforms_with_strategy_irrelevant:
assumes "path_conforms_with_strategy p P σ" "v ∉ lset P"
shows "path_conforms_with_strategy p P (σ(v := w))"
using assms apply (coinduction arbitrary: P) by (drule path_conforms_with_strategy.cases) auto

lemma path_conforms_with_strategy_irrelevant_deadend:
assumes "path_conforms_with_strategy p P σ" "deadend v ∨ v ∉ VV p" "valid_path P"
shows "path_conforms_with_strategy p P (σ(v := w))"
using assms proof (coinduction arbitrary: P)
let ?σ = "σ(v := w)"
case (path_conforms_with_strategy P)
thus ?case proof (cases rule: path_conforms_with_strategy.cases)
case (path_conforms_VVp v' w Ps)
have "w = ?σ v'" proof-
from ‹valid_path P› have "¬deadend v'"
using local.path_conforms_VVp(1) valid_path_cons_simp by blast
with assms(2) have "v' ≠ v" using local.path_conforms_VVp(2) by blast
thus "w = ?σ v'" by (simp add: local.path_conforms_VVp(3))
qed
moreover
have "∃P. LCons w Ps = P ∧ path_conforms_with_strategy p P σ ∧ (deadend v ∨ v ∉ VV p) ∧ valid_path P"
proof-
have "valid_path (LCons w Ps)"
using local.path_conforms_VVp(1) path_conforms_with_strategy(3) valid_path_ltl' by blast
thus ?thesis using local.path_conforms_VVp(4) path_conforms_with_strategy(2) by blast
qed
ultimately show ?thesis using local.path_conforms_VVp(1,2) by blast
next
case (path_conforms_VVpstar v' Ps)
have "∃P. path_conforms_with_strategy p Ps σ ∧ (deadend v ∨ v ∉ VV p) ∧ valid_path Ps"
using local.path_conforms_VVpstar(1,3) path_conforms_with_strategy(2,3) valid_path_ltl' by blast
thus ?thesis by (simp add: local.path_conforms_VVpstar(1,2))
qed simp_all
qed

lemma path_conforms_with_strategy_irrelevant_updates:
assumes "path_conforms_with_strategy p P σ" "⋀v. v ∈ lset P ⟹ σ v = σ' v"
shows "path_conforms_with_strategy p P σ'"
using assms proof (coinduction arbitrary: P)
case (path_conforms_with_strategy P)
thus ?case proof (cases rule: path_conforms_with_strategy.cases)
case (path_conforms_VVp v' w Ps)
have "w = σ' v'" using local.path_conforms_VVp(1,3) path_conforms_with_strategy(2) by auto
thus ?thesis using local.path_conforms_VVp(1,4) path_conforms_with_strategy(2) by auto
qed simp_all
qed

lemma path_conforms_with_strategy_irrelevant':
assumes "path_conforms_with_strategy p P (σ(v := w))" "v ∉ lset P"
shows "path_conforms_with_strategy p P σ"
by (metis assms fun_upd_triv fun_upd_upd path_conforms_with_strategy_irrelevant)

lemma path_conforms_with_strategy_irrelevant_deadend':
assumes "path_conforms_with_strategy p P (σ(v := w))" "deadend v ∨ v ∉ VV p" "valid_path P"
shows "path_conforms_with_strategy p P σ"
by (metis assms fun_upd_triv fun_upd_upd path_conforms_with_strategy_irrelevant_deadend)

lemma path_conforms_with_strategy_start:
"path_conforms_with_strategy p (LCons v (LCons w P)) σ ⟹ v ∈ VV p ⟹ σ v = w"
by (drule path_conforms_with_strategy.cases) simp_all

lemma path_conforms_with_strategy_lappend:
assumes
P: "lfinite P" "¬lnull P" "path_conforms_with_strategy p P σ"
and P': "¬lnull P'" "path_conforms_with_strategy p P' σ"
and conforms: "llast P ∈ VV p ⟹ σ (llast P) = lhd P'"
shows "path_conforms_with_strategy p (lappend P P') σ"
using assms proof (induct P rule: lfinite_induct)
case (LCons P)
show ?case proof (cases)
assume "lnull (ltl P)"
then obtain v0 where v0: "P = LCons v0 LNil"
by (metis LCons.prems(1) lhd_LCons_ltl llist.collapse(1))
have "path_conforms_with_strategy p (LCons (lhd P) P') σ" proof (cases)
assume "lhd P ∈ VV p"
moreover with v0 have "lhd P' = σ (lhd P)"
using LCons.prems(5) by auto
ultimately show ?thesis
using path_conforms_VVp[of "lhd P" p "lhd P'" σ]
by (metis (no_types) LCons.prems(4) ‹¬lnull P'› lhd_LCons_ltl)
next
assume "lhd P ∉ VV p"
thus ?thesis using path_conforms_VVpstar using LCons.prems(4) v0 by blast
qed
thus ?thesis by (simp add: v0)
next
assume "¬lnull (ltl P)"
hence *: "path_conforms_with_strategy p (lappend (ltl P) P') σ"
by (metis LCons.hyps(3) LCons.prems(1) LCons.prems(2) LCons.prems(5) LCons.prems(5)
assms(4) assms(5) lhd_LCons_ltl llast_LCons2 path_conforms_with_strategy_ltl)
have "path_conforms_with_strategy p (LCons (lhd P) (lappend (ltl P) P')) σ" proof (cases)
assume "lhd P ∈ VV p"
moreover hence "lhd (ltl P) = σ (lhd P)"
by (metis LCons.prems(1) LCons.prems(2) ‹¬lnull (ltl P)›
lhd_LCons_ltl path_conforms_with_strategy_start)
ultimately show ?thesis
using path_conforms_VVp[of "lhd P" p "lhd (ltl P)" σ] * ‹¬lnull (ltl P)›
by (metis lappend_code(2) lhd_LCons_ltl)
next
assume "lhd P ∉ VV p"
thus ?thesis by (simp add: "*" path_conforms_VVpstar)
qed
with ‹¬lnull P› show "path_conforms_with_strategy p (lappend P P') σ"
by (metis lappend_code(2) lhd_LCons_ltl)
qed
qed simp

lemma path_conforms_with_strategy_VVpstar:
assumes "lset P ⊆ VV p**"
shows "path_conforms_with_strategy p P σ"
using assms proof (coinduction arbitrary: P)
case (path_conforms_with_strategy P)
moreover have "⋀v Ps. P = LCons v Ps ⟹ ?case" using path_conforms_with_strategy by auto
ultimately show ?case by (cases "P = LNil", simp) (metis lnull_def not_lnull_conv)
qed

lemma subgame_path_conforms_with_strategy:
assumes V': "V' ⊆ V" and P: "path_conforms_with_strategy p P σ" "lset P ⊆ V'"
shows "ParityGame.path_conforms_with_strategy (subgame V') p P σ"
proof-
have "lset P ⊆ V⇘subgame V'⇙" unfolding subgame_def using P(2) V' by auto
with P(1) show ?thesis
by (coinduction arbitrary: P rule: ParityGame.path_conforms_with_strategy.coinduct[OF subgame_ParityGame])
(cases rule: path_conforms_with_strategy.cases, auto)
qed

lemma (in vmc_path) subgame_path_vmc_path:
assumes V': "V' ⊆ V" and P: "lset P ⊆ V'"
shows "vmc_path (subgame V') P v0 p σ"
proof-
interpret G': ParityGame "subgame V'" using subgame_ParityGame by blast
show ?thesis proof
show "G'.valid_path P" using subgame_valid_path P_valid P by blast
show "G'.maximal_path P" using subgame_maximal_path V' P_maximal P by blast
show "G'.path_conforms_with_strategy p P σ"
using subgame_path_conforms_with_strategy V' P_conforms P by blast
qed simp_all
qed

subsection ‹Greedy Conforming Path›

text ‹
Given a starting point and two strategies, there exists a path conforming to both strategies.
Here we define this path.  Incidentally, this also shows that the assumptions of the locales
‹vmc_path› and ‹vmc2_path› are satisfiable.

We are only interested in proving the existence of such a path, so the definition
(i.e., the implementation) and most lemmas are private.
›

context begin

private primcorec greedy_conforming_path :: "Player ⇒ 'a Strategy ⇒ 'a Strategy ⇒ 'a ⇒ 'a Path" where
"greedy_conforming_path p σ σ' v0 =
LCons v0 (if deadend v0
then LNil
else if v0 ∈ VV p
then greedy_conforming_path p σ σ' (σ v0)
else greedy_conforming_path p σ σ' (σ' v0))"

private lemma greedy_path_LNil: "greedy_conforming_path p σ σ' v0 ≠ LNil"
using greedy_conforming_path.disc_iff llist.discI(1) by blast

private lemma greedy_path_lhd: "greedy_conforming_path p σ σ' v0 = LCons v P ⟹ v = v0"
using greedy_conforming_path.code by auto

private lemma greedy_path_deadend_v0: "greedy_conforming_path p σ σ' v0 = LCons v P ⟹ P = LNil ⟷ deadend v0"
by (metis (no_types, lifting) greedy_conforming_path.disc_iff
greedy_conforming_path.simps(3) llist.disc(1) ltl_simps(2))

private corollary greedy_path_deadend_v:
"greedy_conforming_path p σ σ' v0 = LCons v P ⟹ P = LNil ⟷ deadend v"
using greedy_path_deadend_v0 greedy_path_lhd by metis
corollary greedy_path_deadend_v': "greedy_conforming_path p σ σ' v0 = LCons v LNil ⟹ deadend v"
using greedy_path_deadend_v by blast

private lemma greedy_path_ltl:
assumes "greedy_conforming_path p σ σ' v0 = LCons v P"
shows "P = LNil ∨ P = greedy_conforming_path p σ σ' (σ v0) ∨ P = greedy_conforming_path p σ σ' (σ' v0)"
apply (insert assms, frule greedy_path_lhd)
apply (cases "deadend v0", simp add: greedy_conforming_path.code)
by (metis (no_types, lifting) greedy_conforming_path.sel(2) ltl_simps(2))

private lemma greedy_path_ltl_ex:
assumes "greedy_conforming_path p σ σ' v0 = LCons v P"
shows "P = LNil ∨ (∃v. P = greedy_conforming_path p σ σ' v)"
using assms greedy_path_ltl by blast

private lemma greedy_path_ltl_VVp:
assumes "greedy_conforming_path p σ σ' v0 = LCons v0 P" "v0 ∈ VV p" "¬deadend v0"
shows "σ v0 = lhd P"
using assms greedy_conforming_path.code by auto

private lemma greedy_path_ltl_VVpstar:
assumes "greedy_conforming_path p σ σ' v0 = LCons v0 P" "v0 ∈ VV p**" "¬deadend v0"
shows "σ' v0 = lhd P"
using assms greedy_conforming_path.code by auto

private lemma greedy_conforming_path_properties:
assumes "v0 ∈ V" "strategy p σ" "strategy p** σ'"
shows
greedy_path_not_null:  "¬lnull (greedy_conforming_path p σ σ' v0)"
and greedy_path_v0:        "greedy_conforming_path p σ σ' v0 $0 = v0" and greedy_path_valid: "valid_path (greedy_conforming_path p σ σ' v0)" and greedy_path_maximal: "maximal_path (greedy_conforming_path p σ σ' v0)" and greedy_path_conforms: "path_conforms_with_strategy p (greedy_conforming_path p σ σ' v0) σ" and greedy_path_conforms': "path_conforms_with_strategy p** (greedy_conforming_path p σ σ' v0) σ'" proof- define P where [simp]: "P = greedy_conforming_path p σ σ' v0" show "¬lnull P" "P$ 0 = v0" by (simp_all add: lnth_0_conv_lhd)

{
fix v0 assume "v0 ∈ V"
let ?P = "greedy_conforming_path p σ σ' v0"
assume asm: "¬(∃v. ?P = LCons v LNil)"
obtain P' where P': "?P = LCons v0 P'" by (metis greedy_path_LNil greedy_path_lhd neq_LNil_conv)
hence "¬deadend v0" using asm greedy_path_deadend_v0 ‹v0 ∈ V› by blast
from P' have 1: "¬lnull P'" using asm llist.collapse(1) ‹v0 ∈ V› greedy_path_deadend_v0 by blast
moreover from P' ‹¬deadend v0› assms(2,3) ‹v0 ∈ V›
have "v0→lhd P'"
unfolding strategy_def using greedy_path_ltl_VVp greedy_path_ltl_VVpstar
by (cases "v0 ∈ VV p") auto
moreover hence "lhd P' ∈ V" by blast
moreover hence "∃v. P' = greedy_conforming_path p σ σ' v ∧ v ∈ V"
by (metis P' calculation(1) greedy_conforming_path.simps(2) greedy_path_ltl_ex lnull_def)
text ‹The conjunction of all the above.›
ultimately
have "∃P'. ?P = LCons v0 P' ∧ ¬lnull P' ∧ v0→lhd P' ∧ lhd P' ∈ V
∧ (∃v. P' = greedy_conforming_path p σ σ' v ∧ v ∈ V)"
using P' by blast
} note coinduction_helper = this

show "valid_path P" using assms unfolding P_def
proof (coinduction arbitrary: v0 rule: valid_path.coinduct)
case (valid_path v0)
from ‹v0 ∈ V› assms(2,3) show ?case
using coinduction_helper[of v0] greedy_path_lhd by blast
qed

show "maximal_path P" using assms unfolding P_def
proof (coinduction arbitrary: v0)
case (maximal_path v0)
from ‹v0 ∈ V› assms(2,3) show ?case
using coinduction_helper[of v0] greedy_path_deadend_v' by blast
qed

{
fix p'' σ'' assume p'': "(p'' = p ∧ σ'' = σ) ∨ (p'' = p** ∧ σ'' = σ')"
moreover with assms have "strategy p'' σ''" by blast
hence "path_conforms_with_strategy p'' P σ''" using ‹v0 ∈ V› unfolding P_def
proof (coinduction arbitrary: v0)
case (path_conforms_with_strategy v0)
show ?case proof (cases "v0 ∈ VV p''")
case True
{ assume "¬(∃v. greedy_conforming_path p σ σ' v0 = LCons v LNil)"
with ‹v0 ∈ V› obtain P' where
P': "greedy_conforming_path p σ σ' v0 = LCons v0 P'" "¬lnull P'" "v0→lhd P'"
"lhd P' ∈ V" "∃v. P' = greedy_conforming_path p σ σ' v ∧ v ∈ V"
using coinduction_helper by blast
with ‹v0 ∈ VV p''› p'' have "σ'' v0 = lhd P'"
using greedy_path_ltl_VVp greedy_path_ltl_VVpstar by blast
with ‹v0 ∈ VV p''› P'(1,2,5) have ?path_conforms_VVp
using greedy_conforming_path.code path_conforms_with_strategy(1) by fastforce
}
thus ?thesis by auto
next
case False
thus ?thesis using coinduction_helper[of v0] path_conforms_with_strategy by auto
qed
qed
}
thus "path_conforms_with_strategy p P σ" "path_conforms_with_strategy p** P σ'" by blast+
qed

corollary strategy_conforming_path_exists:
assumes "v0 ∈ V" "strategy p σ" "strategy p** σ'"
obtains P where "vmc2_path G P v0 p σ σ'"
proof
show "vmc2_path G (greedy_conforming_path p σ σ' v0) v0 p σ σ'"
using assms by unfold_locales (simp_all add: greedy_conforming_path_properties)
qed

corollary strategy_conforming_path_exists_single:
assumes "v0 ∈ V" "strategy p σ"
obtains P where "vmc_path G P v0 p σ"
proof
show "vmc_path G (greedy_conforming_path p σ σ_arbitrary v0) v0 p σ"
using assms by unfold_locales (simp_all add: greedy_conforming_path_properties)
qed

end

end

subsection ‹Valid Maximal Conforming Paths›

text ‹Now is the time to add some lemmas to the locale ‹vmc_path›.›

context vmc_path begin
lemma Ptl_conforms [simp]: "path_conforms_with_strategy p (ltl P) σ"
using P_conforms path_conforms_with_strategy_ltl by blast
lemma Pdrop_conforms [simp]: "path_conforms_with_strategy p (ldropn n P) σ"
using P_conforms path_conforms_with_strategy_drop by blast
lemma prefix_conforms [simp]: "path_conforms_with_strategy p (ltake n P) σ"
using P_conforms path_conforms_with_strategy_prefix by blast
lemma extension_conforms [simp]:
"(v' ∈ VV p ⟹ σ v' = v0) ⟹ path_conforms_with_strategy p (LCons v' P) σ"
by (metis P_LCons P_conforms path_conforms_VVp path_conforms_VVpstar)

lemma extension_valid_maximal_conforming:
assumes "v'→v0" "v' ∈ VV p ⟹ σ v' = v0"
shows "vmc_path G (LCons v' P) v' p σ"
using assms by unfold_locales simp_all

lemma vmc_path_ldropn:
assumes "enat n < llength P"
shows "vmc_path G (ldropn n P) (P $n) p σ" using assms by unfold_locales (simp_all add: lhd_ldropn) lemma conforms_to_another_strategy: "path_conforms_with_strategy p P σ' ⟹ vmc_path G P v0 p σ'" using P_not_null P_valid P_maximal P_v0 by unfold_locales blast+ end lemma (in ParityGame) valid_maximal_conforming_path_0: assumes "¬lnull P" "valid_path P" "maximal_path P" "path_conforms_with_strategy p P σ" shows "vmc_path G P (P$ 0) p σ"
using assms by unfold_locales (simp_all add: lnth_0_conv_lhd)

subsection ‹Valid Maximal Conforming Paths with One Edge›

text ‹
We define a locale for valid maximal conforming paths that contain at least one edge.
This is equivalent to the first node being no deadend.  This assumption allows us to prove
much stronger lemmas about @{term "ltl P"} compared to @{term "vmc_path"}.
›

locale vmc_path_no_deadend = vmc_path +
assumes v0_no_deadend [simp]: "¬deadend v0"
begin
definition "w0 ≡ lhd (ltl P)"

lemma Ptl_not_null [simp]: "¬lnull (ltl P)"
using P_LCons P_maximal maximal_no_deadend v0_no_deadend by metis
lemma Ptl_LCons: "ltl P = LCons w0 (ltl (ltl P))" unfolding w0_def by simp
lemma P_LCons': "P = LCons v0 (LCons w0 (ltl (ltl P)))" using P_LCons Ptl_LCons by simp
lemma v0_edge_w0 [simp]: "v0→w0" using P_valid P_LCons' by (metis valid_path_edges')

lemma Ptl_0: "ltl P $0 = lhd (ltl P)" by (simp add: lhd_conv_lnth) lemma P_Suc_0: "P$ Suc 0 = w0" by (simp add: P_lnth_Suc Ptl_0 w0_def)
lemma Ptl_edge [simp]: "v0 → lhd (ltl P)" by (metis P_LCons' P_valid valid_path_edges' w0_def)

lemma v0_conforms: "v0 ∈ VV p ⟹ σ v0 = w0"
using path_conforms_with_strategy_start by (metis P_LCons' P_conforms)

lemma w0_V [simp]: "w0 ∈ V" by (metis Ptl_LCons Ptl_valid valid_path_cons_simp)
lemma w0_lset_P [simp]: "w0 ∈ lset P" by (metis P_LCons' lset_intros(1) lset_intros(2))

lemma vmc_path_ltl [simp]: "vmc_path G (ltl P) w0 p σ" by (unfold_locales) (simp_all add: w0_def)
end

context vmc_path begin

lemma vmc_path_lnull_ltl_no_deadend:
"¬lnull (ltl P) ⟹ vmc_path_no_deadend G P v0 p σ"
using P_0 P_no_deadends by (unfold_locales) (metis enat_ltl_Suc lnull_0_llength)

lemma vmc_path_conforms:
assumes "enat (Suc n) < llength P" "P $n ∈ VV p" shows "σ (P$ n) = P $Suc n" proof- define P' where "P' = ldropn n P" then interpret P': vmc_path G P' "P$ n" p σ using vmc_path_ldropn assms(1) Suc_llength by blast
have "¬deadend (P $n)" using assms(1) P_no_deadends by blast then interpret P': vmc_path_no_deadend G P' "P$ n" p σ by unfold_locales
have "σ (P $n) = P'.w0" using P'.v0_conforms assms(2) by blast thus ?thesis using P'_def P'.P_Suc_0 assms(1) by simp qed subsection ‹@{term lset} Induction Schemas for Paths› text ‹Let us define an induction schema useful for proving @{term "lset P ⊆ S"}.› lemma vmc_path_lset_induction [consumes 1, case_names base step]: assumes "Q P" and base: "v0 ∈ S" and step_assumption: "⋀P v0. ⟦ vmc_path_no_deadend G P v0 p σ; v0 ∈ S; Q P ⟧ ⟹ Q (ltl P) ∧ (vmc_path_no_deadend.w0 P) ∈ S" shows "lset P ⊆ S" proof fix v assume "v ∈ lset P" thus "v ∈ S" using vmc_path_axioms assms(1,2) proof (induct arbitrary: v0 rule: llist_set_induct) case (find P) then interpret vmc_path G P v0 p σ by blast show ?case by (simp add: find.prems(3)) next case (step P v) then interpret vmc_path G P v0 p σ by blast show ?case proof (cases) assume "lnull (ltl P)" hence "P = LCons v LNil" by (metis llist.disc(2) lset_cases step.hyps(2)) thus ?thesis using step.prems(3) P_LCons by blast next assume "¬lnull (ltl P)" then interpret vmc_path_no_deadend G P v0 p σ using vmc_path_lnull_ltl_no_deadend by blast show "v ∈ S" using step.hyps(3) step_assumption[OF vmc_path_no_deadend_axioms ‹v0 ∈ S› ‹Q P›] vmc_path_ltl by blast qed qed qed text ‹@{thm vmc_path_lset_induction} without the Q predicate.› corollary vmc_path_lset_induction_simple [case_names base step]: assumes base: "v0 ∈ S" and step: "⋀P v0. ⟦ vmc_path_no_deadend G P v0 p σ; v0 ∈ S ⟧ ⟹ vmc_path_no_deadend.w0 P ∈ S" shows "lset P ⊆ S" using assms vmc_path_lset_induction[of "λP. True"] by blast text ‹Another induction schema for proving @{term "lset P ⊆ S"} based on closure properties.› lemma vmc_path_lset_induction_closed_subset [case_names VVp VVpstar v0 disjoint]: assumes VVp: "⋀v. ⟦ v ∈ S; ¬deadend v; v ∈ VV p ⟧ ⟹ σ v ∈ S ∪ T" and VVpstar: "⋀v w. ⟦ v ∈ S; ¬deadend v; v ∈ VV p** ; v→w ⟧ ⟹ w ∈ S ∪ T" and v0: "v0 ∈ S" and disjoint: "lset P ∩ T = {}" shows "lset P ⊆ S" using disjoint proof (induct rule: vmc_path_lset_induction) case (step P v0) interpret vmc_path_no_deadend G P v0 p σ using step.hyps(1) . have "lset (ltl P) ∩ T = {}" using step.hyps(3) by (meson disjoint_eq_subset_Compl lset_ltl order.trans) moreover have "w0 ∈ S ∪ T" using assms(1,2)[of v0] step.hyps(2) v0_no_deadend v0_conforms by (cases "v0 ∈ VV p") simp_all ultimately show ?case using step.hyps(3) w0_lset_P by blast qed (insert v0) end end  Theory AttractingStrategy section ‹Attracting Strategies› theory AttractingStrategy imports Main Strategy begin text ‹Here we introduce the concept of attracting strategies.› context ParityGame begin subsection ‹Paths Visiting a Set› text ‹A path that stays in ‹A› until eventually it visits ‹W›.› definition "visits_via P A W ≡ ∃n. enat n < llength P ∧ P$ n ∈ W ∧ lset (ltake (enat n) P) ⊆ A"

lemma visits_via_monotone: "⟦ visits_via P A W; A ⊆ A' ⟧ ⟹ visits_via P A' W"
unfolding visits_via_def by blast

lemma visits_via_visits: "visits_via P A W ⟹ lset P ∩ W ≠ {}"
unfolding visits_via_def by (meson disjoint_iff_not_equal in_lset_conv_lnth)

lemma (in vmc_path) visits_via_trivial: "v0 ∈ W ⟹ visits_via P A W"
unfolding visits_via_def apply (rule exI[of _ 0]) using zero_enat_def by auto

lemma visits_via_LCons:
assumes "visits_via P A W"
shows "visits_via (LCons v0 P) (insert v0 A) W"
proof-
obtain n where n: "enat n < llength P" "P $n ∈ W" "lset (ltake (enat n) P) ⊆ A" using assms unfolding visits_via_def by blast define P' where "P' = LCons v0 P" have "enat (Suc n) < llength P'" unfolding P'_def by (metis n(1) ldropn_Suc_LCons ldropn_Suc_conv_ldropn ldropn_eq_LConsD) moreover have "P'$ Suc n ∈ W" unfolding P'_def by (simp add: n(2))
moreover have "lset (ltake (enat (Suc n)) P') ⊆ insert v0 A"
using lset_ltake_Suc[of P' v0 n A] unfolding P'_def by (simp add: n(3))
ultimately show ?thesis unfolding visits_via_def P'_def by blast
qed

lemma (in vmc_path_no_deadend) visits_via_ltl:
assumes "visits_via P A W"
and v0: "v0 ∉ W"
shows "visits_via (ltl P) A W"
proof-
obtain n where n: "enat n < llength P" "P $n ∈ W" "lset (ltake (enat n) P) ⊆ A" using assms(1)[unfolded visits_via_def] by blast have "n ≠ 0" using v0 n(2) DiffE by force then obtain n' where n': "Suc n' = n" using nat.exhaust by metis have "∃n. enat n < llength (ltl P) ∧ (ltl P)$ n ∈ W ∧ lset (ltake (enat n) (ltl P)) ⊆ A"
apply (rule exI[of _ n'])
using n n' enat_Suc_ltl[of n' P] P_lnth_Suc lset_ltake_ltl[of n' P] by auto
thus ?thesis using visits_via_def by blast
qed

lemma (in vm_path) visits_via_deadend:
assumes "visits_via P A (deadends p)"
shows "winning_path p** P"
using assms visits_via_visits visits_deadend by blast

subsection ‹Attracting Strategy from a Single Node›

text ‹
All @{term σ}-paths starting from @{term v0} visit @{term W} and until then they stay in @{term A}.
›
definition strategy_attracts_via :: "Player ⇒ 'a Strategy ⇒ 'a ⇒ 'a set ⇒ 'a set ⇒ bool" where
"strategy_attracts_via p σ v0 A W ≡ ∀P. vmc_path G P v0 p σ ⟶ visits_via P A W"

lemma (in vmc_path) strategy_attracts_viaE:
assumes "strategy_attracts_via p σ v0 A W"
shows "visits_via P A W"
using strategy_attracts_via_def assms vmc_path_axioms by blast

lemma (in vmc_path) strategy_attracts_via_SucE:
assumes "strategy_attracts_via p σ v0 A W" "v0 ∉ W"
shows "∃n. enat (Suc n) < llength P ∧ P $Suc n ∈ W ∧ lset (ltake (enat (Suc n)) P) ⊆ A" proof- obtain n where n: "enat n < llength P" "P$ n ∈ W" "lset (ltake (enat n) P) ⊆ A"
using strategy_attracts_viaE[unfolded visits_via_def] assms(1) by blast
have "n ≠ 0" using assms(2) n(2) by (metis P_0)
thus ?thesis using n not0_implies_Suc by blast
qed

lemma (in vmc_path) strategy_attracts_via_lset:
assumes "strategy_attracts_via p σ v0 A W"
shows "lset P ∩ W ≠ {}"
using assms[THEN strategy_attracts_viaE, unfolded visits_via_def]
by (meson disjoint_iff_not_equal lset_lnth_member subset_refl)

lemma strategy_attracts_via_v0:
assumes σ: "strategy p σ" "strategy_attracts_via p σ v0 A W"
and v0: "v0 ∈ V"
shows "v0 ∈ A ∪ W"
proof-
obtain P where "vmc_path G P v0 p σ" using strategy_conforming_path_exists_single assms by blast
then interpret vmc_path G P v0 p σ .
obtain n where n: "enat n < llength P" "P $n ∈ W" "lset (ltake (enat n) P) ⊆ A" using σ(2)[unfolded strategy_attracts_via_def visits_via_def] vmc_path_axioms by blast show ?thesis proof (cases "n = 0") case True thus ?thesis using n(2) by simp next case False hence "lhd (ltake (enat n) P) = lhd P" by (simp add: enat_0_iff(1)) hence "v0 ∈ lset (ltake (enat n) P)" by (metis ‹n ≠ 0› P_not_null P_v0 enat_0_iff(1) llist.set_sel(1) ltake.disc(2)) thus ?thesis using n(3) by blast qed qed corollary strategy_attracts_not_outside: "⟦ v0 ∈ V - A - W; strategy p σ ⟧ ⟹ ¬strategy_attracts_via p σ v0 A W" using strategy_attracts_via_v0 by blast lemma strategy_attracts_viaI [intro]: assumes "⋀P. vmc_path G P v0 p σ ⟹ visits_via P A W" shows "strategy_attracts_via p σ v0 A W" unfolding strategy_attracts_via_def using assms by blast lemma strategy_attracts_via_no_deadends: assumes "v ∈ V" "v ∈ A - W" "strategy_attracts_via p σ v A W" shows "¬deadend v" proof assume "deadend v" define P where [simp]: "P = LCons v LNil" interpret vmc_path G P v p σ proof show "valid_path P" using ‹v ∈ A - W› ‹v ∈ V› valid_path_base' by auto show "maximal_path P" using ‹deadend v› by (simp add: maximal_path.intros(2)) show "path_conforms_with_strategy p P σ" by (simp add: path_conforms_LCons_LNil) qed simp_all have "visits_via P A W" using assms(3) strategy_attracts_viaE by blast moreover have "llength P = eSuc 0" by simp ultimately have "P$ 0 ∈ W" by (simp add: enat_0_iff(1) visits_via_def)
with ‹v ∈ A - W› show False by auto
qed

lemma attractor_strategy_on_extends:
"⟦ strategy_attracts_via p σ v0 A W; A ⊆ A' ⟧ ⟹ strategy_attracts_via p σ v0 A' W"
unfolding strategy_attracts_via_def using visits_via_monotone by blast

lemma strategy_attracts_via_trivial: "v0 ∈ W ⟹ strategy_attracts_via p σ v0 A W"
proof
fix P assume "v0 ∈ W" "vmc_path G P v0 p σ"
then interpret vmc_path G P v0 p σ by blast
show "visits_via P A W" using visits_via_trivial using ‹v0 ∈ W› by blast
qed

lemma strategy_attracts_via_successor:
assumes σ: "strategy p σ" "strategy_attracts_via p σ v0 A W"
and v0: "v0 ∈ A - W"
and w0: "v0→w0" "v0 ∈ VV p ⟹ σ v0 = w0"
shows "strategy_attracts_via p σ w0 A W"
proof
fix P assume "vmc_path G P w0 p σ"
then interpret vmc_path G P w0 p σ .
define P' where [simp]: "P' = LCons v0 P"
then interpret P': vmc_path G P' v0 p σ
using extension_valid_maximal_conforming w0 by blast
interpret P': vmc_path_no_deadend G P' v0 p σ using ‹v0→w0› by unfold_locales blast
have "visits_via P' A W" using σ(2) P'.strategy_attracts_viaE by blast
thus "visits_via P A W" using P'.visits_via_ltl v0 by simp
qed

lemma strategy_attracts_VVp:
assumes σ: "strategy p σ" "strategy_attracts_via p σ v0 A W"
and v: "v0 ∈ A - W" "v0 ∈ VV p" "¬deadend v0"
shows "σ v0 ∈ A ∪ W"
proof-
have "v0→σ v0" using σ(1)[unfolded strategy_def] v(2,3) by blast
hence "strategy_attracts_via p σ (σ v0) A W"
using strategy_attracts_via_successor σ v(1) by blast
thus ?thesis using strategy_attracts_via_v0 ‹v0→σ v0› σ(1) by blast
qed

lemma strategy_attracts_VVpstar:
assumes "strategy p σ" "strategy_attracts_via p σ v0 A W"
and "v0 ∈ A - W" "v0 ∉ VV p" "w0 ∈ V - A - W"
shows "¬v0 → w0"
by (metis assms strategy_attracts_not_outside strategy_attracts_via_successor)

subsection ‹Attracting strategy from a set of nodes›

text ‹
All @{term σ}-paths starting from @{term A} visit @{term W} and until then they stay in @{term A}.
›
definition strategy_attracts :: "Player ⇒ 'a Strategy ⇒ 'a set ⇒ 'a set ⇒ bool" where
"strategy_attracts p σ A W ≡ ∀v0 ∈ A. strategy_attracts_via p σ v0 A W"

lemma (in vmc_path) strategy_attractsE:
assumes "strategy_attracts p σ A W" "v0 ∈ A"
shows "visits_via P A W"
using assms(1)[unfolded strategy_attracts_def] assms(2) strategy_attracts_viaE by blast

lemma strategy_attractsI [intro]:
assumes "⋀P v. ⟦ v ∈ A; vmc_path G P v p σ ⟧ ⟹ visits_via P A W"
shows "strategy_attracts p σ A W"
unfolding strategy_attracts_def using assms by blast

lemma (in vmc_path) strategy_attracts_lset:
assumes "strategy_attracts p σ A W" "v0 ∈ A"
shows "lset P ∩ W ≠ {}"
using assms(1)[unfolded strategy_attracts_def] assms(2) strategy_attracts_via_lset(1)[of A W]
by blast

lemma strategy_attracts_empty [simp]: "strategy_attracts p σ {} W" by blast

lemma strategy_attracts_invalid_path:
assumes P: "P = LCons v (LCons w P')" "v ∈ A - W" "w ∉ A ∪ W"
shows "¬visits_via P A W" (is "¬?A")
proof
assume ?A
then obtain n where n: "enat n < llength P" "P $n ∈ W" "lset (ltake (enat n) P) ⊆ A" unfolding visits_via_def by blast have "n ≠ 0" using ‹v ∈ A - W› n(2) P(1) DiffD2 by force moreover have "n ≠ Suc 0" using ‹w ∉ A ∪ W› n(2) P(1) by auto ultimately have "Suc (Suc 0) ≤ n" by presburger hence "lset (ltake (enat (Suc (Suc 0))) P) ⊆ A" using n(3) by (meson contra_subsetD enat_ord_simps(1) lset_ltake_prefix lset_lnth_member lset_subset) moreover have "enat (Suc 0) < llength (ltake (eSuc (eSuc 0)) P)" proof- have *: "enat (Suc (Suc 0)) < llength P" using ‹Suc (Suc 0) ≤ n› n(1) by (meson enat_ord_simps(2) le_less_linear less_le_trans neq_iff) have "llength (ltake (enat (Suc (Suc 0))) P) = min (enat (Suc (Suc 0))) (llength P)" by simp hence "llength (ltake (enat (Suc (Suc 0))) P) = enat (Suc (Suc 0))" using * by (simp add: min_absorb1) thus ?thesis by (simp add: eSuc_enat zero_enat_def) qed ultimately have "ltake (enat (Suc (Suc 0))) P$ Suc 0 ∈ A" by (simp add: lset_lnth_member)
hence "P $Suc 0 ∈ A" by (simp add: lnth_ltake) thus False using P(1,3) by auto qed text ‹ If @{term A} is an attractor set of @{term W} and an edge leaves @{term A} without going through @{term W}, then @{term v} belongs to @{term "VV p"} and the attractor strategy @{term σ} avoids this edge. All other cases give a contradiction. › lemma strategy_attracts_does_not_leave: assumes σ: "strategy_attracts p σ A W" "strategy p σ" and v: "v→w" "v ∈ A - W" "w ∉ A ∪ W" shows "v ∈ VV p ∧ σ v ≠ w" proof (rule ccontr) assume contra: "¬(v ∈ VV p ∧ σ v ≠ w)" (* Define a strategy for p** which tries to take this edge. *) define σ' where "σ' = σ_arbitrary(v := w)" hence "strategy p** σ'" using ‹v→w› by (simp add: valid_strategy_updates) then obtain P where P: "vmc2_path G P v p σ σ'" using ‹v→w› strategy_conforming_path_exists σ(2) by blast then interpret vmc2_path G P v p σ σ' . interpret vmc_path_no_deadend G P v p σ using ‹v→w› by unfold_locales blast interpret comp: vmc_path_no_deadend G P v "p**" σ' using ‹v→w› by unfold_locales blast have "w = w0" using contra σ'_def v0_conforms comp.v0_conforms by (cases "v ∈ VV p") auto hence "¬visits_via P A W" using strategy_attracts_invalid_path[of P v w "ltl (ltl P)"] v(2,3) P_LCons' by simp thus False by (meson DiffE σ(1) strategy_attractsE v(2)) qed text ‹ Given an attracting strategy @{term σ}, we can turn every strategy @{term σ'} into an attracting strategy by overriding @{term σ'} on a suitable subset of the nodes. This also means that an attracting strategy is still attracting if we override it outside of @{term "A - W"}. › lemma strategy_attracts_irrelevant_override: assumes "strategy_attracts p σ A W" "strategy p σ" "strategy p σ'" shows "strategy_attracts p (override_on σ' σ (A - W)) A W" proof (rule strategy_attractsI, rule ccontr) fix P v let ?σ = "override_on σ' σ (A - W)" assume "vmc_path G P v p ?σ" then interpret vmc_path G P v p ?σ . assume "v ∈ A" hence "P$ 0 ∈ A" using ‹v ∈ A› by simp
moreover assume contra: "¬visits_via P A W"
ultimately have "P $0 ∈ A - W" unfolding visits_via_def by (meson DiffI P_len not_less0 lset_ltake) have "¬lset P ⊆ A - W" proof assume "lset P ⊆ A - W" hence "⋀v. v ∈ lset P ⟹ override_on σ' σ (A - W) v = σ v" by auto hence "path_conforms_with_strategy p P σ" using path_conforms_with_strategy_irrelevant_updates[OF P_conforms] by blast hence "vmc_path G P (P$ 0) p σ"
using conforms_to_another_strategy P_0 by blast
thus False
using contra ‹P $0 ∈ A› assms(1) by (meson vmc_path.strategy_attractsE) qed hence "∃n. enat n < llength P ∧ P$ n ∉ A - W" by (meson lset_subset)
then obtain n where n: "enat n < llength P ∧ P $n ∉ A - W" "⋀i. i < n ⟹ ¬(enat i < llength P ∧ P$ i ∉ A - W)"
using ex_least_nat_le[of "λn. enat n < llength P ∧ P $n ∉ A - W"] by blast hence n_min: "⋀i. i < n ⟹ P$ i ∈ A - W"
using dual_order.strict_trans enat_ord_simps(2) by blast
have "n ≠ 0" using ‹P $0 ∈ A - W› n(1) by meson then obtain n' where n': "Suc n' = n" using not0_implies_Suc by blast hence "P$ n' ∈ A - W" using n_min by blast
moreover have "P $n' → P$ Suc n'" using P_valid n(1) n' valid_path_edges by blast
moreover have "P $Suc n' ∉ A ∪ W" proof- have "P$ n ∉ W" using contra n(1) n_min unfolding visits_via_def
by (meson Diff_subset lset_ltake subsetCE)
thus ?thesis using n(1) n' by blast
qed
ultimately have "P $n' ∈ VV p ∧ σ (P$ n') ≠ P $Suc n'" using strategy_attracts_does_not_leave[of p σ A W "P$ n'" "P $Suc n'"] assms(1,2) by blast thus False using n(1) n' vmc_path_conforms ‹P$ n' ∈ A - W› by (metis override_on_apply_in)
qed

lemma strategy_attracts_trivial [simp]: "strategy_attracts p σ W W"
by (simp add: strategy_attracts_def strategy_attracts_via_trivial)

text ‹If a @{term σ}-conforming path @{term P} hits an attractor @{term A}, it will visit @{term W}.›
lemma (in vmc_path) attracted_path:
assumes "W ⊆ V"
and σ: "strategy_attracts p σ A W"
and P_hits_A: "lset P ∩ A ≠ {}"
shows "lset P ∩ W ≠ {}"
proof-
obtain n where n: "enat n < llength P" "P $n ∈ A" using P_hits_A by (meson lset_intersect_lnth) define P' where "P' = ldropn n P" interpret vmc_path G P' "P$ n" p σ unfolding P'_def using vmc_path_ldropn n(1) by blast
have "visits_via P' A W" using σ n(2) strategy_attractsE by blast
thus ?thesis unfolding P'_def using visits_via_visits in_lset_ldropnD[of _ n P] by blast
qed

lemma attracted_strategy_step:
assumes σ: "strategy p σ" "strategy_attracts p σ A W"
and v0: "¬deadend v0" "v0 ∈ A - W" "v0 ∈ VV p"
shows "σ v0 ∈ A ∪ W"
by (metis DiffD1 strategy_attracts_VVp assms strategy_attracts_def)

lemma (in vmc_path_no_deadend) attracted_path_step:
assumes σ: "strategy_attracts p σ A W"
and v0: "v0 ∈ A - W"
shows "w0 ∈ A ∪ W"
by (metis (no_types) DiffD1 P_LCons' σ strategy_attractsE strategy_attracts_invalid_path v0)

end ― ‹context ParityGame›

end


Theory Attractor

section ‹Attractor Sets›
text ‹\label{sec:attractor}›

theory Attractor
imports
Main
AttractingStrategy
begin

text ‹Here we define the @{term p}-attractor of a set of nodes.›

context ParityGame begin

text ‹We define the conditions for a node to be directly attracted from a given set.›
definition directly_attracted :: "Player ⇒ 'a set ⇒ 'a set" where
"directly_attracted p S ≡ {v ∈ V - S. ¬deadend v ∧
(v ∈ VV p   ⟶ (∃w. v→w ∧ w ∈ S))
∧ (v ∈ VV p** ⟶ (∀w. v→w ⟶ w ∈ S))}"

abbreviation "attractor_step p W S ≡ W ∪ S ∪ directly_attracted p S"

text ‹The ‹p›-attractor set of ‹W›, defined as a least fixed point.›
definition attractor :: "Player ⇒ 'a set ⇒ 'a set" where
"attractor p W = lfp (attractor_step p W)"

subsection ‹@{const directly_attracted}›

text ‹Show a few basic properties of @{const directly_attracted}.›
lemma directly_attracted_disjoint     [simp]: "directly_attracted p W ∩ W = {}"
and directly_attracted_empty        [simp]: "directly_attracted p {} = {}"
and directly_attracted_V_empty      [simp]: "directly_attracted p V = {}"
and directly_attracted_bounded_by_V [simp]: "directly_attracted p W ⊆ V"
and directly_attracted_contains_no_deadends [elim]: "v ∈ directly_attracted p W ⟹ ¬deadend v"
unfolding directly_attracted_def by blast+

subsection ‹‹attractor_step››

lemma attractor_step_empty: "attractor_step p {} {} = {}"
and attractor_step_bounded_by_V: "⟦ W ⊆ V; S ⊆ V ⟧ ⟹ attractor_step p W S ⊆ V"
by simp_all

text ‹
The definition of @{const attractor} uses @{const lfp}.  For this to be well-defined, we
need show that ‹attractor_step› is monotone.
›

lemma attractor_step_mono: "mono (attractor_step p W)"
unfolding directly_attracted_def by (rule monoI) auto

subsection ‹Basic Properties of an Attractor›

lemma attractor_unfolding: "attractor p W = attractor_step p W (attractor p W)"
unfolding attractor_def using attractor_step_mono lfp_unfold by blast
lemma attractor_lowerbound: "attractor_step p W S ⊆ S ⟹ attractor p W ⊆ S"
unfolding attractor_def using attractor_step_mono by (simp add: lfp_lowerbound)
lemma attractor_set_non_empty: "W ≠ {} ⟹ attractor p W ≠ {}"
and attractor_set_base: "W ⊆ attractor p W"
using attractor_unfolding by auto
lemma attractor_in_V: "W ⊆ V ⟹ attractor p W ⊆ V"
using attractor_lowerbound attractor_step_bounded_by_V by auto

subsection ‹Attractor Set Extensions›

lemma attractor_set_VVp:
assumes "v ∈ VV p" "v→w" "w ∈ attractor p W"
shows "v ∈ attractor p W"
apply (subst attractor_unfolding) unfolding directly_attracted_def using assms by auto

lemma attractor_set_VVpstar:
assumes "¬deadend v" "⋀w. v→w ⟹ w ∈ attractor p W"
shows "v ∈ attractor p W"
apply (subst attractor_unfolding) unfolding directly_attracted_def using assms by auto

subsection ‹Removing an Attractor›

lemma removing_attractor_induces_no_deadends:
assumes "v ∈ S - attractor p W" "v→w" "w ∈ S" "⋀w. ⟦ v ∈ VV p**; v→w ⟧ ⟹ w ∈ S"
shows "∃w ∈ S - attractor p W. v→w"
proof-
have "v ∈ V" using ‹v→w› by blast
thus ?thesis proof (cases rule: VV_cases)
assume "v ∈ VV p"
thus ?thesis using attractor_set_VVp assms by blast
next
assume "v ∈ VV p**"
thus ?thesis using attractor_set_VVpstar assms by (metis Diff_iff edges_are_in_V(2))
qed
qed

text ‹Removing the attractor sets of deadends leaves a subgame without deadends.›

lemma subgame_without_deadends:
assumes V'_def: "V' = V - attractor p (deadends p**) - attractor p** (deadends p****)"
(is "V' = V - ?A - ?B")
and v: "v ∈ V⇘subgame V'⇙"
shows "¬Digraph.deadend (subgame V') v"
proof (cases)
assume "deadend v"
have v: "v ∈ V - ?A - ?B" using v unfolding V'_def subgame_def by simp
{ fix p' assume "v ∈ VV p'**"
hence "v ∈ attractor p' (deadends p'**)"
using ‹deadend v› attractor_set_base[of "deadends p'**" p']
unfolding deadends_def by blast
hence False using v by (cases p'; cases p) auto
}
thus ?thesis using v by blast
next
assume "¬deadend v"
have v: "v ∈ V - ?A - ?B" using v unfolding V'_def subgame_def by simp
define G' where "G' = subgame V'"
interpret G': ParityGame G' unfolding G'_def using subgame_ParityGame .
show ?thesis proof
assume "Digraph.deadend (subgame V') v"
hence "G'.deadend v" unfolding G'_def .
have all_in_attractor: "⋀w. v→w ⟹ w ∈ ?A ∨ w ∈ ?B" proof (rule ccontr)
fix w
assume "v→w" "¬(w ∈ ?A ∨ w ∈ ?B)"
hence "w ∈ V'" unfolding V'_def by blast
hence "w ∈ V⇘G'⇙" unfolding G'_def subgame_def using ‹v→w› by auto
hence "v →⇘G'⇙ w" using ‹v→w› assms(2) unfolding G'_def subgame_def by auto
thus False using ‹G'.deadend v› using ‹w ∈ V⇘G'⇙› by blast
qed
{ fix p' assume "v ∈ VV p'"
{ assume "∃w. v→w ∧ w ∈ attractor p' (deadends p'**)"
hence "v ∈ attractor p' (deadends p'**)" using ‹v ∈ VV p'› attractor_set_VVp by blast
hence False using v by (cases p'; cases p) auto
}
hence "⋀w. v→w ⟹ w ∈ attractor p'** (deadends p'****)"
using all_in_attractor by (cases p'; cases p) auto
hence "v ∈ attractor p'** (deadends p'****)"
using ‹¬deadend v› ‹v ∈ VV p'› attractor_set_VVpstar by auto
hence False using v by (cases p'; cases p) auto
}
thus False using v by blast
qed
qed

subsection ‹Attractor Set Induction›

lemma mono_restriction_is_mono: "mono f ⟹ mono (λS. f (S ∩ V))"
unfolding mono_def by (meson inf_mono monoD subset_refl)

text ‹
Here we prove a powerful induction schema for @{term attractor}.  Being able to prove this is the
only reason why we do not use \texttt{inductive\_set} to define the attractor set.

See also \url{https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-October/msg00123.html}
›
lemma attractor_set_induction [consumes 1, case_names step union]:
assumes "W ⊆ V"
and step: "⋀S. S ⊆ V ⟹ P S ⟹ P (attractor_step p W S)"
and union: "⋀M. ∀S ∈ M. S ⊆ V ∧ P S ⟹ P (⋃M)"
shows "P (attractor p W)"
proof-
let ?P = "λS. P (S ∩ V)"
let ?f = "λS. attractor_step p W (S ∩ V)"
let ?A = "lfp ?f"
let ?B = "lfp (attractor_step p W)"
have f_mono: "mono ?f"
using mono_restriction_is_mono[of "attractor_step p W"] attractor_step_mono by simp
have P_A: "?P ?A" proof (rule lfp_ordinal_induct_set)
show "⋀S. ?P S ⟹ ?P (W ∪ (S ∩ V) ∪ directly_attracted p (S ∩ V))"
by (metis assms(1) attractor_step_bounded_by_V inf.absorb1 inf_le2 local.step)
show "⋀M. ∀S ∈ M. ?P S ⟹ ?P (⋃M)" proof-
fix M
let ?M = "{S ∩ V | S. S ∈ M}"
assume "∀S∈M. ?P S"
hence "∀S ∈ ?M. S ⊆ V ∧ P S" by auto
hence *: "P (⋃?M)" by (simp add: union)
have "⋃?M = (⋃M) ∩ V" by blast
thus "?P (⋃M)" using * by auto
qed
qed (insert f_mono)

have *: "W ∪ (V ∩ V) ∪ directly_attracted p (V ∩ V) ⊆ V"
using ‹W ⊆ V› attractor_step_bounded_by_V by auto
have "?A ⊆ V" "?B ⊆ V" using * by (simp_all add: lfp_lowerbound)

have "?A = ?f ?A" using f_mono lfp_unfold by blast
hence "?A = W ∪ (?A ∩ V) ∪ directly_attracted p (?A ∩ V)" using ‹?A ⊆ V› by simp
hence *: "attractor_step p W ?A ⊆ ?A" using ‹?A ⊆ V› inf.absorb1 by fastforce

have "?B = attractor_step p W ?B" using attractor_step_mono lfp_unfold by blast
hence "?f ?B ⊆ ?B" using ‹?B ⊆ V› by (metis (no_types, lifting) equalityD2 le_iff_inf)

have "?A = ?B" proof
show "?A ⊆ ?B" using ‹?f ?B ⊆ ?B› by (simp add: lfp_lowerbound)
show "?B ⊆ ?A" using * by (simp add: lfp_lowerbound)
qed
hence "?P ?B" using P_A by (simp add: attractor_def)
thus ?thesis using ‹?B ⊆ V› by (simp add: attractor_def le_iff_inf)
qed

end ― ‹context ParityGame›

end


Theory WinningStrategy

section ‹Winning Strategies›

theory WinningStrategy
imports
Main
Strategy
begin

context ParityGame begin

text ‹
Here we define winning strategies.

A strategy is winning for player @{term p} from @{term v0} if every maximal @{term σ}-path
starting in @{term v0} is winning.
›
definition winning_strategy :: "Player ⇒ 'a Strategy ⇒ 'a ⇒ bool" where
"winning_strategy p σ v0 ≡ ∀P. vmc_path G P v0 p σ ⟶ winning_path p P"

lemma winning_strategyI [intro]:
assumes "⋀P. vmc_path G P v0 p σ ⟹ winning_path p P"
shows "winning_strategy p σ v0"
unfolding winning_strategy_def using assms by blast

lemma (in vmc_path) paths_hits_winning_strategy_is_winning:
assumes σ: "winning_strategy p σ v"
and v: "v ∈ lset P"
shows "winning_path p P"
proof-
obtain n where n: "enat n < llength P" "P $n = v" using v by (meson in_lset_conv_lnth) interpret P': vmc_path G "ldropn n P" v p σ using n vmc_path_ldropn by blast have "winning_path p (ldropn n P)" using σ by (simp add: winning_strategy_def P'.vmc_path_axioms) thus ?thesis using winning_path_drop_add P_valid n(1) by blast qed text ‹There cannot exist winning strategies for both players for the same node.› lemma winning_strategy_only_for_one_player: assumes σ: "strategy p σ" "winning_strategy p σ v" and σ': "strategy p** σ'" "winning_strategy p** σ' v" and v: "v ∈ V" shows "False" proof- obtain P where "vmc2_path G P v p σ σ'" using assms strategy_conforming_path_exists by blast then interpret vmc2_path G P v p σ σ' . have "winning_path p P" using paths_hits_winning_strategy_is_winning σ(2) v0_lset_P by blast moreover have "winning_path p** P" using comp.paths_hits_winning_strategy_is_winning σ'(2) v0_lset_P by blast ultimately show False using P_valid paths_are_winning_for_one_player by blast qed subsection ‹Deadends› lemma no_winning_strategy_on_deadends: assumes "v ∈ VV p" "deadend v" "strategy p σ" shows "¬winning_strategy p σ v" proof- obtain P where "vmc_path G P v p σ" using strategy_conforming_path_exists_single assms by blast then interpret vmc_path G P v p σ . have "P = LCons v LNil" using P_deadend_v0_LCons ‹deadend v› by blast hence "¬winning_path p P" unfolding winning_path_def using ‹v ∈ VV p› by auto thus ?thesis using winning_strategy_def vmc_path_axioms by blast qed lemma winning_strategy_on_deadends: assumes "v ∈ VV p" "deadend v" "strategy p σ" shows "winning_strategy p** σ v" proof fix P assume "vmc_path G P v p** σ" then interpret vmc_path G P v "p**" σ . have "P = LCons v LNil" using P_deadend_v0_LCons ‹deadend v› by blast thus "winning_path p** P" unfolding winning_path_def using ‹v ∈ VV p› P_valid paths_are_winning_for_one_player by auto qed subsection ‹Extension Theorems› lemma strategy_extends_VVp: assumes v0: "v0 ∈ VV p" "¬deadend v0" and σ: "strategy p σ" "winning_strategy p σ v0" shows "winning_strategy p σ (σ v0)" proof fix P assume "vmc_path G P (σ v0) p σ" then interpret vmc_path G P "σ v0" p σ . have "v0→σ v0" using v0 σ(1) strategy_def by blast hence "winning_path p (LCons v0 P)" using σ(2) extension_valid_maximal_conforming winning_strategy_def by blast thus "winning_path p P" using winning_path_ltl[of p "LCons v0 P"] by simp qed lemma strategy_extends_VVpstar: assumes v0: "v0 ∈ VV p**" "v0→w0" and σ: "winning_strategy p σ v0" shows "winning_strategy p σ w0" proof fix P assume "vmc_path G P w0 p σ" then interpret vmc_path G P w0 p σ . have "winning_path p (LCons v0 P)" using extension_valid_maximal_conforming VV_impl1 σ v0 winning_strategy_def by auto thus "winning_path p P" using winning_path_ltl[of p "LCons v0 P"] by auto qed lemma strategy_extends_backwards_VVpstar: assumes v0: "v0 ∈ VV p**" and σ: "strategy p σ" "⋀w. v0→w ⟹ winning_strategy p σ w" shows "winning_strategy p σ v0" proof fix P assume "vmc_path G P v0 p σ" then interpret vmc_path G P v0 p σ . show "winning_path p P" proof (cases) assume "deadend v0" thus ?thesis using P_deadend_v0_LCons winning_path_def v0 by auto next assume "¬deadend v0" then interpret vmc_path_no_deadend G P v0 p σ by unfold_locales interpret ltlP: vmc_path G "ltl P" w0 p σ using vmc_path_ltl . have "winning_path p (ltl P)" using σ(2) v0_edge_w0 vmc_path_ltl winning_strategy_def by blast thus "winning_path p P" using winning_path_LCons by (metis P_LCons' ltlP.P_LCons ltlP.P_not_null) qed qed lemma strategy_extends_backwards_VVp: assumes v0: "v0 ∈ VV p" "σ v0 = w" "v0→w" and σ: "strategy p σ" "winning_strategy p σ w" shows "winning_strategy p σ v0" proof fix P assume "vmc_path G P v0 p σ" then interpret vmc_path G P v0 p σ . have "¬deadend v0" using ‹v0→w› by blast then interpret vmc_path_no_deadend G P v0 p σ by unfold_locales have "winning_path p (ltl P)" using σ(2)[unfolded winning_strategy_def] v0(1,2) v0_conforms vmc_path_ltl by presburger thus "winning_path p P" using winning_path_LCons by (metis P_LCons Ptl_not_null) qed end ― ‹context ParityGame› end  Theory WellOrderedStrategy section ‹Well-Ordered Strategy› theory WellOrderedStrategy imports Main Strategy begin text ‹ Constructing a uniform strategy from a set of strategies on a set of nodes often works by well-ordering the strategies and then choosing the minimal strategy on each node. Then every path eventually follows one strategy because we choose the strategies along the path to be non-increasing in the well-ordering. The following locale formalizes this idea. We will use this to construct uniform attractor and winning strategies. › locale WellOrderedStrategies = ParityGame + fixes S :: "'a set" and p :: Player ― ‹The set of good strategies on a node @{term v}› and good :: "'a ⇒ 'a Strategy set" and r :: "('a Strategy × 'a Strategy) set" assumes S_V: "S ⊆ V" ― ‹@{term r} is a wellorder on the set of all strategies which are good somewhere.› and r_wo: "well_order_on {σ. ∃v ∈ S. σ ∈ good v} r" ― ‹Every node has a good strategy.› and good_ex: "⋀v. v ∈ S ⟹ ∃σ. σ ∈ good v" ― ‹good strategies are well-formed strategies.› and good_strategies: "⋀v σ. σ ∈ good v ⟹ strategy p σ" ― ‹A good strategy on @{term v} is also good on possible successors of @{term v}.› and strategies_continue: "⋀v w σ. ⟦ v ∈ S; v→w; v ∈ VV p ⟹ σ v = w; σ ∈ good v ⟧ ⟹ σ ∈ good w" begin text ‹The set of all strategies which are good somewhere.› abbreviation "Strategies ≡ {σ. ∃v ∈ S. σ ∈ good v}" definition minimal_good_strategy where "minimal_good_strategy v σ ≡ σ ∈ good v ∧ (∀σ'. (σ', σ) ∈ r - Id ⟶ σ' ∉ good v)" no_notation binomial (infixl "choose" 65) text ‹Among the good strategies on @{term v}, choose the minimum.› definition choose where "choose v ≡ THE σ. minimal_good_strategy v σ" text ‹ Define a strategy which uses the minimum strategy on all nodes of @{term S}. Of course, we need to prove that this is a well-formed strategy. › definition well_ordered_strategy where "well_ordered_strategy ≡ override_on σ_arbitrary (λv. choose v v) S" text ‹Show some simple properties of the binary relation @{term r} on the set @{const Strategies}.› lemma r_refl [simp]: "refl_on Strategies r" using r_wo unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by blast lemma r_total [simp]: "total_on Strategies r" using r_wo unfolding well_order_on_def linear_order_on_def by blast lemma r_trans [simp]: "trans r" using r_wo unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by blast lemma r_wf [simp]: "wf (r - Id)" using well_order_on_def r_wo by blast text ‹@{const choose} always chooses a minimal good strategy on @{term S}.› lemma choose_works: assumes "v ∈ S" shows "minimal_good_strategy v (choose v)" proof- have wf: "wf (r - Id)" using well_order_on_def r_wo by blast obtain σ where σ1: "minimal_good_strategy v σ" unfolding minimal_good_strategy_def by (meson good_ex[OF ‹v ∈ S›] wf wf_eq_minimal) hence σ: "σ ∈ good v" "⋀σ'. (σ', σ) ∈ r - Id ⟹ σ' ∉ good v" unfolding minimal_good_strategy_def by auto { fix σ' assume "minimal_good_strategy v σ'" hence σ': "σ' ∈ good v" "⋀σ. (σ, σ') ∈ r - Id ⟹ σ ∉ good v" unfolding minimal_good_strategy_def by auto have "(σ, σ') ∉ r - Id" using σ(1) σ'(2) by blast moreover have "(σ', σ) ∉ r - Id" using σ(2) σ'(1) by auto moreover have "σ ∈ Strategies" using σ(1) ‹v ∈ S› by auto moreover have "σ' ∈ Strategies" using σ'(1) ‹v ∈ S› by auto ultimately have "σ' = σ" using r_wo Linear_order_in_diff_Id well_order_on_Field well_order_on_def by fastforce } with σ1 have "∃!σ. minimal_good_strategy v σ" by blast thus ?thesis using theI'[of "minimal_good_strategy v", folded choose_def] by blast qed corollary assumes "v ∈ S" shows choose_good: "choose v ∈ good v" and choose_minimal: "⋀σ'. (σ', choose v) ∈ r - Id ⟹ σ' ∉ good v" and choose_strategy: "strategy p (choose v)" using choose_works[OF assms, unfolded minimal_good_strategy_def] good_strategies by blast+ corollary choose_in_Strategies: "v ∈ S ⟹ choose v ∈ Strategies" using choose_good by blast lemma well_ordered_strategy_valid: "strategy p well_ordered_strategy" proof- { fix v assume "v ∈ S" "v ∈ VV p" "¬deadend v" moreover have "strategy p (choose v)" using choose_works[OF ‹v ∈ S›, unfolded minimal_good_strategy_def, THEN conjunct1] good_strategies by blast ultimately have "v→(λv. choose v v) v" using strategy_def by blast } thus ?thesis unfolding well_ordered_strategy_def using valid_strategy_updates_set by force qed subsection ‹Strategies on a Path› text ‹Maps a path to its strategies.› definition "path_strategies ≡ lmap choose" lemma path_strategies_in_Strategies: assumes "lset P ⊆ S" shows "lset (path_strategies P) ⊆ Strategies" using path_strategies_def assms choose_in_Strategies by auto lemma path_strategies_good: assumes "lset P ⊆ S" "enat n < llength P" shows "path_strategies P$ n ∈ good (P $n)" by (simp add: path_strategies_def assms choose_good lset_lnth_member) lemma path_strategies_strategy: assumes "lset P ⊆ S" "enat n < llength P" shows "strategy p (path_strategies P$ n)"
using path_strategies_good assms good_strategies by blast

lemma path_strategies_monotone_Suc:
assumes P: "lset P ⊆ S" "valid_path P" "path_conforms_with_strategy p P well_ordered_strategy"
"enat (Suc n) < llength P"
shows "(path_strategies P $Suc n, path_strategies P$ n) ∈ r"
proof-
define P' where "P' = ldropn n P"
hence "enat (Suc 0) < llength P'" using P(4)
by (metis enat_ltl_Suc ldrop_eSuc_ltl ldropn_Suc_conv_ldropn llist.disc(2) lnull_0_llength ltl_ldropn)
then obtain v w Ps where vw: "P' = LCons v (LCons w Ps)"
by (metis ldropn_0 ldropn_Suc_conv_ldropn ldropn_lnull lnull_0_llength)
moreover have "lset P' ⊆ S" unfolding P'_def using P(1) lset_ldropn_subset[of n P] by blast
ultimately have "v ∈ S" "w ∈ S" by auto
moreover have "v→w" using valid_path_edges'[of v w Ps, folded vw] valid_path_drop[OF P(2)] P'_def by blast
moreover have "choose v ∈ good v" using choose_good ‹v ∈ S› by blast
moreover have "v ∈ VV p ⟹ choose v v = w" proof-
assume "v ∈ VV p"
moreover have "path_conforms_with_strategy p P' well_ordered_strategy"
unfolding P'_def using path_conforms_with_strategy_drop P(3) by blast
ultimately have "well_ordered_strategy v = w" using vw path_conforms_with_strategy_start by blast
thus "choose v v = w" unfolding well_ordered_strategy_def using ‹v ∈ S› by auto
qed
ultimately have "choose v ∈ good w" using strategies_continue by blast
hence *: "(choose v, choose w) ∉ r - Id" using choose_minimal ‹w ∈ S› by blast

have "(choose w, choose v) ∈ r" proof (cases)
assume "choose v = choose w"
thus ?thesis using r_refl refl_onD choose_in_Strategies[OF ‹v ∈ S›] by fastforce
next
assume "choose v ≠ choose w"
thus ?thesis using * r_total choose_in_Strategies[OF ‹v ∈ S›] choose_in_Strategies[OF ‹w ∈ S›]
by (metis (lifting) Linear_order_in_diff_Id r_wo well_order_on_Field well_order_on_def)
qed
hence "(path_strategies P' $Suc 0, path_strategies P'$ 0) ∈ r"
unfolding path_strategies_def using vw by simp
thus ?thesis unfolding path_strategies_def P'_def
using lnth_lmap_ldropn[OF Suc_llength[OF P(4)], of choose]
lnth_lmap_ldropn_Suc[OF P(4), of choose]
by simp
qed

lemma path_strategies_monotone:
assumes P: "lset P ⊆ S" "valid_path P" "path_conforms_with_strategy p P well_ordered_strategy"
"n < m" "enat m < llength P"
shows "(path_strategies P $m, path_strategies P$ n) ∈ r"
using assms proof (induct "m - n" arbitrary: n m)
case (Suc d)
show ?case proof (cases)
assume "d = 0"
thus ?thesis using path_strategies_monotone_Suc[OF P(1,2,3)]
by (metis (no_types) Suc.hyps(2) Suc.prems(4,5) Suc_diff_Suc Suc_inject Suc_leI diff_is_0_eq diffs0_imp_equal)
next
assume "d ≠ 0"
have "m ≠ 0" using Suc.hyps(2) by linarith
then obtain m' where m': "Suc m' = m" using not0_implies_Suc by blast
hence "d = m' - n" using Suc.hyps(2) by presburger
moreover hence "n < m'" using ‹d ≠ 0› by presburger
ultimately have "(path_strategies P $m', path_strategies P$ n) ∈ r"
using Suc.hyps(1)[of m' n, OF _ P(1,2,3)] Suc.prems(5) dual_order.strict_trans enat_ord_simps(2) m'
by blast
thus ?thesis
using m' path_strategies_monotone_Suc[OF P(1,2,3)] by (metis (no_types) Suc.prems(5) r_trans trans_def)
qed
qed simp

lemma path_strategies_eventually_constant:
assumes "¬lfinite P" "lset P ⊆ S" "valid_path P" "path_conforms_with_strategy p P well_ordered_strategy"
shows "∃n. ∀m ≥ n. path_strategies P $n = path_strategies P$ m"
proof-
define σ_set where "σ_set = lset (path_strategies P)"
have "∃σ. σ ∈ σ_set" unfolding σ_set_def path_strategies_def
using assms(1) lfinite_lmap lset_nth_member_inf by blast
then obtain σ' where σ': "σ' ∈ σ_set" "⋀τ. (τ, σ') ∈ r - Id ⟹ τ ∉ σ_set"
using wfE_min[of "r - Id" _ σ_set] by auto
obtain n where n: "path_strategies P $n = σ'" using σ'(1) lset_lnth[of σ'] unfolding σ_set_def by blast { fix m assume "n ≤ m" have "path_strategies P$ n = path_strategies P $m" proof (rule ccontr) assume *: "path_strategies P$ n ≠ path_strategies P $m" with ‹n ≤ m› have "n < m" using le_imp_less_or_eq by blast with path_strategies_monotone have "(path_strategies P$ m, path_strategies P $n) ∈ r" using assms by (simp add: infinite_small_llength) with * have "(path_strategies P$ m, path_strategies P $n) ∈ r - Id" by simp with σ'(2) n have "path_strategies P$ m ∉ σ_set" by blast
thus False unfolding σ_set_def path_strategies_def
using assms(1) lfinite_lmap lset_nth_member_inf by blast
qed
}
thus ?thesis by blast
qed

subsection ‹Eventually One Strategy›

text ‹
The key lemma: Every path that stays in @{term S} and follows @{const well_ordered_strategy}
eventually follows one strategy because the strategies are well-ordered and non-increasing
along the path.
›

lemma path_eventually_conforms_to_σ_map_n:
assumes "lset P ⊆ S" "valid_path P" "path_conforms_with_strategy p P well_ordered_strategy"
shows "∃n. path_conforms_with_strategy p (ldropn n P) (path_strategies P $n)" proof (cases) assume "lfinite P" then obtain n where "llength P = enat n" using lfinite_llength_enat by blast hence "ldropn n P = LNil" by simp thus ?thesis by (metis path_conforms_LNil) next assume "¬lfinite P" then obtain n where n: "⋀m. n ≤ m ⟹ path_strategies P$ n = path_strategies P $m" using path_strategies_eventually_constant assms by blast let ?σ = well_ordered_strategy define P' where "P' = ldropn n P" { fix v assume "v ∈ lset P'" hence "v ∈ S" using ‹lset P ⊆ S› P'_def in_lset_ldropnD by fastforce from ‹v ∈ lset P'› obtain m where m: "enat m < llength P'" "P'$ m = v" by (meson in_lset_conv_lnth)
hence "P $m + n = v" unfolding P'_def by (simp add: ‹¬lfinite P› infinite_small_llength) moreover have "?σ v = choose v v" unfolding well_ordered_strategy_def using ‹v ∈ S› by auto ultimately have "?σ v = (path_strategies P$ m + n) v"
unfolding path_strategies_def using infinite_small_llength[OF ‹¬lfinite P›] by simp
hence "?σ v = (path_strategies P $n) v" using n[of "m + n"] by simp } moreover have "path_conforms_with_strategy p P' well_ordered_strategy" unfolding P'_def by (simp add: assms(3) path_conforms_with_strategy_drop) ultimately show ?thesis using path_conforms_with_strategy_irrelevant_updates P'_def by blast qed end ― ‹WellOrderedStrategies› end  Theory WinningRegion section ‹Winning Regions› theory WinningRegion imports Main WinningStrategy begin text ‹ Here we define winning regions of parity games. The winning region for player ‹p› is the set of nodes from which ‹p› has a positional winning strategy. › context ParityGame begin definition "winning_region p ≡ { v ∈ V. ∃σ. strategy p σ ∧ winning_strategy p σ v }" lemma winning_regionI [intro]: assumes "v ∈ V" "strategy p σ" "winning_strategy p σ v" shows "v ∈ winning_region p" using assms unfolding winning_region_def by blast lemma winning_region_in_V [simp]: "winning_region p ⊆ V" unfolding winning_region_def by blast lemma winning_region_deadends: assumes "v ∈ VV p" "deadend v" shows "v ∈ winning_region p**" proof show "v ∈ V" using ‹v ∈ VV p› by blast show "winning_strategy p** σ_arbitrary v" using assms winning_strategy_on_deadends by simp qed simp subsection ‹Paths in Winning Regions› lemma (in vmc_path) paths_stay_in_winning_region: assumes σ': "strategy p σ'" "winning_strategy p σ' v0" and σ: "⋀v. v ∈ winning_region p ⟹ σ' v = σ v" shows "lset P ⊆ winning_region p" proof fix x assume "x ∈ lset P" thus "x ∈ winning_region p" using assms vmc_path_axioms proof (induct arbitrary: v0 rule: llist_set_induct) case (find P v0) interpret vmc_path G P v0 p σ using find.prems(4) . show ?case using P_v0 σ'(1) find.prems(2) v0_V unfolding winning_region_def by blast next case (step P x v0) interpret vmc_path G P v0 p σ using step.prems(4) . show ?case proof (cases) assume "lnull (ltl P)" thus ?thesis using P_lnull_ltl_LCons step.hyps(2) by auto next assume "¬lnull (ltl P)" then interpret vmc_path_no_deadend G P v0 p σ using P_no_deadend_v0 by unfold_locales have "winning_strategy p σ' w0" proof (cases) assume "v0 ∈ VV p" hence "winning_strategy p σ' (σ' v0)" using strategy_extends_VVp local.step(4) step.prems(2) v0_no_deadend by blast moreover have "σ v0 = w0" using v0_conforms ‹v0 ∈ VV p› by blast moreover have "σ' v0 = σ v0" using σ assms(1) step.prems(2) v0_V unfolding winning_region_def by blast ultimately show ?thesis by simp next assume "v0 ∉ VV p" thus ?thesis using v0_V strategy_extends_VVpstar step(4) step.prems(2) by simp qed thus ?thesis using step.hyps(3) step(4) σ vmc_path_ltl by blast qed qed qed lemma (in vmc_path) path_hits_winning_region_is_winning: assumes σ': "strategy p σ'" "⋀v. v ∈ winning_region p ⟹ winning_strategy p σ' v" and σ: "⋀v. v ∈ winning_region p ⟹ σ' v = σ v" and P: "lset P ∩ winning_region p ≠ {}" shows "winning_path p P" proof- obtain n where n: "enat n < llength P" "P$ n ∈ winning_region p"
using P by (meson lset_intersect_lnth)
define P' where "P' = ldropn n P"
then interpret P': vmc_path G P' "P $n" p σ unfolding P'_def using vmc_path_ldropn n(1) by blast have "winning_strategy p σ' (P$ n)" using σ'(2) n(2) by blast
hence "lset P' ⊆ winning_region p"
using P'.paths_stay_in_winning_region[OF σ'(1) _ σ]
by blast
hence "⋀v. v ∈ lset P' ⟹ σ v = σ' v" using σ by auto
hence "path_conforms_with_strategy p P' σ'"
using path_conforms_with_strategy_irrelevant_updates P'.P_conforms
by blast
then interpret P': vmc_path G P' "P $n" p σ' using P'.conforms_to_another_strategy by blast have "winning_path p P'" using σ'(2) n(2) P'.vmc_path_axioms winning_strategy_def by blast thus "winning_path p P" unfolding P'_def using winning_path_drop_add n(1) P_valid by blast qed subsection ‹Irrelevant Updates› text ‹Updating a winning strategy outside of the winning region is irrelevant.› lemma winning_strategy_updates: assumes σ: "strategy p σ" "winning_strategy p σ v0" and v: "v ∉ winning_region p" "v→w" shows "winning_strategy p (σ(v := w)) v0" proof fix P assume "vmc_path G P v0 p (σ(v := w))" then interpret vmc_path G P v0 p "σ(v := w)" . have "⋀v'. v' ∈ winning_region p ⟹ σ v' = (σ(v := w)) v'" using v by auto hence "v ∉ lset P" using v paths_stay_in_winning_region σ unfolding winning_region_def by blast hence "path_conforms_with_strategy p P σ" using P_conforms path_conforms_with_strategy_irrelevant' by blast thus "winning_path p P" using conforms_to_another_strategy σ(2) winning_strategy_def by blast qed subsection ‹Extending Winning Regions› lemma winning_region_extends_VVp: assumes v: "v ∈ VV p" "v→w" and w: "w ∈ winning_region p" shows "v ∈ winning_region p" proof (rule ccontr) obtain σ where σ: "strategy p σ" "winning_strategy p σ w" using w unfolding winning_region_def by blast let ?σ = "σ(v := w)" assume contra: "v ∉ winning_region p" moreover have "strategy p ?σ" using valid_strategy_updates σ(1) ‹v→w› by blast moreover hence "winning_strategy p ?σ v" using winning_strategy_updates σ contra v strategy_extends_backwards_VVp by auto ultimately show False using ‹v→w› unfolding winning_region_def by auto qed text ‹ Unfortunately, we cannot prove the corresponding theorem ‹winning_region_extends_VVpstar› for @{term "VV p**"}-nodes yet. First, we need to show that there exists a uniform winning strategy on @{term "winning_region p"}. We will prove ‹winning_region_extends_VVpstar› as soon as we have this. › end ― ‹context ParityGame› end  Theory UniformStrategy section ‹Uniform Strategies› text ‹Theorems about how to get a uniform strategy given strategies for each node.› theory UniformStrategy imports Main AttractingStrategy WinningStrategy WellOrderedStrategy WinningRegion begin context ParityGame begin subsection ‹A Uniform Attractor Strategy› lemma merge_attractor_strategies: assumes "S ⊆ V" and strategies_ex: "⋀v. v ∈ S ⟹ ∃σ. strategy p σ ∧ strategy_attracts_via p σ v S W" shows "∃σ. strategy p σ ∧ strategy_attracts p σ S W" proof- define good where "good v = {σ. strategy p σ ∧ strategy_attracts_via p σ v S W }" for v let ?G = "{σ. ∃v ∈ S - W. σ ∈ good v}" obtain r where r: "well_order_on ?G r" using well_order_on by blast interpret WellOrderedStrategies G "S - W" p good r proof show "S - W ⊆ V" using ‹S ⊆ V› by blast next show "⋀v. v ∈ S - W ⟹ ∃σ. σ ∈ good v" unfolding good_def using strategies_ex by blast next show "⋀v σ. σ ∈ good v ⟹ strategy p σ" unfolding good_def by blast next fix v w σ assume v: "v ∈ S - W" "v→w" "v ∈ VV p ⟹ σ v = w" "σ ∈ good v" hence σ: "strategy p σ" "strategy_attracts_via p σ v S W" unfolding good_def by simp_all hence "strategy_attracts_via p σ w S W" using strategy_attracts_via_successor v by blast thus "σ ∈ good w" unfolding good_def using σ(1) by blast qed (insert r) have S_W_no_deadends: "⋀v. v ∈ S - W ⟹ ¬deadend v" using strategy_attracts_via_no_deadends[of _ S W] strategies_ex by (metis (no_types) Diff_iff S_V rev_subsetD) { fix v0 assume "v0 ∈ S" fix P assume P: "vmc_path G P v0 p well_ordered_strategy" then interpret vmc_path G P v0 p well_ordered_strategy . have "visits_via P S W" proof (rule ccontr) assume contra: "¬visits_via P S W" hence "lset P ⊆ S - W" proof (induct rule: vmc_path_lset_induction) case base show "v0 ∈ S - W" using ‹v0 ∈ S› contra visits_via_trivial by blast next case (step P v0) interpret vmc_path_no_deadend G P v0 p well_ordered_strategy using step.hyps(1) . have "insert v0 S = S" using step.hyps(2) by blast hence *: "¬visits_via (ltl P) S W" using visits_via_LCons[of "ltl P" S W v0, folded P_LCons] step.hyps(3) by auto hence **: "w0 ∉ W" using vmc_path.visits_via_trivial[OF vmc_path_ltl] by blast have "w0 ∈ S ∪ W" proof (cases) assume "v0 ∈ VV p" hence "well_ordered_strategy v0 = w0" using v0_conforms by blast hence "choose v0 v0 = w0" using step.hyps(2) well_ordered_strategy_def by auto moreover have "strategy_attracts_via p (choose v0) v0 S W" using choose_good good_def step.hyps(2) by blast ultimately show ?thesis by (metis strategy_attracts_via_successor strategy_attracts_via_v0 choose_strategy step.hyps(2) v0_edge_w0 w0_V) qed (metis DiffD1 assms(2) step.hyps(2) strategy_attracts_via_successor strategy_attracts_via_v0 v0_edge_w0 w0_V) with * ** show ?case by blast qed have "¬lfinite P" proof assume "lfinite P" hence "deadend (llast P)" using P_maximal P_not_null maximal_ends_on_deadend by blast moreover have "llast P ∈ S - W" using ‹lset P ⊆ S - W› P_not_null ‹lfinite P› lfinite_lset by blast ultimately show False using S_W_no_deadends by blast qed obtain n where n: "path_conforms_with_strategy p (ldropn n P) (path_strategies P$ n)"
using path_eventually_conforms_to_σ_map_n[OF ‹lset P ⊆ S - W› P_valid P_conforms]
by blast
define σ' where [simp]: "σ' = path_strategies P $n" define P' where [simp]: "P' = ldropn n P" interpret vmc_path G P' "lhd P'" p σ' proof show "¬lnull P'" unfolding P'_def using ‹¬lfinite P› lfinite_ldropn lnull_imp_lfinite by blast qed (simp_all add: n) have "strategy p σ'" unfolding σ'_def using path_strategies_strategy ‹lset P ⊆ S - W› ‹¬lfinite P› infinite_small_llength by blast moreover have "strategy_attracts_via p σ' (lhd P') S W" proof- have "P$ n ∈ S - W" using ‹lset P ⊆ S - W› ‹¬lfinite P› lset_nth_member_inf by blast
hence "σ' ∈ good (P $n)" using path_strategies_good σ'_def ‹¬lfinite P› ‹lset P ⊆ S - W› by blast hence "strategy_attracts_via p σ' (P$ n) S W" unfolding good_def by blast
thus ?thesis unfolding P'_def using P_0 by (simp add: ‹¬lfinite P› infinite_small_llength)
qed
moreover from ‹lset P ⊆ S - W› have "lset P' ⊆ S - W"
unfolding P'_def using lset_ldropn_subset[of n P] by blast
ultimately show False using strategy_attracts_via_lset by blast
qed
}
thus ?thesis using well_ordered_strategy_valid by blast
qed

subsection ‹A Uniform Winning Strategy›

text ‹
Let @{term S} be the winning region of player @{term p}.
Then there exists a uniform winning strategy on @{term S}.
›

lemma merge_winning_strategies:
shows "∃σ. strategy p σ ∧ (∀v ∈ winning_region p. winning_strategy p σ v)"
proof-
define good where "good v = {σ. strategy p σ ∧ winning_strategy p σ v}" for v
let ?G = "{σ. ∃v ∈ winning_region p. σ ∈ good v}"
obtain r where r: "well_order_on ?G r" using well_order_on by blast

have no_VVp_deadends: "⋀v. ⟦ v ∈ winning_region p; v ∈ VV p ⟧ ⟹ ¬deadend v"
using no_winning_strategy_on_deadends unfolding winning_region_def by blast

interpret WellOrderedStrategies G "winning_region p" p good r proof
show "⋀v. v ∈ winning_region p ⟹ ∃σ. σ ∈ good v"
unfolding good_def winning_region_def by blast
next
show "⋀v σ. σ ∈ good v ⟹ strategy p σ" unfolding good_def by blast
next
fix v w σ assume v: "v ∈ winning_region p" "v→w" "v ∈ VV p ⟹ σ v = w" "σ ∈ good v"
hence σ: "strategy p σ" "winning_strategy p σ v" unfolding good_def by simp_all
hence "winning_strategy p σ w" proof (cases)
assume *: "v ∈ VV p"
hence **: "σ v = w" using v(3) by blast
have "¬deadend v" using no_VVp_deadends ‹v ∈ VV p› v(1) by blast
with * ** show ?thesis using strategy_extends_VVp σ by blast
next
assume "v ∉ VV p"
thus ?thesis using strategy_extends_VVpstar σ ‹v→w› by blast
qed
thus "σ ∈ good w" unfolding good_def using σ(1) by blast
qed (insert winning_region_in_V r)

{
fix v0 assume "v0 ∈ winning_region p"
fix P assume P: "vmc_path G P v0 p well_ordered_strategy"
then interpret vmc_path G P v0 p well_ordered_strategy .

have "lset P ⊆ winning_region p" proof (induct rule: vmc_path_lset_induction_simple)
case (step P v0)
interpret vmc_path_no_deadend G P v0 p well_ordered_strategy using step.hyps(1) .
{ assume "v0 ∈ VV p"
hence "well_ordered_strategy v0 = w0" using v0_conforms by blast
hence "choose v0 v0 = w0" by (simp add: step.hyps(2) well_ordered_strategy_def)
}
hence "choose v0 ∈ good w0" using strategies_continue choose_good step.hyps(2) by simp
thus ?case unfolding good_def winning_region_def using w0_V by blast
qed (insert ‹v0 ∈ winning_region p›)

have "winning_path p P" proof (rule ccontr)
assume contra: "¬winning_path p P"

have "¬lfinite P" proof
assume "lfinite P"
hence "deadend (llast P)" using maximal_ends_on_deadend by simp
moreover have "llast P ∈ winning_region p"
using ‹lset P ⊆ winning_region p› P_not_null ‹lfinite P› lfinite_lset by blast
moreover have "llast P ∈ VV p"
using contra paths_are_winning_for_one_player ‹lfinite P›
unfolding winning_path_def by simp
ultimately show False using no_VVp_deadends by blast
qed

obtain n where n: "path_conforms_with_strategy p (ldropn n P) (path_strategies P $n)" using path_eventually_conforms_to_σ_map_n[OF ‹lset P ⊆ winning_region p› P_valid P_conforms] by blast define σ' where [simp]: "σ' = path_strategies P$ n"
define P' where [simp]: "P' = ldropn n P"
interpret P': vmc_path G P' "lhd P'" p σ' proof
show "¬lnull P'" using ‹¬lfinite P› unfolding P'_def
using lfinite_ldropn lnull_imp_lfinite by blast
qed (simp_all add: n)
have "strategy p σ'" unfolding σ'_def
using path_strategies_strategy ‹lset P ⊆ winning_region p› ‹¬lfinite P› by blast
moreover have "winning_strategy p σ' (lhd P')" proof-
have "P $n ∈ winning_region p" using ‹lset P ⊆ winning_region p› ‹¬lfinite P› lset_nth_member_inf by blast hence "σ' ∈ good (P$ n)"
using path_strategies_good choose_good σ'_def ‹¬lfinite P› ‹lset P ⊆ winning_region p›
by blast
hence "winning_strategy p σ' (P $n)" unfolding good_def by blast thus ?thesis unfolding P'_def using P_0 ‹¬lfinite P› by (simp add: infinite_small_llength lhd_ldropn) qed ultimately have "winning_path p P'" unfolding winning_strategy_def using P'.vmc_path_axioms by blast moreover have "¬lfinite P'" using ‹¬lfinite P› P'_def by simp ultimately show False using contra winning_path_drop_add[OF P_valid] by auto qed } thus ?thesis unfolding winning_strategy_def using well_ordered_strategy_valid by auto qed subsection ‹Extending Winning Regions› text ‹ Now we are finally able to prove the complement of ‹winning_region_extends_VVp› for @{term "VV p**"} nodes, which was still missing. › lemma winning_region_extends_VVpstar: assumes v: "v ∈ VV p**" and w: "⋀w. v→w ⟹ w ∈ winning_region p" shows "v ∈ winning_region p" proof- obtain σ where σ: "strategy p σ" "⋀v. v ∈ winning_region p ⟹ winning_strategy p σ v" using merge_winning_strategies by blast have "winning_strategy p σ v" using strategy_extends_backwards_VVpstar[OF v σ(1)] σ(2) w by blast thus ?thesis unfolding winning_region_def using v σ(1) by blast qed text ‹It immediately follows that removing a winning region cannot create new deadends.› lemma removing_winning_region_induces_no_deadends: assumes "v ∈ V - winning_region p" "¬deadend v" shows "∃w ∈ V - winning_region p. v→w" using assms winning_region_extends_VVp winning_region_extends_VVpstar by blast end ― ‹context ParityGame› end  Theory AttractorStrategy section ‹Attractor Strategies› theory AttractorStrategy imports Main Attractor UniformStrategy begin text ‹This section proves that every attractor set has an attractor strategy.› context ParityGame begin lemma strategy_attracts_extends_VVp: assumes σ: "strategy p σ" "strategy_attracts p σ S W" and v0: "v0 ∈ VV p" "v0 ∈ directly_attracted p S" "v0 ∉ S" shows "∃σ. strategy p σ ∧ strategy_attracts_via p σ v0 (insert v0 S) W" proof- from v0(1,2) obtain w where "v0→w" "w ∈ S" using directly_attracted_def by blast from ‹w ∈ S› σ(2) have "strategy_attracts_via p σ w S W" unfolding strategy_attracts_def by blast let ?σ = "σ(v0 := w)" ― ‹Extend @{term σ} to the new node.› have "strategy p ?σ" using σ(1) ‹v0→w› valid_strategy_updates by blast moreover have "strategy_attracts_via p ?σ v0 (insert v0 S) W" proof fix P assume "vmc_path G P v0 p ?σ" then interpret vmc_path G P v0 p ?σ . have "¬deadend v0" using ‹v0→w› by blast then interpret vmc_path_no_deadend G P v0 p ?σ by unfold_locales define P'' where [simp]: "P'' = ltl P" have "lhd P'' = w" using v0(1) v0_conforms w0_def by auto hence "vmc_path G P'' w p ?σ" using vmc_path_ltl by (simp add: w0_def) have *: "v0 ∉ S - W" using ‹v0 ∉ S› by blast have "override_on (σ(v0 := w)) σ (S - W) = ?σ" by (rule ext) (metis * fun_upd_def override_on_def) hence "strategy_attracts p ?σ S W" using strategy_attracts_irrelevant_override[OF σ(2,1) ‹strategy p ?σ›] by simp hence "strategy_attracts_via p ?σ w S W" unfolding strategy_attracts_def using ‹w ∈ S› by blast hence "visits_via P'' S W" unfolding strategy_attracts_via_def using ‹vmc_path G P'' w p ?σ› by blast thus "visits_via P (insert v0 S) W" using visits_via_LCons[of "ltl P" S W v0] P_LCons by simp qed ultimately show ?thesis by blast qed lemma strategy_attracts_extends_VVpstar: assumes σ: "strategy_attracts p σ S W" and v0: "v0 ∉ VV p" "v0 ∈ directly_attracted p S" shows "strategy_attracts_via p σ v0 (insert v0 S) W" proof fix P assume "vmc_path G P v0 p σ" then interpret vmc_path G P v0 p σ . have "¬deadend v0" using v0(2) directly_attracted_contains_no_deadends by blast then interpret vmc_path_no_deadend G P v0 p σ by unfold_locales have "visits_via (ltl P) S W" using vmc_path.strategy_attractsE[OF vmc_path_ltl σ] v0 directly_attracted_def by simp thus "visits_via P (insert v0 S) W" using visits_via_LCons[of "ltl P" S W v0] P_LCons by simp qed lemma attractor_has_strategy_single: assumes "W ⊆ V" and v0_def: "v0 ∈ attractor p W" (is "_ ∈ ?A") shows "∃σ. strategy p σ ∧ strategy_attracts_via p σ v0 ?A W" using assms proof (induct arbitrary: v0 rule: attractor_set_induction) case (step S) have "v0 ∈ W ⟹ ∃σ. strategy p σ ∧ strategy_attracts_via p σ v0 {} W" using strategy_attracts_via_trivial valid_arbitrary_strategy by blast moreover { assume *: "v0 ∈ directly_attracted p S" "v0 ∉ S" from assms(1) step.hyps(1) step.hyps(2) have "∃σ. strategy p σ ∧ strategy_attracts p σ S W" using merge_attractor_strategies by auto with * have "∃σ. strategy p σ ∧ strategy_attracts_via p σ v0 (insert v0 S) W" using strategy_attracts_extends_VVp strategy_attracts_extends_VVpstar by blast } ultimately show ?case using step.prems step.hyps(2) attractor_strategy_on_extends[of p _ v0 "insert v0 S" W "W ∪ S ∪ directly_attracted p S"] attractor_strategy_on_extends[of p _ v0 "S" W "W ∪ S ∪ directly_attracted p S"] attractor_strategy_on_extends[of p _ v0 "{}" W "W ∪ S ∪ directly_attracted p S"] by blast next case (union M) hence "∃S. S ∈ M ∧ v0 ∈ S" by blast thus ?case by (meson Union_upper attractor_strategy_on_extends union.hyps) qed subsection ‹Existence› text ‹Prove that every attractor set has an attractor strategy.› theorem attractor_has_strategy: assumes "W ⊆ V" shows "∃σ. strategy p σ ∧ strategy_attracts p σ (attractor p W) W" proof- let ?A = "attractor p W" have "?A ⊆ V" by (simp add: ‹W ⊆ V› attractor_in_V) moreover have "⋀v. v ∈ ?A ⟹ ∃σ. strategy p σ ∧ strategy_attracts_via p σ v ?A W" using ‹W ⊆ V› attractor_has_strategy_single by blast ultimately show ?thesis using merge_attractor_strategies ‹W ⊆ V› by blast qed end ― ‹context ParityGame› end  Theory PositionalDeterminacy section ‹Positional Determinacy of Parity Games› theory PositionalDeterminacy imports Main AttractorStrategy begin context ParityGame begin subsection ‹Induction Step› text ‹ The proof of positional determinacy is by induction over the size of the finite set @{term "ω  V"}, the set of priorities. The following lemma is the induction step. For now, we assume there are no deadends in the graph. Later we will get rid of this assumption. › lemma positional_strategy_induction_step: assumes "v ∈ V" and no_deadends: "⋀v. v ∈ V ⟹ ¬deadend v" and IH: "⋀(G :: ('a, 'b) ParityGame_scheme) v. ⟦ card (ω⇘G⇙  V⇘G⇙) < card (ω  V); v ∈ V⇘G⇙; ParityGame G; ⋀v. v ∈ V⇘G⇙ ⟹ ¬Digraph.deadend G v ⟧ ⟹ ∃p. v ∈ ParityGame.winning_region G p" shows "∃p. v ∈ winning_region p" proof- text ‹First, we determine the minimum priority and the player who likes it.› define min_prio where "min_prio = Min (ω  V)" have "∃p. winning_priority p min_prio" by auto then obtain p where p: "winning_priority p min_prio" by blast text ‹Then we define the tentative winning region of player @{term "p**"}. The rest of the proof is to show that this is the complete winning region. › define W1 where "W1 = winning_region p**" text ‹For this, we define several more sets of nodes. First, ‹U› is the tentative winning region of player @{term p}. › define U where "U = V - W1" define K where "K = U ∩ (ω - {min_prio})" define V' where "V' = U - attractor p K" define G' where [simp]: "G' = subgame V'" interpret G': ParityGame G' using subgame_ParityGame by simp have U_equiv: "⋀v. v ∈ V ⟹ v ∈ U ⟷ v ∉ winning_region p**" unfolding U_def W1_def by blast have "V' ⊆ V" unfolding U_def V'_def by blast hence [simp]: "V⇘G'⇙ = V'" unfolding G'_def by simp have "V⇘G'⇙ ⊆ V" "E⇘G'⇙ ⊆ E" "ω⇘G'⇙ = ω" unfolding G'_def by (simp_all add: subgame_ω) have "G'.VV p = V' ∩ VV p" unfolding G'_def using subgame_VV by simp have V_decomp: "V = attractor p K ∪ V' ∪ W1" proof- have "V ⊆ attractor p K ∪ V' ∪ W1" unfolding V'_def U_def by blast moreover have "attractor p K ⊆ V" using attractor_in_V[of K] unfolding K_def U_def by blast ultimately show ?thesis unfolding W1_def winning_region_def using ‹V' ⊆ V› by blast qed have G'_no_deadends: "⋀v. v ∈ V⇘G'⇙ ⟹ ¬G'.deadend v" proof- fix v assume "v ∈ V⇘G'⇙" hence *: "v ∈ U - attractor p K" using ‹V⇘G'⇙ = V'› V'_def by blast moreover hence "∃w ∈ U. v→w" using removing_winning_region_induces_no_deadends[of v "p**"] no_deadends U_equiv U_def by blast moreover have "⋀w. ⟦ v ∈ VV p**; v→w ⟧ ⟹ w ∈ U" using * U_equiv winning_region_extends_VVp by blast ultimately have "∃w ∈ V'. v→w" using U_equiv winning_region_extends_VVp removing_attractor_induces_no_deadends V'_def by blast thus "¬G'.deadend v" using ‹v ∈ V⇘G'⇙› ‹V' ⊆ V› by simp qed text ‹ By definition of @{term W1}, we obtain a winning strategy on @{term W1} for player @{term "p**"}. › obtain σW1 where σW1: "strategy p** σW1" "⋀v. v ∈ W1 ⟹ winning_strategy p** σW1 v" unfolding W1_def using merge_winning_strategies by blast { fix v assume "v ∈ V⇘G'⇙" text ‹Apply the induction hypothesis to get the winning strategy for @{term v} in @{term G'}.› have G'_winning_strategy: "∃p. v ∈ G'.winning_region p" proof- have "card (ω⇘G'⇙  V⇘G'⇙) < card (ω  V)" proof- { assume "min_prio ∈ ω⇘G'⇙  V⇘G'⇙" then obtain v where v: "v ∈ V⇘G'⇙" "ω⇘G'⇙ v = min_prio" by blast hence "v ∈ ω - {min_prio}" using ‹ω⇘G'⇙ = ω› by simp hence False using V'_def K_def attractor_set_base ‹V⇘G'⇙ = V'› v(1) by (metis DiffD1 DiffD2 IntI contra_subsetD) } hence "min_prio ∉ ω⇘G'⇙  V⇘G'⇙" by blast moreover have "min_prio ∈ ω  V" unfolding min_prio_def using priorities_finite Min_in assms(1) by blast moreover have "ω⇘G'⇙  V⇘G'⇙ ⊆ ω  V" unfolding G'_def by simp ultimately show ?thesis by (metis priorities_finite psubsetI psubset_card_mono) qed thus ?thesis using IH[of G'] ‹v ∈ V⇘G'⇙› G'_no_deadends G'.ParityGame_axioms by blast qed text ‹ It turns out the winning region of player @{term "p**"} is empty, so we have a strategy for player @{term p}. › have "v ∈ G'.winning_region p" proof (rule ccontr) assume "¬?thesis" moreover obtain p' σ where p': "G'.strategy p' σ" "G'.winning_strategy p' σ v" using G'_winning_strategy unfolding G'.winning_region_def by blast ultimately have "p' ≠ p" using ‹v ∈ V⇘G'⇙› unfolding G'.winning_region_def by blast hence "p' = p**" by (cases p; cases p') auto with p' have σ: "G'.strategy p** σ" "G'.winning_strategy p** σ v" by simp_all have "v ∈ winning_region p**" proof show "v ∈ V" using ‹v ∈ V⇘G'⇙› ‹V⇘G'⇙ ⊆ V› by blast define σ' where "σ' = override_on (override_on σ_arbitrary σW1 W1) σ V'" thus "strategy p** σ'" using valid_strategy_updates_set_strong valid_arbitrary_strategy σW1(1) valid_strategy_supergame σ(1) G'_no_deadends ‹V⇘G'⇙ = V'› unfolding G'_def by blast show "winning_strategy p** σ' v" proof (rule winning_strategyI, rule ccontr) fix P assume "vmc_path G P v p** σ'" then interpret vmc_path G P v "p**" σ' . assume "¬winning_path p** P" text ‹ First we show that @{term P} stays in @{term V'}, because if it stays in @{term V'}, then it conforms to @{term σ}, so it must be winning for @{term "p**"}.› have "lset P ⊆ V'" proof (induct rule: vmc_path_lset_induction_closed_subset) fix v assume "v ∈ V'" "¬deadend v" "v ∈ VV p**" hence "v ∈ ParityGame.VV (subgame V') p**" by auto moreover have "¬G'.deadend v" using G'_no_deadends ‹V⇘G'⇙ = V'› ‹v ∈ V'› by blast ultimately have "σ v ∈ V'" using subgame_strategy_stays_in_subgame p'(1) ‹p' = p**› unfolding G'_def by blast thus "σ' v ∈ V' ∪ W1" unfolding σ'_def using ‹v ∈ V'› by simp next fix v w assume "v ∈ V'" "¬deadend v" "v ∈ VV p****" "v→w" show "w ∈ V' ∪ W1" proof (rule ccontr) assume "w ∉ V' ∪ W1" hence "w ∈ attractor p K" using V_decomp ‹v→w› by blast hence "v ∈ attractor p K" using ‹v ∈ VV p****› attractor_set_VVp ‹v→w› by auto thus False using ‹v ∈ V'› V'_def by blast qed next have "⋀v. v ∈ W1 ⟹ σW1 v = σ' v" unfolding σ'_def V'_def U_def by simp thus "lset P ∩ W1 = {}" using path_hits_winning_region_is_winning σW1 ‹¬winning_path p** P› unfolding W1_def by blast next show "v ∈ V'" using ‹V⇘G'⇙ = V'› ‹v ∈ V⇘G'⇙› by blast qed text ‹This concludes the proof of @{term "lset P ⊆ V'"}.› hence "G'.valid_path P" using subgame_valid_path by simp moreover have "G'.maximal_path P" using ‹lset P ⊆ V'› subgame_maximal_path ‹V' ⊆ V› by simp moreover have "G'.path_conforms_with_strategy p** P σ" proof- have "G'.path_conforms_with_strategy p** P σ'" using subgame_path_conforms_with_strategy ‹V' ⊆ V› ‹lset P ⊆ V'› by simp moreover have "⋀v. v ∈ lset P ⟹ σ' v = σ v" using ‹lset P ⊆ V'› σ'_def by auto ultimately show ?thesis using G'.path_conforms_with_strategy_irrelevant_updates by blast qed ultimately have "G'.winning_path p** P" using σ(2) G'.winning_strategy_def G'.valid_maximal_conforming_path_0 P_0 P_not_null by blast moreover have "G'.VV p**** ⊆ VV p****" using subgame_VV_subset G'_def by blast ultimately show False using G'.winning_path_supergame[of "p**"] ‹ω⇘G'⇙ = ω› ‹¬winning_path p** P› ParityGame_axioms by blast qed qed moreover have "v ∈ V" using ‹V⇘G'⇙ ⊆ V› ‹v ∈ V⇘G'⇙› by blast ultimately have "v ∈ W1" unfolding W1_def winning_region_def by blast thus False using ‹v ∈ V⇘G'⇙› using U_def V'_def ‹V⇘G'⇙ = V'› ‹v ∈ V⇘G'⇙› by blast qed } note recursion = this text ‹ We compose a winning strategy for player @{term p} on @{term "V - W1"} out of three pieces. › text ‹ First, if we happen to land in the attractor region of @{term K}, we follow the attractor strategy. This is good because the priority of the nodes in @{term K} is good for player @{term p}, so he likes to go there.› obtain σ1 where σ1: "strategy p σ1" "strategy_attracts p σ1 (attractor p K) K" using attractor_has_strategy[of K p] K_def U_def by auto text ‹Next, on @{term G'} we follow the winning strategy whose existence we proved earlier.› have "G'.winning_region p = V⇘G'⇙" using recursion unfolding G'.winning_region_def by blast then obtain σ2 where σ2: "⋀v. v ∈ V⇘G'⇙ ⟹ G'.strategy p σ2" "⋀v. v ∈ V⇘G'⇙ ⟹ G'.winning_strategy p σ2 v" using G'.merge_winning_strategies by blast text ‹ As a last option we choose an arbitrary successor but avoid entering @{term W1}. In particular, this defines the strategy on the set @{term K}.› define succ where "succ v = (SOME w. v→w ∧ (v ∈ W1 ∨ w ∉ W1))" for v text ‹Compose the three pieces.› define σ where "σ = override_on (override_on succ σ2 V') σ1 (attractor p K - K)" have "attractor p K ∩ W1 = {}" proof (rule ccontr) assume "attractor p K ∩ W1 ≠ {}" then obtain v where v: "v ∈ attractor p K" "v ∈ W1" by blast hence "v ∈ V" using W1_def winning_region_def by blast obtain P where "vmc2_path G P v p σ1 σW1" using strategy_conforming_path_exists σW1(1) σ1(1) ‹v ∈ V› by blast then interpret vmc2_path G P v p σ1 σW1 . have "strategy_attracts_via p σ1 v (attractor p K) K" using v(1) σ1(2) strategy_attracts_def by blast hence "lset P ∩ K ≠ {}" using strategy_attracts_viaE visits_via_visits by blast hence "¬lset P ⊆ W1" unfolding K_def U_def by blast thus False unfolding W1_def using comp.paths_stay_in_winning_region σW1 v(2) by auto qed text ‹On specific sets, @{term σ} behaves like one of the three pieces.› have σ_σ1: "⋀v. v ∈ attractor p K - K ⟹ σ v = σ1 v" unfolding σ_def by simp have σ_σ2: "⋀v. v ∈ V' ⟹ σ v = σ2 v" unfolding σ_def V'_def by auto have σ_K: "⋀v. v ∈ K ∪ W1 ⟹ σ v = succ v" proof- fix v assume v: "v ∈ K ∪ W1" hence "v ∉ V'" unfolding V'_def U_def using attractor_set_base by auto with v show "σ v = succ v" unfolding σ_def U_def using ‹attractor p K ∩ W1 = {}› by (metis (mono_tags, lifting) Diff_iff IntI UnE override_on_def override_on_emptyset) qed text ‹Show that @{term succ} succeeds in avoiding entering @{term W1}.› { fix v assume v: "v ∈ VV p" hence "¬deadend v" using no_deadends by blast have "∃w. v→w ∧ (v ∈ W1 ∨ w ∉ W1)" proof (cases) assume "v ∈ W1" thus ?thesis using no_deadends ‹¬deadend v› by blast next assume "v ∉ W1" show ?thesis proof (rule ccontr) assume "¬(∃w. v→w ∧ (v ∈ W1 ∨ w ∉ W1))" hence "⋀w. v→w ⟹ winning_strategy p** σW1 w" using σW1(2) by blast hence "winning_strategy p** σW1 v" using strategy_extends_backwards_VVpstar σW1(1) ‹v ∈ VV p› by simp hence "v ∈ W1" unfolding W1_def winning_region_def using σW1(1) ‹¬deadend v› by blast thus False using ‹v ∉ W1› by blast qed qed hence "v→succ v" "v ∈ W1 ∨ succ v ∉ W1" unfolding succ_def using someI_ex[of "λw. v→w ∧ (v ∈ W1 ∨ w ∉ W1)"] by blast+ } note succ_works = this have "strategy p σ" proof fix v assume v: "v ∈ VV p" "¬deadend v" hence "v ∈ attractor p K - K ⟹ v→σ v" using σ_σ1 σ1(1) v unfolding strategy_def by auto moreover have "v ∈ V' ⟹ v→σ v" proof- assume "v ∈ V'" moreover have "v ∈ V⇘G'⇙" using ‹v ∈ V'› ‹V⇘G'⇙ = V'› by blast moreover have "v ∈ G'.VV p" using ‹G'.VV p = V' ∩ VV p› ‹v ∈ V'› ‹v ∈ VV p› by blast moreover have "¬Digraph.deadend G' v" using G'_no_deadends ‹v ∈ V⇘G'⇙› by blast ultimately have "v →⇘G'⇙ σ2 v" using σ2(1) G'.strategy_def[of p σ2] by blast with ‹v ∈ V'› show "v→σ v" using ‹E⇘G'⇙ ⊆ E› σ_σ2 by (metis subsetCE) qed moreover have "v ∈ K ∪ W1 ⟹ v→σ v" using succ_works(1) v σ_K by auto moreover have "v ∈ V" using ‹v ∈ VV p› by blast ultimately show "v→σ v" using V_decomp by blast qed have σ_attracts: "strategy_attracts p σ (attractor p K) K" proof- have "strategy_attracts p (override_on σ σ1 (attractor p K - K)) (attractor p K) K" using strategy_attracts_irrelevant_override σ1 ‹strategy p σ› by blast moreover have "σ = override_on σ σ1 (attractor p K - K)" by (rule ext) (simp add: override_on_def σ_σ1) ultimately show ?thesis by simp qed text ‹Show that @{term σ} is a winning strategy on @{term "V - W1"}.› have "∀v ∈ V - W1. winning_strategy p σ v" proof (intro ballI winning_strategyI) fix v P assume P: "v ∈ V - W1" "vmc_path G P v p σ" interpret vmc_path G P v p σ using P(2) . have "lset P ⊆ V - W1" proof (induct rule: vmc_path_lset_induction_closed_subset) fix v assume "v ∈ V - W1" "¬deadend v" "v ∈ VV p" show "σ v ∈ V - W1 ∪ {}" proof (rule ccontr) assume "¬?thesis" hence "σ v ∈ W1" using ‹strategy p σ› ‹¬deadend v› ‹v ∈ VV p› unfolding strategy_def by blast hence "v ∉ K" using succ_works(2)[OF ‹v ∈ VV p›] ‹v ∈ V - W1› σ_K by auto moreover have "v ∉ attractor p K - K" proof assume "v ∈ attractor p K - K" hence "σ v ∈ attractor p K" using attracted_strategy_step ‹strategy p σ› σ_attracts ‹¬deadend v› ‹v ∈ VV p› attractor_set_base by blast thus False using ‹σ v ∈ W1› ‹attractor p K ∩ W1 = {}› by blast qed moreover have "v ∉ V'" proof assume "v ∈ V'" have "σ2 v ∈ V⇘G'⇙" proof (rule G'.valid_strategy_in_V[of p σ2 v]) have "v ∈ V⇘G'⇙" using ‹V⇘G'⇙ = V'› ‹v ∈ V'› by simp thus "¬G'.deadend v" using G'_no_deadends by blast show "G'.strategy p σ2" using σ2(1) ‹v ∈ V⇘G'⇙› by blast show "v ∈ G'.VV p" using ‹v ∈ VV p› ‹G'.VV p = V' ∩ VV p› ‹v ∈ V'› by simp qed hence "σ v ∈ V⇘G'⇙" using ‹v ∈ V'› σ_σ2 by simp thus False using ‹V⇘G'⇙ = V'› ‹σ v ∈ W1› V'_def U_def by blast qed ultimately show False using ‹v ∈ V - W1› V_decomp by blast qed next fix v w assume "v ∈ V - W1" "¬deadend v" "v ∈ VV p**" "v→w" show "w ∈ V - W1 ∪ {}" proof (rule ccontr) assume "¬?thesis" hence "w ∈ W1" using ‹v→w› by blast let ?σ = "σW1(v := w)" have "winning_strategy p** σW1 w" using ‹w ∈ W1› σW1(2) by blast moreover have "¬(∃σ. strategy p** σ ∧ winning_strategy p** σ v)" using ‹v ∈ V - W1› unfolding W1_def winning_region_def by blast ultimately have "winning_strategy p** ?σ w" using winning_strategy_updates[of "p**" σW1 w v w] σW1(1) ‹v→w› unfolding winning_region_def by blast moreover have "strategy p** ?σ" using ‹v→w› σW1(1) valid_strategy_updates by blast ultimately have "winning_strategy p** ?σ v" using strategy_extends_backwards_VVp[of v "p**" ?σ w] ‹v ∈ VV p**› ‹v→w› by auto hence "v ∈ W1" unfolding W1_def winning_region_def using ‹strategy p** ?σ› ‹v ∈ V - W1› by blast thus False using ‹v ∈ V - W1› by blast qed qed (insert P(1), simp_all) text ‹This concludes the proof of @{term "lset P ⊆ V - W1"}.› hence "lset P ⊆ attractor p K ∪ V'" using V_decomp by blast have "¬lfinite P" using no_deadends lfinite_lset maximal_ends_on_deadend[of P] P_maximal P_not_null lset_P_V by blast text ‹ Every @{term σ}-conforming path starting in @{term "V - W1"} is winning. We distinguish two cases: \begin{enumerate} \item @{term P} eventually stays in @{term V'}. Then @{term P} is winning because @{term σ2} is winning. \item @{term P} visits @{term K} infinitely often. Then @{term P} is winning because of the priority of the nodes in @{term K}. \end{enumerate} › show "winning_path p P" proof (cases) assume "∃n. lset (ldropn n P) ⊆ V'" text ‹The first case: @{term P} eventually stays in @{term V'}.› then obtain n where n: "lset (ldropn n P) ⊆ V'" by blast define P' where "P' = ldropn n P" hence "lset P' ⊆ V'" using n by blast interpret vmc_path': vmc_path G' P' "lhd P'" p σ2 proof show "¬lnull P'" unfolding P'_def using ‹¬lfinite P› lfinite_ldropn lnull_imp_lfinite by blast show "G'.valid_path P'" proof- have "valid_path P'" unfolding P'_def by simp thus ?thesis using subgame_valid_path ‹lset P' ⊆ V'› G'_def by blast qed show "G'.maximal_path P'" proof- have "maximal_path P'" unfolding P'_def by simp thus ?thesis using subgame_maximal_path ‹lset P' ⊆ V'› ‹V' ⊆ V› G'_def by blast qed show "G'.path_conforms_with_strategy p P' σ2" proof- have "path_conforms_with_strategy p P' σ" unfolding P'_def by simp hence "path_conforms_with_strategy p P' σ2" using path_conforms_with_strategy_irrelevant_updates ‹lset P' ⊆ V'› σ_σ2 by blast thus ?thesis using subgame_path_conforms_with_strategy ‹lset P' ⊆ V'› ‹V' ⊆ V› G'_def by blast qed qed simp have "G'.winning_strategy p σ2 (lhd P')" using ‹lset P' ⊆ V'› vmc_path'.P_not_null σ2(2)[of "lhd P'"] ‹V⇘G'⇙ = V'› llist.set_sel(1) by blast hence "G'.winning_path p P'" using G'.winning_strategy_def vmc_path'.vmc_path_axioms by blast moreover have "G'.VV p** ⊆ VV p**" unfolding G'_def using subgame_VV by simp ultimately have "winning_path p P'" using G'.winning_path_supergame[of p P' G] ‹ω⇘G'⇙ = ω› ParityGame_axioms by blast thus ?thesis unfolding P'_def using infinite_small_llength[OF ‹¬lfinite P›] winning_path_drop_add[of P p n] P_valid by blast next assume asm: "¬(∃n. lset (ldropn n P) ⊆ V')" text ‹The second case: @{term P} visits @{term K} infinitely often. Then @{term min_prio} occurs infinitely often on @{term P}.› have "min_prio ∈ path_inf_priorities P" unfolding path_inf_priorities_def proof (intro CollectI allI) fix n obtain k1 where k1: "ldropn n P$ k1 ∉ V'" using asm by (metis lset_lnth subsetI)
define k2 where "k2 = k1 + n"
interpret vmc_path G "ldropn k2 P" "P $k2" p σ using vmc_path_ldropn infinite_small_llength ‹¬lfinite P› by blast have "P$ k2 ∉ V'" unfolding k2_def
using k1 lnth_ldropn infinite_small_llength[OF ‹¬lfinite P›] by simp
hence "P $k2 ∈ attractor p K" using ‹¬lfinite P› ‹lset P ⊆ V - W1› by (metis DiffI U_def V'_def lset_nth_member_inf) then obtain k3 where k3: "ldropn k2 P$ k3 ∈ K"
using σ_attracts strategy_attractsE unfolding G'.visits_via_def by blast
define k4 where "k4 = k3 + k2"
hence "P $k4 ∈ K" using k3 lnth_ldropn infinite_small_llength[OF ‹¬lfinite P›] by simp moreover have "k4 ≥ n" unfolding k4_def k2_def using le_add2 le_trans by blast moreover have "ldropn n P$ k4 - n = P $(k4 - n) + n" using lnth_ldropn infinite_small_llength ‹¬lfinite P› by blast ultimately have "ldropn n P$ k4 - n ∈ K" by simp
hence "lset (ldropn n P) ∩ K ≠ {}"
using ‹¬lfinite P› lfinite_ldropn in_lset_conv_lnth[of "ldropn n P \$ k4 - n"]
by blast
thus "min_prio ∈ lset (ldropn n (lmap ω P))" unfolding K_def by auto
qed
thus ?thesis unfolding winning_path_def
using path_inf_priorities_at_least_min_prio[OF P_valid, folded min_prio_def]
‹winning_priority p min_prio› ‹¬lfinite P›
by blast
qed
qed
hence "∀v ∈ V. ∃p σ. strategy p σ ∧ winning_strategy p σ v"
unfolding W1_def winning_region_def using ‹strategy p σ› by blast
hence "∃p σ. strategy p σ ∧ winning_strategy p σ v" using ‹v ∈ V› by simp
thus ?thesis unfolding winning_region_def using ‹v ∈ V› by blast
qed

subsection ‹Positional Determinacy without Deadends›

theorem positional_strategy_exists_without_deadends:
assumes "v ∈ V" "⋀v. v ∈ V ⟹ ¬deadend v"
shows "∃p. v ∈ winning_region p"
using assms ParityGame_axioms
by (induct "card (ω  V)" arbitrary: G v rule: nat_less_induct)
(rule ParityGame.positional_strategy_induction_step, simp_all)

subsection ‹Positional Determinacy with Deadends›

text ‹
Prove a stronger version of the previous theorem: Allow deadends.
›
theorem positional_strategy_exists:
assumes "v0 ∈ V"
shows "∃p. v0 ∈ winning_region p"
proof-
{ fix p
define A where "A = attractor p (deadends p**)"
assume v0_in_attractor: "v0 ∈ attractor p (deadends p**)"
then obtain σ where σ: "strategy p σ" "strategy_attracts p σ A (deadends p**)"
using attractor_has_strategy[of "deadends p**" "p"] A_def deadends_in_V by blast

have "A ⊆ V" using A_def using attractor_in_V deadends_in_V by blast
hence "A - deadends p** ⊆ V" by auto

have "winning_strategy p σ v0" proof (unfold winning_strategy_def, intro allI impI)
fix P assume "vmc_path G P v0 p σ"
then interpret vmc_path G P v0 p σ .
show "winning_path p P"
using visits_deadend[of "p**"] σ(2) strategy_attracts_lset v0_in_attractor
unfolding A_def by simp
qed
hence "∃p σ. strategy p σ ∧ winning_strategy p σ v0" using σ by blast
} note lemma_path_to_deadend = this
define A where "A p = attractor p (deadends p**)" for p
text ‹Remove the attractor sets of the sets of deadends.›
define V' where "V' = V - A Even - A Odd"
hence "V' ⊆ V" by blast
show ?thesis proof (cases)
assume "v0 ∈ V'"
define G' where "G' = subgame V'"
interpret G': ParityGame G' unfolding G'_def using subgame_ParityGame .
have "V⇘G'⇙ = V'" unfolding G'_def using ‹V' ⊆ V› by simp
hence "v0 ∈ V⇘G'⇙" using ‹v0 ∈ V'› by simp
moreover have V'_no_deadends: "⋀v. v ∈ V⇘G'⇙ ⟹ ¬G'.deadend v" proof-
fix v assume "v ∈ V⇘G'⇙"
moreover have "V' = V - A Even - A Even**" using V'_def by simp
ultimately show "¬G'.deadend v"
using subgame_without_deadends ‹v ∈ V⇘G'⇙› unfolding A_def G'_def by blast
qed
ultimately obtain p σ where σ: "G'.strategy p σ" "G'.winning_strategy p σ v0"
using G'.positional_strategy_exists_without_deadends
unfolding G'.winning_region_def
by blast

have V'_no_deadends': "⋀v. v ∈ V' ⟹ ¬deadend v" proof-
fix v assume "v ∈ V'"
hence "¬G'.deadend v" using V'_no_deadends ‹V' ⊆ V› unfolding G'_def by auto
thus "¬deadend v" unfolding G'_def using ‹V' ⊆ V› by auto
qed

obtain σ_attr
where σ_attr: "strategy p σ_attr" "strategy_attracts p σ_attr (A p) (deadends p**)"
using attractor_has_strategy[OF deadends_in_V] unfolding A_def by blast
define σ' where "σ' = override_on σ σ_attr (A Even ∪ A Odd)"
have σ'_is_σ_on_V': "⋀v. v ∈ V' ⟹ σ' v = σ v"
unfolding V'_def σ'_def A_def by (cases p) simp_all

have "strategy p σ'" proof-
have "σ' = override_on σ_attr σ (UNIV - A Even - A Odd)"
unfolding σ'_def override_on_def by (rule ext) simp
moreover have "strategy p (override_on σ_attr σ V')"
using valid_strategy_supergame σ_attr(1) σ(1) V'_no_deadends ‹V⇘G'⇙ = V'›
unfolding G'_def by blast
ultimately show ?thesis by (simp add: valid_strategy_only_in_V V'_def override_on_def)
qed
moreover have "winning_strategy p σ' v0" proof (rule winning_strategyI, rule ccontr)
fix P assume "vmc_path G P v0 p σ'"
then interpret vmc_path G P v0 p σ' .
interpret vmc_path_no_deadend G P v0 p σ'
using V'_no_deadends' ‹v0 ∈ V'› by unfold_locales
assume contra: "¬winning_path p P"

have "lset P ⊆ V'" proof (induct rule: vmc_path_lset_induction_closed_subset)
fix v assume "v ∈ V'" "¬deadend v" "v ∈ VV p"
hence "v ∈ G'.VV p" unfolding G'_def by (simp add: ‹v ∈ V'›)
moreover have "¬G'.deadend v" using V'_no_deadends ‹v ∈ V'› ‹V⇘G'⇙ = V'› by blast
moreover have "G'.strategy p σ'"
using G'.valid_strategy_only_in_V σ'_def σ'_is_σ_on_V' σ(1) ‹V⇘G'⇙ = V'› by auto
ultimately show "σ' v ∈ V' ∪ A p" using subgame_strategy_stays_in_subgame
unfolding G'_def by blast
next
fix v w assume "v ∈ V'" "¬deadend v" "v ∈ VV p**" "v→w"
have "w ∉ A p**" proof
assume "w ∈ A p**"
hence "v ∈ A p**" unfolding A_def
using ‹v ∈ VV p**› ‹v→w› attractor_set_VVp by blast
thus False using ‹v ∈ V'› unfolding V'_def by (cases p) auto
qed
thus "w ∈ V' ∪ A p" unfolding V'_def using ‹v→w› by (cases p) auto
next
show "lset P ∩ A p = {}" proof (rule ccontr)
assume "lset P ∩ A p ≠ {}"
have "strategy_attracts p (override_on σ' σ_attr (A p - deadends p**))
(A p)
(deadends p**)"
using strategy_attracts_irrelevant_override[OF σ_attr(2) σ_attr(1) ‹strategy p σ'›]
by blast
moreover have "override_on σ' σ_attr (A p - deadends p**) = σ'"
by (rule ext, unfold σ'_def, cases p) (simp_all add: override_on_def)
ultimately have "strategy_attracts p σ' (A p) (deadends p**)" by simp
hence "lset P ∩ deadends p** ≠ {}"
using ‹lset P ∩ A p ≠ {}› attracted_path[OF deadends_in_V] by simp
thus False using contra visits_deadend[of "p**"] by simp
qed
qed (insert ‹v0 ∈ V'›)

then interpret vmc_path G' P v0 p σ'
unfolding G'_def using subgame_path_vmc_path[OF ‹V' ⊆ V›] by blast
have "G'.path_conforms_with_strategy p P σ" proof-
have "⋀v. v ∈ lset P ⟹ σ' v = σ v"
using σ'_is_σ_on_V' ‹V⇘G'⇙ = V'› lset_P_V by blast
thus "G'.path_conforms_with_strategy p P σ"
using P_conforms G'.path_conforms_with_strategy_irrelevant_updates by blast
qed
then interpret vmc_path G' P v0 p σ using conforms_to_another_strategy by blast
have "G'.winning_path p P"
using σ(2)[unfolded G'.winning_strategy_def] vmc_path_axioms by blast
from ‹¬winning_path p P›
G'.winning_path_supergame[OF this ParityGame_axioms, unfolded G'_def]
subgame_VV_subset[of "p**" V']
subgame_ω[of V']
show False by blast
qed
ultimately show ?thesis unfolding winning_region_def using ‹v0 ∈ V› by blast
next
assume "v0 ∉ V'"
then obtain p where "v0 ∈ attractor p (deadends p**)"
unfolding V'_def A_def using ‹v0 ∈ V› by blast
thus ?thesis unfolding winning_region_def
using lemma_path_to_deadend ‹v0 ∈ V› by blast
qed
qed

subsection ‹The Main Theorem: Positional Determinacy›
text ‹\label{subsec:positional_determinacy}›

text ‹
Prove the main theorem: The winning regions of player \Even and \Odd are a partition of the set
of nodes @{term V}.
›

theorem partition_into_winning_regions:
shows "V = winning_region Even ∪ winning_region Odd"
and "winning_region Even ∩ winning_region Odd = {}"
proof
show "V ⊆ winning_region Even ∪ winning_region Odd"
by (rule subsetI) (metis (full_types) Un_iff other_other_player positional_strategy_exists)
next
show "winning_region Even ∪ winning_region Odd ⊆ V"
by (rule subsetI) (meson Un_iff subsetCE winning_region_in_V)
next
show "winning_region Even ∩ winning_region Odd = {}"
using winning_strategy_only_for_one_player[of Even]
unfolding winning_region_def by auto
qed

end ― ‹context ParityGame›

end


Theory AttractorInductive

section ‹Defining the Attractor with \texttt{inductive\_set}›

theory AttractorInductive
imports
Main
Attractor
begin

context ParityGame begin

text ‹
In section \ref{sec:attractor} we defined @{const attractor} manually via @{const lfp}.
We can also define it with \texttt{inductive\_set}.  In this section, we do exactly this and
prove that the new definition yields the same set as the old definition.
›

subsection ‹@{term attractor_inductive}›

text ‹The attractor set of a given set of nodes, defined inductively.›
inductive_set attractor_inductive :: "Player ⇒ 'a set ⇒ 'a set"
for p :: Player and W :: "'a set" where
Base [intro!]: "v ∈ W ⟹ v ∈ attractor_inductive p W"
| VVp: "⟦ v ∈ VV p; ∃w. v→w ∧ w ∈ attractor_inductive p W ⟧
⟹ v ∈ attractor_inductive p W"
| VVpstar: "⟦ v ∈ VV p**; ¬deadend v; ∀w. v→w ⟶ w ∈ attractor_inductive p W ⟧
⟹ v ∈ attractor_inductive p W"

text ‹
We show that the inductive definition and the definition via least fixed point are the same.
›
lemma attractor_inductive_is_attractor:
assumes "W ⊆ V"
shows "attractor_inductive p W = attractor p W"
proof
show "attractor_inductive p W ⊆ attractor p W" proof
fix v assume "v ∈ attractor_inductive p W"
thus "v ∈ attractor p W" proof (induct rule: attractor_inductive.induct)
case (Base v) thus ?case using attractor_set_base by auto
next
case (VVp v) thus ?case using attractor_set_VVp by auto
next
case (VVpstar v) thus ?case using attractor_set_VVpstar by auto
qed
qed
show "attractor p W ⊆ attractor_inductive p W"
proof-
define P where "P S ⟷ S ⊆ attractor_inductive p W" for S
from ‹W ⊆ V› have "P (attractor p W)" proof (induct rule: attractor_set_induction)
case (step S)
hence "S ⊆ attractor_inductive p W" using P_def by simp
have "W ∪ S ∪ directly_attracted p S ⊆ attractor_inductive p W" proof
fix v assume "v ∈ W ∪ S ∪ directly_attracted p S"
moreover
{ assume "v ∈ W" hence "v ∈ attractor_inductive p W" by blast }
moreover
{ assume "v ∈ S" hence "v ∈ attractor_inductive p W"
by (meson ‹S ⊆ attractor_inductive p W› rev_subsetD) }
moreover
{ assume v_attracted: "v ∈ directly_attracted p S"
hence "v ∈ V" using ‹S ⊆ V› attractor_step_bounded_by_V by blast
hence "v ∈ attractor_inductive p W" proof (cases rule: VV_cases)
assume "v ∈ VV p"
hence "∃w. v→w ∧ w ∈ S" using v_attracted directly_attracted_def by blast
hence "∃w. v→w ∧ w ∈ attractor_inductive p W"
using ‹S ⊆ attractor_inductive p W› by blast
thus ?thesis by (simp add: ‹v ∈ VV p› attractor_inductive.VVp)
next
assume "v ∈ VV p**"
hence *: "∀w. v→w ⟶ w ∈ S" using v_attracted directly_attracted_def by blast
have "¬deadend v" using v_attracted directly_attracted_def by blast
show ?thesis proof (rule ccontr)
assume "v ∉ attractor_inductive p W"
hence "∃w. v→w ∧ w ∉ attractor_inductive p W"
by (metis attractor_inductive.VVpstar ‹v ∈ VV p**› ‹¬deadend v›)
hence "∃w. v→w ∧ w ∉ S" using ‹S ⊆ attractor_inductive p W› by (meson subsetCE)
thus False using * by blast
qed
qed
}
ultimately show "v ∈ attractor_inductive p W" by (meson UnE)
qed
thus "P (W ∪ S ∪ directly_attracted p S)" using P_def by simp
qed (simp add: P_def Sup_least)
thus ?thesis using P_def by simp
qed
qed

end

end


Theory Graph_TheoryCompatibility

section ‹Compatibility with the Graph Theory Package›

theory Graph_TheoryCompatibility
imports
ParityGame
Graph_Theory.Digraph
Graph_Theory.Digraph_Isomorphism
begin

text ‹
In this section, we show that our @{locale Digraph} locale is compatible to the
@{locale nomulti_digraph} locale from the graph theory package from the Archive of Formal Proofs.

For this, we will define two functions converting between the different types and show that with
these conversion functions the locales interpret each other.  Together, this indicates that our
definition of digraph is reasonable.
›

subsection ‹To Graph Theory›

text ‹We can easily convert our graphs into @{type pre_digraph} objects.›
definition to_pre_digraph :: "('a, 'b) Graph_scheme ⇒ ('a, 'a × 'a) pre_digraph"
where "to_pre_digraph G ≡ ⦇
pre_digraph.verts = Graph.verts G,
pre_digraph.arcs = Graph.arcs G,
tail = fst,
head = snd
⦈"

text ‹
With this conversion function, our @{locale Digraph} locale contains the locale
@{locale nomulti_digraph} from the graph theory package.
›
context Digraph begin
interpretation is_nomulti_digraph: nomulti_digraph "to_pre_digraph G" proof
fix e assume *: "e ∈ pre_digraph.arcs (to_pre_digraph G)"
show "tail (to_pre_digraph G) e ∈ pre_digraph.verts (to_pre_digraph G)"
by (metis * edges_are_in_V(1) pre_digraph.ext_inject pre_digraph.surjective prod.collapse to_pre_digraph_def)
show "head (to_pre_digraph G) e ∈ pre_digraph.verts (to_pre_digraph G)"
by (metis * edges_are_in_V(2) pre_digraph.ext_inject pre_digraph.surjective prod.collapse to_pre_digraph_def)
qed (simp add: arc_to_ends_def to_pre_digraph_def)
end

subsection ‹From Graph Theory›

text ‹We can also convert in the other direction.›
definition from_pre_digraph :: "('a, 'b) pre_digraph ⇒ 'a Graph"
where "from_pre_digraph G ≡ ⦇
Graph.verts = pre_digraph.verts G,
Graph.arcs = arcs_ends G
⦈"

context nomulti_digraph begin
interpretation is_Digraph: Digraph "from_pre_digraph G" proof-
{
fix v w assume "(v,w) ∈ E⇘from_pre_digraph G⇙"
then obtain e where e: "e ∈ pre_digraph.arcs G" "tail G e = v" "head G e = w"
unfolding from_pre_digraph_def by auto
hence "(v,w) ∈ V⇘from_pre_digraph G⇙ × V⇘from_pre_digraph G⇙"
unfolding from_pre_digraph_def by auto
}
thus "Digraph (from_pre_digraph G)" by (simp add: Digraph.intro subrelI)
qed
end

subsection ‹Isomorphisms›

text ‹
We also show that our conversion functions make sense.  That is, we show that they are nearly
inverses of each other.  Unfortunately, @{const from_pre_digraph} irretrievably loses information
about the arcs, and only keeps tail/head intact, so the best we can get for this case is that the
back-and-forth converted graphs are isomorphic.
›

lemma graph_conversion_bij: "G = from_pre_digraph (to_pre_digraph G)"
unfolding to_pre_digraph_def from_pre_digraph_def arcs_ends_def arc_to_ends_def by auto

lemma (in nomulti_digraph) graph_conversion_bij2: "digraph_iso G (to_pre_digraph (from_pre_digraph G))"
proof-
define iso
where "iso = ⦇
iso_verts = id :: 'a ⇒ 'a,
iso_arcs = arc_to_ends G,
iso_head = snd,
iso_tail = fst
⦈"

have "inj_on (iso_verts iso) (pre_digraph.verts G)" unfolding iso_def by auto
moreover have "inj_on (iso_arcs iso) (pre_digraph.arcs G)"
unfolding iso_def arc_to_ends_def by (simp add: arc_to_ends_def inj_onI no_multi_arcs)
moreover have "∀a ∈ pre_digraph.arcs G.
iso_verts iso (tail G a) = iso_tail iso (iso_arcs iso a)
∧ iso_verts iso (head G a) = iso_head iso (iso_arcs iso a)"
unfolding iso_def by (simp add: arc_to_ends_def)

ultimately have "digraph_isomorphism iso"
unfolding digraph_isomorphism_def using arc_to_ends_def wf_digraph_axioms by blast

moreover have "to_pre_digraph (from_pre_digraph G) = app_iso iso G"
unfolding to_pre_digraph_def from_pre_digraph_def iso_def app_iso_def by (simp_all add: arcs_ends_def)

ultimately show ?thesis unfolding digraph_iso_def by blast
qed

end
`