1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{a{\isadigit{1}}}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{List functions% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 Define a function \isa{sum}, which computes the sum of |
|
12 elements of a list of natural numbers.% |
|
13 \end{isamarkuptext}% |
|
14 \isamarkuptrue% |
|
15 \ \ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse% |
|
16 % |
|
17 \begin{isamarkuptext}% |
|
18 Then, define a function \isa{flatten} which flattens a list |
|
19 of lists by appending the member lists.% |
|
20 \end{isamarkuptext}% |
|
21 \isamarkuptrue% |
|
22 \ \ flatten\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse% |
|
23 % |
|
24 \begin{isamarkuptext}% |
|
25 Test your function by applying them to the following example lists:% |
|
26 \end{isamarkuptext}% |
|
27 \isamarkuptrue% |
|
28 \isacommand{lemma}\ {\isachardoublequote}sum\ {\isacharbrackleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{8}}{\isacharbrackright}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse% |
|
29 \isanewline |
|
30 \isamarkupfalse% |
|
31 \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% |
|
32 \isamarkupfalse% |
|
33 % |
|
34 \begin{isamarkuptext}% |
|
35 Prove the following statements, or give a counterexample:% |
|
36 \end{isamarkuptext}% |
|
37 \isamarkuptrue% |
|
38 \isacommand{lemma}\ {\isachardoublequote}length\ {\isacharparenleft}flatten\ xs{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharparenleft}map\ length\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
39 \isanewline |
|
40 \isamarkupfalse% |
|
41 \isacommand{lemma}\ sum{\isacharunderscore}append{\isacharcolon}\ {\isachardoublequote}sum\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ sum\ xs\ {\isacharplus}\ sum\ ys{\isachardoublequote}\isamarkupfalse% |
|
42 \isanewline |
|
43 \isamarkupfalse% |
|
44 \isacommand{lemma}\ flatten{\isacharunderscore}append{\isacharcolon}\ {\isachardoublequote}flatten\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ flatten\ xs\ {\isacharat}\ flatten\ ys{\isachardoublequote}\isamarkupfalse% |
|
45 \isanewline |
|
46 \isamarkupfalse% |
|
47 \isacommand{lemma}\ {\isachardoublequote}flatten\ {\isacharparenleft}map\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ rev\ {\isacharparenleft}flatten\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
48 \isanewline |
|
49 \isamarkupfalse% |
|
50 \isacommand{lemma}\ {\isachardoublequote}flatten\ {\isacharparenleft}rev\ {\isacharparenleft}map\ rev\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ rev\ {\isacharparenleft}flatten\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
51 \isanewline |
|
52 \isamarkupfalse% |
|
53 \isacommand{lemma}\ {\isachardoublequote}list{\isacharunderscore}all\ {\isacharparenleft}list{\isacharunderscore}all\ P{\isacharparenright}\ xs\ {\isacharequal}\ list{\isacharunderscore}all\ P\ {\isacharparenleft}flatten\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
54 \isanewline |
|
55 \isamarkupfalse% |
|
56 \isacommand{lemma}\ {\isachardoublequote}flatten\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ flatten\ xs{\isachardoublequote}\isamarkupfalse% |
|
57 \isanewline |
|
58 \isamarkupfalse% |
|
59 \isacommand{lemma}\ {\isachardoublequote}sum\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ sum\ xs{\isachardoublequote}\isamarkupfalse% |
|
60 \isamarkupfalse% |
|
61 % |
|
62 \begin{isamarkuptext}% |
|
63 Find a predicate \isa{P} which satisfies% |
|
64 \end{isamarkuptext}% |
|
65 \isamarkuptrue% |
|
66 \isacommand{lemma}\ {\isachardoublequote}list{\isacharunderscore}all\ P\ xs\ {\isasymlongrightarrow}\ length\ xs\ {\isasymle}\ sum\ xs{\isachardoublequote}\isamarkupfalse% |
|
67 \isamarkupfalse% |
|
68 % |
|
69 \begin{isamarkuptext}% |
|
70 Define, by means of primitive recursion, a function \isa{exists} which checks whether an element satisfying a given property is |
|
71 contained in the list:% |
|
72 \end{isamarkuptext}% |
|
73 \isamarkuptrue% |
|
74 \ \ list{\isacharunderscore}exists\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
75 % |
|
76 \begin{isamarkuptext}% |
|
77 Test your function on the following examples:% |
|
78 \end{isamarkuptext}% |
|
79 \isamarkuptrue% |
|
80 \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% |
|
81 \isanewline |
|
82 \isamarkupfalse% |
|
83 \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% |
|
84 \isamarkupfalse% |
|
85 % |
|
86 \begin{isamarkuptext}% |
|
87 Prove the following statements:% |
|
88 \end{isamarkuptext}% |
|
89 \isamarkuptrue% |
|
90 \isacommand{lemma}\ list{\isacharunderscore}exists{\isacharunderscore}append{\isacharcolon}\ \isanewline |
|
91 \ \ {\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% |
|
92 \isanewline |
|
93 \isamarkupfalse% |
|
94 \isacommand{lemma}\ {\isachardoublequote}list{\isacharunderscore}exists\ {\isacharparenleft}list{\isacharunderscore}exists\ P{\isacharparenright}\ xs\ {\isacharequal}\ list{\isacharunderscore}exists\ P\ {\isacharparenleft}flatten\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
95 \isamarkupfalse% |
|
96 % |
|
97 \begin{isamarkuptext}% |
|
98 You could have defined \isa{list{\isacharunderscore}exists} only with the aid of |
|
99 \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}.% |
|
100 \end{isamarkuptext}% |
|
101 \isamarkuptrue% |
|
102 \isanewline |
|
103 \isamarkupfalse% |
|
104 \end{isabellebody}% |
|
105 %%% Local Variables: |
|
106 %%% mode: latex |
|
107 %%% TeX-master: "root" |
|
108 %%% End: |
|