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

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

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