1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Exercises/2003/a1/ROOT.ML Tue Apr 06 16:16:36 2004 +0200
1.3 @@ -0,0 +1,1 @@
1.4 + use_thy "a1";
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/Exercises/2003/a1/generated/a1.tex Tue Apr 06 16:16:36 2004 +0200
2.3 @@ -0,0 +1,109 @@
2.4 +%
2.5 +\begin{isabellebody}%
2.6 +\def\isabellecontext{a{\isadigit{1}}}%
2.7 +\isamarkupfalse%
2.8 +%
2.9 +\isamarkupsubsection{Lists%
2.10 +}
2.11 +\isamarkuptrue%
2.12 +%
2.13 +\begin{isamarkuptext}%
2.14 +Define a function \isa{occurs}, such that \isa{occurs\ x\ xs}
2.15 +is the number of occurrences of the element \isa{x} in the list
2.16 +\isa{xs}.%
2.17 +\end{isamarkuptext}%
2.18 +\isamarkuptrue%
2.19 +\ \ occurs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
2.20 +%
2.21 +\begin{isamarkuptext}%
2.22 +Prove or disprove (by counter example) the theorems that follow. You may have to prove some lemmas first.
2.23 +
2.24 +Use the \isa{{\isacharbrackleft}simp{\isacharbrackright}}-attribute only if the equation is truly a
2.25 +simplification and is necessary for some later proof.
2.26 +
2.27 +In the case of a non-theorem try to find a suitable assumption under which the theorem holds.%
2.28 +\end{isamarkuptext}%
2.29 +\isamarkuptrue%
2.30 +\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ occurs\ a\ xs\ {\isacharplus}\ occurs\ a\ ys\ {\isachardoublequote}\isamarkupfalse%
2.31 +\isanewline
2.32 +\isamarkupfalse%
2.33 +\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ xs\ {\isacharequal}\ occurs\ a\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
2.34 +\isanewline
2.35 +\isamarkupfalse%
2.36 +\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ xs\ {\isacharless}{\isacharequal}\ length\ xs{\isachardoublequote}\isamarkupfalse%
2.37 +\isanewline
2.38 +\isamarkupfalse%
2.39 +\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ {\isacharparenleft}replicate\ n\ a{\isacharparenright}\ {\isacharequal}\ n{\isachardoublequote}\isamarkupfalse%
2.40 +\isamarkupfalse%
2.41 +%
2.42 +\begin{isamarkuptext}%
2.43 +Define a function \isa{areAll}, such that \isa{areAll\ xs\ x} is true iff all elements of \isa{xs} are equal to \isa{x}.%
2.44 +\end{isamarkuptext}%
2.45 +\isamarkuptrue%
2.46 +\ \ areAll\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
2.47 +\isanewline
2.48 +\isamarkupfalse%
2.49 +\isacommand{theorem}\ {\isachardoublequote}areAll\ xs\ a\ {\isasymlongrightarrow}\ occurs\ a\ xs\ {\isacharequal}\ length\ xs{\isachardoublequote}\isamarkupfalse%
2.50 +\isanewline
2.51 +\isamarkupfalse%
2.52 +\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ xs\ {\isacharequal}\ length\ xs\ {\isasymlongrightarrow}\ areAll\ xs\ a{\isachardoublequote}\isamarkupfalse%
2.53 +\isamarkupfalse%
2.54 +%
2.55 +\begin{isamarkuptext}%
2.56 +Define two functions to delete elements from a list:
2.57 +\isa{del{\isadigit{1}}\ x\ xs} deletes the first (leftmost) occurrence of \isa{x} from \isa{xs}.
2.58 +\isa{delall\ x\ xs} deletes all occurrences of \isa{x} from \isa{xs}.%
2.59 +\end{isamarkuptext}%
2.60 +\isamarkuptrue%
2.61 +\ \ delall\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
2.62 +\ \ del{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
2.63 +\isanewline
2.64 +\isamarkupfalse%
2.65 +\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ {\isacharparenleft}delall\ a\ xs{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isamarkupfalse%
2.66 +\ \isanewline
2.67 +\isamarkupfalse%
2.68 +\isacommand{theorem}\ {\isachardoublequote}Suc\ {\isacharparenleft}occurs\ a\ {\isacharparenleft}del{\isadigit{1}}\ a\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ occurs\ a\ xs{\isachardoublequote}\isamarkupfalse%
2.69 +\isamarkupfalse%
2.70 +%
2.71 +\begin{isamarkuptext}%
2.72 +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}.%
2.73 +\end{isamarkuptext}%
2.74 +\isamarkuptrue%
2.75 +\ \ replace\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
2.76 +\isanewline
2.77 +\isamarkupfalse%
2.78 +\isacommand{theorem}\ {\isachardoublequote}occurs\ a\ xs\ {\isacharequal}\ occurs\ b\ {\isacharparenleft}replace\ a\ b\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
2.79 +\isamarkupfalse%
2.80 +%
2.81 +\begin{isamarkuptext}%
2.82 +With the help of \isa{occurs}, define a function \isa{remDups} that removes all duplicates from a list.%
2.83 +\end{isamarkuptext}%
2.84 +\isamarkuptrue%
2.85 +\ \ remDups\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
2.86 +%
2.87 +\begin{isamarkuptext}%
2.88 +Use \isa{occurs} to formulate and prove a lemma that expresses the fact that \isa{remDups} never inserts a new element into a list.%
2.89 +\end{isamarkuptext}%
2.90 +\isamarkuptrue%
2.91 +%
2.92 +\begin{isamarkuptext}%
2.93 +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}).%
2.94 +\end{isamarkuptext}%
2.95 +\isamarkuptrue%
2.96 +%
2.97 +\begin{isamarkuptext}%
2.98 +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.%
2.99 +\end{isamarkuptext}%
2.100 +\isamarkuptrue%
2.101 +\ \ unique\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isamarkupfalse%
2.102 +%
2.103 +\begin{isamarkuptext}%
2.104 +Formulate and prove the correctness of \isa{remDups} with the help of \isa{unique}.%
2.105 +\end{isamarkuptext}%
2.106 +\isamarkuptrue%
2.107 +\isamarkupfalse%
2.108 +\end{isabellebody}%
2.109 +%%% Local Variables:
2.110 +%%% mode: latex
2.111 +%%% TeX-master: "root"
2.112 +%%% End:
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/Exercises/2003/a1/generated/session.tex Tue Apr 06 16:16:36 2004 +0200
3.3 @@ -0,0 +1,6 @@
3.4 +\input{a1.tex}
3.5 +
3.6 +%%% Local Variables:
3.7 +%%% mode: latex
3.8 +%%% TeX-master: "root"
3.9 +%%% End: