Quelle  ParityGame.thy

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 → w ≡ (v,w) ∈ E"

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_'" "E ⊆ E_'"
  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 _V' ⊆ V"
  and subgame_E [simp]: "E _V' ⊆ E"
  and subgame_ψ: "ψ _V' = ψ"
  unfolding subgame_def by simp_all

lemma
  assumes "V' ⊆ V"
  shows subgame_V' [simp]: "V _V' = V'"
    and subgame_E' [simp]: "E _V' = E ∩ (V _V' × V _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 (ψ _V' ` V <sub>V'</sub>)" proof-
  have "finite (ψ ` V _V')" using subgame_V priorities_finite
    by (meson finite_subset image_mono)
  thus ?thesis by (simp add: subgame_def)
qed

lemma subgame_ψ_subset [simp]: "ψ _V' ` V <sub>V'</sub> ⊆ ψ ` 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 _V' ⊆ V _V' × V _V'"
    using subgame_Digraph[unfolded Digraph_def] .
  show "V0 _V' ⊆ V _V'" unfolding subgame_def using valid_player0_set by auto
  show "finite (ψ _V' ` V _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 _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 _V'" "w ∈ V _V'" using IH(2) by auto
      moreover hence "v → _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 _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**" "ψ = ψ_'"
  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