1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{a{\isadigit{1}}}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{Lists% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 Define a universal and an existential quantifier on lists. |
|
12 Expression \isa{alls\ P\ xs} should be true iff \isa{P\ x} holds |
|
13 for every element \isa{x} of \isa{xs}, and \isa{exs\ P\ xs} |
|
14 should be true iff \isa{P\ x} holds for some element \isa{x} of |
|
15 \isa{xs}.% |
|
16 \end{isamarkuptext}% |
|
17 \isamarkuptrue% |
|
18 \isacommand{consts}\ \isanewline |
|
19 \ \ alls\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
|
20 \ \ exs\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isamarkupfalse% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 Prove or disprove (by counter example) the following theorems. |
|
24 You may have to prove some lemmas first. |
|
25 |
|
26 Use the \isa{{\isacharbrackleft}simp{\isacharbrackright}}-attribute only if the equation is truly a |
|
27 simplification and is necessary for some later proof.% |
|
28 \end{isamarkuptext}% |
|
29 \isamarkuptrue% |
|
30 \isacommand{lemma}\ {\isachardoublequote}alls\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\ xs\ {\isacharequal}\ {\isacharparenleft}alls\ P\ xs\ {\isasymand}\ alls\ Q\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
31 \isanewline |
|
32 \isamarkupfalse% |
|
33 \isacommand{lemma}\ {\isachardoublequote}alls\ P\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ alls\ P\ xs{\isachardoublequote}\isamarkupfalse% |
|
34 \isanewline |
|
35 \isamarkupfalse% |
|
36 \isacommand{lemma}\ {\isachardoublequote}exs\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\ xs\ {\isacharequal}\ {\isacharparenleft}exs\ P\ xs\ {\isasymand}\ exs\ Q\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
37 \isanewline |
|
38 \isamarkupfalse% |
|
39 \isacommand{lemma}\ {\isachardoublequote}exs\ P\ {\isacharparenleft}map\ f\ xs{\isacharparenright}\ {\isacharequal}\ exs\ {\isacharparenleft}P\ o\ f{\isacharparenright}\ xs{\isachardoublequote}\isamarkupfalse% |
|
40 \isanewline |
|
41 \isamarkupfalse% |
|
42 \isacommand{lemma}\ {\isachardoublequote}exs\ P\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ exs\ P\ xs{\isachardoublequote}\isamarkupfalse% |
|
43 \isamarkupfalse% |
|
44 % |
|
45 \begin{isamarkuptext}% |
|
46 Find a term \isa{Z} such that the following equation holds:% |
|
47 \end{isamarkuptext}% |
|
48 \isamarkuptrue% |
|
49 \isacommand{lemma}\ {\isachardoublequote}exs\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P\ x\ {\isasymor}\ Q\ x{\isacharparenright}\ xs\ {\isacharequal}\ Z{\isachardoublequote}\isamarkupfalse% |
|
50 \isamarkupfalse% |
|
51 % |
|
52 \begin{isamarkuptext}% |
|
53 Express the existential via the universal quantifier --- |
|
54 \isa{exs} should not occur on the right-hand side:% |
|
55 \end{isamarkuptext}% |
|
56 \isamarkuptrue% |
|
57 \isacommand{lemma}\ {\isachardoublequote}exs\ P\ xs\ {\isacharequal}\ Z{\isachardoublequote}\isamarkupfalse% |
|
58 \isamarkupfalse% |
|
59 % |
|
60 \begin{isamarkuptext}% |
|
61 Define a function \isa{is{\isacharunderscore}in\ x\ xs} that checks if \isa{x} occurs in |
|
62 \isa{xs}. Now express \isa{is{\isacharunderscore}in} via \isa{exs}:% |
|
63 \end{isamarkuptext}% |
|
64 \isamarkuptrue% |
|
65 \isacommand{lemma}\ {\isachardoublequote}is{\isacharunderscore}in\ a\ xs\ {\isacharequal}\ Z{\isachardoublequote}\isamarkupfalse% |
|
66 \isamarkupfalse% |
|
67 % |
|
68 \begin{isamarkuptext}% |
|
69 Define a function \isa{nodups\ xs} that is true iff |
|
70 \isa{xs} does not contain duplicates, and a function \isa{deldups\ xs} that removes all duplicates. Note that \isa{deldups\ {\isacharbrackleft}x{\isacharcomma}\ y{\isacharcomma}\ x{\isacharbrackright}} |
|
71 (where \isa{x} and \isa{y} are distinct) can be either |
|
72 \isa{{\isacharbrackleft}x{\isacharcomma}\ y{\isacharbrackright}} or \isa{{\isacharbrackleft}y{\isacharcomma}\ x{\isacharbrackright}}. |
|
73 |
|
74 Prove or disprove (by counter example) the following theorems.% |
|
75 \end{isamarkuptext}% |
|
76 \isamarkuptrue% |
|
77 \isacommand{lemma}\ {\isachardoublequote}length\ {\isacharparenleft}deldups\ xs{\isacharparenright}\ {\isacharless}{\isacharequal}\ length\ xs{\isachardoublequote}\isamarkupfalse% |
|
78 \isanewline |
|
79 \isamarkupfalse% |
|
80 \isacommand{lemma}\ {\isachardoublequote}nodups\ {\isacharparenleft}deldups\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
81 \isanewline |
|
82 \isamarkupfalse% |
|
83 \isacommand{lemma}\ {\isachardoublequote}deldups\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ {\isacharparenleft}deldups\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
84 \isamarkupfalse% |
|
85 \isamarkupfalse% |
|
86 \end{isabellebody}% |
|
87 %%% Local Variables: |
|
88 %%% mode: latex |
|
89 %%% TeX-master: "root" |
|
90 %%% End: |
|