# HG changeset patch
# User nipkow
# Date 1374241684 -7200
# Node ID 5f86b30badd9222979ca3395eacbdab3154218ae
# Parent  c12602c1b13b0ee6d57a74bcc8ef40583b460c56
added exerciese

diff -r c12602c1b13b -r 5f86b30badd9 src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Fri Jul 19 12:00:31 2013 +0200
+++ b/src/Doc/ProgProve/Isar.thy	Fri Jul 19 15:48:04 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}