Session GaleStewart_Games

Theory MoreCoinductiveList2

section ‹Coinductive lists›

theory MoreCoinductiveList2
  imports Parity_Game.MoreCoinductiveList (* for notation and lemmas like infinite_small_llength *)
begin

lemma ltake_infinity[simp]: "ltake  x = x" by (simp add: ltake_all)

lemma coinductive_eq_iff_lnth_eq:
  "a = b  (llength a = llength b  ( n. enat n < llength a  a $ n = b $ n))"
proof
  assume "llength a = llength b  (n. enat n < llength a  a $ n = b $ n)"
  hence len:"llength a = llength b"
    and lnth:"enat n < llength a  a $ n = b $ n" for n by auto
  show "a = b" proof(cases "llength a")
    case (enat nat)
    hence leq:"llist_of (list_of (ltake nat a)) = a" "llist_of (list_of (ltake nat b)) = b"
      by (auto simp add: len llength_eq_enat_lfiniteD ltake_all)
    with lnth_llist_of lnth
    have [intro]:"i < length (list_of (ltake (enat nat) a))  ltake (enat nat) a $ i = ltake (enat nat) b $ i" for i 
      by (metis enat_ord_code(4) enat_ord_simps(2) lfinite_ltake llength_llist_of llist_of_list_of)
    from len have [intro]:"length (list_of (ltake (enat nat) a)) = length (list_of (ltake (enat nat) b))"
      by (simp add: length_list_of_conv_the_enat)
    have "list_of (ltake nat a) = list_of (ltake nat b)" by(subst list_eq_iff_nth_eq, auto)
    then show ?thesis using leq by metis
  next
    case infinity
    hence inf:"¬ lfinite a" "¬ lfinite b" using len llength_eq_infty_conv_lfinite by auto
    from lnth[unfolded infinity] have "(($) a) = (($) b)" by auto
    then show ?thesis using inf[THEN inf_llist_lnth] by metis
  qed
qed auto

lemma coinductive_eq_I:
  assumes "(llength a = llength b  ( n. enat n < llength a  a $ n = b $ n))"
  shows "a = b"
  using coinductive_eq_iff_lnth_eq assms by auto
text ‹Our co-inductive lists will have Option types in them, so we can return None for out of bounds.›
definition lnth_option where
  "lnth_option xs i  if enat i < llength xs then xs $ i else None"

lemma enat_times_less:
  "enat c * enat lst < y * enat c  lst < y"
by (cases y;auto)

lemma llist_eq_lcons:
  assumes "a  LNil" "b  LNil" "lhd a = lhd b" "ltl a = ltl b"
  shows "a = b"
using assms by(cases a;cases b;auto)

end

Theory MoreENat

subsection ‹Theorems about the extended naturals›

text ‹Extended naturals are the natural numbers plus infinity.
      They are slightly more cumbersome to reason about, and this file contains
      some lemmas that should help with that.›

theory MoreENat
  imports MoreCoinductiveList2
begin

lemma eSuc_n_not_le_n[simp]:
"(eSuc x  x)  x = "
  by (metis enat_ord_simps(3) Suc_n_not_le_n antisym ile_eSuc le_add2 plus_1_eq_Suc the_enat_eSuc)

lemma mult_two_impl1[elim]:
  assumes "a * 2 = 2 * b"
  shows "(a::enat) = b" using assms by(cases a;cases b,auto simp add: mult_2 mult_2_right)

lemma mult_two_impl2[dest]:
  assumes "a * 2 = 1 + 2 * b"
  shows "(a::enat) =   b="
  apply(cases a;cases b)
  using assms Suc_double_not_eq_double[unfolded mult_2, symmetric] 
  by (auto simp add: mult_2 one_enat_def mult_2_right)

lemma mult_two_impl3[dest]:
  assumes "a * 2 = 1 + (2 * b - 1)"
  shows "(a::enat) = b  a  1"
  using assms by(cases a;cases b,auto simp add: one_enat_def mult_2 mult_2_right)

lemma mult_two_impl4[dest]:
  assumes "a * 2 = 2 * b - 1"
  shows "((a::enat) = 0  b = 0)  (a =   b=)"
proof(cases a;cases b)
  fix anat bnat
  assume *:"a = enat anat" "b = enat bnat"
  hence "anat + anat = bnat + bnat - Suc 0"
    using assms by (auto simp add:enat_0_iff one_enat_def mult_2 mult_2_right)
  thus ?thesis unfolding * using Suc_double_not_eq_double[unfolded mult_2, symmetric]
    by (metis Suc_pred add_gr_0 enat_0_iff(1) neq0_conv not_less0 zero_less_diff)
qed(insert assms,auto simp add:enat_0_iff one_enat_def mult_2 mult_2_right)


lemma times_two_div_two[intro]:
  assumes "enat n < x" shows "2 * enat (n div 2) < x"
proof -
  have "2 * n div 2  n" by auto
  hence "2 * enat (n div 2)  enat n"
    using enat_numeral enat_ord_simps(2) linorder_not_less mult.commute times_enat_simps(1) 
  by (metis div_times_less_eq_dividend)
  with assms show ?thesis by auto
qed

lemma enat_sum_le[simp]:
  shows "enat (a + b)  c  b  c"
  by (meson dual_order.trans enat_ord_simps(1) le_add2)


lemma enat_Suc_nonzero[simp]:
shows "enat (Suc n) 0"
 by (metis Zero_not_Suc enat.inject zero_enat_def)

end

Theory MorePrefix

section ‹Extra theorems on prefixes of Lists and their coinductive counterparts›

theory MorePrefix
  imports MoreCoinductiveList2 (* for notation and lemmas like infinite_small_llength *)
begin

subsection ‹ Reasoning about prefixes ›
lemma head_prefixes [simp]:
  "prefixes list ! 0 = []"
  by (metis hd_conv_nth hd_prefixes prefixes_not_Nil)

lemma non_head_prefixes [simp]:
  assumes "n < length p" shows "(prefixes p ! Suc n)  []"
proof -
  have "0 < length (prefixes p)" "Suc n < length (prefixes p)" by (auto simp: assms)
  then show ?thesis by (metis Zero_not_Suc distinct_prefixes head_prefixes nth_eq_iff_index_eq)
qed

lemma last_prefixes:
  assumes "i < length p"
  shows "last (tl (prefixes p) ! i) = p ! i"
  using assms
proof(induct p arbitrary:i)
  case (Cons a p i)
  show ?case proof(cases i)
    case (Suc nat)
    with Cons have "p ! nat = last (tl (prefixes p) ! nat)" "nat < length p" by auto
    then show ?thesis unfolding Suc by(auto simp:nth_tl)
  qed auto
qed force

lemma take_1_prefixes[simp]:
  "take (Suc 0) (prefixes list) = [[]]"
  by (simp add: take_Suc)

lemma map_last_prefixes [simp]:
  shows "map last (tl (prefixes p)) = p"
  unfolding list_eq_iff_nth_eq
  using last_prefixes by auto

lemma ltake_zero[simp]: "ltake (enat (0::nat)) lst = LNil"
  (* nitpick finds a counterexample in Isabelle2021*)
  by (simp add: zero_enat_def)

lemma ltakes_one_iterates:
  "ltake (enat (Suc 0)) (iterates f p) = LCons p LNil"
  by (metis One_nat_def iterates_lmap ltake_eSuc_LCons ltake_zero one_eSuc one_enat_def zero_enat_def)

lemma ltakes_suc_iterates[simp]:
  "ltake (enat (Suc n)) (iterates f p) = LCons p (ltake (enat n) (iterates f (f p)))"
  by (induct n,force simp:ltakes_one_iterates,metis eSuc_enat iterates.code ltake_eSuc_LCons)

lemma prefixes_nth_take[simp]:
  assumes "i  length p"
  shows "prefixes p ! i = take i p"
  using assms proof(induct p arbitrary:i)
  case (Cons a p i) thus ?case by (cases i, auto)
qed auto

lemma tl_prefixes_idx:
  assumes "i < length p"
  shows "tl (prefixes p) ! i = take (Suc i) p"
  using assms by(induct p,auto)

lemma list_of_lappend_llist_of[simp]:
  assumes "lfinite q"
  shows "list_of (lappend (llist_of p) q) = append p (list_of q)"
  using assms by(induct p,auto)

lemma nth_prefixes:
  "n < length p  ¬ Suc n < length p  tl (prefixes p) ! n = p"
  by(induct p arbitrary:n,auto)

lemma take_Suc_prefix:
  "prefix (take n p) (take (Suc n) p)"
proof(induct p arbitrary:n)
  case (Cons a p n)
  then show ?case by(cases n,auto)
qed auto

lemma nth_prefixes_is_prefix:
  "n < length p   prefix ((prefixes p) ! n) ((prefixes p) ! Suc n)"
  by(induct "length p" n arbitrary:p rule:diff_induct,auto simp:take_Suc_prefix)

lemma nth_prefixes_is_prefix_tl:
  "Suc n < length p   prefix (tl (prefixes p) ! n) (tl (prefixes p) ! Suc n)"
  by (cases p) (auto simp:nth_prefixes_is_prefix take_Suc_prefix)

lemma prefix_same_length_eq:
  shows "(prefix a b  length a = length b)  a = b"
  by (metis prefix_length_le prefix_length_prefix prefix_order.antisym prefix_order.order_refl)

lemma prefix_takeI:
  assumes "prefix a b" "n  length a"
  shows "prefix a (take n b)"
  using assms 
  by (smt (verit) prefix_length_prefix length_take min.absorb2 nat_le_linear take_all take_is_prefix)

thm prefix_length_prefix (* compare to *)
lemma lprefix_llength_lprefix:
  assumes "lprefix a c" "lprefix b c" "llength a  llength b"
  shows "lprefix a b"
  using assms
  by (metis dual_order.antisym lprefix_down_linear lprefix_llength_eq_imp_eq lprefix_llength_le)

thm prefix_takeI (* compare to *)
lemma lprefix_ltakeI:
  assumes "lprefix a b" "llength a  n"
  shows "lprefix a (ltake n b)"
  by (smt (verit, best) dual_order.antisym lappend_eq_lappend_conv lappend_ltake_ldrop llength_ltake
                        assms lprefix_conv_lappend lprefix_down_linear lprefix_llength_le min_def)

abbreviation augment_list where
  "augment_list σ p  p @ [σ p]"

lemma length_augment_list:
  "length ((augment_list f ^^ n) p) = n + length p"
  by(induct n,auto)

lemma augment_list_nonempty:
  assumes "p[]" shows "(augment_list f ^^ i) p  []"
  using assms by(cases i,auto)

lemma augment_list_Suc_prefix:
  "prefix ((augment_list f ^^ n) p) ((augment_list f ^^ Suc n) p)"
  by(cases n,auto simp:take_Suc_prefix)

lemma augment_list_prefix:
  "n  m  prefix ((augment_list f ^^ n) p) ((augment_list f ^^ m) p)"
proof(induct "m-n" arbitrary:m n)
  case (Suc x)
  hence [simp]:"Suc (x + n) = m" by auto
  from Suc.hyps(2) 
    prefix_order.order.trans[OF Suc.hyps(1)[of "x + n" n] augment_list_Suc_prefix[of "x+n" f p]]
  show ?case by auto
qed auto

lemma augment_list_nonsense[dest]:
assumes "(augment_list σ ^^ n) p = []"
shows "n=0" "p=[]"
using assms by(induct n,auto)

lemma prefix_augment:
  shows "prefix p ((augment_list s ^^ n) p)"
  by (induct n,auto simp:prefix_def)


end

Theory AlternatingLists

section ‹ Alternating lists ›

text ‹In lists where even and odd elements play different roles, it helps to define functions to
      take out the even elements. We defined the function (l)alternate on (coinductive) lists to
      do exactly this, and define certain properties.›

theory AlternatingLists
  imports MoreCoinductiveList2 (* for notation and lemmas like infinite_small_llength *)
begin

text ‹The functions ``alternate" and ``lalternate" are our main workhorses:
      they take every other item, so every item at even indices.›

fun alternate where
  "alternate Nil = Nil" |
  "alternate (Cons x xs) = Cons x (alternate (tl xs))"

text ‹``lalternate" takes every other item from a co-inductive list.›
primcorec lalternate :: "'a llist  'a llist"
  where
    "lalternate xs = (case xs of LNil  LNil |
                                 (LCons x xs)  LCons x (lalternate (ltl xs)))"

lemma lalternate_ltake:
  "ltake (enat n) (lalternate xs) = lalternate (ltake (2*n) xs)"
proof(induct n arbitrary:xs)
  case 0
  then show ?case by (metis LNil_eq_ltake_iff enat_defs(1) lalternate.ctr(1) lnull_def mult_zero_right)
next
  case (Suc n)
  hence lt:"ltake (enat n) (lalternate (ltl (ltl xs))) = lalternate (ltake (enat (2 * n)) (ltl (ltl xs)))".
  show ?case
  proof(cases "lalternate xs")
    case LNil
    then show ?thesis by(metis lalternate.disc(2) lnull_def ltake_LNil)
  next
    case (LCons x21 x22)
    thus ?thesis unfolding ltake_ltl mult_Suc_right add_2_eq_Suc
      using eSuc_enat lalternate.code lalternate.ctr(1) lhd_LCons_ltl llist.sel(1)
      by (smt (z3) lt ltake_ltl llist.simps(3) llist.simps(5) ltake_eSuc_LCons)
  qed
qed

lemma lalternate_llist_of[simp]:
  "lalternate (llist_of xs) = llist_of (alternate xs)"
proof(induct "alternate xs" arbitrary:xs)
  case Nil
  then show ?case
    by (metis alternate.elims lalternate.ctr(1) list.simps(3) llist_of.simps(1) lnull_llist_of)
next
  case (Cons a xs)
  then show ?case by(cases xs,auto simp: lalternate.ctr)
qed

lemma lalternate_finite_helper: (* The other direction is proved later, added as SIMP rule *)
  assumes "lfinite (lalternate xs)"
  shows "lfinite xs"
using assms proof(induct "lalternate xs" arbitrary:xs rule:lfinite_induct)
  case LNil
  then show ?case unfolding lalternate.code[of xs] by(cases xs;auto)
next
  case (LCons xs)
  then show ?case unfolding lalternate.code[of xs] by(cases "xs";cases "ltl xs";auto)
qed

lemma alternate_list_of: (* Note that this only holds for finite lists,
                    as the other direction is left undefined with arguments (not just undefined) *)
  assumes "lfinite xs"
  shows "alternate (list_of xs) = list_of (lalternate xs)"
  using assms by (metis lalternate_llist_of list_of_llist_of llist_of_list_of)

lemma alternate_length:
  "length (alternate xs) = (1+length xs) div 2"
  by (induct xs rule:induct_list012;simp)

lemma lalternate_llength:
  "llength (lalternate xs) * 2 = (1+llength xs)  llength (lalternate xs) * 2 = llength xs"
proof(cases "lfinite xs")
  case True
  let ?xs = "list_of xs"
  have "length (alternate ?xs) = (1+length ?xs) div 2" using alternate_length by auto
  hence "length (alternate ?xs) * 2 = (1+length ?xs)  length (alternate ?xs) * 2 = length ?xs"
    by auto
  then show ?thesis using alternate_list_of[OF True] lalternate_llist_of True
    length_list_of_conv_the_enat[OF True] llist_of_list_of[OF True]
    by (metis llength_llist_of numeral_One of_nat_eq_enat of_nat_mult of_nat_numeral plus_enat_simps(1))
next
  case False
  have "¬ lfinite (lalternate xs)" using False lalternate_finite_helper by auto
  hence l1:"llength (lalternate xs) = " by(rule not_lfinite_llength)
  from False have l2:"llength xs = " using not_lfinite_llength by auto
  show ?thesis using l1 l2 by (simp add: mult_2_right)
qed

lemma lalternate_finite[simp]:
  shows "lfinite (lalternate xs) = lfinite xs"
proof(cases "lfinite xs")
  case True
  then show ?thesis
  proof(cases "lfinite (lalternate xs)")
    case False
    hence False using not_lfinite_llength[OF False] True[unfolded lfinite_conv_llength_enat]
                      lalternate_llength[of xs]
                by (auto simp:one_enat_def numeral_eq_enat)
    thus ?thesis by metis
  qed auto
next
  case False
  then show ?thesis using lalternate_finite_helper by blast
qed

lemma nth_alternate:
  assumes "2*n < length xs"
  shows "alternate xs ! n = xs ! (2 * n)"
  using assms proof (induct xs arbitrary:n rule:induct_list012)
  case (3 x y zs)
  then show ?case proof(cases n)
    case (Suc nat)
    show ?thesis using "3.hyps"(1) "3.prems" Suc by force
  qed simp
qed auto

lemma lnth_lalternate:
  assumes "2*n < llength xs"
  shows "lalternate xs $ n = xs $ (2 * n)"
proof -
  let ?xs = "ltake (2*Suc n) xs"
  have "lalternate ?xs $ n = ?xs $ (2 * n)"
    using assms alternate_list_of[of "ltake (2*Suc n) xs"] nth_alternate[of n "list_of ?xs"]
    by (smt (z3) Suc_1 Suc_mult_less_cancel1 enat_ord_simps(2) infinite_small_llength lalternate_ltake length_list_of lessI llength_eq_enat_lfiniteD llength_ltake' ltake_all not_less nth_list_of numeral_eq_enat the_enat.simps times_enat_simps(1))
  thus ?thesis
    by (metis Suc_1 Suc_mult_less_cancel1 enat_ord_simps(2) lalternate_ltake lessI lnth_ltake)
qed

lemma lnth_lalternate2[simp]:
  assumes "n < llength (lalternate xs)"
  shows "lalternate xs $ n = xs $ (2 * n)"
proof -
  from assms have "2*enat n < llength xs"
    by (metis enat_numeral lalternate_ltake leI linorder_neq_iff llength_ltake' ltake_all times_enat_simps(1))
  from lnth_lalternate[OF this] show ?thesis.
qed

end

Theory GaleStewartGames

section ‹Gale Stewart Games›

text ‹Gale Stewart Games are infinite two player games.›
(* [Gale & Stewart 1953] David Gale, F. M. Stewart, Infinite games with perfect information,
   Contributions to the Theory of Games II, ed. H. W. Kuhn and A. W. Tucker,
   Annals of Mathematics Studies 28, Princeton University Press (1953), pp 245–266. *)

theory GaleStewartGames
  imports AlternatingLists MorePrefix MoreENat
begin

subsection ‹Basic definitions and their properties.›

text ‹A GSgame G(A) is defined by a set of sequences that denote the winning games for the first
      player. Our notion of GSgames generalizes both finite and infinite games by setting a game length.
      Note that the type of n is 'enat' (extended nat): either a nonnegative integer or infinity.
      Our only requirement on GSgames is that the winning games must have the length as specified
      as the length of the game. This helps certain theorems about winning look a bit more natural.›

locale GSgame =
  fixes A N
  assumes length:"eA. llength e = 2*N"
begin

text ‹A position is a finite sequence of valid moves.›
definition "position" where
  "position (e::'a list)  length e  2*N"

lemma position_maxlength_cannotbe_augmented:
assumes "length p = 2*N"
shows "¬ position (p @ [m])"
 by (auto simp:position_def assms[symmetric])

text ‹A play is a sequence of valid moves of the right length.›
definition "play" where
  "play (e::'a llist)  llength e = 2*N"

lemma plays_are_positions_conv:
  shows "play (llist_of p)  position p  length p = 2*N" 
unfolding play_def position_def by auto

lemma finite_plays_are_positions:
  assumes "play p" "lfinite p"
  shows "position (list_of p)"
using assms 
unfolding play_def position_def by (cases "lfinite p";auto simp:length_list_of)

end

text ‹We call our players Even and Odd, where Even makes the first move.
      This means that Even is to make moves on plays of even length, and Odd on the others.
      This corresponds nicely to Even making all the moves in an even position, as
      the `nth' and `lnth' functions as predefined in Isabelle's library count from 0.
      In literature the players are sometimes called I and II.›

text ‹A strategy for Even/Odd is simply a function that takes a position of even/odd length and
      returns a move. We use total functions for strategies. This means that their Isabelle-type
      determines that it is a strategy. Consequently, we do not have a definition of 'strategy'.
      Nevertheless, we will use $\sigma$ as a letter to indicate when something is a strategy.
      We can combine two strategies into one function, which gives a collective strategy that
      we will refer to as the joint strategy.›

definition joint_strategy  :: "('b list  'a)  ('b list  'a)  ('b list  'a)" where
  "joint_strategy σe σo p = (if even (length p) then σe p else σo p)"

text ‹Following a strategy leads to an infinite sequence of moves.
      Note that we are not in the context of 'GSGame' where 'N' determines the length of our plays:
      we just let sequences go on ad infinitum here.
      Rather than reasoning about our own recursive definitions,
      we build this infinite sequence by reusing definitions that are already in place.
      We do this by first defining all prefixes of the infinite sequence we are interested in.
      This gives an infinite list such that the nth element is of length n.
      Note that this definition allows us to talk about how a strategy would continue if it were
      played from an arbitrary position (not necessarily one that is reached via that strategy). ›

definition strategy_progression where
  "strategy_progression σ p = lappend (llist_of (prefixes p)) (ltl (iterates (augment_list σ) p))"

lemma induced_play_infinite:
  "¬ lfinite (strategy_progression σ p)"
unfolding strategy_progression_def by auto

lemma plays_from_strategy_lengths[simp]:
  "length (strategy_progression σ p $ i) = i"
proof(induct i)
  case 0
  then show ?case by(cases p;auto simp:strategy_progression_def lnth_lappend take_map ltake_lappend)
next
  case (Suc i)
  then show ?case
    by (cases "i<length p") (auto simp:strategy_progression_def lnth_lappend length_augment_list tl_prefixes_idx)
qed

lemma length_plays_from_strategy[simp]:
  "llength (strategy_progression σ p) = "
  unfolding strategy_progression_def by auto
lemma length_ltl_plays_from_strategy[simp]:
  "llength (ltl (strategy_progression σ p)) = "
  unfolding strategy_progression_def by auto

lemma plays_from_strategy_chain_Suc:
  shows "prefix (strategy_progression σ p  $  n) (strategy_progression σ p  $  Suc n)"
  unfolding strategy_progression_def
  by (auto simp:take_Suc_prefix nth_prefixes lnth_lappend nth_prefixes_is_prefix_tl
                augment_list_prefix)

lemma plays_from_strategy_chain:
  shows "n  m  prefix (strategy_progression σ p  $  n) (strategy_progression σ p  $  m)"
proof (induct "m-n" arbitrary:m n)
  case (Suc x)
  hence [simp]:"Suc (x + n) = m" by auto
  from Suc.hyps(2) 
    prefix_order.order.trans[OF Suc.hyps(1)[of "x + n" n] plays_from_strategy_chain_Suc[of _ _ "x+n"]]
  show ?case by auto
qed auto

lemma plays_from_strategy_remains_const:
  assumes "n  i"
  shows "take n (strategy_progression σ p  $  i)  =  strategy_progression σ p  $  n"
  apply(rule sym,subst prefix_same_length_eq[symmetric])
  using assms plays_from_strategy_chain[OF assms] 
  by (auto intro!:prefix_takeI)

lemma infplays_augment_one[simp]:
  "strategy_progression σ (p @ [σ p]) = strategy_progression σ p"
proof(induct p)
  note defs = strategy_progression_def
  {
    case Nil
    then show ?case
      by (auto simp:defs iterates.code[of _ "[σ []]"])
  next
    case (Cons a p)
    then show ?case
      by (auto simp:defs iterates.code[of _ "a # p @ [σ (a # p)]"] lappend_llist_of_LCons)
  }
qed

lemma infplays_augment_many[simp]:
  "strategy_progression σ ((augment_list σ ^^ n) p) = strategy_progression σ p"
by(induct n,auto)

lemma infplays_augment_one_joint[simp]:
  "even (length p)  strategy_progression (joint_strategy σe σo) (augment_list σe p)
                     = strategy_progression (joint_strategy σe σo) p"
  "odd (length p)   strategy_progression (joint_strategy σe σo) (augment_list σo p)
                     = strategy_progression (joint_strategy σe σo) p"
using infplays_augment_one[of "joint_strategy σe σo" p]
unfolding joint_strategy_def by auto

text ‹Following two different strategies from a single position will lead to the same plays
      if the strategies agree on moves played after that position.
      This lemma allows us to ignore the behavior of strategies for moves that are already played. ›
lemma infplays_eq:
  assumes " p'. prefix p p'  augment_list s1 p' = augment_list s2 p'"
  shows "strategy_progression s1 p = strategy_progression s2 p"
proof -
  from assms[of p] have [intro]:"s1 p = s2 p" by auto
  have "(augment_list s1 ^^ n) (augment_list s1 p) =
          (augment_list s2 ^^ n) (augment_list s2 p)" for n
    proof(induct n)
    case (Suc n)
    with assms[OF prefix_order.order.trans[OF _ prefix_augment]]
    show ?case by (auto)
  qed auto
  hence "strategy_progression s1 p $ n = strategy_progression s2 p $ n"
    for n (* different n *) unfolding strategy_progression_def lnth_lappend by auto
  thus ?thesis by(intro coinductive_eq_I,auto)
qed


context GSgame
begin

text ‹By looking at the last elements of the infinite progression,
      we can get a single sequence, which we trim down to the right length.
      Since it has the right length, this always forms a play.
      We therefore name this the 'induced play'. ›

definition induced_play where
  "induced_play σ  ltake (2*N) o lmap last o ltl o strategy_progression σ"

lemma induced_play_infinite_le[simp]:
  "enat x < llength (strategy_progression σ p)"
  "enat x < llength (lmap f (strategy_progression σ p))"
  "enat x < llength (ltake (2*N) (lmap f (strategy_progression σ p)))  x < 2*N"
using induced_play_infinite by auto

lemma induced_play_is_lprefix:
  assumes "position p"
  shows "lprefix (llist_of p) (induced_play σ p)"
proof -
  have l:"llength (llist_of p)  2 * N" using assms unfolding position_def by auto
  have "lprefix (llist_of p) (lmap last (ltl (llist_of (prefixes p))))" by auto
  hence "lprefix (llist_of p) ((lmap last o ltl o strategy_progression σ) p)"
    unfolding strategy_progression_def by(auto simp add: lmap_lappend_distrib lprefix_lappend)
  thus ?thesis unfolding induced_play_def o_def
    using lprefix_ltakeI[OF _ l] by blast
qed

lemma length_induced_play[simp]:
  "llength (induced_play s p) = 2 * N"
  unfolding induced_play_def by auto

lemma induced_play_lprefix_non_positions: (* 'opposite' of induced_play_is_lprefix *)
  assumes "length (p::'a list)  2 * N"
  shows "induced_play σ p = ltake (2 * N) (llist_of p)"
proof(cases "N")
  case (enat nat)
  let ?p = "take (2 * nat) p"
  from assms have [intro]:"2 * N  enat (length p)" by auto
  have [intro]:"2 * N  enat (min (length p) (2 * nat))" unfolding enat
    by (metis assms enat min.orderI min_def numeral_eq_enat times_enat_simps(1))
  have [intro]:"enat (min (length p) (2 * nat)) = 2 * N"
    by (metis (mono_tags, lifting) assms enat min.absorb2 min_enat_simps(1)
        numeral_eq_enat times_enat_simps(1))
  have n:"2 * N  llength (llist_of p)" "2 * N  llength (llist_of (take (2 * nat) p))" by auto
  have pp:"position ?p"
    apply(subst position_def) (* for some reason 'unfolding' does not work here, tested in Isabelle 2021 *)
    by (metis (no_types, lifting) assms dual_order.order_iff_strict enat llength_llist_of
               llength_ltake' ltake_llist_of numeral_eq_enat take_all times_enat_simps(1))
  have lp:"lprefix (llist_of ?p) (induced_play σ ?p)" by(rule induced_play_is_lprefix[OF pp])
  (* this would make a great separate lemma, but we have a conversion between N and its nat
     to make that more involved *)
  have "ltake (2 * N) (llist_of p) = ltake (2 * N) (llist_of (take (2 * nat) p))"
    unfolding ltake_llist_of[symmetric] enat ltake_ltake numeral_eq_enat by auto
  hence eq:"induced_play σ p = induced_play σ ?p"
    unfolding induced_play_def strategy_progression_def
    by(auto simp add: lmap_lappend_distrib n[THEN ltake_lappend1])
  have "llist_of (take (2 * nat) p) = induced_play σ p"
    by(rule lprefix_llength_eq_imp_eq[OF lp[folded eq]],auto)
  then show ?thesis
     unfolding enat ltake_llist_of[symmetric] (* simp applies this one in the wrong direction *)
               numeral_eq_enat times_enat_simps(1) by metis
next
  case infinity
  hence "2 * N = " by (simp add: imult_is_infinity)
  then show ?thesis using assms by auto
qed

lemma infplays_augment_many_lprefix[simp]:
  shows "lprefix (llist_of ((augment_list σ ^^ n) p)) (induced_play σ p)
        = position ((augment_list σ ^^ n) p)" (is "?lhs = ?rhs")
proof
  assume ?lhs
  from lprefix_llength_le[OF this] show ?rhs unfolding induced_play_def
    by (auto simp:position_def length_augment_list) next
  assume assm:?rhs
  from induced_play_is_lprefix[OF this, of "σ"]
  show ?lhs unfolding induced_play_def by simp
qed

subsection ‹ Winning strategies ›

text ‹ A strategy is winning (in position p) if, no matter the moves by the other player,
       it leads to a sequence in the winning set. ›
definition strategy_winning_by_Even where
  "strategy_winning_by_Even σe p  ( σo. induced_play (joint_strategy σe σo) p  A)"
definition strategy_winning_by_Odd where
  "strategy_winning_by_Odd σo p  ( σe. induced_play (joint_strategy σe σo) p  A)"

text ‹ It immediately follows that not both players can have a winning strategy. ›
lemma at_most_one_player_winning:
shows "¬ ( σe. strategy_winning_by_Even σe p)  ¬ ( σo. strategy_winning_by_Odd σo p)"
  unfolding strategy_winning_by_Even_def strategy_winning_by_Odd_def by auto

text ‹ If a player whose turn it is not makes any move, winning strategies remain winning.
       All of the following proofs are duplicated for Even and Odd,
       as the game is entirely symmetrical. These 'dual' theorems can be obtained
       by considering a game in which an additional first and final move are played yet ignored,
       but it is quite convenient to have both theorems at hand regardless, and the proofs are
       quite small, so we accept the code duplication. ›

lemma any_moves_remain_winning_Even:
  assumes "odd (length p)" "strategy_winning_by_Even σ p"
  shows "strategy_winning_by_Even σ (p @ [m])"
unfolding strategy_winning_by_Even_def proof
  fix σo
  let ?s = "σo(p:=m)"
  have prfx:"prefix (p @ [m]) p' 
             p' @ [joint_strategy σ σo p'] = p' @ [joint_strategy σ ?s p']"
    for p' by (auto simp: joint_strategy_def)
  from assms(2)[unfolded strategy_winning_by_Even_def,rule_format,of ?s]
       infplays_augment_one_joint(2)[OF assms(1)]
  have "induced_play (joint_strategy σ ?s) (augment_list ?s p)  A"
    by (metis (mono_tags, lifting) induced_play_def comp_apply)
  thus "induced_play (joint_strategy σ σo) (p @ [m])  A"
    unfolding induced_play_def o_def
    using infplays_eq[OF prfx] by auto
qed

lemma any_moves_remain_winning_Odd:
  assumes "even (length p)" "strategy_winning_by_Odd σ p"
  shows "strategy_winning_by_Odd σ (p @ [m])"
unfolding strategy_winning_by_Odd_def proof
  fix σe
  let ?s = "σe(p:=m)"
  have prfx:"prefix (p @ [m]) p' 
             p' @ [joint_strategy σe σ p'] = p' @ [joint_strategy ?s σ p']"
    for p' by (auto simp:joint_strategy_def)
  from assms(2)[unfolded strategy_winning_by_Odd_def,rule_format,of ?s]
       infplays_augment_one_joint(1)[OF assms(1)]
  have "induced_play (joint_strategy ?s σ) (augment_list ?s p)  A"
    by (metis (mono_tags, lifting) induced_play_def comp_apply)
  thus "induced_play (joint_strategy σe σ) (p @ [m])  A"
    unfolding induced_play_def o_def
    using infplays_eq[OF prfx] by auto
qed

text ‹ If a player does not have a winning strategy,
       a move by that player will not give it one. ›

lemma non_winning_moves_remains_non_winning_Even:
  assumes "even (length p)" " σ. ¬ strategy_winning_by_Even σ p"
  shows "¬ strategy_winning_by_Even σ (p @ [m])"
proof(rule contrapos_nn[of " σ. strategy_winning_by_Even σ p"])
  assume a:"strategy_winning_by_Even σ (p @ [m])"
  let ?s = "σ(p:=m)"
  have prfx:"prefix (p @ [m]) p' 
             p' @ [joint_strategy σ σo p'] = p' @ [joint_strategy ?s σo p']"
    for p' σo by (auto simp:joint_strategy_def)
  from a infplays_eq[OF prfx]
  have "strategy_winning_by_Even ?s (p @ [m])"
    unfolding strategy_winning_by_Even_def induced_play_def by simp
  hence "strategy_winning_by_Even ?s p" 
    using infplays_augment_one_joint(1)[OF assms(1)] 
    unfolding strategy_winning_by_Even_def induced_play_def o_def
    by (metis fun_upd_same)
  thus "σ. strategy_winning_by_Even σ p" by blast next
  from assms(2) show "¬ ( σ. strategy_winning_by_Even σ p)" by meson
qed

lemma non_winning_moves_remains_non_winning_Odd:
  assumes "odd (length p)" " σ. ¬ strategy_winning_by_Odd σ p"
  shows "¬ strategy_winning_by_Odd σ (p @ [m])"
proof(rule contrapos_nn[of " σ. strategy_winning_by_Odd σ p"])
  assume a:"strategy_winning_by_Odd σ (p @ [m])"
  let ?s = "σ(p:=m)"
  have prfx:"prefix (p @ [m]) p' 
             p' @ [joint_strategy σe σ p'] = p' @ [joint_strategy σe ?s p']"
    for p' σe by (auto simp:joint_strategy_def)
  from a infplays_eq[OF prfx]
  have "strategy_winning_by_Odd ?s (p @ [m])"
    unfolding strategy_winning_by_Odd_def induced_play_def by simp
  hence "strategy_winning_by_Odd ?s p" 
    using infplays_augment_one_joint(2)[OF assms(1)] 
    unfolding strategy_winning_by_Odd_def induced_play_def o_def
    by (metis fun_upd_same)
  thus "σ. strategy_winning_by_Odd σ p" by blast next
  from assms(2) show "¬ ( σ. strategy_winning_by_Odd σ p)" by meson
qed

text ‹ If a player whose turn it is makes a move according to its stragey,
       the new position will remain winning. ›

lemma winning_moves_remain_winning_Even:
  assumes "even (length p)" "strategy_winning_by_Even σ p"
  shows "strategy_winning_by_Even σ (p @ [σ p])"
using assms infplays_augment_one
unfolding induced_play_def strategy_winning_by_Even_def by auto

lemma winning_moves_remain_winning_Odd:
  assumes "odd (length p)" "strategy_winning_by_Odd σ p"
  shows "strategy_winning_by_Odd σ (p @ [σ p])"
using assms infplays_augment_one
unfolding induced_play_def strategy_winning_by_Odd_def by auto

text ‹ We speak of winning positions as those positions in which the player has a winning strategy.
       This is mainly for presentation purposes. ›

abbreviation winning_position_Even where
  "winning_position_Even p  position p  ( σ. strategy_winning_by_Even σ p)"
abbreviation winning_position_Odd where
  "winning_position_Odd p  position p  ( σ. strategy_winning_by_Odd σ p)"

lemma winning_position_can_remain_winning_Even:
  assumes "even (length p)" " m. position (p @ [m])" "winning_position_Even p"
  shows " m. winning_position_Even (p @ [m])"
using assms winning_moves_remain_winning_Even[OF assms(1)] by auto

lemma winning_position_can_remain_winning_Odd:
  assumes "odd (length p)" " m. position (p @ [m])" "winning_position_Odd p"
  shows " m. winning_position_Odd (p @ [m])"
using assms winning_moves_remain_winning_Odd[OF assms(1)] by auto

lemma winning_position_will_remain_winning_Even:
  assumes "odd (length p)" "position (p @ [m])" "winning_position_Even p"
  shows "winning_position_Even (p @ [m])"
using assms any_moves_remain_winning_Even[OF assms(1)] by auto

lemma winning_position_will_remain_winning_Odd:
  assumes "even (length p)" "position (p @ [m])" "winning_position_Odd p"
  shows "winning_position_Odd (p @ [m])"
using assms any_moves_remain_winning_Odd[OF assms(1)] by auto

lemma induced_play_eq:
assumes " p'. prefix p p'  (augment_list s1) p' = (augment_list s2) p'"
shows "induced_play s1 p = induced_play s2 p"
unfolding induced_play_def by (auto simp:infplays_eq[OF assms[rule_format]])

end

end

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

Theory GaleStewartDeterminedGames

subsection ‹Determined games›

theory GaleStewartDeterminedGames
  imports GaleStewartDefensiveStrategies
begin

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, but this is very much the GS variation
   of finite games, as definitions still use coinductive lists rather than the more common
   inductive (and finite) ones. *)
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

text ‹ By proving that every position is determined, this proves that every game is determined
       (since a game is determined if its initial position [] is) ›
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
lemma empty_position: "position []" using zero_enat_def position_def by auto
lemmas every_game_is_determined = every_position_is_determined[OF empty_position]


text ‹ We expect that this theorem can be easier to apply without the 'position p' requirement,
       so we present that theorem as well. ›
lemma every_position_has_winning_strategy:
  shows "( σ. strategy_winning_by_Even σ p)  ( σ. strategy_winning_by_Odd σ p)" (is "?we  ?wo")
proof(cases "position p")
  case True
  then show ?thesis using every_position_is_determined by blast
next
  case False
  hence "2 * N  enat (length p)" unfolding position_def by force
  from induced_play_lprefix_non_positions[OF this]
  show ?thesis unfolding strategy_winning_by_Even_def strategy_winning_by_Odd_def by simp
qed

end

end