|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{a{\isadigit{4}}}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{Natural Deduction -- Predicate Logic; Sets as Lists% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \isamarkupsubsubsection{Predicate Logic Formulae% |
|
11 } |
|
12 \isamarkuptrue% |
|
13 % |
|
14 \begin{isamarkuptext}% |
|
15 We are again talking about proofs in the calculus of Natural |
|
16 Deduction. In addition to the rules of section~\ref{psv0304a3}, you may now also use |
|
17 |
|
18 |
|
19 \isa{exI{\isacharcolon}}~\isa{P\ x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ P\ x}\\ |
|
20 \isa{exE{\isacharcolon}}~\isa{{\isasymlbrakk}{\isasymexists}x{\isachardot}\ P\ x{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q}\\ |
|
21 \isa{allI{\isacharcolon}}~\isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ P\ x}\\ |
|
22 \isa{allE{\isacharcolon}}~\isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x{\isacharsemicolon}\ P\ x\ {\isasymLongrightarrow}\ R{\isasymrbrakk}\ {\isasymLongrightarrow}\ R}\\ |
|
23 |
|
24 Give a proof of the following propositions or an argument why the formula is not valid:% |
|
25 \end{isamarkuptext}% |
|
26 \isamarkuptrue% |
|
27 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ P\ x\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
28 \isanewline |
|
29 \isamarkupfalse% |
|
30 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymlongrightarrow}\ Q{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
31 \isanewline |
|
32 \isamarkupfalse% |
|
33 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}{\isasymforall}\ x{\isachardot}\ P\ x{\isacharparenright}\ \ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ x{\isachardot}\ Q\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}\ x{\isachardot}\ {\isacharparenleft}P\ x\ {\isasymand}\ Q\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
34 \isanewline |
|
35 \isamarkupfalse% |
|
36 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}{\isasymforall}\ x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymforall}\ x{\isachardot}\ Q\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}\ x{\isachardot}\ {\isacharparenleft}P\ x\ {\isasymor}\ Q\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
37 \isanewline |
|
38 \isamarkupfalse% |
|
39 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}{\isasymexists}\ x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}\ x{\isachardot}\ Q\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}\ x{\isachardot}\ {\isacharparenleft}P\ x\ {\isasymor}\ Q\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
40 \isanewline |
|
41 \isamarkupfalse% |
|
42 \isacommand{lemma}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ {\isacharparenleft}P\ x\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
43 \isamarkupfalse% |
|
44 % |
|
45 \isamarkupsubsubsection{Sets as Lists% |
|
46 } |
|
47 \isamarkuptrue% |
|
48 % |
|
49 \begin{isamarkuptext}% |
|
50 Finite sets can obviously be implemented by lists. In the |
|
51 following, you will be asked to implement the set operations union, |
|
52 intersection and difference and to show that these implementations are |
|
53 correct. Thus, for a function% |
|
54 \end{isamarkuptext}% |
|
55 \isamarkuptrue% |
|
56 \ \ list{\isacharunderscore}union\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a\ list{\isacharcomma}\ {\isacharprime}a\ list{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse% |
|
57 % |
|
58 \begin{isamarkuptext}% |
|
59 to be defined by you it has to be shown that% |
|
60 \end{isamarkuptext}% |
|
61 \isamarkuptrue% |
|
62 \isacommand{lemma}\ {\isachardoublequote}set\ {\isacharparenleft}list{\isacharunderscore}union\ xs\ ys{\isacharparenright}\ {\isacharequal}\ set\ xs\ {\isasymunion}\ set\ ys{\isachardoublequote}\isamarkupfalse% |
|
63 \isamarkupfalse% |
|
64 % |
|
65 \begin{isamarkuptext}% |
|
66 In addition, the functions should be space efficient in the |
|
67 sense that one obtains lists without duplicates (\isa{distinct}) |
|
68 whenever the parameters of the functions are duplicate-free. Thus, for |
|
69 example,% |
|
70 \end{isamarkuptext}% |
|
71 \isamarkuptrue% |
|
72 \isacommand{lemma}\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \isanewline |
|
73 \ \ {\isachardoublequote}distinct\ xs\ {\isasymlongrightarrow}\ distinct\ ys\ {\isasymlongrightarrow}\ {\isacharparenleft}distinct\ {\isacharparenleft}list{\isacharunderscore}union\ xs\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
74 \isamarkupfalse% |
|
75 % |
|
76 \begin{isamarkuptext}% |
|
77 \emph{Hint:} \isa{distinct} is defined in \isa{List{\isachardot}thy}. Also the function \isa{mem} and the lemma \isa{set{\isacharunderscore}mem{\isacharunderscore}eq} may be useful.% |
|
78 \end{isamarkuptext}% |
|
79 \isamarkuptrue% |
|
80 % |
|
81 \isamarkupsubsubsection{Quantification over Sets% |
|
82 } |
|
83 \isamarkuptrue% |
|
84 % |
|
85 \begin{isamarkuptext}% |
|
86 Define a set \isa{S} such that the following proposition holds:% |
|
87 \end{isamarkuptext}% |
|
88 \isamarkuptrue% |
|
89 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}{\isasymforall}\ x\ {\isasymin}\ A{\isachardot}\ P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ x\ {\isasymin}\ B{\isachardot}\ P\ x{\isacharparenright}{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}\ x\ {\isasymin}\ S{\isachardot}\ P\ x{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
90 \isamarkupfalse% |
|
91 % |
|
92 \begin{isamarkuptext}% |
|
93 Define a predicate \isa{P} such that% |
|
94 \end{isamarkuptext}% |
|
95 \isamarkuptrue% |
|
96 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}\ x\ {\isasymin}\ A{\isachardot}\ P\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isasymLongrightarrow}\ \ {\isasymforall}\ y\ {\isasymin}\ f\ {\isacharbackquote}\ A{\isachardot}\ Q\ y{\isachardoublequote}\isamarkupfalse% |
|
97 \isanewline |
|
98 \isanewline |
|
99 \isamarkupfalse% |
|
100 \isanewline |
|
101 \isamarkupfalse% |
|
102 \end{isabellebody}% |
|
103 %%% Local Variables: |
|
104 %%% mode: latex |
|
105 %%% TeX-master: "root" |
|
106 %%% End: |