diff --git a/thys/GaleStewart_Games/GaleStewartGames.thy b/thys/GaleStewart_Games/GaleStewartGames.thy --- a/thys/GaleStewart_Games/GaleStewartGames.thy +++ b/thys/GaleStewart_Games/GaleStewartGames.thy @@ -1,403 +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"]] + prefix_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]] + with assms[OF prefix_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/MorePrefix.thy b/thys/GaleStewart_Games/MorePrefix.thy --- a/thys/GaleStewart_Games/MorePrefix.thy +++ b/thys/GaleStewart_Games/MorePrefix.thy @@ -1,148 +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]] + prefix_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