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
    ― ‹The set of good strategies on a node @{term v}›
    and good :: "'a ⇒ 'a Strategy set"
    and r :: "('a Strategy × 'a Strategy) set"
  assumes S_V: "S ⊆ V"
    ― ‹@{term r} is a wellorder on the set of all strategies which are good somewhere.›
    and r_wo: "well_order_on {σ. ∃v ∈ S. σ ∈ good v} r"
    ― ‹Every node has a good strategy.›
    and good_ex: "⋀v. v ∈ S ⟹ ∃σ. σ ∈ good v"
    ― ‹good strategies are well-formed strategies.›
    and good_strategies: "⋀v σ. σ ∈ good v ⟹ strategy p σ"
    ― ‹A good strategy on @{term v} is also good on possible successors of @{term v}.›
    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)"

unbundle no binomial_syntax

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 ― ‹WellOrderedStrategies›

end