# 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 "(\ys zs. xs = ys @ zs \ length ys = length zs) + \ (\ys zs. xs = ys @ zs \ 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,\] = [x\<^sub>1,\,x\<^sub>k]"} and +@{text"drop k [x\<^sub>1,\] = [x\<^bsub>k+1\<^esub>,\]"}. 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}