# 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 "(\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}