--- a/src/Doc/ProgProve/Bool_nat_list.thy Sat Jul 20 16:45:00 2013 +0200
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Sun Jul 21 14:02:33 2013 +0200
@@ -419,9 +419,10 @@
\begin{exercise}
Define your own addition, multiplication, and exponentiation functions on type
-@{typ nat}. Prove as many of the standard equational rules as possible, e.g.\
+@{typ nat}. Prove as many of the standard equational laws as possible, e.g.\
associativity, commutativity and distributivity.
\end{exercise}
+
\begin{exercise}
Define your own sorting function on the predefined lists.
Prove that the result is sorted and that every element occurs as many times
--- a/src/Doc/ProgProve/Isar.thy Sat Jul 20 16:45:00 2013 +0200
+++ b/src/Doc/ProgProve/Isar.thy Sun Jul 21 14:02:33 2013 +0200
@@ -1075,7 +1075,7 @@
@{text induct} method.
\end{warn}
-\section*{Exercises}
+\subsection{Exercises}
\begin{exercise}
Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"}
--- a/src/Doc/ProgProve/Types_and_funs.thy Sat Jul 20 16:45:00 2013 +0200
+++ b/src/Doc/ProgProve/Types_and_funs.thy Sun Jul 21 14:02:33 2013 +0200
@@ -483,7 +483,7 @@
Method @{text auto} can be modified in exactly the same way.
-\section*{Exercises}
+\subsection{Exercises}
\exercise
Define arithmetic expressions in one variable over integers (type @{typ int})
@@ -506,6 +506,8 @@
that transforms an expression into a polynomial. This may require auxiliary
functions. Prove that @{text coeffs} preserves the value of the expression:
\mbox{@{prop"evalp (coeffs e) x = eval e x"}.}
+Hint: simplifying with @{thm[source] algebra_simps} takes care of
+common algebraic properties of @{text "+"} and @{text "*"}.
\endexercise
*}
(*<*)