-
Notifications
You must be signed in to change notification settings - Fork 0
/
cw1q1.thy
88 lines (72 loc) · 2.01 KB
/
cw1q1.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
theory cw1q1
imports Main
begin
lemma 1: "A \<or> A \<longrightarrow> A"
apply(rule impI)
apply(erule disjE)
by assumption
lemma 2: "A \<and> A \<longrightarrow> A"
apply(rule impI)
apply(erule conjE)
by assumption
lemma 3: "(\<not>P \<or> R) \<longrightarrow> (P \<longrightarrow> R)"
apply(rule impI)+
apply(erule disjE)
apply(erule notE)
by assumption
lemma 4: "(\<exists>x. P x \<and> Q x) \<longrightarrow> (\<exists>x. P x) \<and> (\<exists>x. Q x)"
apply(rule impI)
apply(rule conjI)
apply(erule exE)+
apply(erule conjE)+
apply(rule exI)
apply(assumption)
apply(erule exE)
apply(erule conjE)
apply(rule exI)
by assumption
lemma 5: "(\<not>(\<exists>x. \<not>P x) \<or> R) \<longrightarrow> ((\<exists>x. \<not>P x) \<longrightarrow> R)"
apply(rule impI)+
apply(erule disjE)
apply(erule exE)
apply(erule notE)
apply(rule exI)
apply(rule notI)
apply(erule notE)
apply(assumption)
apply(erule exE)
by assumption
lemma 6: "(\<not>(\<exists>x. \<not>P x) \<or> R) \<longrightarrow> ((\<exists>x. \<not>P x) \<longrightarrow> R)"
apply(rule impI)+
apply(erule disjE)
apply(erule exE)
apply(erule notE)
apply(rule exI)
apply(rule notI)
apply(erule notE)
apply(assumption)
apply(erule exE)
by assumption
lemma 7: "(\<forall>x. P x) \<longrightarrow> \<not>(\<exists>x. \<not>P x)"
apply(rule impI)
apply(rule notI)
apply(erule exE)
apply(erule allE)
apply(erule notE)
by assumption
lemma 8: "P \<or> \<not>P"
apply(rule disjCI)
apply(rule ccontr)
apply(erule notE)
by assumption
lemma 9: "\<not>\<not>P \<longrightarrow> P"
apply(rule impI)
apply(rule mp)
apply(rule impI)
apply auto
sorry
lemma 10: "(\<not>P \<longrightarrow> P) \<longrightarrow> P"
lemma 11: "(\<not>P \<longrightarrow> False)\<longrightarrow>P"
lemma 12: "(\<not>(\<forall>x. P x \<or> R x)) = (\<exists>x. \<not>P x \<and> \<not>R x)"
lemma 13: "(\<exists>x. P x \<or> R x) = (\<not>((\<forall>x. \<not>P x) \<and> \<not>(\<exists>x. R x)))"
end