# HG changeset patch
# User nipkow
# Date 1383409174 -3600
# Node ID 2975658d49cd1395ba94c015ef8d357813c826e3
# Parent  b1d955791529f093d72809bf92cfd1b382951f18
more exercises

diff -r b1d955791529 -r 2975658d49cd src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Fri Nov 01 18:51:14 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Sat Nov 02 17:19:34 2013 +0100
@@ -787,10 +787,21 @@
 assumptions. The \isacom{for} clause seen in the definition of the reflexive
 transitive closure merely simplifies the form of the induction rule.
 
+
 \subsection{Exercises}
 
+\begin{exercise}
+Formalise the following definition of palindromes
+\begin{itemize}
+\item The empty list and a singleton list are palindromes.
+\item If @{text xs} is a palindrome, so is @{term "a # xs @ [a]"}.
+\end{itemize}
+as an inductive predicate @{text "palindrome ::"} @{typ "'a list \<Rightarrow> bool"}
+and prove that @{prop "rev xs = xs"} if @{text xs} is a palindrome.
+\end{exercise}
+
 \exercise
-We also could have defined @{const star} as follows:
+We could also have defined @{const star} as follows:
 *}
 
 inductive star' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r where