# HG changeset patch
# User kleing
# Date 1046534252 -3600
# Node ID ed4e97874454f4421188a495f0e9ec1bea7c838f
# Parent  399c8103a98f4822e91978db031857e640b5fd27
keep a copy of generated files in repository

diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2000/a1/generated/Arithmetic.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2000/a1/generated/Arithmetic.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,92 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Arithmetic}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Arithmetic%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Power%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a primitive recursive function $pow~x~n$ that
+computes $x^n$ on natural numbers.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove the well known equation $x^{m \cdot n} = (x^m)^n$:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ pow{\isacharunderscore}mult{\isacharcolon}\ {\isachardoublequote}pow\ x\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ pow\ {\isacharparenleft}pow\ x\ m{\isacharparenright}\ n{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Hint: prove a suitable lemma first.  If you need to appeal to
+associativity and commutativity of multiplication: the corresponding
+simplification rules are named \isa{mult{\isacharunderscore}ac}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Summation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a (primitive recursive) function $sum~ns$ that sums a list
+of natural numbers: $sum [n_1, \dots, n_k] = n_1 + \cdots + n_k$.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Show that $sum$ is compatible with $rev$. You may need a lemma.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ sum{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}sum\ {\isacharparenleft}rev\ ns{\isacharparenright}\ {\isacharequal}\ sum\ ns{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function $Sum~f~k$ that sums $f$ from $0$
+up to $k-1$: $Sum~f~k = f~0 + \cdots + f(k - 1)$.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ Sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isacharequal}{\isachargreater}\ nat{\isacharparenright}\ {\isacharequal}{\isachargreater}\ nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Show the following equations for the pointwise summation of functions.
+Determine first what the expression \isa{whatever} should be.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}Sum\ {\isacharparenleft}{\isacharpercent}i{\isachardot}\ f\ i\ {\isacharplus}\ g\ i{\isacharparenright}\ k\ {\isacharequal}\ Sum\ f\ k\ {\isacharplus}\ Sum\ g\ k{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}Sum\ f\ {\isacharparenleft}k\ {\isacharplus}\ l{\isacharparenright}\ {\isacharequal}\ Sum\ f\ k\ {\isacharplus}\ Sum\ whatever\ l{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+What is the relationship between \isa{sum} and \isa{Sum}?
+Prove the following equation, suitably instantiated.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}Sum\ f\ k\ {\isacharequal}\ sum\ whatever{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Hint: familiarize yourself with the predefined functions \isa{map} and
+\isa{{\isacharbrackleft}i{\isachardot}{\isachardot}j{\isacharparenleft}{\isacharbrackright}} on lists in theory List.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2000/a1/generated/Hanoi.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2000/a1/generated/Hanoi.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,56 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Hanoi}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{The towers of Hanoi \label{psv2000hanoi}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We are given 3 pegs $A$, $B$ and $C$, and $n$ disks with a hole, such
+that no two disks have the same diameter.  Initially all $n$ disks
+rest on peg $A$, ordered according to their size, with the largest one
+at the bottom. The aim is to transfer all $n$ disks from $A$ to $C$ by
+a sequence of single-disk moves such that we never place a larger disk
+on top of a smaller one. Peg $B$ may be used for intermediate storage.
+
+\begin{center}
+\includegraphics[width=0.8\textwidth]{Hanoi}
+\end{center}
+
+\medskip The pegs and moves can be modelled as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ peg\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isanewline
+\isamarkupfalse%
+\isacommand{types}\ move\ {\isacharequal}\ {\isachardoublequote}peg\ {\isacharasterisk}\ peg{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a primitive recursive function%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ moves\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ peg\ {\isacharequal}{\isachargreater}\ peg\ {\isacharequal}{\isachargreater}\ peg\ {\isacharequal}{\isachargreater}\ move\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+such that \isa{moves}$~n~a~b~c$ returns a list of (legal)
+moves that transfer $n$ disks from peg $a$ via $b$ to $c$.
+Show that this requires $2^n - 1$ moves:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}length\ {\isacharparenleft}moves\ n\ a\ b\ c{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}{\isacharcircum}n\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Hint: You need to strengthen the theorem for the
+induction to go through. Beware: subtraction on natural numbers
+behaves oddly: $n - m = 0$ if $n \le m$.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2000/a1/generated/Snoc.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2000/a1/generated/Snoc.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,34 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Snoc}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a primitive recursive function \isa{snoc} that appends an element
+at the \emph{right} end of a list. Do not use \isa{{\isacharat}} itself.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ snoc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove the following theorem:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ rev{\isacharunderscore}cons{\isacharcolon}\ {\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ snoc\ {\isacharparenleft}rev\ xs{\isacharparenright}\ x{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Hint: you need to prove a suitable lemma first.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2000/a1/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2000/a1/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,10 @@
+\input{Snoc.tex}
+
+\input{Arithmetic.tex}
+
+\input{Hanoi.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/Makefile	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,42 @@
+#
+# $Id$
+#
+# IsaMakefile for PSV2001
+#
+
+SESSIONS = a1 a2 a3 a5
+
+## targets
+
+default: sessions
+sessions: $(SESSIONS)
+
+
+## a1
+
+a1: a1/generated/session.tex
+
+a1/generated/session.tex: a1/ROOT.ML a1/*.thy
+	isatool make
+
+## a2
+
+a2: a2/generated/session.tex
+
+a2/generated/session.tex: a2/ROOT.ML a2/*.thy
+	isatool make
+
+## a3
+
+a3: a3/generated/session.tex
+
+a3/generated/session.tex: a3/ROOT.ML a3/*.thy
+	isatool make
+
+## a5
+
+a5: a5/generated/session.tex
+
+a5/generated/session.tex: a5/ROOT.ML a5/*.thy
+	isatool make
+
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a1/generated/Aufgabe1.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a1/generated/Aufgabe1.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,84 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Aufgabe{\isadigit{1}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a function \isa{replace}, such that \isa{replace\ x\ y\ zs}
+yields \isa{zs} with every occurrence of \isa{x} replaced by \isa{y}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ replace\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove or disprove (by counter example) the following theorems.
+You may have to prove some lemmas first.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}rev{\isacharparenleft}replace\ x\ y\ zs{\isacharparenright}\ {\isacharequal}\ replace\ x\ y\ {\isacharparenleft}rev\ zs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}replace\ x\ y\ {\isacharparenleft}replace\ u\ v\ zs{\isacharparenright}\ {\isacharequal}\ replace\ u\ v\ {\isacharparenleft}replace\ x\ y\ zs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}replace\ y\ z\ {\isacharparenleft}replace\ x\ y\ zs{\isacharparenright}\ {\isacharequal}\ replace\ x\ z\ zs{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define two functions for removing elements from a list:
+\isa{del{\isadigit{1}}\ x\ xs} deletes the first occurrence (from the left) of
+\isa{x} in \isa{xs}, \isa{delall\ x\ xs} all of them.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ del{\isadigit{1}}\ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ delall\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove or disprove (by counter example) the following theorems.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}del{\isadigit{1}}\ x\ {\isacharparenleft}delall\ x\ xs{\isacharparenright}\ {\isacharequal}\ delall\ x\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}delall\ x\ {\isacharparenleft}delall\ x\ xs{\isacharparenright}\ {\isacharequal}\ delall\ x\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}delall\ x\ {\isacharparenleft}del{\isadigit{1}}\ x\ xs{\isacharparenright}\ {\isacharequal}\ delall\ x\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}del{\isadigit{1}}\ x\ {\isacharparenleft}del{\isadigit{1}}\ y\ zs{\isacharparenright}\ {\isacharequal}\ del{\isadigit{1}}\ y\ {\isacharparenleft}del{\isadigit{1}}\ x\ zs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}delall\ x\ {\isacharparenleft}del{\isadigit{1}}\ y\ zs{\isacharparenright}\ {\isacharequal}\ del{\isadigit{1}}\ y\ {\isacharparenleft}delall\ x\ zs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}delall\ x\ {\isacharparenleft}delall\ y\ zs{\isacharparenright}\ {\isacharequal}\ delall\ y\ {\isacharparenleft}delall\ x\ zs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}del{\isadigit{1}}\ y\ {\isacharparenleft}replace\ x\ y\ xs{\isacharparenright}\ {\isacharequal}\ del{\isadigit{1}}\ x\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}delall\ y\ {\isacharparenleft}replace\ x\ y\ xs{\isacharparenright}\ {\isacharequal}\ delall\ x\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}replace\ x\ y\ {\isacharparenleft}delall\ x\ zs{\isacharparenright}\ {\isacharequal}\ delall\ x\ zs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}replace\ x\ y\ {\isacharparenleft}delall\ z\ zs{\isacharparenright}\ {\isacharequal}\ delall\ z\ {\isacharparenleft}replace\ x\ y\ zs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}rev{\isacharparenleft}del{\isadigit{1}}\ x\ xs{\isacharparenright}\ {\isacharequal}\ del{\isadigit{1}}\ x\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}rev{\isacharparenleft}delall\ x\ xs{\isacharparenright}\ {\isacharequal}\ delall\ x\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a1/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a1/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,6 @@
+\input{Aufgabe1.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a2/generated/Aufgabe2.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a2/generated/Aufgabe2.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,82 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Aufgabe{\isadigit{2}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Trees%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In the sequel we work with skeletons of binary trees where
+neither the leaves (``tip'') nor the nodes contain any information:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ tree\ {\isacharequal}\ Tp\ {\isacharbar}\ Nd\ tree\ tree\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{tips} that counts the tips of a
+tree, and a function \isa{height} that computes the height of a
+tree.
+
+Complete binary trees of a given height are generated as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ cbt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ tree{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\isanewline
+{\isachardoublequote}cbt\ {\isadigit{0}}\ {\isacharequal}\ Tp{\isachardoublequote}\isanewline
+{\isachardoublequote}cbt{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Nd\ {\isacharparenleft}cbt\ n{\isacharparenright}\ {\isacharparenleft}cbt\ n{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+We will now focus on these complete binary trees.
+
+Instead of generating complete binary trees, we can also \emph{test}
+if a binary tree is complete. Define a function \isa{iscbt\ f}
+(where \isa{f} is a function on trees) that checks for completeness:
+\isa{Tp} is complete and \isa{Nd\ l\ r} ist complete iff \isa{l} and
+\isa{r} are complete and \isa{f\ l\ {\isacharequal}\ f\ r}.
+
+We now have 3 functions on trees, namely \isa{tips}, \isa{height}
+und \isa{size}. The latter is defined automatically --- look it up
+in the tutorial.  Thus we also have 3 kinds of completeness: complete
+wrt.\ \isa{tips}, complete wrt.\ \isa{height} and complete wrt.\
+\isa{size}. Show that
+\begin{itemize}
+\item the 3 notions are the same (e.g.\ \isa{iscbt\ tips\ t\ {\isacharequal}\ iscbt\ size\ t}),
+      and
+\item the 3 notions describe exactly the trees generated by \isa{cbt}:
+the result of \isa{cbt} is complete (in the sense of \isa{iscbt},
+wrt.\ any function on trees), and if a tree is complete in the sense of
+\isa{iscbt}, it is the result of \isa{cbt} (applied to a suitable number
+--- which one?)
+\end{itemize}
+Find a function \isa{f} such that \isa{iscbt\ f} is different from
+\isa{iscbt\ size}.
+
+Hints:
+\begin{itemize}
+\item Work out and prove suitable relationships between \isa{tips},
+      \isa{height} und \isa{size}.
+
+\item If you need lemmas dealing only with the basic arithmetic operations
+(\isa{{\isacharplus}}, \isa{{\isacharasterisk}}, \isa{{\isacharcircum}} etc), you can ``prove'' them
+with the command \isa{sorry}, if neither \isa{arith} nor you can
+find a proof. Not \isa{apply\ sorry}, just \isa{sorry}.
+
+\item
+You do not need to show that every notion is equal to every other
+notion.  It suffices to show that $A = C$ und $B = C$ --- $A = B$ is a
+trivial consequence. However, the difficulty of the proof will depend
+on which of the equivalences you prove.
+
+\item There is \isa{{\isasymand}} and \isa{{\isasymlongrightarrow}}.
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a2/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a2/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,6 @@
+\input{Aufgabe2.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a3/generated/Trie1.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a3/generated/Trie1.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,99 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Trie{\isadigit{1}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Tries%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Section~3.4.4 of \cite{isabelle-tutorial} is a case study
+about so-called \emph{tries}, a data structure for fast indexing with
+strings. Read that section.
+
+The data type of tries over the alphabet type \isa{{\isacharprime}a} und the value
+type \isa{{\isacharprime}v} is defined as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isacharequal}\ Trie\ \ {\isachardoublequote}{\isacharprime}v\ option{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ trie{\isacharparenright}\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+A trie consists of an optional value and an association list
+that maps letters of the alphabet to subtrees. Type \isa{{\isacharprime}a\ option} is
+defined in section~2.5.3 of \cite{isabelle-tutorial}.
+
+There are also two selector functions \isa{value} and \isa{alist}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\ {\isachardoublequote}value\ {\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ ov{\isachardoublequote}\ \isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{consts}\ alist\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ trie{\isacharparenright}\ list{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\ {\isachardoublequote}alist\ {\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ al{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Furthermore there is a function \isa{lookup} on tries
+defined with the help of the generic search function \isa{assoc} on
+association lists:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ assoc\ {\isacharcolon}{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}key\ {\isacharasterisk}\ {\isacharprime}val{\isacharparenright}list\ {\isasymRightarrow}\ {\isacharprime}key\ {\isasymRightarrow}\ {\isacharprime}val\ option{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\ {\isachardoublequote}assoc\ {\isacharbrackleft}{\isacharbrackright}\ x\ {\isacharequal}\ None{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}assoc\ {\isacharparenleft}p{\isacharhash}ps{\isacharparenright}\ x\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}let\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ p\ in\ if\ a\ {\isacharequal}\ x\ then\ Some\ b\ else\ assoc\ ps\ x{\isacharparenright}{\isachardoublequote}\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{consts}\ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\ {\isachardoublequote}lookup\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ value\ t{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}lookup\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ None\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ lookup\ at\ as{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Finally, \isa{update} updates the value associated with some
+string with a new value, overwriting the old one:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ update\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\isanewline
+\ \ {\isachardoublequote}update\ t\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ v\ {\isacharequal}\ Trie\ {\isacharparenleft}Some\ v{\isacharparenright}\ {\isacharparenleft}alist\ t{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}update\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ v\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}let\ tt\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ {\isacharbrackleft}{\isacharbrackright}\ \isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ at{\isacharparenright}\isanewline
+\ \ \ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}\ update\ tt\ as\ v{\isacharparenright}\ {\isacharhash}\ alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+The following theorem tells us that \isa{update} behaves as
+expected:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}{\isasymforall}t\ v\ bs{\isachardot}\ lookup\ {\isacharparenleft}update\ t\ as\ v{\isacharparenright}\ bs\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}if\ as\ {\isacharequal}\ bs\ then\ Some\ v\ else\ lookup\ t\ bs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+As a warming up exercise, define a function%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ modify\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ option\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+for inserting as well as deleting elements from a trie. Show
+that \isa{modify} satisfies a suitably modified version of the
+correctness theorem for \isa{update}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a3/generated/Trie2.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a3/generated/Trie2.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,32 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Trie{\isadigit{2}}}%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Die above definition of \isa{update} has the disadvantage
+that it often creates junk: each association list it passes through is
+extended at the left end with a new (letter,value) pair without
+removing any old association of that letter which may already be
+present.  Logically, such cleaning up is unnecessary because \isa{assoc} always searches the list from the left. However, it constitutes
+a space leak: the old associations cannot be garbage collected because
+physically they are still reachable. This problem can be solved by
+means of a function%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ overwrite\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+that does not just add new pairs at the front but replaces old
+associations by new pairs if possible.
+
+Define \isa{overwrite}, modify \isa{modify} to employ \isa{overwrite}, and show the same relationship between \isa{modify} and
+\isa{lookup} as before.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a3/generated/Trie3.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a3/generated/Trie3.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,26 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Trie{\isadigit{3}}}%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Instead of association lists we can also use partial functions
+that map letters to subtrees. Partiality can be modelled with the help
+of type \isa{{\isacharprime}a\ option}: if \isa{f} is a function of type
+\mbox{\isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option}}, set \isa{f\ a\ {\isacharequal}\ Some\ b}
+if \isa{a} should be mapped to some \isa{b} and set \isa{f\ a\ {\isacharequal}\ None} otherwise.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isacharequal}\ Trie\ \ {\isachardoublequote}{\isacharprime}v\ option{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ trie\ option{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Modify the definitions of \isa{lookup} and \isa{modify}
+accordingly and show the same correctness theorem as above.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a3/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a3/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,10 @@
+\input{Trie1.tex}
+
+\input{Trie2.tex}
+
+\input{Trie3.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a5/generated/Aufgabe5.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a5/generated/Aufgabe5.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,165 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Aufgabe{\isadigit{5}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Interval lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Sets of natural numbers can be implemented as lists of
+intervals, where an interval is simply a pair of numbers. For example
+the set \isa{{\isacharbraceleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{7}}{\isacharcomma}\ {\isadigit{8}}{\isacharcomma}\ {\isadigit{9}}{\isacharbraceright}} can be represented by the
+list \isa{{\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isadigit{5}}{\isacharcomma}\ {\isadigit{5}}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isadigit{7}}{\isacharcomma}\ {\isadigit{9}}{\isacharparenright}{\isacharbrackright}}. A typical application
+is the list of free blocks of dynamically allocated memory.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Definitions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We introduce the type%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{types}\ intervals\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}nat{\isacharasterisk}nat{\isacharparenright}\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+This type contains all possible lists of pairs of natural
+numbers, even those that we may not recognize as meaningful
+representations of sets. Thus you should introduce an \emph{invariant}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}intervals\ {\isacharequal}{\isachargreater}\ bool{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+that characterizes exactly those interval lists representing
+sets.  (The reason why we call this an invariant will become clear
+below.)  For efficiency reasons intervals should be sorted in
+ascending order, the lower bound of each interval should be less or
+equal the upper bound, and the intervals should be chosen as large as
+possible, i.e.\ no two adjecent intervals should overlap or even touch
+each other.  It turns out to be convenient to define \isa{Aufgabe{\isadigit{5}}{\isachardot}inv} in
+terms of a more general function%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ inv{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ intervals\ {\isacharequal}{\isachargreater}\ bool{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+such that the additional argument is a lower bound for the
+intervals in the list.
+
+To relate intervals back to sets define an \emph{abstraktion funktion}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ set{\isacharunderscore}of\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}intervals\ {\isacharequal}{\isachargreater}\ nat\ set{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+that yields the set corresponding to an interval list (that
+satisfies the invariant).
+
+Finally, define two primitive recursive functions%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat{\isacharasterisk}nat{\isacharparenright}\ {\isacharequal}{\isachargreater}\ intervals\ {\isacharequal}{\isachargreater}\ intervals{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ rem\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat{\isacharasterisk}nat{\isacharparenright}\ {\isacharequal}{\isachargreater}\ intervals\ {\isacharequal}{\isachargreater}\ intervals{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+for inserting and deleting an interval from an interval
+list. The result should again satisfies the invariant. Hence the name:
+\isa{inv} is invariant under the application of the operations
+\isa{add} and \isa{rem} --- if \isa{inv} holds for the input, it
+must also hold for the output.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Proving the invariant%
+}
+\isamarkuptrue%
+\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}\isanewline
+\isamarkupfalse%
+\isacommand{declare}\ split{\isacharunderscore}split\ {\isacharbrackleft}split{\isacharbrackright}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Start off by proving the monotonicity of \isa{inv{\isadigit{2}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ inv{\isadigit{2}}{\isacharunderscore}monotone{\isacharcolon}\ {\isachardoublequote}inv{\isadigit{2}}\ m\ ins\ {\isasymLongrightarrow}\ n{\isasymle}m\ {\isasymLongrightarrow}\ inv{\isadigit{2}}\ n\ ins{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Now show that \isa{add} and \isa{rem} preserve the invariant:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ inv{\isacharunderscore}add{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ i{\isasymle}j{\isacharsemicolon}\ inv\ ins\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ inv\ {\isacharparenleft}add\ {\isacharparenleft}i{\isacharcomma}j{\isacharparenright}\ ins{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ inv{\isacharunderscore}rem{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ i{\isasymle}j{\isacharsemicolon}\ inv\ ins\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ inv\ {\isacharparenleft}rem\ {\isacharparenleft}i{\isacharcomma}j{\isacharparenright}\ ins{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Hint: you should first prove a more general statement
+(involving \isa{inv{\isadigit{2}}}). This will probably involve some advanced
+forms of induction discussed in section~9.3.1 of
+\cite{isabelle-tutorial}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Proving correctness of the implementation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Show the correctness of \isa{add} and \isa{rem} wrt.\
+their counterparts \isa{{\isasymunion}} and \isa{{\isacharminus}} on sets:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ set{\isacharunderscore}of{\isacharunderscore}add{\isacharcolon}\ \isanewline
+\ \ {\isachardoublequote}{\isasymlbrakk}\ i{\isasymle}j{\isacharsemicolon}\ inv\ ins\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ set{\isacharunderscore}of\ {\isacharparenleft}add\ {\isacharparenleft}i{\isacharcomma}j{\isacharparenright}\ ins{\isacharparenright}\ {\isacharequal}\ set{\isacharunderscore}of\ {\isacharbrackleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isacharbrackright}\ {\isasymunion}\ set{\isacharunderscore}of\ ins{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ set{\isacharunderscore}of{\isacharunderscore}rem{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}{\isasymlbrakk}\ i\ {\isasymle}\ j{\isacharsemicolon}\ inv\ ins\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ set{\isacharunderscore}of\ {\isacharparenleft}rem\ {\isacharparenleft}i{\isacharcomma}j{\isacharparenright}\ ins{\isacharparenright}\ {\isacharequal}\ set{\isacharunderscore}of\ ins\ {\isacharminus}\ set{\isacharunderscore}of\ {\isacharbrackleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Hints: in addition to the hints above, you may also find it
+useful to prove some relationship between \isa{inv{\isadigit{2}}} and \isa{set{\isacharunderscore}of} as a lemma.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{General hints%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{itemize}
+
+\item You should be familiar both with simplification and predicate
+calculus reasoning. Automatic tactics like \isa{blast} and \isa{force} can simplify the proof.
+
+\item
+Equality of two sets can often be proved via the rule \isa{set{\isacharunderscore}ext}:
+\begin{isabelle}%
+{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharparenleft}x\ {\isasymin}\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymin}\ B{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isacharequal}\ B%
+\end{isabelle}
+
+\item 
+Potentially useful theorems for the simplification of sets include \\
+\isa{Un{\isacharunderscore}Diff{\isacharcolon}}~\isa{A\ {\isasymunion}\ B\ {\isacharminus}\ C\ {\isacharequal}\ A\ {\isacharminus}\ C\ {\isasymunion}\ {\isacharparenleft}B\ {\isacharminus}\ C{\isacharparenright}} \\
+\isa{Diff{\isacharunderscore}triv{\isacharcolon}}~\isa{A\ {\isasyminter}\ B\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymLongrightarrow}\ A\ {\isacharminus}\ B\ {\isacharequal}\ A}.
+
+\item 
+Theorems can be instantiated and simplified via \isa{of} and
+\isa{{\isacharbrackleft}simplified{\isacharbrackright}} (see \cite{isabelle-tutorial}).
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2001/a5/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a5/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,6 @@
+\input{Aufgabe5.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/Makefile	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,48 @@
+#
+# $Id$
+#
+# IsaMakefile for PSV2002
+#
+
+SESSIONS = a1 a2 a3 a5 a6
+
+## targets
+
+default: sessions
+sessions: $(SESSIONS)
+
+
+## a1
+
+a1: a1/generated/session.tex
+
+a1/generated/session.tex: a1/ROOT.ML a1/*.thy
+	isatool make
+
+## a2
+
+a2: a2/generated/session.tex
+
+a2/generated/session.tex: a2/ROOT.ML a2/*.thy
+	isatool make
+
+## a3
+
+a3: a3/generated/session.tex
+
+a3/generated/session.tex: a3/ROOT.ML a3/*.thy
+	isatool make
+
+## a5
+
+a5: a5/generated/session.tex
+
+a5/generated/session.tex: a5/ROOT.ML a5/*.thy
+	isatool make
+
+## a6
+
+a6: a6/generated/session.tex
+
+a6/generated/session.tex: a6/ROOT.ML a6/*.thy
+	isatool make
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a1/generated/a1.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a1/generated/a1.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,90 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{1}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a universal and an existential quantifier on lists.
+Expression \isa{alls\ P\ xs} should be true iff \isa{P\ x} holds
+for every element \isa{x} of \isa{xs}, and \isa{exs\ P\ xs}
+should be true iff \isa{P\ x} holds for some element \isa{x} of
+\isa{xs}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ \isanewline
+\ \ alls\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
+\ \ exs\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove or disprove (by counter example) the following theorems.
+You may have to prove some lemmas first.
+
+Use the \isa{{\isacharbrackleft}simp{\isacharbrackright}}-attribute only if the equation is truly a
+simplification and is necessary for some later proof.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}alls\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\ xs\ {\isacharequal}\ {\isacharparenleft}alls\ P\ xs\ {\isasymand}\ alls\ Q\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}alls\ P\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ alls\ P\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}exs\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\ xs\ {\isacharequal}\ {\isacharparenleft}exs\ P\ xs\ {\isasymand}\ exs\ Q\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}exs\ P\ {\isacharparenleft}map\ f\ xs{\isacharparenright}\ {\isacharequal}\ exs\ {\isacharparenleft}P\ o\ f{\isacharparenright}\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}exs\ P\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ exs\ P\ xs{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Find a term \isa{Z} such that the following equation holds:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}exs\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P\ x\ {\isasymor}\ Q\ x{\isacharparenright}\ xs\ {\isacharequal}\ Z{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Express the existential via the universal quantifier ---
+\isa{exs} should not occur on the right-hand side:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}exs\ P\ xs\ {\isacharequal}\ Z{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{is{\isacharunderscore}in\ x\ xs} that checks if \isa{x} occurs in
+\isa{xs} vorkommt. Now express \isa{is{\isacharunderscore}in} via \isa{exs}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}is{\isacharunderscore}in\ a\ xs\ {\isacharequal}\ Z{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{nodups\ xs} that is true iff
+\isa{xs} does not contain duplicates, and a function \isa{deldups\ xs} that removes all duplicates. Note that \isa{deldups\ {\isacharbrackleft}x{\isacharcomma}\ y{\isacharcomma}\ x{\isacharbrackright}}
+(where \isa{x} and \isa{y} are distinct) can be either
+\isa{{\isacharbrackleft}x{\isacharcomma}\ y{\isacharbrackright}} or \isa{{\isacharbrackleft}y{\isacharcomma}\ x{\isacharbrackright}}.
+
+Prove or disprove (by counter example) the following theorems.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}length\ {\isacharparenleft}deldups\ xs{\isacharparenright}\ {\isacharless}{\isacharequal}\ length\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}nodups\ {\isacharparenleft}deldups\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}deldups\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ {\isacharparenleft}deldups\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a1/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a1/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,6 @@
+\input{a1.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a2/generated/a2.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a2/generated/a2.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,137 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{2}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Sorting \label{psv2002a2}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+For simplicity we sort natural numbers.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Sorting with lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The task is to define insertion sort and prove its correctness.
+The following functions are required:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ \isanewline
+\ \ insort\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isanewline
+\ \ sort\ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isanewline
+\ \ le\ \ \ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
+\ \ sorted\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+In your definition, \isa{insort\ x\ xs} should insert a
+number \isa{x} into an already sorted list \isa{xs}, and \isa{sort\ ys} should build on \isa{insort} to produce the sorted
+version of \isa{ys}.
+
+To show that the resulting list is indeed sorted we need a predicate
+\isa{sorted} that checks if each element in the list is less or equal
+to the following ones; \isa{le\ n\ xs} should be true iff
+\isa{n} is less or equal to all elements of \isa{xs}.
+
+Start out by showing a monotonicity property of \isa{le}.
+For technical reasons the lemma should be phrased as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ le\ y\ xs\ {\isasymlongrightarrow}\ le\ x\ xs{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Now show the following correctness theorem:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}sorted\ {\isacharparenleft}sort\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+This theorem alone is too weak. It does not guarantee that the
+sorted list contains the same elements as the input. In the worst
+case, \isa{sort} might always return \isa{{\isacharbrackleft}{\isacharbrackright}} --- surely an
+undesirable implementation of sorting.
+
+Define a function \isa{count\ xs\ x} that counts how often \isa{x}
+occurs in \isa{xs}. Show that%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}count\ {\isacharparenleft}sort\ xs{\isacharparenright}\ x\ {\isacharequal}\ count\ xs\ x{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\isamarkupsubsubsection{Sorting with trees%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Our second sorting algorithm uses trees. Thus you should first
+define a data type \isa{bintree} of binary trees that are either
+empty or consist of a node carrying a natural number and two subtrees.
+
+Define a function \isa{tsorted} that checks if a binary tree is
+sorted. It is convenien to employ two auxiliary functions \isa{tge}/\isa{tle} that test whether a number is
+greater-or-equal/less-or-equal to all elements of a tree.
+
+Finally define a function \isa{tree{\isacharunderscore}of} that turns a list into a
+sorted tree. It is helpful to base \isa{tree{\isacharunderscore}of} on a function
+\isa{ins\ n\ b} that inserts a number \isa{n} into a sorted tree
+\isa{b}.
+
+Show%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}tsorted\ {\isacharparenleft}tree{\isacharunderscore}of\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Again we have to show that no elements are lost (or added).
+As for lists, define a function \isa{tcount\ x\ b} that counts the
+number of occurrences of the number \isa{x} in the tree \isa{b}.
+Show%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}tcount\ {\isacharparenleft}tree{\isacharunderscore}of\ xs{\isacharparenright}\ x\ {\isacharequal}\ count\ xs\ x{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Now we are ready to sort lists. We know how to produce an
+ordered tree from a list. Thus we merely need a function \isa{list{\isacharunderscore}of} that turns an (ordered) tree into an (ordered) list.
+Define this function and prove%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}sorted\ {\isacharparenleft}list{\isacharunderscore}of\ {\isacharparenleft}tree{\isacharunderscore}of\ xs{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}count\ {\isacharparenleft}list{\isacharunderscore}of\ {\isacharparenleft}tree{\isacharunderscore}of\ xs{\isacharparenright}{\isacharparenright}\ n\ {\isacharequal}\ count\ xs\ n{\isachardoublequote}\ \ \ \ \isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Hints:
+\begin{itemize}
+\item
+Try to formulate all your lemmas as equations rather than implications
+because that often simplifies their proof.
+Make sure that the right-hand side is (in some sense)
+simpler than the left-hand side.
+\item
+Eventually you need to relate \isa{sorted} and \isa{tsorted}.
+This is facilitated by a function \isa{ge} on lists (analogously to
+\isa{tge} on trees) and the following lemma (that you will need to prove):
+\begin{isabelle}%
+sorted\ {\isacharparenleft}a\ {\isacharat}\ x\ {\isacharhash}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}sorted\ a\ {\isasymand}\ sorted\ b\ {\isasymand}\ ge\ x\ a\ {\isasymand}\ le\ x\ b{\isacharparenright}%
+\end{isabelle}
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a2/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a2/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,6 @@
+\input{a2.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a3/generated/a3.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a3/generated/a3.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,50 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{3}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Compilation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This exercise deals with the compiler example in section~3.3
+of \cite{isabelle-tutorial}. The simple side effect free expressions
+are extended with side effects.
+\begin{enumerate}
+
+\item Read sections 3.3 and 8.2 of \cite{isabelle-tutorial}.  Study
+the section about \isa{fun{\isacharunderscore}upd} in theory \isa{Fun} of HOL:
+\isa{fun{\isacharunderscore}upd\ f\ x\ y}, written \isa{f{\isacharparenleft}x{\isacharcolon}{\isacharequal}y{\isacharparenright}}, is \isa{f}
+updated at \isa{x} with new value \isa{y}.
+
+\item Extend data type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ expr} with a new alternative
+\isa{Assign\ x\ e} that shall represent an assignment \isa{x\ {\isacharequal}\ e} of the value of the expression \isa{e} to the variable \isa{x}.
+The value of an assignment shall be the value of \isa{e}.
+
+\item Modify the evaluation function \isa{value} such that it can
+deal with assignments. Note that since the evaluation of an expression
+may now change the environment, it no longer suffices to return only
+the value from the evaluation of an expression.
+
+Define a function \isa{se{\isacharunderscore}free\ {\isacharcolon}{\isacharcolon}\ expr\ {\isasymRightarrow}\ bool} that
+identifies side effect free expressions. Show that \isa{se{\isacharunderscore}free\ e}
+implies that evaluation of \isa{e} does not change the environment.
+
+\item Extend data type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ instr} with a new instruction
+\isa{Store\ x} that stores the topmost element on the stack in
+address/variable \isa{x}, without removing it from the stack.
+Update the machine semantics \isa{exec} accordingly. You will face
+the same problem as in the extension of \isa{value}.
+
+\item Modify the compiler \isa{comp} and its correctness proof to
+accommodate the above changes.
+\end{enumerate}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a3/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a3/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,6 @@
+\input{a3.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a5/generated/a5.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a5/generated/a5.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,55 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{5}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Merge sort%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Implement \emph{merge sort}: a list is sorted by splitting it
+into two lists, sorting them separately, and merging the results.
+
+With the help of \isa{recdef} define two functions%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ merge\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymtimes}\ nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ msort\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+and show%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}sorted\ {\isacharparenleft}msort\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}count\ {\isacharparenleft}msort\ xs{\isacharparenright}\ x\ {\isacharequal}\ count\ xs\ x{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+where \isa{sorted} and \isa{count} are defined as in
+section~\ref{psv2002a2}.
+
+Hints:
+\begin{itemize}
+\item For \isa{recdef} see section~3.5 of \cite{isabelle-tutorial}.
+
+\item To split a list into two halves of almost equal length you can
+use the functions \mbox{\isa{n\ div\ {\isadigit{2}}}}, \isa{take} und \isa{drop},
+where \isa{take\ n\ xs} returns the first \isa{n} elements of
+\isa{xs} and \isa{drop\ n\ xs} the remainder.
+
+\item Here are some potentially useful lemmas:\\
+  \isa{linorder{\isacharunderscore}not{\isacharunderscore}le{\isacharcolon}} \isa{{\isacharparenleft}{\isasymnot}\ x\ {\isasymle}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isacharless}\ x{\isacharparenright}}\\
+  \isa{order{\isacharunderscore}less{\isacharunderscore}le{\isacharcolon}} \isa{{\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymle}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}}\\
+  \isa{min{\isacharunderscore}def{\isacharcolon}} \isa{min\ a\ b\ {\isasymequiv}\ if\ a\ {\isasymle}\ b\ then\ a\ else\ b}
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a5/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a5/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,6 @@
+\input{a5.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a6/generated/a6.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a6/generated/a6.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,31 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{6}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{The towers of Hanoi%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In section \ref{psv2000hanoi} we introduced the towers of Hanoi and
+defined a function \isa{moves} to generate the moves to solve the
+puzzle.  Now it is time to show that \isa{moves} is correct. This
+means that
+\begin{itemize}
+\item when executing the list of moves, the result is indeed the
+intended one, i.e.\ all disks are moved from one peg to another, and
+\item all of the moves are legal, i.e.\ never place a larger disk
+on top of a smaller one.
+\end{itemize}
+Hint: this is a nontrivial undertaking. The complexity of your proofs
+will depend crucially on your choice of model and you may have to
+revise your model as you proceed with the proof.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/2002/a6/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2002/a6/generated/session.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,6 @@
+\input{a6.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 399c8103a98f -r ed4e97874454 doc-src/Exercises/Makefile
--- a/doc-src/Exercises/Makefile	Sat Mar 01 16:45:51 2003 +0100
+++ b/doc-src/Exercises/Makefile	Sat Mar 01 16:57:32 2003 +0100
@@ -8,23 +8,23 @@
 	latex exercises
 	latex exercises
 
-pdf: gen
+pdf: gen 
 	pdflatex exercises
 	bibtex exercises
 	pdflatex exercises
 	pdflatex exercises
 
 g2000:
-	cd 2000; isatool make
+	cd 2000; make
 
 g2001:
-	cd 2001; isatool make
+	cd 2001; make
 
 g2002:
-	cd 2002; isatool make
+	cd 2002; make
 
 clean:
 	rm -f *.log *.aux *.bbl *.blg *.toc *.out *~
 
 realclean: clean
-	rm -rf exercises.pdf */*/generated
+	rm -rf exercises.pdf execrcises.dvi