Theory WinningRegion

section ‹Winning Regions›

theory WinningRegion
imports
  Main
  WinningStrategy
begin

text ‹
  Here we define winning regions of parity games.  The winning region for player ‹p› is the
  set of nodes from which ‹p› has a positional winning strategy.
›

context ParityGame begin

definition "winning_region p ≡ { v ∈ V. ∃σ. strategy p σ ∧ winning_strategy p σ v }"

lemma winning_regionI [intro]:
  assumes "v ∈ V" "strategy p σ" "winning_strategy p σ v"
  shows "v ∈ winning_region p"
  using assms unfolding winning_region_def by blast

lemma winning_region_in_V [simp]: "winning_region p ⊆ V" unfolding winning_region_def by blast

lemma winning_region_deadends:
  assumes "v ∈ VV p" "deadend v"
  shows "v ∈ winning_region p**"
proof
  show "v ∈ V" using ‹v ∈ VV p› by blast
  show "winning_strategy p** σ_arbitrary v" using assms winning_strategy_on_deadends by simp
qed simp

subsection ‹Paths in Winning Regions›

lemma (in vmc_path) paths_stay_in_winning_region:
  assumes σ': "strategy p σ'" "winning_strategy p σ' v0"
    and σ: "⋀v. v ∈ winning_region p ⟹ σ' v = σ v"
  shows "lset P ⊆ winning_region p"
proof
  fix x assume "x ∈ lset P"
  thus "x ∈ winning_region p" using assms vmc_path_axioms
  proof (induct arbitrary: v0 rule: llist_set_induct)
    case (find P v0)
    interpret vmc_path G P v0 p σ using find.prems(4) .
    show ?case using P_v0 σ'(1) find.prems(2) v0_V unfolding winning_region_def by blast
  next
    case (step P x v0)
    interpret vmc_path G P v0 p σ using step.prems(4) .
    show ?case proof (cases)
      assume "lnull (ltl P)"
      thus ?thesis using P_lnull_ltl_LCons step.hyps(2) by auto
    next
      assume "¬lnull (ltl P)"
      then interpret vmc_path_no_deadend G P v0 p σ using P_no_deadend_v0 by unfold_locales
      have "winning_strategy p σ' w0" proof (cases)
        assume "v0 ∈ VV p"
        hence "winning_strategy p σ' (σ' v0)"
          using strategy_extends_VVp local.step(4) step.prems(2) v0_no_deadend by blast
        moreover have "σ v0 = w0" using v0_conforms ‹v0 ∈ VV p› by blast
        moreover have "σ' v0 = σ v0"
          using σ assms(1) step.prems(2) v0_V unfolding winning_region_def by blast
        ultimately show ?thesis by simp
      next
        assume "v0 ∉ VV p"
        thus ?thesis using v0_V strategy_extends_VVpstar step(4) step.prems(2) by simp
      qed
      thus ?thesis using step.hyps(3) step(4) σ vmc_path_ltl by blast
    qed
  qed
qed

lemma (in vmc_path) path_hits_winning_region_is_winning:
  assumes σ': "strategy p σ'" "⋀v. v ∈ winning_region p ⟹ winning_strategy p σ' v"
    and σ: "⋀v. v ∈ winning_region p ⟹ σ' v = σ v"
    and P: "lset P ∩ winning_region p ≠ {}"
  shows "winning_path p P"
proof-
  obtain n where n: "enat n < llength P" "P $ n ∈ winning_region p"
    using P by (meson lset_intersect_lnth)
  define P' where "P' = ldropn n P"
  then interpret P': vmc_path G P' "P $ n" p σ
    unfolding P'_def using vmc_path_ldropn n(1) by blast
  have "winning_strategy p σ' (P $ n)" using σ'(2) n(2) by blast
  hence "lset P' ⊆ winning_region p"
    using P'.paths_stay_in_winning_region[OF σ'(1) _ σ]
    by blast
  hence "⋀v. v ∈ lset P' ⟹ σ v = σ' v" using σ by auto
  hence "path_conforms_with_strategy p P' σ'"
    using path_conforms_with_strategy_irrelevant_updates P'.P_conforms
    by blast
  then interpret P': vmc_path G P' "P $ n" p σ' using P'.conforms_to_another_strategy by blast
  have "winning_path p P'" using σ'(2) n(2) P'.vmc_path_axioms winning_strategy_def by blast
  thus "winning_path p P" unfolding P'_def using winning_path_drop_add n(1) P_valid by blast
qed

subsection ‹Irrelevant Updates›

text ‹Updating a winning strategy outside of the winning region is irrelevant.›

lemma winning_strategy_updates:
  assumes σ: "strategy p σ" "winning_strategy p σ v0"
    and v: "v ∉ winning_region p" "v→w"
  shows "winning_strategy p (σ(v := w)) v0"
proof
  fix P assume "vmc_path G P v0 p (σ(v := w))"
  then interpret vmc_path G P v0 p "σ(v := w)" .
  have "⋀v'. v' ∈ winning_region p ⟹ σ v' = (σ(v := w)) v'" using v by auto
  hence "v ∉ lset P" using v paths_stay_in_winning_region σ unfolding winning_region_def by blast
  hence "path_conforms_with_strategy p P σ"
    using P_conforms path_conforms_with_strategy_irrelevant' by blast
  thus "winning_path p P" using conforms_to_another_strategy σ(2) winning_strategy_def by blast
qed

subsection ‹Extending Winning Regions›

lemma winning_region_extends_VVp:
  assumes v: "v ∈ VV p" "v→w" and w: "w ∈ winning_region p"
  shows "v ∈ winning_region p"
proof (rule ccontr)
  obtain σ where σ: "strategy p σ" "winning_strategy p σ w"
    using w unfolding winning_region_def by blast
  let ?σ = "σ(v := w)"
  assume contra: "v ∉ winning_region p"
  moreover have "strategy p ?σ" using valid_strategy_updates σ(1) ‹v→w› by blast
  moreover hence "winning_strategy p ?σ v"
    using winning_strategy_updates σ contra v strategy_extends_backwards_VVp
    by auto
  ultimately show False using ‹v→w› unfolding winning_region_def by auto
qed

text ‹
  Unfortunately, we cannot prove the corresponding theorem ‹winning_region_extends_VVpstar›
  for @{term "VV p**"}-nodes yet.
  First, we need to show that there exists a uniform winning strategy on @{term "winning_region p"}.
  We will prove ‹winning_region_extends_VVpstar› as soon as we have this.
›

end ― ‹context ParityGame›

end