replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
%
\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: