1 |
|
2 (*<*) theory a4 = Main: (*>*) |
|
3 |
|
4 subsection {* Natural Deduction -- Predicate Logic; Sets as Lists *} |
|
5 |
|
6 |
|
7 subsubsection {* Predicate Logic Formulae *} |
|
8 |
|
9 text {* |
|
10 |
|
11 We are again talking about proofs in the calculus of Natural |
|
12 Deduction. In addition to the rules of section~\ref{psv0304a3}, you may now also use |
|
13 |
|
14 |
|
15 @{text "exI:"}~@{thm exI[no_vars]}\\ |
|
16 @{text "exE:"}~@{thm exE[no_vars]}\\ |
|
17 @{text "allI:"}~@{thm allI[no_vars]}\\ |
|
18 @{text "allE:"}~@{thm allE[no_vars]}\\ |
|
19 |
|
20 Give a proof of the following propositions or an argument why the formula is not valid: |
|
21 *} |
|
22 |
|
23 |
|
24 lemma "(\<exists>x. \<forall>y. P x y) \<longrightarrow> (\<forall>y. \<exists>x. P x y)" |
|
25 (*<*) oops (*>*) |
|
26 |
|
27 lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)" |
|
28 (*<*) oops (*>*) |
|
29 |
|
30 lemma "((\<forall> x. P x) \<and> (\<forall> x. Q x)) = (\<forall> x. (P x \<and> Q x))" |
|
31 (*<*) oops (*>*) |
|
32 |
|
33 lemma "((\<forall> x. P x) \<or> (\<forall> x. Q x)) = (\<forall> x. (P x \<or> Q x))" |
|
34 (*<*) oops (*>*) |
|
35 |
|
36 lemma "((\<exists> x. P x) \<or> (\<exists> x. Q x)) = (\<exists> x. (P x \<or> Q x))" |
|
37 (*<*) oops (*>*) |
|
38 |
|
39 lemma "\<exists>x. (P x \<longrightarrow> (\<forall>x. P x))" |
|
40 (*<*) oops (*>*) |
|
41 |
|
42 |
|
43 subsubsection {* Sets as Lists *} |
|
44 |
|
45 text {* Finite sets can obviously be implemented by lists. In the |
|
46 following, you will be asked to implement the set operations union, |
|
47 intersection and difference and to show that these implementations are |
|
48 correct. Thus, for a function *} |
|
49 |
|
50 (*<*) consts (*>*) |
|
51 list_union :: "['a list, 'a list] \<Rightarrow> 'a list" |
|
52 |
|
53 text {* to be defined by you it has to be shown that *} |
|
54 |
|
55 lemma "set (list_union xs ys) = set xs \<union> set ys" |
|
56 (*<*) oops (*>*) |
|
57 |
|
58 |
|
59 text {* In addition, the functions should be space efficient in the |
|
60 sense that one obtains lists without duplicates (@{text "distinct"}) |
|
61 whenever the parameters of the functions are duplicate-free. Thus, for |
|
62 example, *} |
|
63 |
|
64 |
|
65 lemma [rule_format]: |
|
66 "distinct xs \<longrightarrow> distinct ys \<longrightarrow> (distinct (list_union xs ys))" |
|
67 (*<*) oops (*>*) |
|
68 |
|
69 text {* \emph{Hint:} @{text "distinct"} is defined in @{text |
|
70 List.thy}. Also the function @{text mem} and the lemma @{text |
|
71 set_mem_eq} may be useful. *} |
|
72 |
|
73 |
|
74 subsubsection {* Quantification over Sets *} |
|
75 |
|
76 text {* Define a set @{text S} such that the following proposition holds: *} |
|
77 |
|
78 lemma "((\<forall> x \<in> A. P x) \<and> (\<forall> x \<in> B. P x)) \<longrightarrow> (\<forall> x \<in> S. P x)" |
|
79 (*<*) oops (*>*) |
|
80 |
|
81 |
|
82 text {* Define a predicate @{text P} such that *} |
|
83 |
|
84 lemma "\<forall> x \<in> A. P (f x) \<Longrightarrow> \<forall> y \<in> f ` A. Q y" |
|
85 (*<*) oops (*>*) |
|
86 |
|
87 |
|
88 |
|
89 (*<*) end (*>*) |
|
90 |
|