author  wenzelm 
Sat, 09 Jul 2011 21:53:27 +0200  
changeset 43721  fad8634cee62 
parent 43560  d1650e3720fd 
child 45594  d320f2f9f331 
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 >> 

42814  76 
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s)) 
30549  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 {* 
42799  170 
structure Cla = Classical 
42793  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 
structure Basic_Classical: BASIC_CLASSICAL = Cla; 

181 
open Basic_Classical; 

182 
*} 

183 

43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42814
diff
changeset

184 
setup {* 
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42814
diff
changeset

185 
ML_Antiquote.value @{binding claset} 
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42814
diff
changeset

186 
(Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())") 
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42814
diff
changeset

187 
*} 
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42814
diff
changeset

188 

10383  189 
setup Cla.setup 
42793  190 

191 
(*Propositional rules*) 

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

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

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

195 

196 
(*Quantifier rules*) 

197 
lemmas [intro!] = allI ex_ex1I 

198 
and [intro] = exI 

199 
and [elim!] = exE alt_ex1E 

200 
and [elim] = allE 

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

10383  202 

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

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

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

205 
( 
42477  206 
structure Classical = Cla 
42802  207 
val Trueprop_const = dest_Const @{const Trueprop} 
41310  208 
val equality_name = @{const_name eq} 
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

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

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

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

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

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

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

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

216 

9487  217 
setup Blast.setup 
13550  218 

219 

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

21539  221 
by blast 
20223  222 

223 
(* Elimination of True from asumptions: *) 

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

225 
proof 

226 
assume "True \<Longrightarrow> PROP P" 

227 
from this and TrueI show "PROP P" . 

228 
next 

229 
assume "PROP P" 

230 
then show "PROP P" . 

231 
qed 

9487  232 

21539  233 
lemma uncurry: "P > Q > R ==> P & Q > R" 
234 
by blast 

235 

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

237 
by blast 

238 

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

240 
by blast 

241 

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

243 

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

245 

26286  246 

247 

248 
(*** Classical simplification rules ***) 

249 

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

251 
cases boil down to the same thing.*) 

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

253 

254 

255 
(*** Miniscoping: pushing quantifiers in 

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

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

258 
show that this step can increase proof length! 

259 
***) 

260 

261 
(*existential miniscoping*) 

262 
lemma int_ex_simps: 

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

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

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

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

267 
by iprover+ 

268 

269 
(*classical rules*) 

270 
lemma cla_ex_simps: 

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

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

273 
by blast+ 

274 

275 
lemmas ex_simps = int_ex_simps cla_ex_simps 

276 

277 
(*universal miniscoping*) 

278 
lemma int_all_simps: 

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

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

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

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

283 
by iprover+ 

284 

285 
(*classical rules*) 

286 
lemma cla_all_simps: 

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

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

289 
by blast+ 

290 

291 
lemmas all_simps = int_all_simps cla_all_simps 

292 

293 

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

295 

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

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

298 

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

300 

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

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

303 

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

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

306 

307 

308 
lemmas meta_simps = 

309 
triv_forall_equality (* prunes params *) 

310 
True_implies_equals (* prune asms `True' *) 

311 

312 
lemmas IFOL_simps = 

313 
refl [THEN P_iff_T] conj_simps disj_simps not_simps 

314 
imp_simps iff_simps quant_simps 

315 

316 
lemma notFalseI: "~False" by iprover 

317 

318 
lemma cla_simps_misc: 

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

320 
"P  ~P" 

321 
"~P  P" 

322 
"~ ~ P <> P" 

323 
"(~P > P) <> P" 

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

325 

326 
lemmas cla_simps = 

327 
de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 

328 
not_imp not_all not_ex cases_simp cla_simps_misc 

329 

330 

9487  331 
use "simpdata.ML" 
42455  332 

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

42455  335 

42453  336 
ML {* 
337 
(*intuitionistic simprules only*) 

338 
val IFOL_ss = 

339 
FOL_basic_ss 

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

42455  341 
addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}] 
42453  342 
addcongs [@{thm imp_cong}]; 
343 

344 
(*classical simprules too*) 

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

346 
*} 

347 

42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset

348 
setup {* Simplifier.map_simpset_global (K FOL_ss) *} 
42455  349 

9487  350 
setup "Simplifier.method_setup Splitter.split_modifiers" 
351 
setup Splitter.setup 

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

352 
setup clasimp_setup 
18591  353 
setup EqSubst.setup 
15481  354 

355 

14085  356 
subsection {* Other simple lemmas *} 
357 

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

359 
by blast 

360 

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

362 
by blast 

363 

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

365 
by blast 

366 

367 
(** Monotonicity of implications **) 

368 

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

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

371 

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

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

374 

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

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

377 

378 
lemma imp_refl: "P>P" 

379 
by (rule impI, assumption) 

380 

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

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

383 
by blast 

384 

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

386 
by blast 

387 

11678  388 

389 
subsection {* Proof by cases and induction *} 

390 

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

392 

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

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

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

11678  397 

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

18816  399 
unfolding atomize_all induct_forall_def . 
11678  400 

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

18816  402 
unfolding atomize_imp induct_implies_def . 
11678  403 

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

18816  405 
unfolding atomize_eq induct_equal_def . 
11678  406 

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

407 
lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))" 
18816  408 
unfolding atomize_conj induct_conj_def . 
11988  409 

18456  410 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
411 
lemmas induct_rulify [symmetric, standard] = induct_atomize 

412 
lemmas induct_rulify_fallback = 

413 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11678  414 

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

415 
hide_const induct_forall induct_implies induct_equal induct_conj 
11678  416 

417 

418 
text {* Method setup. *} 

419 

420 
ML {* 

32171  421 
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

422 
( 
22139  423 
val cases_default = @{thm case_split} 
424 
val atomize = @{thms induct_atomize} 

425 
val rulify = @{thms induct_rulify} 

426 
val rulify_fallback = @{thms induct_rulify_fallback} 

34989  427 
val equal_def = @{thm induct_equal_def} 
34914  428 
fun dest_def _ = NONE 
429 
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

430 
); 
11678  431 
*} 
432 

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

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

434 
declare case_split [cases type: o] 
11678  435 

41827  436 
setup Case_Product.setup 
437 

41310  438 

439 
hide_const (open) eq 

440 

4854  441 
end 