Theory WellOrderedStrategy
section ‹Well-Ordered Strategy›
theory WellOrderedStrategy
imports
Main
Strategy
begin
text ‹
Constructing a uniform strategy from a set of strategies on a set of nodes often works by
well-ordering the strategies and then choosing the minimal strategy on each node.
Then every path eventually follows one strategy because we choose the strategies along the path
to be non-increasing in the well-ordering.
The following locale formalizes this idea.
We will use this to construct uniform attractor and winning strategies.
›
locale WellOrderedStrategies = ParityGame +
fixes S :: "'a set"
and p :: Player
and good :: "'a ⇒ 'a Strategy set"
and r :: "('a Strategy × 'a Strategy) set"
assumes S_V: "S ⊆ V"
and r_wo: "well_order_on {σ. ∃v ∈ S. σ ∈ good v} r"
and good_ex: "⋀v. v ∈ S ⟹ ∃σ. σ ∈ good v"
and good_strategies: "⋀v σ. σ ∈ good v ⟹ strategy p σ"
and strategies_continue: "⋀v w σ. ⟦ v ∈ S; v→w; v ∈ VV p ⟹ σ v = w; σ ∈ good v ⟧ ⟹ σ ∈ good w"
begin
text ‹The set of all strategies which are good somewhere.›
abbreviation "Strategies ≡ {σ. ∃v ∈ S. σ ∈ good v}"
definition minimal_good_strategy where
"minimal_good_strategy v σ ≡ σ ∈ good v ∧ (∀σ'. (σ', σ) ∈ r - Id ⟶ σ' ∉ good v)"
no_notation binomial (infixl "choose" 65)
text ‹Among the good strategies on @{term v}, choose the minimum.›
definition choose where
"choose v ≡ THE σ. minimal_good_strategy v σ"
text ‹
Define a strategy which uses the minimum strategy on all nodes of @{term S}.
Of course, we need to prove that this is a well-formed strategy.
›
definition well_ordered_strategy where
"well_ordered_strategy ≡ override_on σ_arbitrary (λv. choose v v) S"
text ‹Show some simple properties of the binary relation @{term r} on the set @{const Strategies}.›
lemma r_refl [simp]: "refl_on Strategies r"
using r_wo unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by blast
lemma r_total [simp]: "total_on Strategies r"
using r_wo unfolding well_order_on_def linear_order_on_def by blast
lemma r_trans [simp]: "trans r"
using r_wo unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by blast
lemma r_wf [simp]: "wf (r - Id)"
using well_order_on_def r_wo by blast
text ‹@{const choose} always chooses a minimal good strategy on @{term S}.›
lemma choose_works:
assumes "v ∈ S"
shows "minimal_good_strategy v (choose v)"
proof-
have wf: "wf (r - Id)" using well_order_on_def r_wo by blast
obtain σ where σ1: "minimal_good_strategy v σ"
unfolding minimal_good_strategy_def by (meson good_ex[OF ‹v ∈ S›] wf wf_eq_minimal)
hence σ: "σ ∈ good v" "⋀σ'. (σ', σ) ∈ r - Id ⟹ σ' ∉ good v"
unfolding minimal_good_strategy_def by auto
{ fix σ' assume "minimal_good_strategy v σ'"
hence σ': "σ' ∈ good v" "⋀σ. (σ, σ') ∈ r - Id ⟹ σ ∉ good v"
unfolding minimal_good_strategy_def by auto
have "(σ, σ') ∉ r - Id" using σ(1) σ'(2) by blast
moreover have "(σ', σ) ∉ r - Id" using σ(2) σ'(1) by auto
moreover have "σ ∈ Strategies" using σ(1) ‹v ∈ S› by auto
moreover have "σ' ∈ Strategies" using σ'(1) ‹v ∈ S› by auto
ultimately have "σ' = σ"
using r_wo Linear_order_in_diff_Id well_order_on_Field well_order_on_def by fastforce
}
with σ1 have "∃!σ. minimal_good_strategy v σ" by blast
thus ?thesis using theI'[of "minimal_good_strategy v", folded choose_def] by blast
qed
corollary
assumes "v ∈ S"
shows choose_good: "choose v ∈ good v"
and choose_minimal: "⋀σ'. (σ', choose v) ∈ r - Id ⟹ σ' ∉ good v"
and choose_strategy: "strategy p (choose v)"
using choose_works[OF assms, unfolded minimal_good_strategy_def] good_strategies by blast+
corollary choose_in_Strategies: "v ∈ S ⟹ choose v ∈ Strategies" using choose_good by blast
lemma well_ordered_strategy_valid: "strategy p well_ordered_strategy"
proof-
{
fix v assume "v ∈ S" "v ∈ VV p" "¬deadend v"
moreover have "strategy p (choose v)"
using choose_works[OF ‹v ∈ S›, unfolded minimal_good_strategy_def, THEN conjunct1] good_strategies
by blast
ultimately have "v→(λv. choose v v) v" using strategy_def by blast
}
thus ?thesis unfolding well_ordered_strategy_def using valid_strategy_updates_set by force
qed
subsection ‹Strategies on a Path›
text ‹Maps a path to its strategies.›
definition "path_strategies ≡ lmap choose"
lemma path_strategies_in_Strategies:
assumes "lset P ⊆ S"
shows "lset (path_strategies P) ⊆ Strategies"
using path_strategies_def assms choose_in_Strategies by auto
lemma path_strategies_good:
assumes "lset P ⊆ S" "enat n < llength P"
shows "path_strategies P $ n ∈ good (P $ n)"
by (simp add: path_strategies_def assms choose_good lset_lnth_member)
lemma path_strategies_strategy:
assumes "lset P ⊆ S" "enat n < llength P"
shows "strategy p (path_strategies P $ n)"
using path_strategies_good assms good_strategies by blast
lemma path_strategies_monotone_Suc:
assumes P: "lset P ⊆ S" "valid_path P" "path_conforms_with_strategy p P well_ordered_strategy"
"enat (Suc n) < llength P"
shows "(path_strategies P $ Suc n, path_strategies P $ n) ∈ r"
proof-
define P' where "P' = ldropn n P"
hence "enat (Suc 0) < llength P'" using P(4)
by (metis enat_ltl_Suc ldrop_eSuc_ltl ldropn_Suc_conv_ldropn llist.disc(2) lnull_0_llength ltl_ldropn)
then obtain v w Ps where vw: "P' = LCons v (LCons w Ps)"
by (metis ldropn_0 ldropn_Suc_conv_ldropn ldropn_lnull lnull_0_llength)
moreover have "lset P' ⊆ S" unfolding P'_def using P(1) lset_ldropn_subset[of n P] by blast
ultimately have "v ∈ S" "w ∈ S" by auto
moreover have "v→w" using valid_path_edges'[of v w Ps, folded vw] valid_path_drop[OF P(2)] P'_def by blast
moreover have "choose v ∈ good v" using choose_good ‹v ∈ S› by blast
moreover have "v ∈ VV p ⟹ choose v v = w" proof-
assume "v ∈ VV p"
moreover have "path_conforms_with_strategy p P' well_ordered_strategy"
unfolding P'_def using path_conforms_with_strategy_drop P(3) by blast
ultimately have "well_ordered_strategy v = w" using vw path_conforms_with_strategy_start by blast
thus "choose v v = w" unfolding well_ordered_strategy_def using ‹v ∈ S› by auto
qed
ultimately have "choose v ∈ good w" using strategies_continue by blast
hence *: "(choose v, choose w) ∉ r - Id" using choose_minimal ‹w ∈ S› by blast
have "(choose w, choose v) ∈ r" proof (cases)
assume "choose v = choose w"
thus ?thesis using r_refl refl_onD choose_in_Strategies[OF ‹v ∈ S›] by fastforce
next
assume "choose v ≠ choose w"
thus ?thesis using * r_total choose_in_Strategies[OF ‹v ∈ S›] choose_in_Strategies[OF ‹w ∈ S›]
by (metis (lifting) Linear_order_in_diff_Id r_wo well_order_on_Field well_order_on_def)
qed
hence "(path_strategies P' $ Suc 0, path_strategies P' $ 0) ∈ r"
unfolding path_strategies_def using vw by simp
thus ?thesis unfolding path_strategies_def P'_def
using lnth_lmap_ldropn[OF Suc_llength[OF P(4)], of choose]
lnth_lmap_ldropn_Suc[OF P(4), of choose]
by simp
qed
lemma path_strategies_monotone:
assumes P: "lset P ⊆ S" "valid_path P" "path_conforms_with_strategy p P well_ordered_strategy"
"n < m" "enat m < llength P"
shows "(path_strategies P $ m, path_strategies P $ n) ∈ r"
using assms proof (induct "m - n" arbitrary: n m)
case (Suc d)
show ?case proof (cases)
assume "d = 0"
thus ?thesis using path_strategies_monotone_Suc[OF P(1,2,3)]
by (metis (no_types) Suc.hyps(2) Suc.prems(4,5) Suc_diff_Suc Suc_inject Suc_leI diff_is_0_eq diffs0_imp_equal)
next
assume "d ≠ 0"
have "m ≠ 0" using Suc.hyps(2) by linarith
then obtain m' where m': "Suc m' = m" using not0_implies_Suc by blast
hence "d = m' - n" using Suc.hyps(2) by presburger
moreover hence "n < m'" using ‹d ≠ 0› by presburger
ultimately have "(path_strategies P $ m', path_strategies P $ n) ∈ r"
using Suc.hyps(1)[of m' n, OF _ P(1,2,3)] Suc.prems(5) dual_order.strict_trans enat_ord_simps(2) m'
by blast
thus ?thesis
using m' path_strategies_monotone_Suc[OF P(1,2,3)] by (metis (no_types) Suc.prems(5) r_trans trans_def)
qed
qed simp
lemma path_strategies_eventually_constant:
assumes "¬lfinite P" "lset P ⊆ S" "valid_path P" "path_conforms_with_strategy p P well_ordered_strategy"
shows "∃n. ∀m ≥ n. path_strategies P $ n = path_strategies P $ m"
proof-
define σ_set where "σ_set = lset (path_strategies P)"
have "∃σ. σ ∈ σ_set" unfolding σ_set_def path_strategies_def
using assms(1) lfinite_lmap lset_nth_member_inf by blast
then obtain σ' where σ': "σ' ∈ σ_set" "⋀τ. (τ, σ') ∈ r - Id ⟹ τ ∉ σ_set"
using wfE_min[of "r - Id" _ σ_set] by auto
obtain n where n: "path_strategies P $ n = σ'"
using σ'(1) lset_lnth[of σ'] unfolding σ_set_def by blast
{
fix m assume "n ≤ m"
have "path_strategies P $ n = path_strategies P $ m" proof (rule ccontr)
assume *: "path_strategies P $ n ≠ path_strategies P $ m"
with ‹n ≤ m› have "n < m" using le_imp_less_or_eq by blast
with path_strategies_monotone have "(path_strategies P $ m, path_strategies P $ n) ∈ r"
using assms by (simp add: infinite_small_llength)
with * have "(path_strategies P $ m, path_strategies P $ n) ∈ r - Id" by simp
with σ'(2) n have "path_strategies P $ m ∉ σ_set" by blast
thus False unfolding σ_set_def path_strategies_def
using assms(1) lfinite_lmap lset_nth_member_inf by blast
qed
}
thus ?thesis by blast
qed
subsection ‹Eventually One Strategy›
text ‹
The key lemma: Every path that stays in @{term S} and follows @{const well_ordered_strategy}
eventually follows one strategy because the strategies are well-ordered and non-increasing
along the path.
›
lemma path_eventually_conforms_to_σ_map_n:
assumes "lset P ⊆ S" "valid_path P" "path_conforms_with_strategy p P well_ordered_strategy"
shows "∃n. path_conforms_with_strategy p (ldropn n P) (path_strategies P $ n)"
proof (cases)
assume "lfinite P"
then obtain n where "llength P = enat n" using lfinite_llength_enat by blast
hence "ldropn n P = LNil" by simp
thus ?thesis by (metis path_conforms_LNil)
next
assume "¬lfinite P"
then obtain n where n: "⋀m. n ≤ m ⟹ path_strategies P $ n = path_strategies P $ m"
using path_strategies_eventually_constant assms by blast
let ?σ = well_ordered_strategy
define P' where "P' = ldropn n P"
{ fix v assume "v ∈ lset P'"
hence "v ∈ S" using ‹lset P ⊆ S› P'_def in_lset_ldropnD by fastforce
from ‹v ∈ lset P'› obtain m where m: "enat m < llength P'" "P' $ m = v" by (meson in_lset_conv_lnth)
hence "P $ m + n = v" unfolding P'_def by (simp add: ‹¬lfinite P› infinite_small_llength)
moreover have "?σ v = choose v v" unfolding well_ordered_strategy_def using ‹v ∈ S› by auto
ultimately have "?σ v = (path_strategies P $ m + n) v"
unfolding path_strategies_def using infinite_small_llength[OF ‹¬lfinite P›] by simp
hence "?σ v = (path_strategies P $ n) v" using n[of "m + n"] by simp
}
moreover have "path_conforms_with_strategy p P' well_ordered_strategy"
unfolding P'_def by (simp add: assms(3) path_conforms_with_strategy_drop)
ultimately show ?thesis
using path_conforms_with_strategy_irrelevant_updates P'_def by blast
qed
end
end