# HG changeset patch
# User traytel
# Date 1374244573 -7200
# Node ID 13e6014ed42bb40a5e8dde053277fdc854b37d3a
# Parent  e2d08b9c90471b806899465374315e956e264b30# Parent  5f86b30badd9222979ca3395eacbdab3154218ae
merged

diff -r e2d08b9c9047 -r 13e6014ed42b src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Fri Jul 19 14:51:45 2013 +0200
+++ b/src/Doc/ProgProve/Isar.thy	Fri Jul 19 16:36:13 2013 +0200
@@ -590,6 +590,8 @@
 the fact just proved, in this case the preceding block. In general,
 \isacom{note} introduces a new name for one or more facts.
 
+\subsection{Exercises}
+
 \exercise
 Give a readable, structured proof of the following lemma:
 *}
@@ -601,6 +603,19 @@
 text{*
 \endexercise
 
+\exercise
+Give a readable, structured proof of the following lemma:
+*}
+lemma "(\<exists>ys zs. xs = ys @ zs \<and> length ys = length zs)
+      \<or> (\<exists>ys zs. xs = ys @ zs \<and> length ys = length zs + 1)"
+(*<*)oops(*>*)
+text{*
+Hint: There are predefined functions @{const_typ take} and @{const_typ drop}
+such that @{text"take k [x\<^sub>1,\<dots>] = [x\<^sub>1,\<dots>,x\<^sub>k]"} and
+@{text"drop k [x\<^sub>1,\<dots>] = [x\<^bsub>k+1\<^esub>,\<dots>]"}. Let @{text simp} and especially
+sledgehammer find and apply the relevant @{const take} and @{const drop} lemmas for you.
+\endexercise
+
 \section{Case Analysis and Induction}
 
 \subsection{Datatype Case Analysis}