Theory GaleStewartDefensiveStrategies

subsection ‹Defensive strategies›

text ‹ A strategy is defensive if a player can avoid reaching winning positions.
       If the opponent is not already in a winning position, such defensive strategies exist.
       In closed games, a defensive strategy is winning for the closed player,
       so these strategies are a crucial step towards proving that such games are determined.
        ›
theory GaleStewartDefensiveStrategies
  imports GaleStewartGames
begin

context GSgame
begin

definition move_defensive_by_Even where
  "move_defensive_by_Even m p ≡ even (length p) ⟶ ¬ winning_position_Odd (p @ [m])"
definition move_defensive_by_Odd where
  "move_defensive_by_Odd m p  ≡ odd (length p) ⟶ ¬ winning_position_Even (p @ [m])"

(* This was a tricky part of the proof, it required explicit use of the choice theorem *)
lemma defensive_move_exists_for_Even:
assumes [intro]:"position p"
shows "winning_position_Odd p ∨ (∃ m. move_defensive_by_Even m p)" (is "?w ∨ ?d")
proof(cases "length p = 2*N ∨ odd (length p)")
  case False
  hence pl[intro]:"length p < 2*N"
    and ev[intro]:"even (length p)" using assms[unfolded position_def] by auto
  show ?thesis proof(rule impI[of "¬ ?d ⟶ ¬ ?w ⟶ False", rule_format], force)
    assume not_def:"¬ ?d"
    from not_def[unfolded move_defensive_by_Even_def]
    have "∀ m. ∃σ. strategy_winning_by_Odd σ (p @ [m])" by blast
    from choice[OF this] obtain σo where
      str_Odd:"⋀ m. strategy_winning_by_Odd (σo m) (p @ [m])" by blast
    define σ where "σ p' = σo (p' ! length p) p'" for p'
    assume not_win:"¬ ?w"
    from not_win[unfolded move_defensive_by_Even_def strategy_winning_by_Odd_def]
    obtain σe where
      str_Even:"induced_play (joint_strategy σe σ) p ∈ A"
      (is "?pe p ∈ A")
           by blast
    let ?pnext = "(p @ [joint_strategy σe σ p])"
    { fix p' m
      assume "prefix (p @ [m]) p'"
      hence "(p' ! length p) = m"
        unfolding prefix_def by auto
    }
    hence eq_a:"∀ p'. prefix ?pnext p' ⟶ p' @ [joint_strategy σe σ p'] =
                                    p' @ [joint_strategy σe (σo (joint_strategy σe σ p)) p']"
      unfolding joint_strategy_def σ_def by auto
    have simps:"?pe p = ?pe (p @ [joint_strategy σe σ p])"
      unfolding induced_play_def by auto
    from str_Even str_Odd[of "joint_strategy σe σ p", unfolded strategy_winning_by_Odd_def, rule_format, of "σe"]
         induced_play_eq[OF eq_a]
    show False unfolding simps by auto
  qed
qed (auto simp: move_defensive_by_Even_def strategy_winning_by_Even_def position_maxlength_cannotbe_augmented)

(* This is a repetition of the proof for defensive_move_exists_for_Even *)
lemma defensive_move_exists_for_Odd:
assumes [intro]:"position p"
shows "winning_position_Even p ∨ (∃ m. move_defensive_by_Odd m p)" (is "?w ∨ ?d")
proof(cases "length p = 2*N ∨ even (length p)")
  case False
  hence pl[intro]:"length p < 2*N"
    and ev[intro]:"odd (length p)" using assms[unfolded position_def] by auto
  show ?thesis proof(rule impI[of "¬ ?d ⟶ ¬ ?w ⟶ False", rule_format], force)
    assume not_def:"¬ ?d"
    from not_def[unfolded move_defensive_by_Odd_def]
    have "∀ m. ∃σ. strategy_winning_by_Even σ (p @ [m])" by blast
    from choice[OF this] obtain σe where
      str_Even:"⋀ m. strategy_winning_by_Even (σe m) (p @ [m])" by blast
    define σ where "σ p' = σe (p' ! length p) p'" for p'
    assume not_win:"¬ ?w"
    from not_win[unfolded move_defensive_by_Odd_def strategy_winning_by_Even_def]
    obtain σo where
      str_Odd:"induced_play (joint_strategy σ σo) p ∉ A"
      (is "?pe p ∉ A")
           by blast
    let ?strat = "joint_strategy σ σo"
    let ?pnext = "(p @ [?strat p])"
    { fix p' m
      assume "prefix (p @ [m]) p'"
      hence "(p' ! length p) = m"
        unfolding prefix_def by auto
    }
    hence eq_a:"∀ p'. prefix ?pnext p' ⟶ p' @ [?strat p'] =
                                    p' @ [joint_strategy (σe (?strat p)) σo p']"
      unfolding joint_strategy_def σ_def by auto
    have simps:"?pe p = ?pe (p @ [?strat p])"
      unfolding induced_play_def by auto
    from str_Odd str_Even[of "?strat p", unfolded strategy_winning_by_Even_def, rule_format]
         induced_play_eq[OF eq_a]
    show False unfolding simps by auto
  qed
qed (auto simp: move_defensive_by_Odd_def strategy_winning_by_Odd_def position_maxlength_cannotbe_augmented)

definition defensive_strategy_Even where
"defensive_strategy_Even p ≡ SOME m. move_defensive_by_Even m p"
definition defensive_strategy_Odd where
"defensive_strategy_Odd p ≡ SOME m. move_defensive_by_Odd m p"

lemma position_augment:
  assumes "position ((augment_list f ^^ n) p)"
  shows "position p"
  using assms length_augment_list[of n f p] unfolding position_def
  by fastforce

lemma defensive_strategy_Odd:
  assumes "¬ winning_position_Even p"
  shows "¬ winning_position_Even (((augment_list (joint_strategy σe defensive_strategy_Odd)) ^^ n) p)"
proof -
  show ?thesis using assms proof(induct n arbitrary:p)
    case (Suc n)
    show ?case proof(cases "position p")
      case True
      from Suc.prems defensive_move_exists_for_Odd[OF True] defensive_strategy_Odd_def someI
      have "move_defensive_by_Odd (defensive_strategy_Odd p) p" by metis
      from this[unfolded move_defensive_by_Odd_def] Suc.prems
           non_winning_moves_remains_non_winning_Even[of p]
      have "¬ winning_position_Even (p @ [joint_strategy σe defensive_strategy_Odd p])"
        by (simp add:  joint_strategy_def True) 
      with Suc.hyps[of "p @ [joint_strategy σe defensive_strategy_Odd p]"]
      show ?thesis unfolding funpow_Suc_right comp_def by fastforce
    qed (insert position_augment,blast)
  qed auto
qed

lemma defensive_strategy_Even:
  assumes "¬ winning_position_Odd p"
  shows "¬ winning_position_Odd (((augment_list (joint_strategy defensive_strategy_Even σo)) ^^ n) p)"
proof -
  show ?thesis using assms proof(induct n arbitrary:p)
    case (Suc n)
    show ?case proof(cases "position p")
      case True
      from Suc.prems defensive_move_exists_for_Even[OF True] defensive_strategy_Even_def someI
      have "move_defensive_by_Even (defensive_strategy_Even p) p" by metis
      from this[unfolded move_defensive_by_Even_def] Suc.prems
           non_winning_moves_remains_non_winning_Odd[of p]
      have "¬ winning_position_Odd (p @ [joint_strategy defensive_strategy_Even σo p])"
        by (simp add: joint_strategy_def True) 
      with Suc.hyps[of "p @ [joint_strategy defensive_strategy_Even σo p]"]
      show ?thesis unfolding funpow_Suc_right comp_def by fastforce
    qed (insert position_augment,blast)
  qed auto
qed


end

locale closed_GSgame = GSgame +
  assumes closed:"e ∈ A ⟹ ∃ p. lprefix (llist_of p) e ∧ (∀ e'. lprefix (llist_of p) e' ⟶ llength e' = 2*N ⟶ e' ∈ A)"

(* Perhaps a misnomer, GSgames are supposed to be infinite ... *)
locale finite_GSgame = GSgame +
  assumes fin:"N ≠ ∞"
begin

text ‹ Finite games are closed games. As a corollary to the GS theorem, this lets us conclude that finite games are determined. ›
sublocale closed_GSgame
proof
  fix e assume eA:"e ∈ A"
  let ?p = "list_of e"
  from eA have len:"llength e = 2*N" using length by blast
  with fin have p:"llist_of ?p = e"
    by (metis llist_of_list_of mult_2 not_lfinite_llength plus_eq_infty_iff_enat)
  hence pfx:"lprefix (llist_of ?p) e" by auto
  { fix e'
    assume "lprefix (llist_of ?p) e'" "llength e' = 2 * N"
    hence "e' = e" using len by (metis lprefix_llength_eq_imp_eq p)
    with eA have "e' ∈ A" by simp
  }
  with pfx show "∃p. lprefix (llist_of p) e ∧ (∀e'. lprefix (llist_of p) e' ⟶ llength e' = 2 * N ⟶ e' ∈ A)"
    by blast
qed
end

context closed_GSgame begin
lemma never_winning_is_losing_even:
  assumes "position p" "∀ n. ¬ winning_position_Even (((augment_list σ) ^^ n) p)"
  shows "induced_play σ p ∉ A"
proof
  assume "induced_play σ p ∈ A"
  from closed[OF this] obtain p' where
    p':"lprefix (llist_of p') (induced_play σ p)"
    "⋀ e. lprefix (llist_of p') e ⟹ llength e = 2 * N ⟹ e ∈ A" by blast
  from lprefix_llength_le[OF p'(1)] have lp':"llength (llist_of p') ≤ 2 * N" by auto
  show False proof (cases "length p' ≤ length p")
    case True
    hence "llength (llist_of p') ≤ llength (llist_of p)" by auto
    from lprefix_llength_lprefix[OF p'(1) _ this]
      induced_play_is_lprefix[OF assms(1)]
      lprefix_trans
    have pref:"lprefix (llist_of p') (induced_play strat p)" for strat by blast
    from assms(2)[rule_format,of 0] assms(1) have "¬ strategy_winning_by_Even σ p" for σ by auto
    from this[unfolded strategy_winning_by_Even_def] obtain strat where
      strat:"induced_play strat p ∉ A" by auto
    from strat p'(2)[OF pref] show False by simp
  next
    case False
    let ?n = "length p' - length p"
    let ?pos = "(augment_list σ ^^ ?n) p"
    from False have "length p' ≥ length p" by auto
    hence [simp]:"length ?pos = length p'"
      by (auto simp:length_augment_list)
    hence pos[intro]:"position ?pos"
      using False lp'(1) unfolding position_def by auto
    have "llist_of p' = llist_of ?pos"
      using p'(1)
      by(intro lprefix_antisym[OF lprefix_llength_lprefix lprefix_llength_lprefix],auto)
    hence p'_pos:"p' = ?pos" by simp
    from assms(2)[rule_format,of ?n] assms(1) have "¬ strategy_winning_by_Even σ ?pos" for σ by auto
    from this[unfolded strategy_winning_by_Even_def] obtain strat where
      strat:"induced_play strat ?pos ∉ A" by auto
    from p'_pos induced_play_is_lprefix[OF pos, of strat]
    have pref:"lprefix (llist_of p') (induced_play strat ?pos)" by simp
    with p'(2)[OF pref] strat show False by simp
  qed
qed

lemma every_position_is_determined:
  assumes "position p"
  shows "winning_position_Even p ∨ winning_position_Odd p" (is "?we ∨ ?wo")
proof(rule impI[of "¬ ?we ⟶ ¬ ?wo ⟶ False",rule_format],force)
  assume "¬ ?we"
  from defensive_strategy_Odd[OF this] never_winning_is_losing_even[OF assms]
  have js_no:"induced_play
         (joint_strategy s defensive_strategy_Odd) p ∉ A" for s
    by auto
  assume "¬ ?wo"
  from this[unfolded strategy_winning_by_Odd_def] assms
  have "∃ s. induced_play
         (joint_strategy s defensive_strategy_Odd) p ∈ A" by simp
  thus False using js_no by simp
qed

end

end