author  wenzelm 
Fri, 24 Jul 2009 21:21:45 +0200  
changeset 32176  893614e2c35c 
parent 32171  220abde9962b 
child 32261  05e687ddbcee 
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" 
23154  14 
("cladata.ML") 
15 
("simpdata.ML") 

18456  16 
begin 
9487  17 

18 

19 
subsection {* The classical axiom *} 

4093  20 

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

21 
axioms 
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 

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

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 

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

14156  171 
setup cla_setup 
10383  172 

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

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

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

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

176 
val thy = @{theory} 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

177 
type claset = Cla.claset 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

178 
val equality_name = @{const_name "op ="} 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

179 
val not_name = @{const_name Not} 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

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

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

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

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

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

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

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

187 
val cla_meth' = Cla.cla_meth' 
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset

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

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

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

191 

9487  192 
setup Blast.setup 
13550  193 

194 

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

21539  196 
by blast 
20223  197 

198 
(* Elimination of True from asumptions: *) 

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

200 
proof 

201 
assume "True \<Longrightarrow> PROP P" 

202 
from this and TrueI show "PROP P" . 

203 
next 

204 
assume "PROP P" 

205 
then show "PROP P" . 

206 
qed 

9487  207 

21539  208 
lemma uncurry: "P > Q > R ==> P & Q > R" 
209 
by blast 

210 

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

212 
by blast 

213 

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

215 
by blast 

216 

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

218 

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

220 

26286  221 

222 

223 
(*** Classical simplification rules ***) 

224 

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

226 
cases boil down to the same thing.*) 

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

228 

229 

230 
(*** Miniscoping: pushing quantifiers in 

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

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

233 
show that this step can increase proof length! 

234 
***) 

235 

236 
(*existential miniscoping*) 

237 
lemma int_ex_simps: 

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

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

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

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

242 
by iprover+ 

243 

244 
(*classical rules*) 

245 
lemma cla_ex_simps: 

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

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

248 
by blast+ 

249 

250 
lemmas ex_simps = int_ex_simps cla_ex_simps 

251 

252 
(*universal miniscoping*) 

253 
lemma int_all_simps: 

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

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

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

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

258 
by iprover+ 

259 

260 
(*classical rules*) 

261 
lemma cla_all_simps: 

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

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

264 
by blast+ 

265 

266 
lemmas all_simps = int_all_simps cla_all_simps 

267 

268 

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

270 

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

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

273 

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

275 

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

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

278 

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

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

281 

282 

283 
lemmas meta_simps = 

284 
triv_forall_equality (* prunes params *) 

285 
True_implies_equals (* prune asms `True' *) 

286 

287 
lemmas IFOL_simps = 

288 
refl [THEN P_iff_T] conj_simps disj_simps not_simps 

289 
imp_simps iff_simps quant_simps 

290 

291 
lemma notFalseI: "~False" by iprover 

292 

293 
lemma cla_simps_misc: 

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

295 
"P  ~P" 

296 
"~P  P" 

297 
"~ ~ P <> P" 

298 
"(~P > P) <> P" 

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

300 

301 
lemmas cla_simps = 

302 
de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 

303 
not_imp not_all not_ex cases_simp cla_simps_misc 

304 

305 

9487  306 
use "simpdata.ML" 
307 
setup simpsetup 

308 
setup "Simplifier.method_setup Splitter.split_modifiers" 

309 
setup Splitter.setup 

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

310 
setup clasimp_setup 
18591  311 
setup EqSubst.setup 
15481  312 

313 

14085  314 
subsection {* Other simple lemmas *} 
315 

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

317 
by blast 

318 

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

320 
by blast 

321 

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

323 
by blast 

324 

325 
(** Monotonicity of implications **) 

326 

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

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

329 

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

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

332 

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

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

335 

336 
lemma imp_refl: "P>P" 

337 
by (rule impI, assumption) 

338 

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

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

341 
by blast 

342 

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

344 
by blast 

345 

11678  346 

347 
subsection {* Proof by cases and induction *} 

348 

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

350 

351 
constdefs 

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

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

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

11678  356 

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

18816  358 
unfolding atomize_all induct_forall_def . 
11678  359 

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

18816  361 
unfolding atomize_imp induct_implies_def . 
11678  362 

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

18816  364 
unfolding atomize_eq induct_equal_def . 
11678  365 

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

366 
lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))" 
18816  367 
unfolding atomize_conj induct_conj_def . 
11988  368 

18456  369 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
370 
lemmas induct_rulify [symmetric, standard] = induct_atomize 

371 
lemmas induct_rulify_fallback = 

372 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11678  373 

18456  374 
hide const induct_forall induct_implies induct_equal induct_conj 
11678  375 

376 

377 
text {* Method setup. *} 

378 

379 
ML {* 

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

381 
( 
22139  382 
val cases_default = @{thm case_split} 
383 
val atomize = @{thms induct_atomize} 

384 
val rulify = @{thms induct_rulify} 

385 
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

386 
); 
11678  387 
*} 
388 

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

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

390 
declare case_split [cases type: o] 
11678  391 

4854  392 
end 