diff --git a/thys/GaleStewart_Games/AlternatingLists.thy b/thys/GaleStewart_Games/AlternatingLists.thy new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/AlternatingLists.thy @@ -0,0 +1,144 @@ +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 \ No newline at end of file diff --git a/thys/GaleStewart_Games/FilteredList.thy b/thys/GaleStewart_Games/FilteredList.thy new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/FilteredList.thy @@ -0,0 +1,310 @@ +theory FilteredList + imports MoreCoinductiveList2 +begin + +subsection \More on filtered lists\ + +text \We will reason about (co-inductive) lists with distinct elements. + However, for our setting, this 'distinct' property only holds on the list after filtering. + For this reason, we need some additional lemmas.\ + +text \Taking a sublist preserves distinctness after filtering.\ +lemma ldistinct_lfilter_ltake[intro]: + assumes "ldistinct (lfilter P xs)" + shows "ldistinct (lfilter P (ltake x xs))" + using assms + by(induct xs,force,force + ,(* sledgehammer found this gem to prove the inductive step via lfilter_lappend_lfinite! + We will use this strategy ourselves later on *) + metis lappend_ltake_ldrop ldistinct_lappend lfilter_lappend_lfinite lfinite_LConsI lfinite_ltake) + +text \The function lfind is used in multiple proofs, all are introduced to prove ltake_lfilter.\ +definition lfind where "lfind P lst = (LEAST i. P (lst $ i))" + +lemma lfilter_lfind: + assumes "lfilter P lst \ LNil" + shows "P (lst $ lfind P lst)" (is ?g1) + "P (lst $ y) \ lfind P lst \ y" (is "?a \ ?g2") + "lfind P lst < llength lst" (is ?g3) +proof - + let ?I = "{n. enat n < llength lst \ P (lst $ n)}" + let ?xs = lst + from assms[unfolded lfilter_conv_lnths] lset_LNil + have "lset (lnths lst {n. enat n < llength lst \ P (lst $ n)}) \ {}" by auto + hence "{?xs $ i |i. enat i < llength ?xs \ i \ ?I} \ {}" using lset_lnths[of ?xs ?I] by metis + then obtain i where p:"P (lst $ i)" "i < llength lst" by auto + from p show ?g1 using LeastI lfind_def by metis + from p show "?a \ ?g2" using Least_le lfind_def by metis + from p show ?g3 using Least_le lfind_def by (metis enat_ord_simps(1) le_less_trans) +qed + +lemma ltake_lfind_lset: + assumes "x \ lset (ltake (enat (lfind P lst)) lst)" + shows "\ P x" +proof(cases "lfilter P (ltake (enat (lfind P lst)) lst) = LNil") + case True + then show ?thesis using assms unfolding lfilter_eq_LNil by auto +next + case False + from assms[unfolded in_lset_conv_lnth] obtain n where + n:"enat n < llength (ltake (enat (lfind P lst)) lst)" "ltake (enat (lfind P lst)) lst $ n = x" + by blast + { assume a:"P x" + (* The idea of this {block} is that the element n must come after (lfind P lst) by lfilter_lfind(2) + but this contradicts n(1). + However, in the last step when writing this proof, sledgehammer found one that didn't use + any of my previous steps, so here's a one-liner: *) + from n Coinductive_List.lset_ltake False a enat_ord_simps(1) leD lfilter_empty_conv lfilter_lfind(2,3) llength_ltake' lnth_ltake subset_eq + have False by metis + } + then show ?thesis by blast +qed + +lemma ltake_lfind_conv: + assumes "lfilter P lst \ LNil" + shows "ltake (lfind P lst) lst = ltakeWhile (Not o P) lst" (is "?t1 = ?t2") + "ldrop (lfind P lst) lst = ldropWhile (Not o P) lst" (is "?t3 = ?t4") +proof - + have lfin:"lfinite ?t1" by simp + have [simp]:"min (enat (lfind P lst)) (llength lst) = (lfind P lst)" + using lfilter_lfind(3)[OF assms] by (metis min.strict_order_iff) + have l1:"llength ?t1 = lfind P lst" by simp + from ltake_lfind_lset ltakeWhile_all + have t:"ltakeWhile (Not o P) ?t1 = ?t1" unfolding o_def by metis + have inset:"lset (ltake (enat (lfind P lst)) lst) \ {x. (Not \ P) x}" + using ltake_lfind_lset[of _ P lst] by auto (* for use in ltakeWhile_lappend2 *) + have isnull:"ltakeWhile (Not \ P) (ldrop (enat (lfind P lst)) lst) = LNil" + apply(cases "ldrop (enat (lfind P lst)) lst") + using lfilter_lfind(1)[OF assms] lhd_ldrop[OF lfilter_lfind(3)[OF assms]] + by auto + have "ltakeWhile (Not o P) ?t1 = ltakeWhile (Not o P) (lappend ?t1 ?t3)" + unfolding ltakeWhile_lappend2[OF inset] isnull lappend_LNil2 t.. + hence leneq:"llength ?t1 = llength ?t2" using t l1 lappend_ltake_ldrop by metis + have "lappend ?t1 ?t3 = lappend ?t2 ?t4" + unfolding lappend_ltakeWhile_ldropWhile[of "Not \ P" lst] + lappend_ltake_ldrop[of "lfind P lst" lst] + by simp + from this[unfolded lappend_eq_lappend_conv[OF leneq]] lfin + show "?t1 = ?t2" "?t3 = ?t4" by auto +qed + +lemma lfilter_hdtl: + assumes "lfilter P lst \ LNil" + shows "\ n. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat n) lst) \ + ltl (lfilter P lst) = lfilter P (ldrop (enat n) lst)" +proof(standard,standard) + note * = lfilter_lfind[OF assms] + let ?n = "Suc (lfind P lst)" + let ?ltake = "ltake (enat ?n) lst" + have ltake:"lappend (ltakeWhile (Not \ P) ?ltake) (ldropWhile (Not \ P) ?ltake) = ?ltake" + (is "lappend ?ltw ?ldw = _") + using lappend_ltakeWhile_ldropWhile by blast + have "llength ?ldw \ 1" + unfolding ldropWhile_lappend ltake_Suc_conv_snoc_lnth[OF *(3)] + using ltake_lfind_lset[of _ P lst] by (auto intro:* simp:one_eSuc) + hence null:"lnull (ltl (ldropWhile (Not \ P) ?ltake))" + unfolding llength_eq_0[symmetric] llength_ltl + by (metis dual_order.order_iff_strict enat_ile epred_0 epred_1 iless_Suc_eq le_zero_eq one_eSuc one_enat_def) + have e:"enat (lfind P lst) < enat (Suc (lfind P lst))" by auto + from * have "P (?ltake $ lfind P lst)" using lnth_ltake[OF e] by metis + hence nonnull:"\ lnull (lfilter P ?ltake)" unfolding lnull_lfilter + by (metis "*"(3) e in_lset_conv_lnth leI llength_ltake' ltake_all) + + show a:"LCons (lhd (lfilter P lst)) LNil = lfilter P ?ltake" (is "?lhs = ?rhs") + proof - + have "lhd (lfilter P ?ltake) = lhd (lfilter P lst)" + by(rule lprefix_lhdD[OF lprefix_lfilterI[OF ltake_is_lprefix] nonnull]) + hence h:"lhd ?lhs = lhd ?rhs" by simp + have "ltl ?rhs = LNil" + unfolding ltl_lfilter using null by (metis lfilter_LNil llist.collapse(1)) + hence t:"ltl ?lhs = ltl ?rhs" by simp + have flt:"?rhs \ LNil" using nonnull by fastforce + show ?thesis by(rule llist_eq_lcons[of ?lhs ?rhs,OF _ flt h t],auto) + qed + + from lappend_ltake_ldrop[of ?n lst] lappend_ltakeWhile_ldropWhile[of "Not \ P" lst] + have "lappend (ltake ?n lst) (ldrop ?n lst) = lappend (ltakeWhile (Not \ P) lst) (ldropWhile (Not \ P) lst)" + by auto + from ltake_lfind_conv(2)[OF assms] + have "ltl (ldropWhile (Not \ P) lst) = ldrop (enat (Suc (lfind P lst))) lst" + unfolding ldrop_eSuc_conv_ltl eSuc_enat[symmetric] by simp + thus "ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)" unfolding ltl_lfilter by metis +qed + +lemma ltake_lfilter: + shows "\ n. ltake (enat x) (lfilter P lst) = lfilter P (ltake (enat n) lst) \ ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)" +proof(induct x) + case 0 + then show ?case by (metis LNil_eq_ltake_iff ldrop_enat ldropn_0 lfilter_code(1) zero_enat_def) +next + let ?fP = "lfilter P" + case (Suc x) + then obtain n where n:"ltake (enat x) (?fP lst) = ?fP (ltake (enat n) lst)" + "ldrop (enat x) (lfilter P lst) = lfilter P (ldrop (enat n) lst)" by blast + consider "lfilter P (ldrop (enat n) lst) \ LNil \ x < llength (?fP lst)" | + "lfilter P (ldrop (enat n) lst) = LNil" | "x \ llength (?fP lst)" by force + then show ?case proof(cases) + case 1 + hence *:"lfilter P (ldrop (enat n) lst) \ LNil" "enat x < llength (lfilter P lst)" by auto + from lappend_ltake_ldrop have "lst = lappend (ltake (enat n) lst) (ldrop (enat n) lst)" by metis + from lfilter_hdtl[OF *(1)] obtain delta where + delta:"LCons (lhd (?fP (ldrop (enat n) lst))) LNil = ?fP (ltake (enat delta) (ldrop (enat n) lst))" + "ltl (lfilter P (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta) (ldrop (enat n) lst))" by blast + have "ltake (enat (Suc x)) (?fP lst) = lappend (?fP (ltake (enat n) lst)) (LCons (?fP lst $ x) LNil)" + using n ltake_Suc_conv_snoc_lnth * by metis + also have "?fP lst $ x = ?fP lst $ (the_enat x)" by auto + also have "\ = lhd (ldrop x (?fP lst))" using lhd_ldrop[symmetric] *(2) by metis + also have "\ = lhd (?fP (ldrop (enat n) lst))" using n by metis + also note delta(1) + finally have take_part:"ltake (enat (Suc x)) (?fP lst) = ?fP (ltake (enat (n + delta)) lst)" + using ltake_plus_conv_lappend + by (metis infinite_small_llength lfilter_lappend_lfinite llength_ltake' ltake_all min.strict_order_iff not_less plus_enat_simps(1)) + have "ldrop (enat (Suc x)) (?fP lst) = ltl (ldrop x (?fP lst))" by (simp add: ltl_ldropn ldrop_eSuc_ltl ldrop_enat) + also have "ldrop x (?fP lst) = ?fP (ldrop (enat n) lst)" using n by metis + also note delta(2) + also have "lfilter P (ldrop (enat delta) (ldrop (enat n) lst)) = lfilter P (ldrop (enat delta + enat n) lst)" + by simp + also have "(enat delta + enat n) = enat (n + delta)" by simp + finally have drop_part:"ldrop (enat (Suc x)) (?fP lst) = ?fP (ldrop (enat (n + delta)) lst)". + from take_part drop_part show ?thesis by blast + next + case 2 + note * = 2 lappend_ltake_ldrop[of "enat n" lst] Suc_llength infinite_small_llength + lappend_LNil2 leI lfilter_lappend_lfinite llength_ltake' min.strict_order_iff n + have take_part:"ltake (enat (Suc x)) (?fP lst) = ?fP (ltake (enat n) lst)" + using * by (smt (z3) ltake_all) + from 2 have drop_part:"ldrop (enat (Suc x)) (?fP lst) = ?fP (ldrop (enat n) lst)" + using * by (smt (z3) ldrop_all) + from take_part drop_part show ?thesis by blast + next + case 3 + then show ?thesis using n dual_order.order_iff_strict eSuc_enat iless_Suc_eq le_less_trans ltake_all ldrop_all + by metis + qed +qed + +lemma filter_obtain_two: + assumes "i < j" "j < length (filter P lst)" + shows "\ i2 j2. i2 < j2 \ j2 < length lst \ lst ! i2 = filter P lst ! i \ lst ! j2 = filter P lst ! j" + using assms +proof(induct lst arbitrary: i j) + case (Cons a lst) + then obtain jprev where jprev:"j = Suc jprev" using lessE by metis + show ?case proof(cases "P a") + case True + hence lnth[simp]:"length (filter P (a # lst)) = Suc (length (filter P lst))" by auto + show ?thesis proof(cases i) + case 0 + from jprev True Cons(3) have "jprev < length (filter P lst) " by auto + from nth_mem[OF this] + have "filter P lst ! jprev \ set lst" by auto + from this[unfolded in_set_conv_nth] obtain j2 where + "j2 i j. i < llength lst \ j < llength lst \ lst $ i = lst $ j \ P (lst $ i) \ i = j" + shows "ldistinct (lfilter P lst)" +proof - +{ fix i j + assume *: "enat i < llength (lfilter P lst)" + "enat j < llength (lfilter P lst)" + "lfilter P lst $ i = lfilter P lst $ j" + "i < j" + hence "lfilter P lst $ i \ lset (lfilter P lst)" + unfolding in_lset_conv_lnth by auto + with lset_lfilter + have P:"P (lfilter P lst $ i)" by auto + let ?maxij = "Suc (max i j)" + from ltake_lfilter obtain maxij where + maxij:"ltake ?maxij (lfilter P lst) = lfilter P (ltake (enat maxij) lst)" + by blast + let ?lst = "ltake (enat maxij) lst" + have "lfinite ?lst" by auto + define flst where "flst = list_of ?lst" + hence flst:"llist_of flst = ?lst" by auto + let ?flst = "llist_of flst" + from * P + have "enat i < llength (lfilter P ?flst)" + "enat j < llength (lfilter P ?flst)" + "lfilter P ?flst $ i = lfilter P ?flst $ j" + and P2:"P (lfilter P ?lst $ i)" + unfolding maxij[symmetric] flst by (auto simp add: lnth_ltake) + hence "i < length (filter P flst)" + "j < length (filter P flst)" + and eq_ij: "filter P flst ! i = filter P flst ! j" + unfolding llength_llist_of lfilter_llist_of lnth_llist_of by auto + with filter_obtain_two[OF *(4) this(2)] obtain i2 j2 + where "i2 < length flst" "j2 < length flst" + "flst ! i2 = filter P flst ! i" + "flst ! j2 = filter P flst ! j" + and ineq:"i2 i j. i < llength lst \ j < llength lst \ P (lst $ i) \ lst $ i = lst $ j \ i = j)" +proof + show "ldistinct (lfilter P lst) \ \i j. enat i < llength lst \ enat j < llength lst \ P (lst $ i) \ lst $ i = lst $ j \ i = j" + by (auto simp add: ldistinct_lfilterE) + show "\i j. enat i < llength lst \ enat j < llength lst \ P (lst $ i) \ lst $ i = lst $ j \ i = j \ ldistinct (lfilter P lst) " + using ldistinct_lfilterI by blast +qed + +end \ No newline at end of file diff --git a/thys/GaleStewart_Games/GaleStewartDefensiveStrategies.thy b/thys/GaleStewart_Games/GaleStewartDefensiveStrategies.thy new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/GaleStewartDefensiveStrategies.thy @@ -0,0 +1,239 @@ +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 \\<^sub>o where + str_Odd:"\ m. strategy_winning_by_Odd (\\<^sub>o m) (p @ [m])" by blast + define \ where "\ p' = \\<^sub>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 \\<^sub>e where + str_Even:"induced_play (joint_strategy \\<^sub>e \) p \ A" + (is "?pe p \ A") + by blast + let ?pnext = "(p @ [joint_strategy \\<^sub>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 \\<^sub>e \ p'] = + p' @ [joint_strategy \\<^sub>e (\\<^sub>o (joint_strategy \\<^sub>e \ p)) p']" + unfolding joint_strategy_def \_def by auto + have simps:"?pe p = ?pe (p @ [joint_strategy \\<^sub>e \ p])" + unfolding induced_play_def by auto + from str_Even str_Odd[of "joint_strategy \\<^sub>e \ p", unfolded strategy_winning_by_Odd_def, rule_format, of "\\<^sub>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 \\<^sub>e where + str_Even:"\ m. strategy_winning_by_Even (\\<^sub>e m) (p @ [m])" by blast + define \ where "\ p' = \\<^sub>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 \\<^sub>o where + str_Odd:"induced_play (joint_strategy \ \\<^sub>o) p \ A" + (is "?pe p \ A") + by blast + let ?strat = "joint_strategy \ \\<^sub>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 (\\<^sub>e (?strat p)) \\<^sub>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 \\<^sub>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 \\<^sub>e defensive_strategy_Odd p])" + by (simp add: joint_strategy_def True) + with Suc.hyps[of "p @ [joint_strategy \\<^sub>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 \\<^sub>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 \\<^sub>o p])" + by (simp add: joint_strategy_def True) + with Suc.hyps[of "p @ [joint_strategy defensive_strategy_Even \\<^sub>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 \ No newline at end of file diff --git a/thys/GaleStewart_Games/GaleStewartDeterminedGames.thy b/thys/GaleStewart_Games/GaleStewartDeterminedGames.thy new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/GaleStewartDeterminedGames.thy @@ -0,0 +1,116 @@ +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 \ No newline at end of file diff --git a/thys/GaleStewart_Games/GaleStewartGames.thy b/thys/GaleStewart_Games/GaleStewartGames.thy new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/GaleStewartGames.thy @@ -0,0 +1,403 @@ +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 \\<^sub>e \\<^sub>o p = (if even (length p) then \\<^sub>e p else \\<^sub>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 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 \\<^sub>e \\<^sub>o) (augment_list \\<^sub>e p) + = strategy_progression (joint_strategy \\<^sub>e \\<^sub>o) p" + "odd (length p) \ strategy_progression (joint_strategy \\<^sub>e \\<^sub>o) (augment_list \\<^sub>o p) + = strategy_progression (joint_strategy \\<^sub>e \\<^sub>o) p" +using infplays_augment_one[of "joint_strategy \\<^sub>e \\<^sub>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 \\<^sub>e p \ (\ \\<^sub>o. induced_play (joint_strategy \\<^sub>e \\<^sub>o) p \ A)" +definition strategy_winning_by_Odd where + "strategy_winning_by_Odd \\<^sub>o p \ (\ \\<^sub>e. induced_play (joint_strategy \\<^sub>e \\<^sub>o) p \ A)" + +text \ It immediately follows that not both players can have a winning strategy. \ +lemma at_most_one_player_winning: +shows "\ (\ \\<^sub>e. strategy_winning_by_Even \\<^sub>e p) \ \ (\ \\<^sub>o. strategy_winning_by_Odd \\<^sub>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 \\<^sub>o + let ?s = "\\<^sub>o(p:=m)" + have prfx:"prefix (p @ [m]) p' \ + p' @ [joint_strategy \ \\<^sub>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 \ \\<^sub>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 \\<^sub>e + let ?s = "\\<^sub>e(p:=m)" + have prfx:"prefix (p @ [m]) p' \ + p' @ [joint_strategy \\<^sub>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 \\<^sub>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 \ \\<^sub>o p'] = p' @ [joint_strategy ?s \\<^sub>o p']" + for p' \\<^sub>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 \\<^sub>e \ p'] = p' @ [joint_strategy \\<^sub>e ?s p']" + for p' \\<^sub>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 \ No newline at end of file diff --git a/thys/GaleStewart_Games/MoreCoinductiveList2.thy b/thys/GaleStewart_Games/MoreCoinductiveList2.thy new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/MoreCoinductiveList2.thy @@ -0,0 +1,51 @@ +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 \ No newline at end of file diff --git a/thys/GaleStewart_Games/MoreENat.thy b/thys/GaleStewart_Games/MoreENat.thy new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/MoreENat.thy @@ -0,0 +1,63 @@ +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 \ No newline at end of file diff --git a/thys/GaleStewart_Games/MorePrefix.thy b/thys/GaleStewart_Games/MorePrefix.thy new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/MorePrefix.thy @@ -0,0 +1,148 @@ +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 \ No newline at end of file diff --git a/thys/GaleStewart_Games/ROOT b/thys/GaleStewart_Games/ROOT new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/ROOT @@ -0,0 +1,14 @@ +chapter AFP + +session "GaleStewart_Games" (AFP) = Parity_Game + + options [timeout = 60] + theories [document = false] + MoreCoinductiveList2 + MoreENat + MorePrefix + theories + GaleStewartGames + GaleStewartDeterminedGames + document_files + "root.bib" + "root.tex" diff --git a/thys/GaleStewart_Games/document/root.bib b/thys/GaleStewart_Games/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/document/root.bib @@ -0,0 +1,52 @@ +%% This BibTeX bibliography file was created using BibDesk. +%% http://bibdesk.sourceforge.net/ + + +%% Created for Sebastiaan Joosten at 2021-04-22 22:55:14 -0400 + + +%% Saved with string encoding Unicode (UTF-8) + + + +@article{Parity_Game-AFP, + author = {Christoph Dittmann}, + date-added = {2021-04-22 22:55:11 -0400}, + date-modified = {2021-04-22 22:55:11 -0400}, + issn = {2150-914x}, + journal = {Archive of Formal Proofs}, + month = nov, + note = {\url{https://isa-afp.org/entries/Parity_Game.html}, Formal proof development}, + title = {Positional Determinacy of Parity Games}, + year = 2015} + +@inproceedings{ZF13, + author = {Zermelo, Ernst}, + booktitle = {Proceedings of the fifth international congress of mathematicians}, + date-added = {2021-04-22 20:21:47 -0400}, + date-modified = {2021-04-22 20:21:55 -0400}, + organization = {Cambridge University Press Cambridge, UK}, + pages = {501--504}, + title = {{\"U}ber eine Anwendung der Mengenlehre auf die Theorie des Schachspiels}, + volume = {2}, + year = {1913}} + +@article{GS53, + author = {Gale, David and Stewart, Frank M}, + date-added = {2021-04-22 20:10:31 -0400}, + date-modified = {2021-04-22 20:10:42 -0400}, + journal = {Contributions to the Theory of Games}, + number = {245-266}, + pages = {2--16}, + title = {Infinite games with perfect information}, + volume = {2}, + year = {1953}} + +@book{LNCS2283, + author = {Tobias Nipkow and Lawrence Paulson and Markus Wenzel}, + note = {\url{http://www.in.tum.de/~nipkow/LNCS2283/}}, + publisher = Springer, + series = LNCS, + title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, + volume = 2283, + year = 2002} diff --git a/thys/GaleStewart_Games/document/root.tex b/thys/GaleStewart_Games/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/GaleStewart_Games/document/root.tex @@ -0,0 +1,57 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{Gale-Stewart Games} +\author{Sebastiaan J.\,C. Joosten} +\maketitle + +\begin{abstract} + This is a formalisation of the main result of Gale and Stewart from 1953, showing that closed finite games are determined. + This property is now known as the Gale Stewart Theorem. + While the original paper shows some additional theorems as well, we only formalize this main result, but do so in a somewhat general way. + We formalize games of a fixed arbitrary length, including infinite length, using co-inductive lists, and show that defensive strategies exist unless the other player is winning. + For closed games, defensive strategies are winning for the closed player, proving that such games are determined. + For finite games, which are a special case in our formalisation, all games are closed. +\end{abstract} + +\tableofcontents + +\section{Introduction} +The original paper from Gale and Stewart~\cite{GS53} uses a function to point to a previous position. +This encoding of sequences is not followed in this formalization, as it is not the way we think of games these days. +Instead, we follow the approach taken in the formalization of Parity Games~\cite{Parity_Game-AFP}, where co-inductive lists are used to talk about possibly infinite plays. +Although we rely on the Parity Games theory for some of the theorems about co-inductive lists, none of the notions about games are shared with that formalization. + +We have proven some basic lemmas about prefixes, extended naturals (natural numbers plus infinity), and defined a function 'alternate' alternating lists. +We have done this in separate Isabelle theory files, so that they can be reused independently without depending on the formalizations of infinite games presented here. +In the same way this formalization is giving a nod to the parity games formalization. +In this document, we only present the alternating lists, as this theory file contains new definitions, which are relevant preliminaries to know about. +The additional lemmas about prefixes and extended natural numbers are less essential, they only contain `obvious' properties, so we have left those theory files out of this document. + + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,596 +1,597 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BNF_CC BNF_Operations BTree Banach_Steinhaus Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties CSP_RefTK DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos DOM_Components DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC +GaleStewart_Games Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpreter_Optimizations Interval_Arithmetic_Word32 Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaGeoCoq Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knuth_Bendix_Order Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mereology Mersenne_Primes MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_arithmetic_LLL_and_HNF_algorithms Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PCF PLM POPLmark-deBruijn PSemigroupsConvolution Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Shadow_DOM Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God UPF UPF_Firewall UTP Universal_Turing_Machine UpDown_Scheme Valuation VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL