author  wenzelm 
Tue, 31 Mar 2015 22:31:05 +0200  
changeset 59886  e0dc738eb08c 
parent 59780  23b67731f4f0 
child 59940  087d81f5213e 
permissions  rwrr 
9487  1 
(* Title: FOL/FOL.thy 
2 
Author: Lawrence C Paulson and Markus Wenzel 

11678  3 
*) 
9487  4 

58889  5 
section {* 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 

9487  16 

17 
subsection {* The classical axiom *} 

4093  18 

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

20 
classical: "(~P ==> P) ==> P" 
4093  21 

9487  22 

11678  23 
subsection {* Lemmas and proof tools *} 
9487  24 

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

27 

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

29 

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

31 
apply (rule classical) 

32 
apply (assumption  erule meta_mp  rule disjI1 notI)+ 

33 
apply (erule notE disjI2)+ 

34 
done 

35 

36 
(*introduction rule involving only EX*) 

37 
lemma ex_classical: 

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

39 
shows "EX x. P(x)" 

40 
apply (rule classical) 

41 
apply (rule exI, erule r) 

42 
done 

43 

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

45 
lemma exCI: 

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

47 
shows "EX x. P(x)" 

48 
apply (rule ex_classical) 

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

50 
apply (erule notE) 

51 
apply (erule exI) 

52 
done 

53 

54 
lemma excluded_middle: "~P  P" 

55 
apply (rule disjCI) 

56 
apply assumption 

57 
done 

58 

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

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

62 
shows Q 

63 
apply (rule excluded_middle [THEN disjE]) 

64 
apply (erule r2) 

65 
apply (erule r1) 

66 
done 

67 

68 
ML {* 

59780  69 
fun case_tac ctxt a fixes = 
70 
Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split} 

21539  71 
*} 
72 

30549  73 
method_setup case_tac = {* 
59780  74 
Args.goal_spec  Scan.lift (Args.name_inner_syntax  Parse.for_fixes) >> 
75 
(fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes)) 

30549  76 
*} "case_tac emulation (dynamic instantiation!)" 
27211  77 

21539  78 

79 
(*** Special elimination rules *) 

80 

81 

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

83 
lemma impCE: 

84 
assumes major: "P>Q" 

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

86 
and r2: "Q ==> R" 

87 
shows R 

88 
apply (rule excluded_middle [THEN disjE]) 

89 
apply (erule r1) 

90 
apply (rule r2) 

91 
apply (erule major [THEN mp]) 

92 
done 

93 

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

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

96 
default: would break old proofs.*) 

97 
lemma impCE': 

98 
assumes major: "P>Q" 

99 
and r1: "Q ==> R" 

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

101 
shows R 

102 
apply (rule excluded_middle [THEN disjE]) 

103 
apply (erule r2) 

104 
apply (rule r1) 

105 
apply (erule major [THEN mp]) 

106 
done 

107 

108 
(*Double negation law*) 

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

110 
apply (rule classical) 

111 
apply (erule notE) 

112 
apply assumption 

113 
done 

114 

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

116 
apply (rule classical) 

117 
apply (drule (1) meta_mp) 

118 
apply (erule (1) notE) 

119 
done 

120 

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

122 

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

126 
assumes major: "P<>Q" 

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

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

129 
shows R 

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

131 
apply (elim impCE) 

132 
apply (erule (1) r2) 

133 
apply (erule (1) notE)+ 

134 
apply (erule (1) r1) 

135 
done 

136 

137 

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

139 
lemma alt_ex1E: 

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

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

142 
shows R 

143 
using major 

144 
proof (rule ex1E) 

145 
fix x 

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

147 
assume "P(x)" 

148 
then show R 

149 
proof (rule r) 

150 
{ fix y y' 

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

51798  152 
with * have "x = y" and "x = y'" by  (tactic "IntPr.fast_tac @{context} 1")+ 
21539  153 
then have "y = y'" by (rule subst) 
154 
} note r' = this 

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

156 
qed 

157 
qed 

9525  158 

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

161 

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

163 
by (rule classical) iprover 

164 

27849  165 

166 
section {* Classical Reasoner *} 

167 

42793  168 
ML {* 
42799  169 
structure Cla = Classical 
42793  170 
( 
171 
val imp_elim = @{thm imp_elim} 

172 
val not_elim = @{thm notE} 

173 
val swap = @{thm swap} 

174 
val classical = @{thm classical} 

175 
val sizef = size_of_thm 

176 
val hyp_subst_tacs = [hyp_subst_tac] 

177 
); 

178 

179 
structure Basic_Classical: BASIC_CLASSICAL = Cla; 

180 
open Basic_Classical; 

181 
*} 

182 

183 
(*Propositional rules*) 

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

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

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

186 
ML {* val prop_cs = claset_of @{context} *} 
42793  187 

188 
(*Quantifier rules*) 

189 
lemmas [intro!] = allI ex_ex1I 

190 
and [intro] = exI 

191 
and [elim!] = exE alt_ex1E 

192 
and [elim] = allE 

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

193 
ML {* val FOL_cs = claset_of @{context} *} 
10383  194 

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

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

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

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

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

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

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

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

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

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

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

208 

13550  209 

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

21539  211 
by blast 
20223  212 

213 
(* Elimination of True from asumptions: *) 

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

215 
proof 

216 
assume "True \<Longrightarrow> PROP P" 

217 
from this and TrueI show "PROP P" . 

218 
next 

219 
assume "PROP P" 

220 
then show "PROP P" . 

221 
qed 

9487  222 

21539  223 
lemma uncurry: "P > Q > R ==> P & Q > R" 
224 
by blast 

225 

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

227 
by blast 

228 

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

230 
by blast 

231 

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

233 

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

235 

26286  236 

237 

238 
(*** Classical simplification rules ***) 

239 

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

241 
cases boil down to the same thing.*) 

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

243 

244 

245 
(*** Miniscoping: pushing quantifiers in 

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

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

248 
show that this step can increase proof length! 

249 
***) 

250 

251 
(*existential miniscoping*) 

252 
lemma int_ex_simps: 

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

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

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

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

257 
by iprover+ 

258 

259 
(*classical rules*) 

260 
lemma cla_ex_simps: 

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

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

263 
by blast+ 

264 

265 
lemmas ex_simps = int_ex_simps cla_ex_simps 

266 

267 
(*universal miniscoping*) 

268 
lemma int_all_simps: 

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

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

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

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

273 
by iprover+ 

274 

275 
(*classical rules*) 

276 
lemma cla_all_simps: 

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

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

279 
by blast+ 

280 

281 
lemmas all_simps = int_all_simps cla_all_simps 

282 

283 

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

285 

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

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

288 

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

290 

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

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

293 

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

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

296 

297 

298 
lemmas meta_simps = 

299 
triv_forall_equality (* prunes params *) 

300 
True_implies_equals (* prune asms `True' *) 

301 

302 
lemmas IFOL_simps = 

303 
refl [THEN P_iff_T] conj_simps disj_simps not_simps 

304 
imp_simps iff_simps quant_simps 

305 

306 
lemma notFalseI: "~False" by iprover 

307 

308 
lemma cla_simps_misc: 

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

310 
"P  ~P" 

311 
"~P  P" 

312 
"~ ~ P <> P" 

313 
"(~P > P) <> P" 

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

315 

316 
lemmas cla_simps = 

317 
de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 

318 
not_imp not_all not_ex cases_simp cla_simps_misc 

319 

320 

48891  321 
ML_file "simpdata.ML" 
42455  322 

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

42455  325 

42453  326 
ML {* 
327 
(*intuitionistic simprules only*) 

328 
val IFOL_ss = 

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

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

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

333 
> simpset_of; 
42453  334 

335 
(*classical simprules too*) 

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

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

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

338 
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

339 
> simpset_of; 
42453  340 
*} 
341 

58826  342 
setup {* 
343 
map_theory_simpset (put_simpset FOL_ss) #> 

344 
Simplifier.method_setup Splitter.split_modifiers 

345 
*} 

52241  346 

347 
ML_file "~~/src/Tools/eqsubst.ML" 

15481  348 

349 

14085  350 
subsection {* Other simple lemmas *} 
351 

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

353 
by blast 

354 

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

356 
by blast 

357 

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

359 
by blast 

360 

361 
(** Monotonicity of implications **) 

362 

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

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

365 

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

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

368 

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

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

371 

372 
lemma imp_refl: "P>P" 

373 
by (rule impI, assumption) 

374 

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

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

377 
by blast 

378 

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

380 
by blast 

381 

11678  382 

383 
subsection {* Proof by cases and induction *} 

384 

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

386 

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

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

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

11678  391 

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

18816  393 
unfolding atomize_all induct_forall_def . 
11678  394 

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

18816  396 
unfolding atomize_imp induct_implies_def . 
11678  397 

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

18816  399 
unfolding atomize_eq induct_equal_def . 
11678  400 

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

401 
lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))" 
18816  402 
unfolding atomize_conj induct_conj_def . 
11988  403 

18456  404 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
45594  405 
lemmas induct_rulify [symmetric] = induct_atomize 
18456  406 
lemmas induct_rulify_fallback = 
407 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11678  408 

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

409 
hide_const induct_forall induct_implies induct_equal induct_conj 
11678  410 

411 

412 
text {* Method setup. *} 

413 

58826  414 
ML_file "~~/src/Tools/induct.ML" 
11678  415 
ML {* 
32171  416 
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

417 
( 
22139  418 
val cases_default = @{thm case_split} 
419 
val atomize = @{thms induct_atomize} 

420 
val rulify = @{thms induct_rulify} 

421 
val rulify_fallback = @{thms induct_rulify_fallback} 

34989  422 
val equal_def = @{thm induct_equal_def} 
34914  423 
fun dest_def _ = NONE 
58957  424 
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

425 
); 
11678  426 
*} 
427 

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

428 
declare case_split [cases type: o] 
11678  429 

58826  430 
ML_file "~~/src/Tools/case_product.ML" 
41827  431 

41310  432 

433 
hide_const (open) eq 

434 

4854  435 
end 