author  wenzelm 
Wed, 13 Jun 2007 18:30:11 +0200  
changeset 23373  ead82c82da9e 
parent 21404  eb85850d3eb7 
child 23822  bfb3b1e1d766 
permissions  rwrr 
12360  1 
(* Title: HOL/ex/Higher_Order_Logic.thy 
2 
ID: $Id$ 

3 
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen 

4 
*) 

5 

6 
header {* Foundations of HOL *} 

7 

16417  8 
theory Higher_Order_Logic imports CPure begin 
12360  9 

10 
text {* 

11 
The following theory development demonstrates HigherOrder Logic 

12 
itself, represented directly within the Pure framework of Isabelle. 

13 
The ``HOL'' logic given here is essentially that of Gordon 

14 
\cite{Gordon:1985:HOL}, although we prefer to present basic concepts 

15 
in a slightly more conventional manner oriented towards plain 

16 
Natural Deduction. 

17 
*} 

18 

19 

20 
subsection {* Pure Logic *} 

21 

14854  22 
classes type 
12360  23 
defaultsort type 
24 

25 
typedecl o 

26 
arities 

27 
o :: type 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19736
diff
changeset

28 
"fun" :: (type, type) type 
12360  29 

30 

31 
subsubsection {* Basic logical connectives *} 

32 

33 
judgment 

34 
Trueprop :: "o \<Rightarrow> prop" ("_" 5) 

35 

36 
consts 

37 
imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) 

38 
All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) 

39 

40 
axioms 

41 
impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" 

42 
impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" 

43 
allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" 

44 
allE [dest]: "\<forall>x. P x \<Longrightarrow> P a" 

45 

46 

47 
subsubsection {* Extensional equality *} 

48 

49 
consts 

50 
equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "=" 50) 

51 

52 
axioms 

53 
refl [intro]: "x = x" 

54 
subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y" 

55 
ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" 

56 
iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B" 

57 

12394  58 
theorem sym [sym]: "x = y \<Longrightarrow> y = x" 
12360  59 
proof  
60 
assume "x = y" 

23373  61 
then show "y = x" by (rule subst) (rule refl) 
12360  62 
qed 
63 

64 
lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x" 

65 
by (rule subst) (rule sym) 

66 

67 
lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y" 

68 
by (rule subst) 

69 

70 
theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z" 

71 
by (rule subst) 

72 

73 
theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B" 

74 
by (rule subst) 

75 

76 
theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A" 

77 
by (rule subst) (rule sym) 

78 

79 

80 
subsubsection {* Derived connectives *} 

81 

19736  82 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

83 
false :: o ("\<bottom>") where 
12360  84 
"\<bottom> \<equiv> \<forall>A. A" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

85 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

86 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

87 
true :: o ("\<top>") where 
12360  88 
"\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

89 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

90 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

91 
not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) where 
12360  92 
"not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

93 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

94 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

95 
conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) where 
12360  96 
"conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

97 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

98 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

99 
disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) where 
12360  100 
"disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

101 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

102 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

103 
Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) where 
12360  104 
"Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" 
105 

19380  106 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset

107 
not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50) where 
19380  108 
"x \<noteq> y \<equiv> \<not> (x = y)" 
12360  109 

110 
theorem falseE [elim]: "\<bottom> \<Longrightarrow> A" 

111 
proof (unfold false_def) 

112 
assume "\<forall>A. A" 

23373  113 
then show A .. 
12360  114 
qed 
115 

116 
theorem trueI [intro]: \<top> 

117 
proof (unfold true_def) 

118 
show "\<bottom> \<longrightarrow> \<bottom>" .. 

119 
qed 

120 

121 
theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A" 

122 
proof (unfold not_def) 

123 
assume "A \<Longrightarrow> \<bottom>" 

23373  124 
then show "A \<longrightarrow> \<bottom>" .. 
12360  125 
qed 
126 

127 
theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B" 

128 
proof (unfold not_def) 

129 
assume "A \<longrightarrow> \<bottom>" 

130 
also assume A 

131 
finally have \<bottom> .. 

23373  132 
then show B .. 
12360  133 
qed 
134 

135 
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B" 

136 
by (rule notE) 

137 

138 
lemmas contradiction = notE notE'  {* proof by contradiction in any order *} 

139 

140 
theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" 

141 
proof (unfold conj_def) 

142 
assume A and B 

143 
show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" 

144 
proof 

145 
fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" 

146 
proof 

147 
assume "A \<longrightarrow> B \<longrightarrow> C" 

23373  148 
also note `A` 
149 
also note `B` 

12360  150 
finally show C . 
151 
qed 

152 
qed 

153 
qed 

154 

155 
theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C" 

156 
proof (unfold conj_def) 

157 
assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" 

158 
assume "A \<Longrightarrow> B \<Longrightarrow> C" 

159 
moreover { 

160 
from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" .. 

161 
also have "A \<longrightarrow> B \<longrightarrow> A" 

162 
proof 

163 
assume A 

23373  164 
then show "B \<longrightarrow> A" .. 
12360  165 
qed 
166 
finally have A . 

167 
} moreover { 

168 
from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" .. 

169 
also have "A \<longrightarrow> B \<longrightarrow> B" 

170 
proof 

171 
show "B \<longrightarrow> B" .. 

172 
qed 

173 
finally have B . 

174 
} ultimately show C . 

175 
qed 

176 

177 
theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B" 

178 
proof (unfold disj_def) 

179 
assume A 

180 
show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" 

181 
proof 

182 
fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" 

183 
proof 

184 
assume "A \<longrightarrow> C" 

23373  185 
also note `A` 
12360  186 
finally have C . 
23373  187 
then show "(B \<longrightarrow> C) \<longrightarrow> C" .. 
12360  188 
qed 
189 
qed 

190 
qed 

191 

192 
theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B" 

193 
proof (unfold disj_def) 

194 
assume B 

195 
show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" 

196 
proof 

197 
fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" 

198 
proof 

199 
show "(B \<longrightarrow> C) \<longrightarrow> C" 

200 
proof 

201 
assume "B \<longrightarrow> C" 

23373  202 
also note `B` 
12360  203 
finally show C . 
204 
qed 

205 
qed 

206 
qed 

207 
qed 

208 

209 
theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" 

210 
proof (unfold disj_def) 

211 
assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" 

212 
assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C" 

213 
from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" .. 

214 
also have "A \<longrightarrow> C" 

215 
proof 

23373  216 
assume A then show C by (rule r1) 
12360  217 
qed 
218 
also have "B \<longrightarrow> C" 

219 
proof 

23373  220 
assume B then show C by (rule r2) 
12360  221 
qed 
222 
finally show C . 

223 
qed 

224 

225 
theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" 

226 
proof (unfold Ex_def) 

227 
assume "P a" 

228 
show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" 

229 
proof 

230 
fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" 

231 
proof 

232 
assume "\<forall>x. P x \<longrightarrow> C" 

23373  233 
then have "P a \<longrightarrow> C" .. 
234 
also note `P a` 

12360  235 
finally show C . 
236 
qed 

237 
qed 

238 
qed 

239 

240 
theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C" 

241 
proof (unfold Ex_def) 

242 
assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" 

243 
assume r: "\<And>x. P x \<Longrightarrow> C" 

244 
from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" .. 

245 
also have "\<forall>x. P x \<longrightarrow> C" 

246 
proof 

247 
fix x show "P x \<longrightarrow> C" 

248 
proof 

249 
assume "P x" 

23373  250 
then show C by (rule r) 
12360  251 
qed 
252 
qed 

253 
finally show C . 

254 
qed 

255 

256 

257 
subsection {* Classical logic *} 

258 

259 
locale classical = 

260 
assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A" 

261 

262 
theorem (in classical) 

263 
Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" 

264 
proof 

265 
assume a: "(A \<longrightarrow> B) \<longrightarrow> A" 

266 
show A 

267 
proof (rule classical) 

268 
assume "\<not> A" 

269 
have "A \<longrightarrow> B" 

270 
proof 

271 
assume A 

23373  272 
with `\<not> A` show B by (rule contradiction) 
12360  273 
qed 
274 
with a show A .. 

275 
qed 

276 
qed 

277 

278 
theorem (in classical) 

279 
double_negation: "\<not> \<not> A \<Longrightarrow> A" 

280 
proof  

281 
assume "\<not> \<not> A" 

282 
show A 

283 
proof (rule classical) 

284 
assume "\<not> A" 

23373  285 
with `\<not> \<not> A` show ?thesis by (rule contradiction) 
12360  286 
qed 
287 
qed 

288 

289 
theorem (in classical) 

290 
tertium_non_datur: "A \<or> \<not> A" 

291 
proof (rule double_negation) 

292 
show "\<not> \<not> (A \<or> \<not> A)" 

293 
proof 

294 
assume "\<not> (A \<or> \<not> A)" 

295 
have "\<not> A" 

296 
proof 

23373  297 
assume A then have "A \<or> \<not> A" .. 
298 
with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction) 

12360  299 
qed 
23373  300 
then have "A \<or> \<not> A" .. 
301 
with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction) 

12360  302 
qed 
303 
qed 

304 

305 
theorem (in classical) 

306 
classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C" 

307 
proof  

308 
assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C" 

309 
from tertium_non_datur show C 

310 
proof 

311 
assume A 

23373  312 
then show ?thesis by (rule r1) 
12360  313 
next 
314 
assume "\<not> A" 

23373  315 
then show ?thesis by (rule r2) 
12360  316 
qed 
317 
qed 

318 

12573  319 
lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A" (* FIXME *) 
320 
proof  

321 
assume r: "\<not> A \<Longrightarrow> A" 

322 
show A 

323 
proof (rule classical_cases) 

23373  324 
assume A then show A . 
12573  325 
next 
23373  326 
assume "\<not> A" then show A by (rule r) 
12573  327 
qed 
328 
qed 

329 

12360  330 
end 