my forest
isa: all examples forested for lec1
+471
-247
trees/isa-0001.tree
trees/isa/isa-0001.tree
trees/isa-0001.tree
trees/isa/isa-0001.tree
-247
trees/isa-0002.tree
-247
trees/isa-0002.tree
···
1
-
\date{2025-11-25}
2
-
\author{liamoc}
3
-
\title{Building up HOL}
4
-
\taxon{Lecture}
5
-
\import{shiki-macros}
6
-
\put\shiki/language{Isabelle Theory}
7
-
8
-
\transclude{isa-0003}
9
-
10
-
\shiki{theory ND
11
-
imports Pure
12
-
begin
13
-
14
-
typedecl bool
15
-
judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5)
16
-
}
17
-
18
-
\transclude{isa-0005}
19
-
\transclude{isa-0004}
20
-
\transclude{isa-0006}
21
-
\transclude{isa-0007}
22
-
\transclude{isa-0008}
23
-
24
-
25
-
\shiki{
26
-
lemma conjE : ‹⟦ A ∧ B ; ⟦ A ; B ⟧ ⟹ C ⟧ ⟹ C›
27
-
apply (frule conjunct1)
28
-
apply (drule conjunct2)
29
-
apply (assumption)
30
-
done
31
-
32
-
lemma impE: ‹⟦ P ⟶ Q; P ; Q ⟹ R ⟧ ⟹ R›
33
-
apply (drule mp)
34
-
apply assumption
35
-
apply assumption
36
-
done}
37
-
38
-
\transclude{isa-0009}
39
-
\transclude{isa-000A}
40
-
\transclude{isa-000B}
41
-
\shiki{
42
-
axiomatization where
43
-
classical: ‹⟦ ¬ P ⟹ P ⟧ ⟹ P›
44
-
45
-
lemma ccontr: "⟦ ¬ P ⟹ False ⟧ ⟹ P"
46
-
apply (rule classical)
47
-
apply (rule FalseE)
48
-
by (assumption)
49
-
50
-
lemma ‹¬ ¬ X ⟶ X›
51
-
apply (rule impI)
52
-
apply (rule ccontr)
53
-
apply (erule notE)
54
-
apply assumption
55
-
done
56
-
57
-
lemma dm1: ‹¬ (A ∧ B) ⟶ ¬ A ∨ ¬ B›
58
-
apply (rule impI)
59
-
apply (rule ccontr)
60
-
apply (erule notE)
61
-
apply (rule conjI)
62
-
apply (rule ccontr)
63
-
apply (erule notE)
64
-
apply (rule disjI1)
65
-
apply assumption
66
-
apply (rule ccontr)
67
-
apply (erule notE)
68
-
apply (rule disjI2)
69
-
apply assumption
70
-
done
71
-
72
-
lemma ‹¬ (A ⟶ B) ⟶ A›
73
-
apply (rule impI)
74
-
apply (rule ccontr)
75
-
apply (erule notE)
76
-
apply (rule impI)
77
-
apply (erule notE)
78
-
apply assumption
79
-
done
80
-
81
-
lemma ‹¬ A ∧ ¬ B ⟶ ¬ (A ∨ B)›
82
-
apply (rule impI)
83
-
apply (erule conjE)
84
-
apply (rule notI)
85
-
apply (erule disjE)
86
-
apply (erule notE, assumption)
87
-
apply (erule notE, assumption)
88
-
done
89
-
90
-
lemma ‹¬ (A ∨ B) ⟶ ¬ A ∧ ¬ B›
91
-
apply (rule impI)
92
-
apply (rule conjI)
93
-
apply (rule notI)
94
-
apply (erule notE)
95
-
apply (rule disjI1)
96
-
apply (assumption)
97
-
apply (rule notI)
98
-
apply (erule notE)
99
-
apply (rule disjI2)
100
-
apply (assumption)
101
-
done
102
-
103
-
lemma ‹(A ⟶ B) ⟶ ((B ⟶ C) ⟶ A) ⟶ B›
104
-
apply (intro impI)
105
-
apply (rule ccontr)
106
-
apply (erule impE)
107
-
apply (drule mp)
108
-
apply (rule impI)
109
-
apply (erule notE)
110
-
apply assumption
111
-
apply assumption
112
-
apply (erule notE)
113
-
apply assumption
114
-
done
115
-
116
-
axiomatization
117
-
All :: ‹('a ⇒ bool) ⇒ bool› (binder "∀" 10) and
118
-
Ex :: ‹('a ⇒ bool) ⇒ bool› (binder "∃" 10)
119
-
where
120
-
allI : ‹⟦ ⋀x. P x ⟧ ⟹ ∀ x. P x› and
121
-
spec : ‹∀ a. P a ⟹ P x› and
122
-
exI : ‹⟦ P x ⟧ ⟹ ∃a. P a› and
123
-
exE : ‹⟦ ∃ x. P x ; ⋀a. P a ⟹ R ⟧ ⟹ R›
124
-
125
-
lemma allE : ‹⟦ ∀a. P a; P x ⟹ R ⟧ ⟹ R›
126
-
apply (drule_tac x = x in spec)
127
-
apply assumption
128
-
done
129
-
130
-
lemma ‹∀x. ¬ P x ⟹ ¬ (∃x. P x)›
131
-
apply (rule notI)
132
-
apply (erule exE)
133
-
apply (erule_tac x = a in allE)
134
-
apply (erule notE)
135
-
apply assumption
136
-
done
137
-
138
-
139
-
lemma foobl: ‹¬ (∃x. P x) ⟹ ∀x. ¬ P x›
140
-
apply (intro allI notI)
141
-
apply (erule notE)
142
-
apply (rule exI)
143
-
apply assumption
144
-
done
145
-
146
-
lemma ‹∃ x y. P x y ⟹ ∃ y x. P x y›
147
-
apply (elim exE)
148
-
apply (intro exI)
149
-
apply assumption
150
-
done
151
-
152
-
lemma ‹∃ x. P x ⟶ Q ⟹ (∀ x. P x) ⟶ Q›
153
-
apply (intro impI)
154
-
apply (elim exE)
155
-
apply (drule_tac x = a in spec)
156
-
apply (drule mp, assumption)
157
-
apply assumption
158
-
done
159
-
160
-
161
-
lemma ‹(∀ x. P x) ⟶ Q ⟹ ∃ x. P x ⟶ Q›
162
-
apply (rule ccontr)
163
-
apply (elim impE)
164
-
apply (intro allI)
165
-
apply (rule ccontr)
166
-
apply (erule notE)
167
-
apply (rule_tac x = x in exI)
168
-
apply (rule impI)
169
-
apply (erule notE)
170
-
apply assumption
171
-
apply (erule notE)
172
-
apply (intro exI)
173
-
apply (rule impI)
174
-
apply assumption
175
-
done
176
-
177
-
lemma ‹(∀ x. P x) ⟶ (∃ x. Q x) ⟹ ∃ x. P x ⟶ Q x›
178
-
apply (rule ccontr)
179
-
apply (elim impE)
180
-
apply (intro allI)
181
-
apply (rule ccontr)
182
-
apply (erule notE)
183
-
apply (rule_tac x = x in exI)
184
-
apply (rule impI)
185
-
apply (erule notE)
186
-
apply assumption
187
-
apply (erule notE)
188
-
apply (erule exE)
189
-
apply (intro exI)
190
-
apply (rule impI)
191
-
apply assumption
192
-
done
193
-
194
-
195
-
lemma ‹ ∃ x. P x ⟶ Q x ⟹ (∀ x. P x) ⟶ (∃ x. Q x)›
196
-
apply (rule impI)
197
-
apply (elim exE)
198
-
apply (drule_tac x = a in spec)
199
-
apply (drule mp, assumption)
200
-
apply (rule exI)
201
-
apply assumption
202
-
done
203
-
204
-
lemma ‹∀ x. ¬ R x ⟶ R (M x) ⟹ ∀ x. R x ∨ R (M x)›
205
-
apply (intro allI)
206
-
apply (erule_tac x = x in allE)
207
-
apply (rule ccontr)
208
-
apply (erule impE)
209
-
apply (rule notI)
210
-
apply (erule notE)
211
-
apply (rule disjI1)
212
-
apply assumption
213
-
apply (erule notE)
214
-
apply (rule disjI2)
215
-
apply assumption
216
-
done
217
-
218
-
lemma helper: "¬ A ⟶ B ⟹ A ∨ B"
219
-
apply (rule ccontr)
220
-
apply (erule impE)
221
-
apply (rule notI)
222
-
apply (erule notE)
223
-
apply (rule disjI1)
224
-
apply assumption
225
-
apply (erule notE)
226
-
apply (rule disjI2)
227
-
apply assumption
228
-
done
229
-
230
-
lemma ‹⟦∀ x. ¬ R x ⟶ R (M x); ∃ x. R x ⟧ ⟹ ∃ x. R x ∧ R (M (M x))›
231
-
apply (erule exE)
232
-
apply (frule_tac x = a in allE, assumption)
233
-
apply (drule_tac x = a in spec)
234
-
apply (frule_tac x = "M a" in spec)
235
-
apply (drule_tac x = "M (M a)" in spec)
236
-
apply (drule helper)+
237
-
apply (elim disjE)
238
-
apply (rule_tac x = a in exI; intro conjI; assumption)
239
-
apply (rule_tac x = "M a" in exI; intro conjI; assumption)
240
-
apply (rule_tac x = a in exI; intro conjI; assumption)
241
-
apply (rule_tac x = a in exI; intro conjI; assumption)
242
-
apply (rule_tac x = a in exI; intro conjI; assumption)
243
-
apply (rule_tac x = "M a" in exI; intro conjI; assumption)
244
-
apply (rule_tac x = a in exI; intro conjI; assumption)
245
-
apply (rule_tac x = a in exI; intro conjI; assumption)
246
-
done
247
-
}
trees/isa-0003.tree
trees/isa/isa-0003.tree
trees/isa-0003.tree
trees/isa/isa-0003.tree
trees/isa-0004.tree
trees/isa/isa-0004.tree
trees/isa-0004.tree
trees/isa/isa-0004.tree
trees/isa-0005.tree
trees/isa/isa-0005.tree
trees/isa-0005.tree
trees/isa/isa-0005.tree
trees/isa-0006.tree
trees/isa/isa-0006.tree
trees/isa-0006.tree
trees/isa/isa-0006.tree
trees/isa-0007.tree
trees/isa/isa-0007.tree
trees/isa-0007.tree
trees/isa/isa-0007.tree
trees/isa-0008.tree
trees/isa/isa-0008.tree
trees/isa-0008.tree
trees/isa/isa-0008.tree
trees/isa-0009.tree
trees/isa/isa-0009.tree
trees/isa-0009.tree
trees/isa/isa-0009.tree
trees/isa-000A.tree
trees/isa/isa-000A.tree
trees/isa-000A.tree
trees/isa/isa-000A.tree
trees/isa-000B.tree
trees/isa/isa-000B.tree
trees/isa-000B.tree
trees/isa/isa-000B.tree
+49
trees/isa/isa-0002.tree
+49
trees/isa/isa-0002.tree
···
1
+
\date{2025-11-25}
2
+
\author{liamoc}
3
+
\title{Building up HOL}
4
+
\taxon{Lecture}
5
+
\import{shiki-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
8
+
\transclude{isa-0003}
9
+
10
+
\shiki{theory ND
11
+
imports Pure
12
+
begin
13
+
14
+
typedecl bool
15
+
judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5)
16
+
}
17
+
18
+
\transclude{isa-0005}
19
+
\transclude{isa-000C}
20
+
\transclude{isa-0004}
21
+
\transclude{isa-0006}
22
+
\transclude{isa-000D}
23
+
\transclude{isa-0007}
24
+
\transclude{isa-0008}
25
+
\transclude{isa-0009}
26
+
\transclude{isa-000A}
27
+
\transclude{isa-000M}
28
+
\transclude{isa-000B}
29
+
30
+
\transclude{isa-000E}
31
+
\transclude{isa-000F}
32
+
\transclude{isa-000G}
33
+
\transclude{isa-000H}
34
+
\transclude{isa-000I}
35
+
\transclude{isa-000J}
36
+
\transclude{isa-000K}
37
+
\transclude{isa-000L}
38
+
\transclude{isa-000N}
39
+
\transclude{isa-000P}
40
+
\transclude{isa-000O}
41
+
\transclude{isa-000Q}
42
+
\transclude{isa-000R}
43
+
\transclude{isa-000S}
44
+
\transclude{isa-000T}
45
+
\transclude{isa-000U}
46
+
\transclude{isa-000V}
47
+
\transclude{isa-000W}
48
+
\transclude{isa-000X}
49
+
\transclude{isa-000Y}
+16
trees/isa/isa-000C.tree
+16
trees/isa/isa-000C.tree
···
1
+
\date{2025-11-25T20:51:35Z}
2
+
\taxon{Theorem}
3
+
\title{Conjunction Elimination}
4
+
\author{liamoc}
5
+
\import{shiki-macros}
6
+
\parent{isa-0002}
7
+
\import{dt-macros}
8
+
\put\shiki/language{Isabelle Theory}
9
+
10
+
\shiki{lemma conjE : ‹⟦ A ∧ B ; ⟦ A ; B ⟧ ⟹ C ⟧ ⟹ C›}
11
+
12
+
\solnblock{\shiki{apply (rule impI)
13
+
apply (frule conjunct1)
14
+
apply (drule conjunct2)
15
+
apply (assumption)
16
+
done}}
+15
trees/isa/isa-000D.tree
+15
trees/isa/isa-000D.tree
···
1
+
\date{2025-11-25T20:51:35Z}
2
+
\taxon{Theorem}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\title{Implication Elimination}
8
+
\put\shiki/language{Isabelle Theory}
9
+
10
+
\shiki{lemma impE: ‹⟦ P ⟶ Q; P ; Q ⟹ R ⟧ ⟹ R›}
11
+
12
+
\solnblock{\shiki{apply (drule mp)
13
+
apply assumption
14
+
apply assumption
15
+
done}}
+12
trees/isa/isa-000E.tree
+12
trees/isa/isa-000E.tree
···
1
+
\date{2025-11-27T03:45:51Z}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\title{Classical Axiom}
8
+
\put\shiki/language{Isabelle Theory}
9
+
10
+
##{\dfrac{\begin{array}{c}\neg P \\ \vdots \\ P \end{array}}{P}}
11
+
\shiki{axiomatization where
12
+
classical: ‹⟦ ¬ P ⟹ P ⟧ ⟹ P›}
+13
trees/isa/isa-000F.tree
+13
trees/isa/isa-000F.tree
···
1
+
\date{2025-11-27T03:45:51Z}
2
+
\taxon{Theorem}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\title{Proof by Contradiction}
8
+
\put\shiki/language{Isabelle Theory}
9
+
10
+
\shiki{lemma ccontr: "⟦ ¬ P ⟹ False ⟧ ⟹ P"}
11
+
\solnblock{\shiki{apply (rule classical)
12
+
apply (rule FalseE)
13
+
by (assumption)}}
+15
trees/isa/isa-000G.tree
+15
trees/isa/isa-000G.tree
···
1
+
\date{2025-11-27T04:03:58Z}
2
+
\taxon{Example}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹¬ ¬ X ⟶ X›}
10
+
11
+
\solnblock{\shiki{apply (rule impI)
12
+
apply (rule ccontr)
13
+
apply (erule notE)
14
+
apply assumption
15
+
done}}
+17
trees/isa/isa-000H.tree
+17
trees/isa/isa-000H.tree
···
1
+
\date{2025-11-27T04:03:58Z}
2
+
\taxon{Example}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹¬ (A ⟶ B) ⟶ A›}
10
+
11
+
\solnblock{\shiki{apply (rule impI)
12
+
apply (rule ccontr)
13
+
apply (erule notE)
14
+
apply (rule impI)
15
+
apply (erule notE)
16
+
apply assumption
17
+
done}}
+23
trees/isa/isa-000I.tree
+23
trees/isa/isa-000I.tree
···
1
+
\date{2025-11-27T04:03:58Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹¬ (A ∧ B) ⟶ ¬ A ∨ ¬ B›}
10
+
11
+
\solnblock{\shiki{apply (rule impI)
12
+
apply (rule ccontr)
13
+
apply (erule notE)
14
+
apply (rule conjI)
15
+
apply (rule ccontr)
16
+
apply (erule notE)
17
+
apply (rule disjI1)
18
+
apply assumption
19
+
apply (rule ccontr)
20
+
apply (erule notE)
21
+
apply (rule disjI2)
22
+
apply assumption
23
+
done}}
+17
trees/isa/isa-000J.tree
+17
trees/isa/isa-000J.tree
···
1
+
\date{2025-11-27T04:03:58Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹¬ A ∧ ¬ B ⟶ ¬ (A ∨ B)›}
10
+
11
+
\solnblock{\shiki{apply (rule impI)
12
+
apply (erule conjE)
13
+
apply (rule notI)
14
+
apply (erule disjE)
15
+
apply (erule notE, assumption)
16
+
apply (erule notE, assumption)
17
+
done}}
+21
trees/isa/isa-000K.tree
+21
trees/isa/isa-000K.tree
···
1
+
\date{2025-11-27T04:03:58Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹¬ (A ∨ B) ⟶ ¬ A ∧ ¬ B›}
10
+
11
+
\solnblock{\shiki{apply (rule impI)
12
+
apply (rule conjI)
13
+
apply (rule notI)
14
+
apply (erule notE)
15
+
apply (rule disjI1)
16
+
apply (assumption)
17
+
apply (rule notI)
18
+
apply (erule notE)
19
+
apply (rule disjI2)
20
+
apply (assumption)
21
+
done}}
+21
trees/isa/isa-000L.tree
+21
trees/isa/isa-000L.tree
···
1
+
\date{2025-11-27T04:03:58Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹(A ⟶ B) ⟶ ((B ⟶ C) ⟶ A) ⟶ B›}
10
+
11
+
\solnblock{\shiki{apply (intro impI)
12
+
apply (rule ccontr)
13
+
apply (erule impE)
14
+
apply (drule mp)
15
+
apply (rule impI)
16
+
apply (erule notE)
17
+
apply assumption
18
+
apply assumption
19
+
apply (erule notE)
20
+
apply assumption
21
+
done}}
+20
trees/isa/isa-000M.tree
+20
trees/isa/isa-000M.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Example}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma imp_as_disj: "¬ A ⟶ B ⟹ A ∨ B" }
10
+
11
+
\solnblock{\shiki{apply (rule ccontr)
12
+
apply (erule impE)
13
+
apply (rule notI)
14
+
apply (erule notE)
15
+
apply (rule disjI1)
16
+
apply assumption
17
+
apply (erule notE)
18
+
apply (rule disjI2)
19
+
apply assumption
20
+
done}}
+14
trees/isa/isa-000N.tree
+14
trees/isa/isa-000N.tree
···
1
+
\date{2025-11-25T20:14:40Z}
2
+
\author{liamoc}
3
+
\title{Universal Quantifiers}
4
+
\taxon{Definition}
5
+
\parent{isa-0002}
6
+
\import{shiki-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{axiomatization
10
+
All :: ‹('a ⇒ bool) ⇒ bool› (binder "∀" 10)
11
+
where
12
+
allI : ‹⟦ ⋀x. P x ⟧ ⟹ ∀ x. P x› and
13
+
spec : ‹∀ a. P a ⟹ P x›
14
+
}
+14
trees/isa/isa-000O.tree
+14
trees/isa/isa-000O.tree
···
1
+
\date{2025-11-25T20:14:40Z}
2
+
\author{liamoc}
3
+
\title{Existential Quantifiers}
4
+
\taxon{Definition}
5
+
\parent{isa-0002}
6
+
\import{shiki-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{axiomatization
10
+
Ex :: ‹('a ⇒ bool) ⇒ bool› (binder "∃" 10)
11
+
where
12
+
exI : ‹⟦ P x ⟧ ⟹ ∃a. P a› and
13
+
exE : ‹⟦ ∃ x. P x ; ⋀a. P a ⟹ R ⟧ ⟹ R›
14
+
}
+15
trees/isa/isa-000P.tree
+15
trees/isa/isa-000P.tree
···
1
+
\date{2025-11-27T05:02:46Z}
2
+
\taxon{Theorem}
3
+
\title{Universal Quantifier Elimination}
4
+
\author{liamoc}
5
+
\import{shiki-macros}
6
+
\parent{isa-0002}
7
+
\import{dt-macros}
8
+
\put\shiki/language{Isabelle Theory}
9
+
10
+
\shiki{lemma allE : ‹⟦ ∀a. P a; P x ⟹ R ⟧ ⟹ R›}
11
+
12
+
\solnblock{\shiki{apply (drule_tac x = x in spec)
13
+
apply assumption
14
+
done}}
15
+
+16
trees/isa/isa-000Q.tree
+16
trees/isa/isa-000Q.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Example}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹∀x. ¬ P x ⟹ ¬ (∃x. P x)›}
10
+
11
+
\solnblock{\shiki{apply (rule notI)
12
+
apply (erule exE)
13
+
apply (erule_tac x = a in allE)
14
+
apply (erule notE)
15
+
apply assumption
16
+
done}}
+15
trees/isa/isa-000R.tree
+15
trees/isa/isa-000R.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Example}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹¬ (∃x. P x) ⟹ ∀x. ¬ P x›}
10
+
11
+
\solnblock{\shiki{apply (intro allI notI)
12
+
apply (erule notE)
13
+
apply (rule exI)
14
+
apply assumption
15
+
done}}
+16
trees/isa/isa-000S.tree
+16
trees/isa/isa-000S.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Example}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹∃ x y. P x y ⟹ ∃ y x. P x y›}
10
+
11
+
\solnblock{\shiki{apply (elim exE)
12
+
apply (intro exI)
13
+
apply assumption
14
+
done}}
15
+
16
+
+18
trees/isa/isa-000T.tree
+18
trees/isa/isa-000T.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹∃ x. P x ⟶ Q ⟹ (∀ x. P x) ⟶ Q›}
10
+
11
+
\solnblock{\shiki{apply (intro impI)
12
+
apply (elim exE)
13
+
apply (drule_tac x = a in spec)
14
+
apply (drule mp, assumption)
15
+
apply assumption
16
+
done}}
17
+
18
+
+26
trees/isa/isa-000U.tree
+26
trees/isa/isa-000U.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹(∀ x. P x) ⟶ Q ⟹ ∃ x. P x ⟶ Q›}
10
+
11
+
\solnblock{\shiki{apply (rule ccontr)
12
+
apply (elim impE)
13
+
apply (intro allI)
14
+
apply (rule ccontr)
15
+
apply (erule notE)
16
+
apply (rule_tac x = x in exI)
17
+
apply (rule impI)
18
+
apply (erule notE)
19
+
apply assumption
20
+
apply (erule notE)
21
+
apply (intro exI)
22
+
apply (rule impI)
23
+
apply assumption
24
+
done}}
25
+
26
+
+27
trees/isa/isa-000V.tree
+27
trees/isa/isa-000V.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹(∀ x. P x) ⟶ (∃ x. Q x) ⟹ ∃ x. P x ⟶ Q x›}
10
+
11
+
\solnblock{\shiki{apply (rule ccontr)
12
+
apply (elim impE)
13
+
apply (intro allI)
14
+
apply (rule ccontr)
15
+
apply (erule notE)
16
+
apply (rule_tac x = x in exI)
17
+
apply (rule impI)
18
+
apply (erule notE)
19
+
apply assumption
20
+
apply (erule notE)
21
+
apply (erule exE)
22
+
apply (intro exI)
23
+
apply (rule impI)
24
+
apply assumption
25
+
done}}
26
+
27
+
+19
trees/isa/isa-000W.tree
+19
trees/isa/isa-000W.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹ ∃ x. P x ⟶ Q x ⟹ (∀ x. P x) ⟶ (∃ x. Q x)›}
10
+
11
+
\solnblock{\shiki{apply (rule impI)
12
+
apply (elim exE)
13
+
apply (drule_tac x = a in spec)
14
+
apply (drule mp, assumption)
15
+
apply (rule exI)
16
+
apply assumption
17
+
done}}
18
+
19
+
+24
trees/isa/isa-000X.tree
+24
trees/isa/isa-000X.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹∀ x. ¬ R x ⟶ R (M x) ⟹ ∀ x. R x ∨ R (M x)›}
10
+
11
+
\solnblock{\shiki{apply (intro allI)
12
+
apply (erule_tac x = x in allE)
13
+
apply (rule ccontr)
14
+
apply (erule impE)
15
+
apply (rule notI)
16
+
apply (erule notE)
17
+
apply (rule disjI1)
18
+
apply assumption
19
+
apply (erule notE)
20
+
apply (rule disjI2)
21
+
apply assumption
22
+
done}}
23
+
24
+
+28
trees/isa/isa-000Y.tree
+28
trees/isa/isa-000Y.tree
···
1
+
\date{2025-11-27T04:46:18Z}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\parent{isa-0002}
6
+
\import{dt-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{lemma ‹⟦∀ x. ¬ R x ⟶ R (M x); ∃ x. R x ⟧ ⟹ ∃ x. R x ∧ R (M (M x))›}
10
+
11
+
\solnblock{\shiki{apply (erule exE)
12
+
apply (frule_tac x = a in allE, assumption)
13
+
apply (drule_tac x = a in spec)
14
+
apply (frule_tac x = "M a" in spec)
15
+
apply (drule_tac x = "M (M a)" in spec)
16
+
apply (drule imp_as_disj)+
17
+
apply (elim disjE)
18
+
apply (rule_tac x = a in exI; intro conjI; assumption)
19
+
apply (rule_tac x = "M a" in exI; intro conjI; assumption)
20
+
apply (rule_tac x = a in exI; intro conjI; assumption)
21
+
apply (rule_tac x = a in exI; intro conjI; assumption)
22
+
apply (rule_tac x = a in exI; intro conjI; assumption)
23
+
apply (rule_tac x = "M a" in exI; intro conjI; assumption)
24
+
apply (rule_tac x = a in exI; intro conjI; assumption)
25
+
apply (rule_tac x = a in exI; intro conjI; assumption)
26
+
done}}
27
+
28
+