Theory UniformStrategy

section ‹Uniform Strategies›

text ‹Theorems about how to get a uniform strategy given strategies for each node.›

theory UniformStrategy
imports
  Main
  AttractingStrategy WinningStrategy WellOrderedStrategy WinningRegion
begin

context ParityGame begin

subsection ‹A Uniform Attractor Strategy›

lemma merge_attractor_strategies:
  assumes "S  V"
    and strategies_ex: "v. v  S  σ. strategy p σ  strategy_attracts_via p σ v S W"
  shows "σ. strategy p σ  strategy_attracts p σ S W"
proof-
  define good where "good v = {σ. strategy p σ  strategy_attracts_via p σ v S W }" for v
  let ?G = "{σ. v  S - W. σ  good v}"
  obtain r where r: "well_order_on ?G r" using well_order_on by blast

  interpret WellOrderedStrategies G "S - W" p good r proof
    show "S - W  V" using S  V by blast
  next
    show "v. v  S - W  σ. σ  good v" unfolding good_def using strategies_ex by blast
  next
    show "v σ. σ  good v  strategy p σ" unfolding good_def by blast
  next
    fix v w σ assume v: "v  S - W" "vw" "v  VV p  σ v = w" "σ  good v"
    hence σ: "strategy p σ" "strategy_attracts_via p σ v S W" unfolding good_def by simp_all
    hence "strategy_attracts_via p σ w S W" using strategy_attracts_via_successor v by blast
    thus "σ  good w" unfolding good_def using σ(1) by blast
  qed (insert r)

  have S_W_no_deadends: "v. v  S - W  ¬deadend v"
    using strategy_attracts_via_no_deadends[of _ S W] strategies_ex
    by (metis (no_types) Diff_iff S_V rev_subsetD)

  {
    fix v0 assume "v0  S"
    fix P assume P: "vmc_path G P v0 p well_ordered_strategy"
    then interpret vmc_path G P v0 p well_ordered_strategy .
    have "visits_via P S W" proof (rule ccontr)
      assume contra: "¬visits_via P S W"

      hence "lset P  S - W" proof (induct rule: vmc_path_lset_induction)
        case base
        show "v0  S - W" using v0  S contra visits_via_trivial by blast
      next
        case (step P v0)
        interpret vmc_path_no_deadend G P v0 p well_ordered_strategy using step.hyps(1) .
        have "insert v0 S = S" using step.hyps(2) by blast
        hence *: "¬visits_via (ltl P) S W"
          using visits_via_LCons[of "ltl P" S W v0, folded P_LCons] step.hyps(3) by auto
        hence **: "w0  W" using vmc_path.visits_via_trivial[OF vmc_path_ltl] by blast
        have "w0  S  W" proof (cases)
          assume "v0  VV p"
          hence "well_ordered_strategy v0 = w0" using v0_conforms by blast
          hence "choose v0 v0 = w0" using step.hyps(2) well_ordered_strategy_def by auto
          moreover have "strategy_attracts_via p (choose v0) v0 S W"
            using choose_good good_def step.hyps(2) by blast
          ultimately show ?thesis
            by (metis strategy_attracts_via_successor strategy_attracts_via_v0
                      choose_strategy step.hyps(2) v0_edge_w0 w0_V)
        qed (metis DiffD1 assms(2) step.hyps(2) strategy_attracts_via_successor
                   strategy_attracts_via_v0 v0_edge_w0 w0_V)
        with * ** show ?case by blast
      qed

      have "¬lfinite P" proof
        assume "lfinite P"
        hence "deadend (llast P)" using P_maximal P_not_null maximal_ends_on_deadend by blast
        moreover have "llast P  S - W" using lset P  S - W P_not_null lfinite P lfinite_lset by blast
        ultimately show False using S_W_no_deadends by blast
      qed

      obtain n where n: "path_conforms_with_strategy p (ldropn n P) (path_strategies P $ n)"
        using path_eventually_conforms_to_σ_map_n[OF lset P  S - W P_valid P_conforms]
          by blast
      define σ' where [simp]: "σ' = path_strategies P $ n"
      define P' where [simp]: "P' = ldropn n P"
      interpret vmc_path G P' "lhd P'" p σ'
      proof
        show "¬lnull P'" unfolding P'_def
          using ¬lfinite P lfinite_ldropn lnull_imp_lfinite by blast
      qed (simp_all add: n)
      have "strategy p σ'" unfolding σ'_def
        using path_strategies_strategy lset P  S - W ¬lfinite P infinite_small_llength
        by blast
      moreover have "strategy_attracts_via p σ' (lhd P') S W" proof-
        have "P $ n  S - W" using lset P  S - W ¬lfinite P lset_nth_member_inf by blast
        hence "σ'  good (P $ n)"
          using path_strategies_good σ'_def ¬lfinite P lset P  S - W by blast
        hence "strategy_attracts_via p σ' (P $ n) S W" unfolding good_def by blast
        thus ?thesis unfolding P'_def using P_0 by (simp add: ¬lfinite P infinite_small_llength)
      qed
      moreover from lset P  S - W have "lset P'  S - W"
        unfolding P'_def using lset_ldropn_subset[of n P] by blast
      ultimately show False using strategy_attracts_via_lset by blast
    qed
  }
  thus ?thesis using well_ordered_strategy_valid by blast
qed


subsection ‹A Uniform Winning Strategy›

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

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

  have no_VVp_deadends: "v.  v  winning_region p; v  VV p   ¬deadend v"
    using no_winning_strategy_on_deadends unfolding winning_region_def by blast

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

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

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

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

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

      obtain n where n: "path_conforms_with_strategy p (ldropn n P) (path_strategies P $ n)"
        using path_eventually_conforms_to_σ_map_n[OF lset P  winning_region p P_valid P_conforms] by blast
      define σ' where [simp]: "σ' = path_strategies P $ n"
      define P' where [simp]: "P' = ldropn n P"
      interpret P': vmc_path G P' "lhd P'" p σ' proof
        show "¬lnull P'" using ¬lfinite P unfolding P'_def
          using lfinite_ldropn lnull_imp_lfinite by blast
      qed (simp_all add: n)
      have "strategy p σ'" unfolding σ'_def
        using path_strategies_strategy lset P  winning_region p ¬lfinite P by blast
      moreover have "winning_strategy p σ' (lhd P')" proof-
        have "P $ n  winning_region p"
          using lset P  winning_region p ¬lfinite P lset_nth_member_inf by blast
        hence "σ'  good (P $ n)"
          using path_strategies_good choose_good σ'_def ¬lfinite P lset P  winning_region p
          by blast
        hence "winning_strategy p σ' (P $ n)" unfolding good_def by blast
        thus ?thesis
          unfolding P'_def using P_0 ¬lfinite P by (simp add: infinite_small_llength lhd_ldropn)
      qed
      ultimately have "winning_path p P'" unfolding winning_strategy_def
        using P'.vmc_path_axioms by blast
      moreover have "¬lfinite P'" using ¬lfinite P P'_def by simp
      ultimately show False using contra winning_path_drop_add[OF P_valid] by auto
    qed
  }
  thus ?thesis unfolding winning_strategy_def using well_ordered_strategy_valid by auto
qed

subsection ‹Extending Winning Regions›

text ‹
  Now we are finally able to prove the complement of winning_region_extends_VVp› for
  @{term "VV p**"} nodes, which was still missing.
›

lemma winning_region_extends_VVpstar:
  assumes v: "v  VV p**" and w: "w. vw  w  winning_region p"
  shows "v  winning_region p"
proof-
  obtain σ where σ: "strategy p σ"  "v. v  winning_region p  winning_strategy p σ v"
    using merge_winning_strategies by blast
  have "winning_strategy p σ v" using strategy_extends_backwards_VVpstar[OF v σ(1)] σ(2) w by blast
  thus ?thesis unfolding winning_region_def using v σ(1) by blast
qed

text ‹It immediately follows that removing a winning region cannot create new deadends.›

lemma removing_winning_region_induces_no_deadends:
  assumes "v  V - winning_region p" "¬deadend v"
  shows "w  V - winning_region p. vw"
  using assms winning_region_extends_VVp winning_region_extends_VVpstar by blast

end ― ‹context ParityGame›

end