author  krauss 
Wed, 13 Sep 2006 12:05:50 +0200  
changeset 20523  36a59e5d0039 
parent 19736  d8d0f8f51d69 
child 21404  eb85850d3eb7 
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" 

61 
thus "y = x" by (rule subst) (rule refl) 

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 
12360  83 
false :: o ("\<bottom>") 
84 
"\<bottom> \<equiv> \<forall>A. A" 

85 
true :: o ("\<top>") 

86 
"\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" 

87 
not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) 

88 
"not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>" 

89 
conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) 

90 
"conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" 

91 
disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) 

92 
"disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" 

93 
Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) 

94 
"Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" 

95 

19380  96 
abbreviation 
97 
not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50) 

98 
"x \<noteq> y \<equiv> \<not> (x = y)" 

12360  99 

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

101 
proof (unfold false_def) 

102 
assume "\<forall>A. A" 

103 
thus A .. 

104 
qed 

105 

106 
theorem trueI [intro]: \<top> 

107 
proof (unfold true_def) 

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

109 
qed 

110 

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

112 
proof (unfold not_def) 

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

114 
thus "A \<longrightarrow> \<bottom>" .. 

115 
qed 

116 

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

118 
proof (unfold not_def) 

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

120 
also assume A 

121 
finally have \<bottom> .. 

122 
thus B .. 

123 
qed 

124 

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

126 
by (rule notE) 

127 

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

129 

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

131 
proof (unfold conj_def) 

132 
assume A and B 

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

134 
proof 

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

136 
proof 

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

138 
also have A . 

139 
also have B . 

140 
finally show C . 

141 
qed 

142 
qed 

143 
qed 

144 

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

146 
proof (unfold conj_def) 

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

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

149 
moreover { 

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

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

152 
proof 

153 
assume A 

154 
thus "B \<longrightarrow> A" .. 

155 
qed 

156 
finally have A . 

157 
} moreover { 

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

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

160 
proof 

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

162 
qed 

163 
finally have B . 

164 
} ultimately show C . 

165 
qed 

166 

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

168 
proof (unfold disj_def) 

169 
assume A 

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

171 
proof 

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

173 
proof 

174 
assume "A \<longrightarrow> C" 

175 
also have A . 

176 
finally have C . 

177 
thus "(B \<longrightarrow> C) \<longrightarrow> C" .. 

178 
qed 

179 
qed 

180 
qed 

181 

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

183 
proof (unfold disj_def) 

184 
assume B 

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

186 
proof 

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

188 
proof 

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

190 
proof 

191 
assume "B \<longrightarrow> C" 

192 
also have B . 

193 
finally show C . 

194 
qed 

195 
qed 

196 
qed 

197 
qed 

198 

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

200 
proof (unfold disj_def) 

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

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

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

204 
also have "A \<longrightarrow> C" 

205 
proof 

206 
assume A thus C by (rule r1) 

207 
qed 

208 
also have "B \<longrightarrow> C" 

209 
proof 

210 
assume B thus C by (rule r2) 

211 
qed 

212 
finally show C . 

213 
qed 

214 

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

216 
proof (unfold Ex_def) 

217 
assume "P a" 

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

219 
proof 

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

221 
proof 

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

223 
hence "P a \<longrightarrow> C" .. 

224 
also have "P a" . 

225 
finally show C . 

226 
qed 

227 
qed 

228 
qed 

229 

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

231 
proof (unfold Ex_def) 

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

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

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

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

236 
proof 

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

238 
proof 

239 
assume "P x" 

240 
thus C by (rule r) 

241 
qed 

242 
qed 

243 
finally show C . 

244 
qed 

245 

246 

247 
subsection {* Classical logic *} 

248 

249 
locale classical = 

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

251 

252 
theorem (in classical) 

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

254 
proof 

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

256 
show A 

257 
proof (rule classical) 

258 
assume "\<not> A" 

259 
have "A \<longrightarrow> B" 

260 
proof 

261 
assume A 

262 
thus B by (rule contradiction) 

263 
qed 

264 
with a show A .. 

265 
qed 

266 
qed 

267 

268 
theorem (in classical) 

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

270 
proof  

271 
assume "\<not> \<not> A" 

272 
show A 

273 
proof (rule classical) 

274 
assume "\<not> A" 

275 
thus ?thesis by (rule contradiction) 

276 
qed 

277 
qed 

278 

279 
theorem (in classical) 

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

281 
proof (rule double_negation) 

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

283 
proof 

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

285 
have "\<not> A" 

286 
proof 

287 
assume A hence "A \<or> \<not> A" .. 

288 
thus \<bottom> by (rule contradiction) 

289 
qed 

290 
hence "A \<or> \<not> A" .. 

291 
thus \<bottom> by (rule contradiction) 

292 
qed 

293 
qed 

294 

295 
theorem (in classical) 

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

297 
proof  

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

299 
from tertium_non_datur show C 

300 
proof 

301 
assume A 

302 
thus ?thesis by (rule r1) 

303 
next 

304 
assume "\<not> A" 

305 
thus ?thesis by (rule r2) 

306 
qed 

307 
qed 

308 

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

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

312 
show A 

313 
proof (rule classical_cases) 

314 
assume A thus A . 

315 
next 

316 
assume "\<not> A" thus A by (rule r) 

317 
qed 

318 
qed 

319 

12360  320 
end 