equal
deleted
inserted
replaced
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Snoc}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{Lists% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 Define a primitive recursive function \isa{snoc} that appends an element |
|
12 at the \emph{right} end of a list. Do not use \isa{{\isacharat}} itself.% |
|
13 \end{isamarkuptext}% |
|
14 \isamarkuptrue% |
|
15 \isacommand{consts}\isanewline |
|
16 \ \ snoc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse% |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 Prove the following theorem:% |
|
20 \end{isamarkuptext}% |
|
21 \isamarkuptrue% |
|
22 \isacommand{theorem}\ rev{\isacharunderscore}cons{\isacharcolon}\ {\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ snoc\ {\isacharparenleft}rev\ xs{\isacharparenright}\ x{\isachardoublequote}\isamarkupfalse% |
|
23 \isamarkupfalse% |
|
24 % |
|
25 \begin{isamarkuptext}% |
|
26 Hint: you need to prove a suitable lemma first.% |
|
27 \end{isamarkuptext}% |
|
28 \isamarkuptrue% |
|
29 \isamarkupfalse% |
|
30 \end{isabellebody}% |
|
31 %%% Local Variables: |
|
32 %%% mode: latex |
|
33 %%% TeX-master: "root" |
|
34 %%% End: |
|