author traytel Fri, 19 Jul 2013 16:36:13 +0200 changeset 52708 13e6014ed42b parent 52707 e2d08b9c9047 (current diff) parent 52706 5f86b30badd9 (diff) child 52709 0e4bacf21e77
merged
```--- 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}```