author  wenzelm 
Fri, 13 May 2011 22:55:00 +0200  
changeset 42793  88bee9f6eec7 
parent 42477  52fa26b6c524 
child 42795  66fcc9882784 
permissions  rwrr 
9487  1 
(* Title: FOL/FOL.thy 
2 
Author: Lawrence C Paulson and Markus Wenzel 

11678  3 
*) 
9487  4 

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

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

12 
"~~/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

13 
"~~/src/Tools/induct.ML" 
41827  14 
"~~/src/Tools/case_product.ML" 
23154  15 
("simpdata.ML") 
18456  16 
begin 
9487  17 

18 

19 
subsection {* The classical axiom *} 

4093  20 

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

22 
classical: "(~P ==> P) ==> P" 
4093  23 

9487  24 

11678  25 
subsection {* Lemmas and proof tools *} 
9487  26 

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

29 

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

31 

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

33 
apply (rule classical) 

34 
apply (assumption  erule meta_mp  rule disjI1 notI)+ 

35 
apply (erule notE disjI2)+ 

36 
done 

37 

38 
(*introduction rule involving only EX*) 

39 
lemma ex_classical: 

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

41 
shows "EX x. P(x)" 

42 
apply (rule classical) 

43 
apply (rule exI, erule r) 

44 
done 

45 

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

47 
lemma exCI: 

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

49 
shows "EX x. P(x)" 

50 
apply (rule ex_classical) 

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

52 
apply (erule notE) 

53 
apply (erule exI) 

54 
done 

55 

56 
lemma excluded_middle: "~P  P" 

57 
apply (rule disjCI) 

58 
apply assumption 

59 
done 

60 

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

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

64 
shows Q 

65 
apply (rule excluded_middle [THEN disjE]) 

66 
apply (erule r2) 

67 
apply (erule r1) 

68 
done 

69 

70 
ML {* 

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

30549  74 
method_setup case_tac = {* 
75 
Args.goal_spec  Scan.lift Args.name_source >> 

76 
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s)) 

77 
*} "case_tac emulation (dynamic instantiation!)" 

27211  78 

21539  79 

80 
(*** Special elimination rules *) 

81 

82 

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

84 
lemma impCE: 

85 
assumes major: "P>Q" 

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

87 
and r2: "Q ==> R" 

88 
shows R 

89 
apply (rule excluded_middle [THEN disjE]) 

90 
apply (erule r1) 

91 
apply (rule r2) 

92 
apply (erule major [THEN mp]) 

93 
done 

94 

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

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

97 
default: would break old proofs.*) 

98 
lemma impCE': 

99 
assumes major: "P>Q" 

100 
and r1: "Q ==> R" 

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

102 
shows R 

103 
apply (rule excluded_middle [THEN disjE]) 

104 
apply (erule r2) 

105 
apply (rule r1) 

106 
apply (erule major [THEN mp]) 

107 
done 

108 

109 
(*Double negation law*) 

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

111 
apply (rule classical) 

112 
apply (erule notE) 

113 
apply assumption 

114 
done 

115 

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

117 
apply (rule classical) 

118 
apply (drule (1) meta_mp) 

119 
apply (erule (1) notE) 

120 
done 

121 

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

123 

42453  124 
(*Classical <> elimination. Proof substitutes P=Q in 
21539  125 
~P ==> ~Q and P ==> Q *) 
126 
lemma iffCE: 

127 
assumes major: "P<>Q" 

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

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

130 
shows R 

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

132 
apply (elim impCE) 

133 
apply (erule (1) r2) 

134 
apply (erule (1) notE)+ 

135 
apply (erule (1) r1) 

136 
done 

137 

138 

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

140 
lemma alt_ex1E: 

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

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

143 
shows R 

144 
using major 

145 
proof (rule ex1E) 

146 
fix x 

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

148 
assume "P(x)" 

149 
then show R 

150 
proof (rule r) 

151 
{ fix y y' 

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

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

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

155 
} note r' = this 

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

157 
qed 

158 
qed 

9525  159 

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

162 

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

164 
by (rule classical) iprover 

165 

27849  166 

167 
section {* Classical Reasoner *} 

168 

42793  169 
ML {* 
170 
structure Cla = ClassicalFun 

171 
( 

172 
val imp_elim = @{thm imp_elim} 

173 
val not_elim = @{thm notE} 

174 
val swap = @{thm swap} 

175 
val classical = @{thm classical} 

176 
val sizef = size_of_thm 

177 
val hyp_subst_tacs = [hyp_subst_tac] 

178 
); 

179 

180 
ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())"); 

181 

182 
structure Basic_Classical: BASIC_CLASSICAL = Cla; 

183 
open Basic_Classical; 

184 
*} 

185 

10383  186 
setup Cla.setup 
42793  187 

188 
(*Propositional rules*) 

189 
lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI 

190 
and [elim!] = conjE disjE impCE FalseE iffCE 

191 
ML {* val prop_cs = @{claset} *} 

192 

193 
(*Quantifier rules*) 

194 
lemmas [intro!] = allI ex_ex1I 

195 
and [intro] = exI 

196 
and [elim!] = exE alt_ex1E 

197 
and [elim] = allE 

198 
ML {* val FOL_cs = @{claset} *} 

10383  199 

32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

200 
ML {* 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

201 
structure Blast = Blast 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

202 
( 
42477  203 
structure Classical = Cla 
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

204 
val thy = @{theory} 
41310  205 
val equality_name = @{const_name eq} 
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

206 
val not_name = @{const_name Not} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32261
diff
changeset

207 
val notE = @{thm notE} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32261
diff
changeset

208 
val ccontr = @{thm ccontr} 
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

209 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

210 
); 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

211 
val blast_tac = Blast.blast_tac; 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

212 
*} 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

213 

9487  214 
setup Blast.setup 
13550  215 

216 

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

21539  218 
by blast 
20223  219 

220 
(* Elimination of True from asumptions: *) 

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

222 
proof 

223 
assume "True \<Longrightarrow> PROP P" 

224 
from this and TrueI show "PROP P" . 

225 
next 

226 
assume "PROP P" 

227 
then show "PROP P" . 

228 
qed 

9487  229 

21539  230 
lemma uncurry: "P > Q > R ==> P & Q > R" 
231 
by blast 

232 

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

234 
by blast 

235 

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

237 
by blast 

238 

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

240 

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

242 

26286  243 

244 

245 
(*** Classical simplification rules ***) 

246 

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

248 
cases boil down to the same thing.*) 

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

250 

251 

252 
(*** Miniscoping: pushing quantifiers in 

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

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

255 
show that this step can increase proof length! 

256 
***) 

257 

258 
(*existential miniscoping*) 

259 
lemma int_ex_simps: 

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

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

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

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

264 
by iprover+ 

265 

266 
(*classical rules*) 

267 
lemma cla_ex_simps: 

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

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

270 
by blast+ 

271 

272 
lemmas ex_simps = int_ex_simps cla_ex_simps 

273 

274 
(*universal miniscoping*) 

275 
lemma int_all_simps: 

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

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

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

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

280 
by iprover+ 

281 

282 
(*classical rules*) 

283 
lemma cla_all_simps: 

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

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

286 
by blast+ 

287 

288 
lemmas all_simps = int_all_simps cla_all_simps 

289 

290 

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

292 

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

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

295 

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

297 

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

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

300 

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

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

303 

304 

305 
lemmas meta_simps = 

306 
triv_forall_equality (* prunes params *) 

307 
True_implies_equals (* prune asms `True' *) 

308 

309 
lemmas IFOL_simps = 

310 
refl [THEN P_iff_T] conj_simps disj_simps not_simps 

311 
imp_simps iff_simps quant_simps 

312 

313 
lemma notFalseI: "~False" by iprover 

314 

315 
lemma cla_simps_misc: 

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

317 
"P  ~P" 

318 
"~P  P" 

319 
"~ ~ P <> P" 

320 
"(~P > P) <> P" 

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

322 

323 
lemmas cla_simps = 

324 
de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 

325 
not_imp not_all not_ex cases_simp cla_simps_misc 

326 

327 

9487  328 
use "simpdata.ML" 
42455  329 

42459  330 
simproc_setup defined_Ex ("EX x. P(x)") = {* fn _ => Quantifier1.rearrange_ex *} 
331 
simproc_setup defined_All ("ALL x. P(x)") = {* fn _ => Quantifier1.rearrange_all *} 

42455  332 

42453  333 
ML {* 
334 
(*intuitionistic simprules only*) 

335 
val IFOL_ss = 

336 
FOL_basic_ss 

337 
addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps}) 

42455  338 
addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}] 
42453  339 
addcongs [@{thm imp_cong}]; 
340 

341 
(*classical simprules too*) 

342 
val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps}); 

343 
*} 

344 

345 
setup {* Simplifier.map_simpset (K FOL_ss) *} 

42455  346 

9487  347 
setup "Simplifier.method_setup Splitter.split_modifiers" 
348 
setup Splitter.setup 

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

349 
setup clasimp_setup 
18591  350 
setup EqSubst.setup 
15481  351 

352 

14085  353 
subsection {* Other simple lemmas *} 
354 

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

356 
by blast 

357 

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

359 
by blast 

360 

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

362 
by blast 

363 

364 
(** Monotonicity of implications **) 

365 

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

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

368 

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

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

371 

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

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

374 

375 
lemma imp_refl: "P>P" 

376 
by (rule impI, assumption) 

377 

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

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

380 
by blast 

381 

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

383 
by blast 

384 

11678  385 

386 
subsection {* Proof by cases and induction *} 

387 

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

389 

36866  390 
definition "induct_forall(P) == \<forall>x. P(x)" 
391 
definition "induct_implies(A, B) == A \<longrightarrow> B" 

392 
definition "induct_equal(x, y) == x = y" 

393 
definition "induct_conj(A, B) == A \<and> B" 

11678  394 

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

18816  396 
unfolding atomize_all induct_forall_def . 
11678  397 

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

18816  399 
unfolding atomize_imp induct_implies_def . 
11678  400 

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

18816  402 
unfolding atomize_eq induct_equal_def . 
11678  403 

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

404 
lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))" 
18816  405 
unfolding atomize_conj induct_conj_def . 
11988  406 

18456  407 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
408 
lemmas induct_rulify [symmetric, standard] = induct_atomize 

409 
lemmas induct_rulify_fallback = 

410 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11678  411 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
34989
diff
changeset

412 
hide_const induct_forall induct_implies induct_equal induct_conj 
11678  413 

414 

415 
text {* Method setup. *} 

416 

417 
ML {* 

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

419 
( 
22139  420 
val cases_default = @{thm case_split} 
421 
val atomize = @{thms induct_atomize} 

422 
val rulify = @{thms induct_rulify} 

423 
val rulify_fallback = @{thms induct_rulify_fallback} 

34989  424 
val equal_def = @{thm induct_equal_def} 
34914  425 
fun dest_def _ = NONE 
426 
fun trivial_tac _ = no_tac 

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

427 
); 
11678  428 
*} 
429 

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

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

431 
declare case_split [cases type: o] 
11678  432 

41827  433 
setup Case_Product.setup 
434 

41310  435 

436 
hide_const (open) eq 

437 

4854  438 
end 