author  wenzelm 
Sun, 11 Jan 2009 21:49:59 +0100  
changeset 29450  ac7f67be7f1f 
parent 28856  5e009a80fe6d 
child 30549  d2d7874648bd 
permissions  rwrr 
9487  1 
(* Title: FOL/FOL.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Markus Wenzel 

11678  4 
*) 
9487  5 

11678  6 
header {* Classical firstorder logic *} 
4093  7 

18456  8 
theory FOL 
15481  9 
imports IFOL 
23154  10 
uses 
24097  11 
"~~/src/Provers/classical.ML" 
12 
"~~/src/Provers/blast.ML" 

13 
"~~/src/Provers/clasimp.ML" 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24097
diff
changeset

14 
"~~/src/Tools/induct.ML" 
23154  15 
("cladata.ML") 
16 
("blastdata.ML") 

17 
("simpdata.ML") 

18456  18 
begin 
9487  19 

20 

21 
subsection {* The classical axiom *} 

4093  22 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset

23 
axioms 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset

24 
classical: "(~P ==> P) ==> P" 
4093  25 

9487  26 

11678  27 
subsection {* Lemmas and proof tools *} 
9487  28 

21539  29 
lemma ccontr: "(\<not> P \<Longrightarrow> False) \<Longrightarrow> P" 
30 
by (erule FalseE [THEN classical]) 

31 

32 
(*** Classical introduction rules for  and EX ***) 

33 

34 
lemma disjCI: "(~Q ==> P) ==> PQ" 

35 
apply (rule classical) 

36 
apply (assumption  erule meta_mp  rule disjI1 notI)+ 

37 
apply (erule notE disjI2)+ 

38 
done 

39 

40 
(*introduction rule involving only EX*) 

41 
lemma ex_classical: 

42 
assumes r: "~(EX x. P(x)) ==> P(a)" 

43 
shows "EX x. P(x)" 

44 
apply (rule classical) 

45 
apply (rule exI, erule r) 

46 
done 

47 

48 
(*version of above, simplifying ~EX to ALL~ *) 

49 
lemma exCI: 

50 
assumes r: "ALL x. ~P(x) ==> P(a)" 

51 
shows "EX x. P(x)" 

52 
apply (rule ex_classical) 

53 
apply (rule notI [THEN allI, THEN r]) 

54 
apply (erule notE) 

55 
apply (erule exI) 

56 
done 

57 

58 
lemma excluded_middle: "~P  P" 

59 
apply (rule disjCI) 

60 
apply assumption 

61 
done 

62 

27115
0dcafa5c9e3f
eliminated obsolete case_split_thm  use case_split;
wenzelm
parents:
26496
diff
changeset

63 
lemma case_split [case_names True False]: 
21539  64 
assumes r1: "P ==> Q" 
65 
and r2: "~P ==> Q" 

66 
shows Q 

67 
apply (rule excluded_middle [THEN disjE]) 

68 
apply (erule r2) 

69 
apply (erule r1) 

70 
done 

71 

72 
ML {* 

27239  73 
fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split} 
21539  74 
*} 
75 

27211  76 
method_setup case_tac = 
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27849
diff
changeset

77 
{* Method.goal_args_ctxt Args.name_source case_tac *} 
27211  78 
"case_tac emulation (dynamic instantiation!)" 
79 

21539  80 

81 
(*** Special elimination rules *) 

82 

83 

84 
(*Classical implies (>) elimination. *) 

85 
lemma impCE: 

86 
assumes major: "P>Q" 

87 
and r1: "~P ==> R" 

88 
and r2: "Q ==> R" 

89 
shows R 

90 
apply (rule excluded_middle [THEN disjE]) 

91 
apply (erule r1) 

92 
apply (rule r2) 

93 
apply (erule major [THEN mp]) 

94 
done 

95 

96 
(*This version of > elimination works on Q before P. It works best for 

97 
those cases in which P holds "almost everywhere". Can't install as 

98 
default: would break old proofs.*) 

99 
lemma impCE': 

100 
assumes major: "P>Q" 

101 
and r1: "Q ==> R" 

102 
and r2: "~P ==> R" 

103 
shows R 

104 
apply (rule excluded_middle [THEN disjE]) 

105 
apply (erule r2) 

106 
apply (rule r1) 

107 
apply (erule major [THEN mp]) 

108 
done 

109 

110 
(*Double negation law*) 

111 
lemma notnotD: "~~P ==> P" 

112 
apply (rule classical) 

113 
apply (erule notE) 

114 
apply assumption 

115 
done 

116 

117 
lemma contrapos2: "[ Q; ~ P ==> ~ Q ] ==> P" 

118 
apply (rule classical) 

119 
apply (drule (1) meta_mp) 

120 
apply (erule (1) notE) 

121 
done 

122 

123 
(*** Tactics for implication and contradiction ***) 

124 

125 
(*Classical <> elimination. Proof substitutes P=Q in 

126 
~P ==> ~Q and P ==> Q *) 

127 
lemma iffCE: 

128 
assumes major: "P<>Q" 

129 
and r1: "[ P; Q ] ==> R" 

130 
and r2: "[ ~P; ~Q ] ==> R" 

131 
shows R 

132 
apply (rule major [unfolded iff_def, THEN conjE]) 

133 
apply (elim impCE) 

134 
apply (erule (1) r2) 

135 
apply (erule (1) notE)+ 

136 
apply (erule (1) r1) 

137 
done 

138 

139 

140 
(*Better for fast_tac: needs no quantifier duplication!*) 

141 
lemma alt_ex1E: 

142 
assumes major: "EX! x. P(x)" 

143 
and r: "!!x. [ P(x); ALL y y'. P(y) & P(y') > y=y' ] ==> R" 

144 
shows R 

145 
using major 

146 
proof (rule ex1E) 

147 
fix x 

148 
assume * : "\<forall>y. P(y) \<longrightarrow> y = x" 

149 
assume "P(x)" 

150 
then show R 

151 
proof (rule r) 

152 
{ fix y y' 

153 
assume "P(y)" and "P(y')" 

154 
with * have "x = y" and "x = y'" by  (tactic "IntPr.fast_tac 1")+ 

155 
then have "y = y'" by (rule subst) 

156 
} note r' = this 

157 
show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r') 

158 
qed 

159 
qed 

9525  160 

26411  161 
lemma imp_elim: "P > Q ==> (~ R ==> P) ==> (Q ==> R) ==> R" 
162 
by (rule classical) iprover 

163 

164 
lemma swap: "~ P ==> (~ R ==> P) ==> R" 

165 
by (rule classical) iprover 

166 

27849  167 

168 
section {* Classical Reasoner *} 

169 

10383  170 
use "cladata.ML" 
171 
setup Cla.setup 

14156  172 
setup cla_setup 
10383  173 

9487  174 
use "blastdata.ML" 
175 
setup Blast.setup 

13550  176 

177 

178 
lemma ex1_functional: "[ EX! z. P(a,z); P(a,b); P(a,c) ] ==> b = c" 

21539  179 
by blast 
20223  180 

181 
(* Elimination of True from asumptions: *) 

182 
lemma True_implies_equals: "(True ==> PROP P) == PROP P" 

183 
proof 

184 
assume "True \<Longrightarrow> PROP P" 

185 
from this and TrueI show "PROP P" . 

186 
next 

187 
assume "PROP P" 

188 
then show "PROP P" . 

189 
qed 

9487  190 

21539  191 
lemma uncurry: "P > Q > R ==> P & Q > R" 
192 
by blast 

193 

194 
lemma iff_allI: "(!!x. P(x) <> Q(x)) ==> (ALL x. P(x)) <> (ALL x. Q(x))" 

195 
by blast 

196 

197 
lemma iff_exI: "(!!x. P(x) <> Q(x)) ==> (EX x. P(x)) <> (EX x. Q(x))" 

198 
by blast 

199 

200 
lemma all_comm: "(ALL x y. P(x,y)) <> (ALL y x. P(x,y))" by blast 

201 

202 
lemma ex_comm: "(EX x y. P(x,y)) <> (EX y x. P(x,y))" by blast 

203 

26286  204 

205 

206 
(*** Classical simplification rules ***) 

207 

208 
(*Avoids duplication of subgoals after expand_if, when the true and false 

209 
cases boil down to the same thing.*) 

210 
lemma cases_simp: "(P > Q) & (~P > Q) <> Q" by blast 

211 

212 

213 
(*** Miniscoping: pushing quantifiers in 

214 
We do NOT distribute of ALL over &, or dually that of EX over  

215 
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 

216 
show that this step can increase proof length! 

217 
***) 

218 

219 
(*existential miniscoping*) 

220 
lemma int_ex_simps: 

221 
"!!P Q. (EX x. P(x) & Q) <> (EX x. P(x)) & Q" 

222 
"!!P Q. (EX x. P & Q(x)) <> P & (EX x. Q(x))" 

223 
"!!P Q. (EX x. P(x)  Q) <> (EX x. P(x))  Q" 

224 
"!!P Q. (EX x. P  Q(x)) <> P  (EX x. Q(x))" 

225 
by iprover+ 

226 

227 
(*classical rules*) 

228 
lemma cla_ex_simps: 

229 
"!!P Q. (EX x. P(x) > Q) <> (ALL x. P(x)) > Q" 

230 
"!!P Q. (EX x. P > Q(x)) <> P > (EX x. Q(x))" 

231 
by blast+ 

232 

233 
lemmas ex_simps = int_ex_simps cla_ex_simps 

234 

235 
(*universal miniscoping*) 

236 
lemma int_all_simps: 

237 
"!!P Q. (ALL x. P(x) & Q) <> (ALL x. P(x)) & Q" 

238 
"!!P Q. (ALL x. P & Q(x)) <> P & (ALL x. Q(x))" 

239 
"!!P Q. (ALL x. P(x) > Q) <> (EX x. P(x)) > Q" 

240 
"!!P Q. (ALL x. P > Q(x)) <> P > (ALL x. Q(x))" 

241 
by iprover+ 

242 

243 
(*classical rules*) 

244 
lemma cla_all_simps: 

245 
"!!P Q. (ALL x. P(x)  Q) <> (ALL x. P(x))  Q" 

246 
"!!P Q. (ALL x. P  Q(x)) <> P  (ALL x. Q(x))" 

247 
by blast+ 

248 

249 
lemmas all_simps = int_all_simps cla_all_simps 

250 

251 

252 
(*** Named rewrite rules proved for IFOL ***) 

253 

254 
lemma imp_disj1: "(P>Q)  R <> (P>Q  R)" by blast 

255 
lemma imp_disj2: "Q  (P>R) <> (P>Q  R)" by blast 

256 

257 
lemma de_Morgan_conj: "(~(P & Q)) <> (~P  ~Q)" by blast 

258 

259 
lemma not_imp: "~(P > Q) <> (P & ~Q)" by blast 

260 
lemma not_iff: "~(P <> Q) <> (P <> ~Q)" by blast 

261 

262 
lemma not_all: "(~ (ALL x. P(x))) <> (EX x.~P(x))" by blast 

263 
lemma imp_all: "((ALL x. P(x)) > Q) <> (EX x. P(x) > Q)" by blast 

264 

265 

266 
lemmas meta_simps = 

267 
triv_forall_equality (* prunes params *) 

268 
True_implies_equals (* prune asms `True' *) 

269 

270 
lemmas IFOL_simps = 

271 
refl [THEN P_iff_T] conj_simps disj_simps not_simps 

272 
imp_simps iff_simps quant_simps 

273 

274 
lemma notFalseI: "~False" by iprover 

275 

276 
lemma cla_simps_misc: 

277 
"~(P&Q) <> ~P  ~Q" 

278 
"P  ~P" 

279 
"~P  P" 

280 
"~ ~ P <> P" 

281 
"(~P > P) <> P" 

282 
"(~P <> ~Q) <> (P<>Q)" by blast+ 

283 

284 
lemmas cla_simps = 

285 
de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 

286 
not_imp not_all not_ex cases_simp cla_simps_misc 

287 

288 

9487  289 
use "simpdata.ML" 
290 
setup simpsetup 

291 
setup "Simplifier.method_setup Splitter.split_modifiers" 

292 
setup Splitter.setup 

26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26411
diff
changeset

293 
setup clasimp_setup 
18591  294 
setup EqSubst.setup 
15481  295 

296 

14085  297 
subsection {* Other simple lemmas *} 
298 

299 
lemma [simp]: "((P>R) <> (Q>R)) <> ((P<>Q)  R)" 

300 
by blast 

301 

302 
lemma [simp]: "((P>Q) <> (P>R)) <> (P > (Q<>R))" 

303 
by blast 

304 

305 
lemma not_disj_iff_imp: "~P  Q <> (P>Q)" 

306 
by blast 

307 

308 
(** Monotonicity of implications **) 

309 

310 
lemma conj_mono: "[ P1>Q1; P2>Q2 ] ==> (P1&P2) > (Q1&Q2)" 

311 
by fast (*or (IntPr.fast_tac 1)*) 

312 

313 
lemma disj_mono: "[ P1>Q1; P2>Q2 ] ==> (P1P2) > (Q1Q2)" 

314 
by fast (*or (IntPr.fast_tac 1)*) 

315 

316 
lemma imp_mono: "[ Q1>P1; P2>Q2 ] ==> (P1>P2)>(Q1>Q2)" 

317 
by fast (*or (IntPr.fast_tac 1)*) 

318 

319 
lemma imp_refl: "P>P" 

320 
by (rule impI, assumption) 

321 

322 
(*The quantifier monotonicity rules are also intuitionistically valid*) 

323 
lemma ex_mono: "(!!x. P(x) > Q(x)) ==> (EX x. P(x)) > (EX x. Q(x))" 

324 
by blast 

325 

326 
lemma all_mono: "(!!x. P(x) > Q(x)) ==> (ALL x. P(x)) > (ALL x. Q(x))" 

327 
by blast 

328 

11678  329 

330 
subsection {* Proof by cases and induction *} 

331 

332 
text {* Proper handling of nonatomic rule statements. *} 

333 

334 
constdefs 

18456  335 
induct_forall where "induct_forall(P) == \<forall>x. P(x)" 
336 
induct_implies where "induct_implies(A, B) == A \<longrightarrow> B" 

337 
induct_equal where "induct_equal(x, y) == x = y" 

338 
induct_conj where "induct_conj(A, B) == A \<and> B" 

11678  339 

340 
lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))" 

18816  341 
unfolding atomize_all induct_forall_def . 
11678  342 

343 
lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))" 

18816  344 
unfolding atomize_imp induct_implies_def . 
11678  345 

346 
lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))" 

18816  347 
unfolding atomize_eq induct_equal_def . 
11678  348 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

349 
lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))" 
18816  350 
unfolding atomize_conj induct_conj_def . 
11988  351 

18456  352 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
353 
lemmas induct_rulify [symmetric, standard] = induct_atomize 

354 
lemmas induct_rulify_fallback = 

355 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11678  356 

18456  357 
hide const induct_forall induct_implies induct_equal induct_conj 
11678  358 

359 

360 
text {* Method setup. *} 

361 

362 
ML {* 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24097
diff
changeset

363 
structure Induct = InductFun 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24097
diff
changeset

364 
( 
22139  365 
val cases_default = @{thm case_split} 
366 
val atomize = @{thms induct_atomize} 

367 
val rulify = @{thms induct_rulify} 

368 
val rulify_fallback = @{thms induct_rulify_fallback} 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24097
diff
changeset

369 
); 
11678  370 
*} 
371 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24097
diff
changeset

372 
setup Induct.setup 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24097
diff
changeset

373 
declare case_split [cases type: o] 
11678  374 

4854  375 
end 