-
Notifications
You must be signed in to change notification settings - Fork 0
/
Week3.thy
231 lines (189 loc) · 5.78 KB
/
Week3.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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
theory Week3
imports Main
begin
(*McGee against MP*)
lemma
assumes A
assumes "\<not>B"
assumes "\<not>C"
shows "A \<longrightarrow> B \<longrightarrow> C"
proof (rule impI)
show "B \<longrightarrow> C"
proof (rule impI)
assume B
(* with `\<not>B` show C by (rule notE) *)
then have False using `\<not>B` by blast
from `\<not>C` show C using `False` by blast
qed
qed
lemma
assumes A
assumes "\<not>B"
assumes "\<not>C"
shows "B \<longrightarrow> C"
proof(rule impI)
assume B
with `\<not>B` show C by (rule notE)
qed
(*Conjunction Elimination*)
thm conjE
lemma "A \<and> B \<longrightarrow> A"
proof(rule impI)
assume "A \<and> B"
then show A by (rule conjE)
qed
lemma "A \<and> B \<longrightarrow> B"
proof(rule impI)
assume "A \<and> B"
then show B by (rule conjE)
qed
(* Exercise 2.1 *)
lemma import:"(A \<longrightarrow> B\<longrightarrow> C) \<longrightarrow>((A \<and> B)\<longrightarrow>C)"
proof(rule impI)
assume "(A \<longrightarrow> B\<longrightarrow> C)"
show "(A \<and> B)\<longrightarrow>C"
proof (rule impI)
assume "A \<and> B"
then have A by (rule conjE)
from `A \<longrightarrow> B\<longrightarrow> C` have "B\<longrightarrow> C" using `A` by (rule mp)
from `A \<and> B` have B by (rule conjE)
from `B\<longrightarrow> C` have C using `B` by (rule mp)
thus C.
qed
qed
(*Conjunction Introduction*)
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume "A \<and> B"
then have A by (rule conjE)
from `A \<and> B` have B by (rule conjE)
from `B` show "B \<and> A" using `A` by (rule conjI)
qed
(* Exercise 3.1 *)
lemma export: "((A \<and> B)\<longrightarrow>C)\<longrightarrow> (A \<longrightarrow> B\<longrightarrow> C)"
proof (rule impI)
assume "(A \<and> B)\<longrightarrow>C"
show "A \<longrightarrow> B\<longrightarrow> C"
proof (rule impI)
assume A
show "B\<longrightarrow> C"
proof (rule impI)
assume B
then have "A \<and> B" using `A` by auto (*rule conjI not working*)
from `(A \<and> B)\<longrightarrow>C` show C using `A \<and> B` by (rule mp)
qed
qed
qed
(* Biconditional Introduction *)
print_statement iffI
lemma
assumes "A \<longrightarrow> B"
assumes "B \<longrightarrow> A"
shows "B \<longleftrightarrow> A"
proof (rule iffI)
assume A
with `A \<longrightarrow> B` show B by (rule mp)
next
assume B
with `B \<longrightarrow> A` show A by (rule mp)
qed
(* Exercise 4.1 *)
lemma "A \<longleftrightarrow> A"
proof
qed (* How is this valid ?*)
(* Biconditional Elimination *)
print_statement iffD1
lemma "(A \<longleftrightarrow> B) \<longrightarrow> A \<longrightarrow> B"
proof(rule impI)
assume "A \<longleftrightarrow> B"
show "A \<longrightarrow>B"
proof(rule impI)
assume A
then show B using `A \<longleftrightarrow> B` by blast
qed
qed
lemma "(A \<longleftrightarrow> B) \<longrightarrow> B \<longrightarrow> A"
proof(rule impI)
assume "A \<longleftrightarrow> B"
show "B \<longrightarrow> A"
proof(rule impI)
assume B
with `A \<longleftrightarrow> B` show A by (rule iffD2)
qed
qed
(* Exercise 5.1 *)
lemma "\<not>(A \<longleftrightarrow> \<not>A)"
proof(rule notI) (* alternative *)
assume "A \<longleftrightarrow> \<not>A"
then have A by blast
from `A \<longleftrightarrow> \<not>A` have "\<not>A" by blast
then show False using `A` by blast
qed
(* Exercises *)
lemma import_export: "((A \<and> B) \<longrightarrow> C) \<longleftrightarrow> (A \<longrightarrow> B\<longrightarrow> C)"
proof (rule iffI)
assume "(A \<and> B) \<longrightarrow> C"
then show "A \<longrightarrow> B \<longrightarrow> C" by blast (* rule Week3.export not working *)
next
assume "A \<longrightarrow> B \<longrightarrow> C"
then show "(A \<and> B) \<longrightarrow> C" by blast (* rule Week3.import not working *)
qed
lemma
assumes "(A \<and> B) \<longrightarrow> C"
assumes A
shows "B \<longrightarrow> C"
proof (rule impI)
assume B
then have "A \<and> B" using `A` by blast (* conjI not working *)
(*then show C using `(A \<and> B) \<longrightarrow> C` by blast (* mp not working*)*)
with `(A \<and> B) \<longrightarrow> C` show C by (rule mp)
qed
lemma
assumes A
assumes "\<not>B"
assumes "\<not>C"
shows "(A \<and> B) \<longrightarrow> C"
proof(rule impI)
assume "A \<and> B"
then have B by (rule conjE)
then have False using `\<not>B` by blast
then show C using `\<not>C` by blast
qed
lemma equivalence_left_to_right: "(A \<longrightarrow> B) \<longrightarrow> (\<not> (A \<and> \<not> B))"
proof(rule impI)
assume "A \<longrightarrow> B"
show "\<not>(A \<and> \<not>B)"
proof (rule notI)
assume "A \<and> \<not> B"
then have "\<not>B" by (rule conjE)
from `A \<and> \<not>B` have A by (rule conjE)
then have B using `A \<longrightarrow> B` by blast
then show False using `\<not>B` by blast
qed
qed
lemma equivalence_right_to_left: "\<not>(A \<and> \<not>B) \<longrightarrow> (A \<longrightarrow> B)"
proof (rule impI)
assume "\<not>(A \<and> \<not>B)"
show "A \<longrightarrow> B"
proof (rule impI)
assume A
then show B using `\<not>(A \<and> \<not>B)` by blast
qed
qed
lemma the_equivalence_thesis: "(A \<longrightarrow> B) \<longleftrightarrow> (\<not>(A \<and> \<not> B))"
proof(rule iffI)
assume "A \<longrightarrow> B"
then show "\<not>(A \<and> \<not> B)" by blast
next
assume "\<not>(A \<and> \<not> B)"
then show "A \<longrightarrow> B" by blast
qed
lemma the_equivalence_thesis2: "(A \<longrightarrow> B) \<longleftrightarrow> (\<not>(A \<and> \<not> B))"
proof(rule iffI)
assume "A \<longrightarrow> B"
with Week3.equivalence_left_to_right show "\<not>(A \<and> \<not> B)" by (rule mp)
next
assume "\<not>(A \<and> \<not> B)"
with Week3.equivalence_right_to_left show "A \<longrightarrow> B" by (rule mp)
qed
end