# 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))"
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:"∀e∈A. 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])"
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])"
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