more exercises
Sat, 02 Nov 2013 17:19:34 +0100
changeset 54231 2975658d49cd
parent 54230 b1d955791529
child 54232 e039a9b9700d
more exercises
--- 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.
+Formalise the following definition of palindromes
+\item The empty list and a singleton list are palindromes.
+\item If @{text xs} is a palindrome, so is @{term "a # xs @ [a]"}.
+as an inductive predicate @{text "palindrome ::"} @{typ "'a list \<Rightarrow> bool"}
+and prove that @{prop "rev xs = xs"} if @{text xs} is a palindrome.
-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