--- a/src/Doc/ProgProve/Bool_nat_list.thy Thu Jul 11 13:33:20 2013 +0200
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Thu Jul 11 21:34:37 2013 +0200
@@ -414,6 +414,19 @@
but underdefined.
\endsem
%
+
+\subsection{Exercises}
+
+\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.\
+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
+in the output as in the input.
+\end{exercise}
*}
(*<*)
end
--- a/src/Doc/ProgProve/Isar.thy Thu Jul 11 13:33:20 2013 +0200
+++ b/src/Doc/ProgProve/Isar.thy Thu Jul 11 21:34:37 2013 +0200
@@ -1048,6 +1048,34 @@
the induction hypotheses are instead found under the name @{text hyps}, like for the simpler
@{text induct} method.
\end{warn}
+
+\section*{Exercises}
+
+\begin{exercise}
+Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"}
+and prove @{prop "x : elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}.
+\end{exercise}
+
+\begin{exercise}
+A context-free grammar can be seen as an inductive definition where each
+nonterminal $A$ is an inductively defined predicate on lists of terminal
+symbols: $A(w)$ mans
+that $w$ is in the language generated by $A$. For example, the production $S
+\to a S b$ can be viewed as the implication @{prop"S w \<Longrightarrow> S (a # w @ [b])"}
+where @{text a} and @{text b} are constructors of some datatype of terminal
+symbols: \isacom{datatype} @{text"tsymbs = a | b | \<dots>"}
+
+Define the two grammars
+\[
+\begin{array}{r@ {\quad}c@ {\quad}l}
+S &\to& \varepsilon \quad\mid\quad a~S~b \quad\mid\quad S~S \\
+T &\to& \varepsilon \quad\mid\quad T~a~T~b
+\end{array}
+\]
+($\varepsilon$ is the empty word)
+as two inductive predicates and prove @{prop"S w \<longleftrightarrow> T w"}.
+\end{exercise}
+
*}
(*
lemma "\<not> ev(Suc(Suc(Suc 0)))"
--- a/src/Doc/ProgProve/Types_and_funs.thy Thu Jul 11 13:33:20 2013 +0200
+++ b/src/Doc/ProgProve/Types_and_funs.thy Thu Jul 11 21:34:37 2013 +0200
@@ -481,6 +481,32 @@
splits all case-expressions over natural numbers. For an arbitrary
datatype @{text t} it is @{text "t.split"} instead of @{thm[source] nat.split}.
Method @{text auto} can be modified in exactly the same way.
+
+
+\section*{Exercises}
+
+\exercise
+Define arithmetic expressions in one variable over integers (type @{typ int})
+as a data type:
+*}
+
+datatype exp = Var | Const int | Add exp exp | Mult exp exp
+
+text{*
+Define a function \noquotes{@{term [source]"eval :: exp \<Rightarrow> int \<Rightarrow> int"}}
+such that @{term"eval e x"} evaluates @{text e} at the value
+@{text x}.
+
+A polynomial can be represented as a list of coefficients, starting with
+the constant. For example, @{term "[4, 2, -1, 3::int]"} represents the
+polynomial $4 + 2x - x^2 + 3x^3$.
+Define a function \noquotes{@{term [source] "evalp :: int list \<Rightarrow> int \<Rightarrow> int"}}
+that evaluates a polynomial at the given value.
+Define a function \noquotes{@{term[source] "coeffs :: exp \<Rightarrow> int list"}}
+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"}.}
+\endexercise
*}
(*<*)
end