# HG changeset patch
# User streckem
# Date 1080723110 -7200
# Node ID 2015348ceecba893bc76728d244f83f5a00bc97b
# Parent  f08ea8e964d85a71757a199986a50f4429131581
new

diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a1/generated/a1.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a1/generated/a1.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,108 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{1}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{List functions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a function \isa{sum}, which computes the sum of
+elements of a list of natural numbers.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Then, define a function \isa{flatten} which flattens a list
+of lists by appending the member lists.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ flatten\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Test your function by applying them to the following example lists:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}sum\ {\isacharbrackleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{8}}{\isacharbrackright}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}flatten\ {\isacharbrackleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{7}}{\isacharcomma}\ {\isadigit{9}}{\isacharbrackright}{\isacharbrackright}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove the following statements, or give a counterexample:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}length\ {\isacharparenleft}flatten\ xs{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharparenleft}map\ length\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ sum{\isacharunderscore}append{\isacharcolon}\ {\isachardoublequote}sum\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ sum\ xs\ {\isacharplus}\ sum\ ys{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ flatten{\isacharunderscore}append{\isacharcolon}\ {\isachardoublequote}flatten\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ flatten\ xs\ {\isacharat}\ flatten\ ys{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}flatten\ {\isacharparenleft}map\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ rev\ {\isacharparenleft}flatten\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}flatten\ {\isacharparenleft}rev\ {\isacharparenleft}map\ rev\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ rev\ {\isacharparenleft}flatten\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}list{\isacharunderscore}all\ {\isacharparenleft}list{\isacharunderscore}all\ P{\isacharparenright}\ xs\ {\isacharequal}\ list{\isacharunderscore}all\ P\ {\isacharparenleft}flatten\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}flatten\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ flatten\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}sum\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ sum\ xs{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Find a predicate \isa{P} which satisfies%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}list{\isacharunderscore}all\ P\ xs\ {\isasymlongrightarrow}\ length\ xs\ {\isasymle}\ sum\ xs{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define, by means of primitive recursion, a function \isa{exists} which checks whether an element satisfying a given property is
+contained in the list:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ list{\isacharunderscore}exists\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Test your function on the following examples:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}list{\isacharunderscore}exists\ {\isacharparenleft}{\isasymlambda}\ n{\isachardot}\ n\ {\isacharless}\ {\isadigit{3}}{\isacharparenright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{7}}{\isacharbrackright}\ {\isacharequal}\ b{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}list{\isacharunderscore}exists\ {\isacharparenleft}{\isasymlambda}\ n{\isachardot}\ n\ {\isacharless}\ {\isadigit{4}}{\isacharparenright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{7}}{\isacharbrackright}\ {\isacharequal}\ b{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove the following statements:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ list{\isacharunderscore}exists{\isacharunderscore}append{\isacharcolon}\ \isanewline
+\ \ {\isachardoublequote}list{\isacharunderscore}exists\ P\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}list{\isacharunderscore}exists\ P\ xs\ {\isasymor}\ list{\isacharunderscore}exists\ P\ ys{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}list{\isacharunderscore}exists\ {\isacharparenleft}list{\isacharunderscore}exists\ P{\isacharparenright}\ xs\ {\isacharequal}\ list{\isacharunderscore}exists\ P\ {\isacharparenleft}flatten\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+You could have defined \isa{list{\isacharunderscore}exists} only with the aid of
+\isa{list{\isacharunderscore}all}. Do this now, i.e. define a function \isa{list{\isacharunderscore}exists{\isadigit{2}}} and show that it is equivalent to \isa{list{\isacharunderscore}exists}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isanewline
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a1/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a1/generated/session.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,6 @@
+\input{a1.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a2/generated/a2.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a2/generated/a2.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,176 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{2}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Folding Lists and Trees%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Some more list functions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Recall the summation function%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\isanewline
+\ \ {\isachardoublequote}sum\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sum\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharplus}\ sum\ xs{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+In the Isabelle library, you will find in theory
+\texttt{List.thy} the functions \isa{foldr} and \isa{foldl}, which
+allow you to define some list functions, among them \isa{sum} and
+\isa{length}. Show the following:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ sum{\isacharunderscore}foldr{\isacharcolon}\ {\isachardoublequote}sum\ xs\ {\isacharequal}\ foldr\ {\isacharparenleft}op\ {\isacharplus}{\isacharparenright}\ xs\ {\isadigit{0}}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ length{\isacharunderscore}foldr{\isacharcolon}\ {\isachardoublequote}length\ xs\ {\isacharequal}\ foldr\ {\isacharparenleft}{\isasymlambda}\ x\ res{\isachardot}\ {\isadigit{1}}\ {\isacharplus}\ res{\isacharparenright}\ xs\ {\isadigit{0}}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Repeated application of \isa{foldr} and \isa{map} has the
+disadvantage that a list is traversed several times. A single traversal is sufficient, as
+illustrated by the following example:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}sum\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ x\ {\isacharplus}\ {\isadigit{3}}{\isacharparenright}\ xs{\isacharparenright}\ {\isacharequal}\ foldr\ h\ xs\ b{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Find terms \isa{h} and \isa{b} which solve this
+equation. Generalize this result, i.e. show for appropriate \isa{h}
+and \isa{b}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}foldr\ g\ {\isacharparenleft}map\ f\ xs{\isacharparenright}\ a\ {\isacharequal}\ foldr\ h\ xs\ b{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Hint: Isabelle can help you find the solution if you use the
+equalities arising during a proof attempt.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The following function \isa{rev{\isacharunderscore}acc} reverses a list in linear time:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ rev{\isacharunderscore}acc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a\ list{\isacharcomma}\ {\isacharprime}a\ list{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\isanewline
+\ \ {\isachardoublequote}rev{\isacharunderscore}acc\ {\isacharbrackleft}{\isacharbrackright}\ ys\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}rev{\isacharunderscore}acc\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ {\isacharparenleft}rev{\isacharunderscore}acc\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Show that \isa{rev{\isacharunderscore}acc} can be defined by means of \isa{foldl}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ rev{\isacharunderscore}acc{\isacharunderscore}foldl{\isacharcolon}\ {\isachardoublequote}rev{\isacharunderscore}acc\ xs\ a\ {\isacharequal}\ foldl\ {\isacharparenleft}{\isasymlambda}\ ys\ x{\isachardot}\ x\ {\isacharhash}\ ys{\isacharparenright}\ a\ xs{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+On the first exercise sheet, we have shown:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ sum{\isacharunderscore}append\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}sum\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ sum\ xs\ {\isacharplus}\ sum\ ys{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}induct\ xs{\isacharparenright}\ auto\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove a similar distributivity property for \isa{foldr},
+i.e. something like \isa{foldr\ f\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ a\ {\isacharequal}\ f\ {\isacharparenleft}foldr\ f\ xs\ a{\isacharparenright}\ {\isacharparenleft}foldr\ f\ ys\ a{\isacharparenright}}. However, you will have to strengthen the premisses
+by taking into account algebraic properties of \isa{f} and \isa{a}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ foldr{\isacharunderscore}append{\isacharcolon}\ {\isachardoublequote}foldr\ f\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ a\ {\isacharequal}\ f\ {\isacharparenleft}foldr\ f\ xs\ a{\isacharparenright}\ {\isacharparenleft}foldr\ f\ ys\ a{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Now, define the function \isa{prod}, which computes the product of all list elements:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+direcly with the aid of  a fold and prove the following:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}prod\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ prod\ xs\ {\isacharasterisk}\ prod\ ys{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\isamarkupsubsubsection{Functions on Trees%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Consider the following type of binary trees:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define functions which convert a tree into a list by traversing it in pre- resp. postorder:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ preorder\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\ \ postorder\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+You have certainly realized that computation of postorder traversal can be efficiently realized with an accumulator, in analogy to  \isa{rev{\isacharunderscore}acc}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ postorder{\isacharunderscore}acc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a\ tree{\isacharcomma}\ {\isacharprime}a\ list{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define this function and show:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}postorder{\isacharunderscore}acc\ t\ xs\ {\isacharequal}\ {\isacharparenleft}postorder\ t{\isacharparenright}\ {\isacharat}\ xs{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\isa{postorder{\isacharunderscore}acc} is the instance of a function
+\isa{foldl{\isacharunderscore}tree}, which is similar to \isa{foldl}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ foldl{\isacharunderscore}tree\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}b\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Show the following:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}\ a{\isachardot}\ postorder{\isacharunderscore}acc\ t\ a\ {\isacharequal}\ foldl{\isacharunderscore}tree\ {\isacharparenleft}{\isasymlambda}\ xs\ x{\isachardot}\ Cons\ x\ xs{\isacharparenright}\ a\ t{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{tree{\isacharunderscore}sum} that computes the sum of
+the elements of a tree of natural numbers:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ tree{\isacharunderscore}sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ tree\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+and show that this function satisfies%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}tree{\isacharunderscore}sum\ t\ {\isacharequal}\ sum\ {\isacharparenleft}preorder\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a2/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a2/generated/session.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,6 @@
+\input{a2.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a3/generated/a3.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a3/generated/a3.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,83 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{3}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Natural deduction -- Propositional Logic \label{psv0304a3}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In this exercise, we will prove some lemmas of propositional
+logic with the aid of a calculus of natural deduction.
+
+For the proofs, you may only use
+
+\begin{itemize}
+\item the following lemmas: \\
+\isa{notI{\isacharcolon}}~\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ False{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymnot}\ A},\\
+\isa{notE{\isacharcolon}}~\isa{{\isasymlbrakk}{\isasymnot}\ A{\isacharsemicolon}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ B},\\
+\isa{conjI{\isacharcolon}}~\isa{{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B},\\ 
+\isa{conjE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymand}\ B{\isacharsemicolon}\ {\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C},\\
+\isa{disjI{\isadigit{1}}{\isacharcolon}}~\isa{A\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B},\\
+\isa{disjI{\isadigit{2}}{\isacharcolon}}~\isa{A\ {\isasymLongrightarrow}\ B\ {\isasymor}\ A},\\
+\isa{disjE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymor}\ B{\isacharsemicolon}\ A\ {\isasymLongrightarrow}\ C{\isacharsemicolon}\ B\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C},\\
+\isa{impI{\isacharcolon}}~\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymlongrightarrow}\ B},\\
+\isa{impE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymlongrightarrow}\ B{\isacharsemicolon}\ A{\isacharsemicolon}\ B\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C},\\
+\isa{mp{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymlongrightarrow}\ B{\isacharsemicolon}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ B}\\
+\isa{iffI{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymLongrightarrow}\ B{\isacharsemicolon}\ B\ {\isasymLongrightarrow}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ A\ {\isacharequal}\ B}, \\
+\isa{iffE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymlbrakk}A\ {\isasymlongrightarrow}\ B{\isacharsemicolon}\ B\ {\isasymlongrightarrow}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C}\\
+\isa{classical{\isacharcolon}}~\isa{{\isacharparenleft}{\isasymnot}\ A\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A}
+
+\item the proof methods \isa{rule}, \isa{erule} and \isa{assumption}
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ I{\isacharcolon}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymor}\ C{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymor}\ {\isacharparenleft}B\ {\isasymor}\ C{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ K{\isacharcolon}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymor}\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymand}\ A{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ S{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B\ {\isasymlongrightarrow}\ C{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymlongrightarrow}\ C{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}B\ {\isasymlongrightarrow}\ C{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymlongrightarrow}\ C{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ {\isasymnot}\ A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ {\isasymnot}\ {\isasymnot}\ A{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymnot}\ A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymnot}\ B\ {\isasymlongrightarrow}\ A{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymor}\ {\isasymnot}\ A{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isacharparenright}\ {\isacharequal} {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a3/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a3/generated/session.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,6 @@
+\input{a3.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a4/generated/a4.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a4/generated/a4.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,106 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{4}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Natural Deduction -- Predicate Logic; Sets as Lists%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Predicate Logic Formulae%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We are again talking about proofs in the calculus of Natural
+Deduction. In addition to the rules of section~\ref{psv0304a3}, you may now also use
+
+
+  \isa{exI{\isacharcolon}}~\isa{P\ x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ P\ x}\\
+  \isa{exE{\isacharcolon}}~\isa{{\isasymlbrakk}{\isasymexists}x{\isachardot}\ P\ x{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q}\\
+  \isa{allI{\isacharcolon}}~\isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ P\ x}\\
+  \isa{allE{\isacharcolon}}~\isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x{\isacharsemicolon}\ P\ x\ {\isasymLongrightarrow}\ R{\isasymrbrakk}\ {\isasymLongrightarrow}\ R}\\
+
+Give a proof of the following propositions or an argument why the formula is not valid:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ P\ x\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymlongrightarrow}\ Q{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}{\isasymforall}\ x{\isachardot}\ P\ x{\isacharparenright}\ \ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ x{\isachardot}\ Q\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}\ x{\isachardot}\ {\isacharparenleft}P\ x\ {\isasymand}\ Q\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}{\isasymforall}\ x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymforall}\ x{\isachardot}\ Q\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}\ x{\isachardot}\ {\isacharparenleft}P\ x\ {\isasymor}\ Q\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}{\isasymexists}\ x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}\ x{\isachardot}\ Q\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}\ x{\isachardot}\ {\isacharparenleft}P\ x\ {\isasymor}\ Q\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ {\isacharparenleft}P\ x\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\isamarkupsubsubsection{Sets as Lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Finite sets can obviously be implemented by lists. In the
+following, you will be asked to implement the set operations union,
+intersection and difference and to show that these implementations are
+correct. Thus, for a function%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ list{\isacharunderscore}union\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a\ list{\isacharcomma}\ {\isacharprime}a\ list{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+to be defined by you it has to be shown that%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}set\ {\isacharparenleft}list{\isacharunderscore}union\ xs\ ys{\isacharparenright}\ {\isacharequal}\ set\ xs\ {\isasymunion}\ set\ ys{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+In addition, the functions should be space efficient in the
+sense that one obtains lists without duplicates (\isa{distinct})
+whenever the parameters of the functions are duplicate-free. Thus, for
+example,%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \isanewline
+\ \ {\isachardoublequote}distinct\ xs\ {\isasymlongrightarrow}\ distinct\ ys\ {\isasymlongrightarrow}\ {\isacharparenleft}distinct\ {\isacharparenleft}list{\isacharunderscore}union\ xs\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\emph{Hint:} \isa{distinct} is defined in \isa{List{\isachardot}thy}. Also the function \isa{mem} and the lemma \isa{set{\isacharunderscore}mem{\isacharunderscore}eq} may be useful.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Quantification over Sets%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a set \isa{S} such that the following proposition holds:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}{\isasymforall}\ x\ {\isasymin}\ A{\isachardot}\ P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ x\ {\isasymin}\ B{\isachardot}\ P\ x{\isacharparenright}{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}\ x\ {\isasymin}\ S{\isachardot}\ P\ x{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a predicate \isa{P} such that%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}\ x\ {\isasymin}\ A{\isachardot}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isasymLongrightarrow}\ \ {\isasymforall}\ y\ {\isasymin}\ f\ {\isacharbackquote}\ A{\isachardot}\ Q\ y{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isanewline
+\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a4/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a4/generated/session.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,6 @@
+\input{a4.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a5/generated/a5.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a5/generated/a5.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,124 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{5}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{The Euclidean Algorithm -- Inductively%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Rules without Base Case%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Show that the following%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ evenempty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{inductive}\ evenempty\isanewline
+\ \ \isakeyword{intros}\isanewline
+\ \ Add{\isadigit{2}}Ie{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ evenempty\ {\isasymLongrightarrow}\ Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ evenempty{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+defines the empty set:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ evenempty{\isacharunderscore}empty{\isacharcolon}\ {\isachardoublequote}evenempty\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\isamarkupsubsubsection{The Euclidean Algorithm%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define inductively the set \isa{gcd}, which characterizes
+the greatest common divisor of two natural numbers:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat{\isacharparenright}\ set{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Here, \isa{{\isacharparenleft}a{\isacharcomma}b{\isacharcomma}g{\isacharparenright}\ {\isasymin}\ gcd} means that \isa{g} is the gcd
+of \isa{a} und \isa{b}. The definition should closely follow the
+Euclidean algorithm.
+
+Reminder: The Euclidean algorithm repeatedly subtracts the smaller
+from the larger number, until one of the numbers is 0. Then, the other
+number is the gcd.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Now, compute the gcd of 15 and 10:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isadigit{5}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}g{\isacharparenright}\ \ {\isasymin}\ gcd{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+How does your algorithm behave on special cases as the following?%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isacharquery}g{\isacharparenright}\ \ {\isasymin}\ gcd{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Show that the gcd is really a divisor (for the proof, you need an appropriate lemma):%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ gcd{\isacharunderscore}divides{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}a{\isacharcomma}b{\isacharcomma}g{\isacharparenright}\ {\isasymin}\ gcd\ {\isasymLongrightarrow}\ g\ dvd\ a\ {\isasymand}\ g\ dvd\ b{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Show that the gcd is the greatest common divisor:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ gcd{\isacharunderscore}greatest\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}a{\isacharcomma}b{\isacharcomma}g{\isacharparenright}\ {\isasymin}\ gcd\ {\isasymLongrightarrow}\isanewline
+\ \ {\isadigit{0}}\ {\isacharless}\ a\ {\isasymor}\ {\isadigit{0}}\ {\isacharless}\ b\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}\ d{\isachardot}\ d\ dvd\ a\ {\isasymlongrightarrow}\ d\ dvd\ b\ {\isasymlongrightarrow}\ d\ {\isasymle}\ g{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Here as well, you will have to prove a suitable lemma. What is
+the precondition \isa{{\isadigit{0}}\ {\isacharless}\ a\ {\isasymor}\ {\isadigit{0}}\ {\isacharless}\ b} good for?
+
+So far, we have only shown that \isa{gcd} is correct, but your
+algorithm might not compute a result for all values \isa{a{\isacharcomma}b}. Thus, show completeness of the algorithm:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ gcd{\isacharunderscore}defined{\isacharcolon}\ {\isachardoublequote}{\isasymforall}\ a\ b{\isachardot}\ {\isasymexists}\ g{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ g{\isacharparenright}\ {\isasymin}\ gcd{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+The following lemma, proved by course-of-value recursion over
+\isa{n}, may be useful. Why does standard induction over natural
+numbers not work here?%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ gcd{\isacharunderscore}defined{\isacharunderscore}aux\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \isanewline
+\ \ {\isachardoublequote}{\isasymforall}\ a\ b{\isachardot}\ {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isasymle}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ g{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ g{\isacharparenright}\ {\isasymin}\ gcd{\isacharparenright}{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}induct\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{apply}\ clarify\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+The idea is to show that \isa{gcd} yields a result for all
+\isa{a{\isacharcomma}\ b} whenever it is known that \isa{gcd} yields a result
+for all \isa{a{\isacharprime}{\isacharcomma}\ b{\isacharprime}} whose sum is smaller than \isa{a\ {\isacharplus}\ b}.
+
+In order to prove this lemma, make case distinctions corresponding to
+the different clauses of the algorithm, and show how to reduce
+computation of \isa{gcd} for \isa{a{\isacharcomma}\ b} to computation of \isa{gcd} for suitable smaller \isa{a{\isacharprime}{\isacharcomma}\ b{\isacharprime}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isanewline
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f08ea8e964d8 -r 2015348ceecb doc-src/Exercises/0304/a5/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/0304/a5/generated/session.tex	Wed Mar 31 10:51:50 2004 +0200
@@ -0,0 +1,6 @@
+\input{a5.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: