author  wenzelm 
Tue, 31 Jul 2007 21:19:18 +0200  
changeset 24097  86734ba03ca2 
parent 23154  5126551e378b 
child 24830  a7b3ab44d993 
permissions  rwrr 
9487  1 
(* Title: FOL/FOL.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Markus Wenzel 

11678  4 
*) 
9487  5 

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

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

13 
"~~/src/Provers/clasimp.ML" 

23154  14 
("cladata.ML") 
15 
("blastdata.ML") 

16 
("simpdata.ML") 

18456  17 
begin 
9487  18 

19 

20 
subsection {* The classical axiom *} 

4093  21 

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

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

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

9487  25 

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

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

30 

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

32 

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

34 
apply (rule classical) 

35 
apply (assumption  erule meta_mp  rule disjI1 notI)+ 

36 
apply (erule notE disjI2)+ 

37 
done 

38 

39 
(*introduction rule involving only EX*) 

40 
lemma ex_classical: 

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

42 
shows "EX x. P(x)" 

43 
apply (rule classical) 

44 
apply (rule exI, erule r) 

45 
done 

46 

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

48 
lemma exCI: 

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

50 
shows "EX x. P(x)" 

51 
apply (rule ex_classical) 

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

53 
apply (erule notE) 

54 
apply (erule exI) 

55 
done 

56 

57 
lemma excluded_middle: "~P  P" 

58 
apply (rule disjCI) 

59 
apply assumption 

60 
done 

61 

62 
(*For disjunctive case analysis*) 

63 
ML {* 

22139  64 
fun excluded_middle_tac sP = 
65 
res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE}) 

21539  66 
*} 
67 

68 
lemma case_split_thm: 

69 
assumes r1: "P ==> Q" 

70 
and r2: "~P ==> Q" 

71 
shows Q 

72 
apply (rule excluded_middle [THEN disjE]) 

73 
apply (erule r2) 

74 
apply (erule r1) 

75 
done 

76 

77 
lemmas case_split = case_split_thm [case_names True False, cases type: o] 

78 

79 
(*HOL's more natural case analysis tactic*) 

80 
ML {* 

22139  81 
fun case_tac a = res_inst_tac [("P",a)] @{thm case_split_thm} 
21539  82 
*} 
83 

84 

85 
(*** Special elimination rules *) 

86 

87 

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

89 
lemma impCE: 

90 
assumes major: "P>Q" 

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

92 
and r2: "Q ==> R" 

93 
shows R 

94 
apply (rule excluded_middle [THEN disjE]) 

95 
apply (erule r1) 

96 
apply (rule r2) 

97 
apply (erule major [THEN mp]) 

98 
done 

99 

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

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

102 
default: would break old proofs.*) 

103 
lemma impCE': 

104 
assumes major: "P>Q" 

105 
and r1: "Q ==> R" 

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

107 
shows R 

108 
apply (rule excluded_middle [THEN disjE]) 

109 
apply (erule r2) 

110 
apply (rule r1) 

111 
apply (erule major [THEN mp]) 

112 
done 

113 

114 
(*Double negation law*) 

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

116 
apply (rule classical) 

117 
apply (erule notE) 

118 
apply assumption 

119 
done 

120 

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

122 
apply (rule classical) 

123 
apply (drule (1) meta_mp) 

124 
apply (erule (1) notE) 

125 
done 

126 

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

128 

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

130 
~P ==> ~Q and P ==> Q *) 

131 
lemma iffCE: 

132 
assumes major: "P<>Q" 

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

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

135 
shows R 

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

137 
apply (elim impCE) 

138 
apply (erule (1) r2) 

139 
apply (erule (1) notE)+ 

140 
apply (erule (1) r1) 

141 
done 

142 

143 

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

145 
lemma alt_ex1E: 

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

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

148 
shows R 

149 
using major 

150 
proof (rule ex1E) 

151 
fix x 

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

153 
assume "P(x)" 

154 
then show R 

155 
proof (rule r) 

156 
{ fix y y' 

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

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

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

160 
} note r' = this 

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

162 
qed 

163 
qed 

9525  164 

10383  165 
use "cladata.ML" 
166 
setup Cla.setup 

14156  167 
setup cla_setup 
168 
setup case_setup 

10383  169 

9487  170 
use "blastdata.ML" 
171 
setup Blast.setup 

13550  172 

173 

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

21539  175 
by blast 
20223  176 

177 
(* Elimination of True from asumptions: *) 

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

179 
proof 

180 
assume "True \<Longrightarrow> PROP P" 

181 
from this and TrueI show "PROP P" . 

182 
next 

183 
assume "PROP P" 

184 
then show "PROP P" . 

185 
qed 

9487  186 

21539  187 
lemma uncurry: "P > Q > R ==> P & Q > R" 
188 
by blast 

189 

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

191 
by blast 

192 

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

194 
by blast 

195 

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

197 

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

199 

9487  200 
use "simpdata.ML" 
201 
setup simpsetup 

202 
setup "Simplifier.method_setup Splitter.split_modifiers" 

203 
setup Splitter.setup 

204 
setup Clasimp.setup 

18591  205 
setup EqSubst.setup 
15481  206 

207 

14085  208 
subsection {* Other simple lemmas *} 
209 

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

211 
by blast 

212 

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

214 
by blast 

215 

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

217 
by blast 

218 

219 
(** Monotonicity of implications **) 

220 

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

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

223 

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

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

226 

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

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

229 

230 
lemma imp_refl: "P>P" 

231 
by (rule impI, assumption) 

232 

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

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

235 
by blast 

236 

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

238 
by blast 

239 

11678  240 

241 
subsection {* Proof by cases and induction *} 

242 

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

244 

245 
constdefs 

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

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

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

11678  250 

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

18816  252 
unfolding atomize_all induct_forall_def . 
11678  253 

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

18816  255 
unfolding atomize_imp induct_implies_def . 
11678  256 

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

18816  258 
unfolding atomize_eq induct_equal_def . 
11678  259 

18456  260 
lemma induct_conj_eq: 
261 
includes meta_conjunction_syntax 

262 
shows "(A && B) == Trueprop(induct_conj(A, B))" 

18816  263 
unfolding atomize_conj induct_conj_def . 
11988  264 

18456  265 
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
266 
lemmas induct_rulify [symmetric, standard] = induct_atomize 

267 
lemmas induct_rulify_fallback = 

268 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

11678  269 

18456  270 
hide const induct_forall induct_implies induct_equal induct_conj 
11678  271 

272 

273 
text {* Method setup. *} 

274 

275 
ML {* 

276 
structure InductMethod = InductMethodFun 

277 
(struct 

22139  278 
val cases_default = @{thm case_split} 
279 
val atomize = @{thms induct_atomize} 

280 
val rulify = @{thms induct_rulify} 

281 
val rulify_fallback = @{thms induct_rulify_fallback} 

11678  282 
end); 
283 
*} 

284 

285 
setup InductMethod.setup 

286 

4854  287 
end 