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