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