# HG changeset patch
# User mehta
# Date 1081260996 -7200
# Node ID 9598f5bdeb9ece8ed155b077c14068af6fcf8995
# Parent  0ccba84113a1553743051e806fa5177a99c28c0b
*** empty log message ***

diff -r 0ccba84113a1 -r 9598f5bdeb9e doc-src/Exercises/2003/a1/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a1/ROOT.ML	Tue Apr 06 16:16:36 2004 +0200
@@ -0,0 +1,1 @@
+  use_thy "a1";
diff -r 0ccba84113a1 -r 9598f5bdeb9e doc-src/Exercises/2003/a1/generated/a1.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a1/generated/a1.tex	Tue Apr 06 16:16:36 2004 +0200
@@ -0,0 +1,109 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{1}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a function \isa{occurs}, such that \isa{occurs\ x\ xs} 
+is the number of occurrences of the element \isa{x} in the list
+\isa{xs}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ occurs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove or disprove (by counter example) the theorems that follow. 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.
+
+In the case of a non-theorem try to find a suitable assumption under which the theorem holds.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ occurs\ a\ xs\ {\isacharplus}\ occurs\ a\ ys\ {\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ xs\ {\isacharequal}\ occurs\ a\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ xs\ {\isacharless}{\isacharequal}\ length\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ {\isacharparenleft}replicate\ n\ a{\isacharparenright}\ {\isacharequal}\ n{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{areAll}, such that \isa{areAll\ xs\ x} is true iff all elements of \isa{xs} are equal to \isa{x}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ areAll\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}areAll\ xs\ a\ {\isasymlongrightarrow}\ occurs\ a\ xs\ {\isacharequal}\ length\ xs{\isachardoublequote}\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ xs\ {\isacharequal}\ length\ xs\ {\isasymlongrightarrow}\ areAll\ xs\ a{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define two functions to delete elements from a list:
+\isa{del{\isadigit{1}}\ x\ xs} deletes the first (leftmost) occurrence of \isa{x} from \isa{xs}.
+\isa{delall\ x\ xs} deletes all occurrences of \isa{x} from \isa{xs}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ delall\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\ \ del{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ {\isacharparenleft}delall\ a\ xs{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isamarkupfalse%
+\ \isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}Suc\ {\isacharparenleft}occurs\ a\ {\isacharparenleft}del{\isadigit{1}}\ a\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ occurs\ a\ xs{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\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%
+\ \ replace\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ xs\ {\isacharequal}\ occurs\ b\ {\isacharparenleft}replace\ a\ b\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+With the help of \isa{occurs}, define a function \isa{remDups} that removes all duplicates from a list.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ remDups\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Use \isa{occurs} to formulate and prove a lemma that expresses the fact that \isa{remDups} never inserts a new element into a list.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Use \isa{occurs} to formulate and prove a lemma that expresses the fact that \isa{remDups} always returns a list without duplicates (i.e.\ the correctness of \isa{remDups}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Now, with the help of \isa{occurs} define a function \isa{unique}, such that \isa{unique\ xs} is true iff every element in \isa{xs} occurs only once.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ unique\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Formulate and prove the correctness of \isa{remDups} with the help of \isa{unique}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 0ccba84113a1 -r 9598f5bdeb9e doc-src/Exercises/2003/a1/generated/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a1/generated/session.tex	Tue Apr 06 16:16:36 2004 +0200
@@ -0,0 +1,6 @@
+\input{a1.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: