# HG changeset patch
# User nipkow
# Date 1381952715 -7200
# Node ID 0941a2024569e2ff1c64ce469d5cfaf16ffe0b14
# Parent  c2f18fd05414bd418818063c51807f8598c53538# Parent  4e7d71037bb62a289ae58037ca168cb668e19615
merged

diff -r c2f18fd05414 -r 0941a2024569 src/Doc/ProgProve/Bool_nat_list.thy
--- a/src/Doc/ProgProve/Bool_nat_list.thy	Wed Oct 16 20:44:33 2013 +0200
+++ b/src/Doc/ProgProve/Bool_nat_list.thy	Wed Oct 16 21:45:15 2013 +0200
@@ -422,10 +422,16 @@
 \subsection{Exercises}
 
 \begin{exercise}
+Use the \isacom{value} command to evaluate the following expressions:
+@{term[source] "1 + (2::nat)"}, @{term[source] "1 + (2::int)"},
+@{term[source] "1 - (2::nat)"} and @{term[source] "1 - (2::int)"}.
+\end{exercise}
+
+\begin{exercise}
 Start from the definition of @{const add} given above.
-Prove it is associative (@{prop"add (add m n) p = add m (add n p)"})
-and commutative (@{prop"add m n = add n m"}). Define a recursive function
-@{text double} @{text"::"} @{typ"nat \<Rightarrow> nat"} and prove that @{prop"double m = add m m"}.
+Prove that @{const add} it is associative and commutative.
+Define a recursive function @{text double} @{text"::"} @{typ"nat \<Rightarrow> nat"}
+and prove @{prop"double m = add m m"}.
 \end{exercise}
 
 \begin{exercise}
@@ -436,11 +442,15 @@
 
 \begin{exercise}
 Define a recursive function @{text "snoc ::"} @{typ"'a list \<Rightarrow> 'a \<Rightarrow> 'a list"}
-that appends an element to the end of a list. Do not use the predefined append
-operator @{text"@"}. With the help of @{text snoc} define a recursive function
-@{text "reverse ::"} @{typ"'a list \<Rightarrow> 'a list"} that reverses a list. Do not
-use the predefined function @{const rev}.
-Prove @{prop"reverse(reverse xs) = xs"}.
+that appends an element to the end of a list. With the help of @{text snoc}
+define a recursive function @{text "reverse ::"} @{typ"'a list \<Rightarrow> 'a list"}
+that reverses a list. Prove @{prop"reverse(reverse xs) = xs"}.
+\end{exercise}
+
+\begin{exercise}
+Define a recursive function @{text "sum ::"} @{typ"nat \<Rightarrow> nat"} such that
+\mbox{@{text"sum n"}} @{text"="} @{text"0 + ... + n"} and prove
+@{prop" sum(n::nat) = n * (n+1) div 2"}.
 \end{exercise}
 *}
 (*<*)