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; vw; 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 "vw" 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