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" "v→w" "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" "v→w" "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 σ ‹v→w› 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. v→w ⟹ 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. v→w" using assms winning_region_extends_VVp winning_region_extends_VVpstar by blast end ― ‹context ParityGame› end