author  wenzelm 
Thu, 18 Apr 2013 17:07:01 +0200  
changeset 51717  9e7d1c139569 
parent 51687  3d8720271ebf 
child 51798  ad3a241def73 
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 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
45654
diff
changeset

9 
keywords "print_claset" "print_induct_rules" :: diag 
18456  10 
begin 
9487  11 

48891  12 
ML_file "~~/src/Provers/classical.ML" 
13 
ML_file "~~/src/Provers/blast.ML" 

14 
ML_file "~~/src/Provers/clasimp.ML" 

15 
ML_file "~~/src/Tools/induct.ML" 

16 
ML_file "~~/src/Tools/case_product.ML" 

17 

9487  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 

10383  184 
setup Cla.setup 
42793  185 

186 
(*Propositional rules*) 

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

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

51687
3d8720271ebf
discontinued obsolete ML antiquotation @{claset};
wenzelm
parents:
48891
diff
changeset

189 
ML {* val prop_cs = claset_of @{context} *} 
42793  190 

191 
(*Quantifier rules*) 

192 
lemmas [intro!] = allI ex_ex1I 

193 
and [intro] = exI 

194 
and [elim!] = exE alt_ex1E 

195 
and [elim] = allE 

51687
3d8720271ebf
discontinued obsolete ML antiquotation @{claset};
wenzelm
parents:
48891
diff
changeset

196 
ML {* val FOL_cs = claset_of @{context} *} 
10383  197 

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

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

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

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

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

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

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

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

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

209 
val blast_tac = Blast.blast_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 

9487  212 
setup Blast.setup 
13550  213 

214 

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

21539  216 
by blast 
20223  217 

218 
(* Elimination of True from asumptions: *) 

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

220 
proof 

221 
assume "True \<Longrightarrow> PROP P" 

222 
from this and TrueI show "PROP P" . 

223 
next 

224 
assume "PROP P" 

225 
then show "PROP P" . 

226 
qed 

9487  227 

21539  228 
lemma uncurry: "P > Q > R ==> P & Q > R" 
229 
by blast 

230 

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

232 
by blast 

233 

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

235 
by blast 

236 

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

238 

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

240 

26286  241 

242 

243 
(*** Classical simplification rules ***) 

244 

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

246 
cases boil down to the same thing.*) 

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

248 

249 

250 
(*** Miniscoping: pushing quantifiers in 

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

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

253 
show that this step can increase proof length! 

254 
***) 

255 

256 
(*existential miniscoping*) 

257 
lemma int_ex_simps: 

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

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

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 
by iprover+ 

263 

264 
(*classical rules*) 

265 
lemma cla_ex_simps: 

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

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

268 
by blast+ 

269 

270 
lemmas ex_simps = int_ex_simps cla_ex_simps 

271 

272 
(*universal miniscoping*) 

273 
lemma int_all_simps: 

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

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

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

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

278 
by iprover+ 

279 

280 
(*classical rules*) 

281 
lemma cla_all_simps: 

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

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

284 
by blast+ 

285 

286 
lemmas all_simps = int_all_simps cla_all_simps 

287 

288 

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

290 

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

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

293 

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

295 

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

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

298 

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

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

301 

302 

303 
lemmas meta_simps = 

304 
triv_forall_equality (* prunes params *) 

305 
True_implies_equals (* prune asms `True' *) 

306 

307 
lemmas IFOL_simps = 

308 
refl [THEN P_iff_T] conj_simps disj_simps not_simps 

309 
imp_simps iff_simps quant_simps 

310 

311 
lemma notFalseI: "~False" by iprover 

312 

313 
lemma cla_simps_misc: 

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

315 
"P  ~P" 

316 
"~P  P" 

317 
"~ ~ P <> P" 

318 
"(~P > P) <> P" 

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

320 

321 
lemmas cla_simps = 

322 
de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 

323 
not_imp not_all not_ex cases_simp cla_simps_misc 

324 

325 

48891  326 
ML_file "simpdata.ML" 
42455  327 

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

42455  330 

42453  331 
ML {* 
332 
(*intuitionistic simprules only*) 

333 
val IFOL_ss = 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset

334 
put_simpset FOL_basic_ss @{context} 
45654  335 
addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps} 
42455  336 
addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}] 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset

337 
> Simplifier.add_cong @{thm imp_cong} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset

338 
> simpset_of; 
42453  339 

340 
(*classical simprules too*) 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset

341 
val FOL_ss = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset

342 
put_simpset IFOL_ss @{context} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset

343 
addsimps @{thms cla_simps cla_ex_simps cla_all_simps} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset

344 
> simpset_of; 
42453  345 
*} 
346 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset

347 
setup {* map_theory_simpset (put_simpset FOL_ss) *} 
42455  348 

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

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

351 
setup clasimp_setup 
18591  352 
setup EqSubst.setup 
15481  353 

354 

14085  355 
subsection {* Other simple lemmas *} 
356 

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

358 
by blast 

359 

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

361 
by blast 

362 

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

364 
by blast 

365 

366 
(** Monotonicity of implications **) 

367 

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

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

370 

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

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

373 

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

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

376 

377 
lemma imp_refl: "P>P" 

378 
by (rule impI, assumption) 

379 

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

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

382 
by blast 

383 

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

385 
by blast 

386 

11678  387 

388 
subsection {* Proof by cases and induction *} 

389 

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

391 

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

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

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

11678  396 

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

18816  398 
unfolding atomize_all induct_forall_def . 
11678  399 

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

18816  401 
unfolding atomize_imp induct_implies_def . 
11678  402 

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

18816  404 
unfolding atomize_eq induct_equal_def . 
11678  405 

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

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

18456  409 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
45594  410 
lemmas induct_rulify [symmetric] = induct_atomize 
18456  411 
lemmas induct_rulify_fallback = 
412 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11678  413 

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

414 
hide_const induct_forall induct_implies induct_equal induct_conj 
11678  415 

416 

417 
text {* Method setup. *} 

418 

419 
ML {* 

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

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

424 
val rulify = @{thms induct_rulify} 

425 
val rulify_fallback = @{thms induct_rulify_fallback} 

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

429 
); 
11678  430 
*} 
431 

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

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

433 
declare case_split [cases type: o] 
11678  434 

41827  435 
setup Case_Product.setup 
436 

41310  437 

438 
hide_const (open) eq 

439 

4854  440 
end 