author | wenzelm |
Sun, 26 Nov 2006 23:43:53 +0100 | |
changeset 21539 | c5cf9243ad62 |
parent 20223 | 89d2758ecddf |
child 22139 | 539a63b98f76 |
permissions | -rw-r--r-- |
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 first-order logic *} |
4093 | 7 |
|
18456 | 8 |
theory FOL |
15481 | 9 |
imports IFOL |
21539 | 10 |
uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") |
18456 | 11 |
begin |
9487 | 12 |
|
13 |
||
14 |
subsection {* The classical axiom *} |
|
4093 | 15 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
16 |
axioms |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
17 |
classical: "(~P ==> P) ==> P" |
4093 | 18 |
|
9487 | 19 |
|
11678 | 20 |
subsection {* Lemmas and proof tools *} |
9487 | 21 |
|
21539 | 22 |
lemma ccontr: "(\<not> P \<Longrightarrow> False) \<Longrightarrow> P" |
23 |
by (erule FalseE [THEN classical]) |
|
24 |
||
25 |
(*** Classical introduction rules for | and EX ***) |
|
26 |
||
27 |
lemma disjCI: "(~Q ==> P) ==> P|Q" |
|
28 |
apply (rule classical) |
|
29 |
apply (assumption | erule meta_mp | rule disjI1 notI)+ |
|
30 |
apply (erule notE disjI2)+ |
|
31 |
done |
|
32 |
||
33 |
(*introduction rule involving only EX*) |
|
34 |
lemma ex_classical: |
|
35 |
assumes r: "~(EX x. P(x)) ==> P(a)" |
|
36 |
shows "EX x. P(x)" |
|
37 |
apply (rule classical) |
|
38 |
apply (rule exI, erule r) |
|
39 |
done |
|
40 |
||
41 |
(*version of above, simplifying ~EX to ALL~ *) |
|
42 |
lemma exCI: |
|
43 |
assumes r: "ALL x. ~P(x) ==> P(a)" |
|
44 |
shows "EX x. P(x)" |
|
45 |
apply (rule ex_classical) |
|
46 |
apply (rule notI [THEN allI, THEN r]) |
|
47 |
apply (erule notE) |
|
48 |
apply (erule exI) |
|
49 |
done |
|
50 |
||
51 |
lemma excluded_middle: "~P | P" |
|
52 |
apply (rule disjCI) |
|
53 |
apply assumption |
|
54 |
done |
|
55 |
||
56 |
(*For disjunctive case analysis*) |
|
57 |
ML {* |
|
58 |
local |
|
59 |
val excluded_middle = thm "excluded_middle" |
|
60 |
val disjE = thm "disjE" |
|
61 |
in |
|
62 |
fun excluded_middle_tac sP = |
|
63 |
res_inst_tac [("Q",sP)] (excluded_middle RS disjE) |
|
64 |
end |
|
65 |
*} |
|
66 |
||
67 |
lemma case_split_thm: |
|
68 |
assumes r1: "P ==> Q" |
|
69 |
and r2: "~P ==> Q" |
|
70 |
shows Q |
|
71 |
apply (rule excluded_middle [THEN disjE]) |
|
72 |
apply (erule r2) |
|
73 |
apply (erule r1) |
|
74 |
done |
|
75 |
||
76 |
lemmas case_split = case_split_thm [case_names True False, cases type: o] |
|
77 |
||
78 |
(*HOL's more natural case analysis tactic*) |
|
79 |
ML {* |
|
80 |
local |
|
81 |
val case_split_thm = thm "case_split_thm" |
|
82 |
in |
|
83 |
fun case_tac a = res_inst_tac [("P",a)] case_split_thm |
|
84 |
end |
|
85 |
*} |
|
86 |
||
87 |
||
88 |
(*** Special elimination rules *) |
|
89 |
||
90 |
||
91 |
(*Classical implies (-->) elimination. *) |
|
92 |
lemma impCE: |
|
93 |
assumes major: "P-->Q" |
|
94 |
and r1: "~P ==> R" |
|
95 |
and r2: "Q ==> R" |
|
96 |
shows R |
|
97 |
apply (rule excluded_middle [THEN disjE]) |
|
98 |
apply (erule r1) |
|
99 |
apply (rule r2) |
|
100 |
apply (erule major [THEN mp]) |
|
101 |
done |
|
102 |
||
103 |
(*This version of --> elimination works on Q before P. It works best for |
|
104 |
those cases in which P holds "almost everywhere". Can't install as |
|
105 |
default: would break old proofs.*) |
|
106 |
lemma impCE': |
|
107 |
assumes major: "P-->Q" |
|
108 |
and r1: "Q ==> R" |
|
109 |
and r2: "~P ==> R" |
|
110 |
shows R |
|
111 |
apply (rule excluded_middle [THEN disjE]) |
|
112 |
apply (erule r2) |
|
113 |
apply (rule r1) |
|
114 |
apply (erule major [THEN mp]) |
|
115 |
done |
|
116 |
||
117 |
(*Double negation law*) |
|
118 |
lemma notnotD: "~~P ==> P" |
|
119 |
apply (rule classical) |
|
120 |
apply (erule notE) |
|
121 |
apply assumption |
|
122 |
done |
|
123 |
||
124 |
lemma contrapos2: "[| Q; ~ P ==> ~ Q |] ==> P" |
|
125 |
apply (rule classical) |
|
126 |
apply (drule (1) meta_mp) |
|
127 |
apply (erule (1) notE) |
|
128 |
done |
|
129 |
||
130 |
(*** Tactics for implication and contradiction ***) |
|
131 |
||
132 |
(*Classical <-> elimination. Proof substitutes P=Q in |
|
133 |
~P ==> ~Q and P ==> Q *) |
|
134 |
lemma iffCE: |
|
135 |
assumes major: "P<->Q" |
|
136 |
and r1: "[| P; Q |] ==> R" |
|
137 |
and r2: "[| ~P; ~Q |] ==> R" |
|
138 |
shows R |
|
139 |
apply (rule major [unfolded iff_def, THEN conjE]) |
|
140 |
apply (elim impCE) |
|
141 |
apply (erule (1) r2) |
|
142 |
apply (erule (1) notE)+ |
|
143 |
apply (erule (1) r1) |
|
144 |
done |
|
145 |
||
146 |
||
147 |
(*Better for fast_tac: needs no quantifier duplication!*) |
|
148 |
lemma alt_ex1E: |
|
149 |
assumes major: "EX! x. P(x)" |
|
150 |
and r: "!!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R" |
|
151 |
shows R |
|
152 |
using major |
|
153 |
proof (rule ex1E) |
|
154 |
fix x |
|
155 |
assume * : "\<forall>y. P(y) \<longrightarrow> y = x" |
|
156 |
assume "P(x)" |
|
157 |
then show R |
|
158 |
proof (rule r) |
|
159 |
{ fix y y' |
|
160 |
assume "P(y)" and "P(y')" |
|
161 |
with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac 1")+ |
|
162 |
then have "y = y'" by (rule subst) |
|
163 |
} note r' = this |
|
164 |
show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r') |
|
165 |
qed |
|
166 |
qed |
|
9525 | 167 |
|
10383 | 168 |
use "cladata.ML" |
169 |
setup Cla.setup |
|
14156 | 170 |
setup cla_setup |
171 |
setup case_setup |
|
10383 | 172 |
|
9487 | 173 |
use "blastdata.ML" |
174 |
setup Blast.setup |
|
13550 | 175 |
|
176 |
||
177 |
lemma ex1_functional: "[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c" |
|
21539 | 178 |
by blast |
20223 | 179 |
|
180 |
(* Elimination of True from asumptions: *) |
|
181 |
lemma True_implies_equals: "(True ==> PROP P) == PROP P" |
|
182 |
proof |
|
183 |
assume "True \<Longrightarrow> PROP P" |
|
184 |
from this and TrueI show "PROP P" . |
|
185 |
next |
|
186 |
assume "PROP P" |
|
187 |
then show "PROP P" . |
|
188 |
qed |
|
9487 | 189 |
|
21539 | 190 |
lemma uncurry: "P --> Q --> R ==> P & Q --> R" |
191 |
by blast |
|
192 |
||
193 |
lemma iff_allI: "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))" |
|
194 |
by blast |
|
195 |
||
196 |
lemma iff_exI: "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))" |
|
197 |
by blast |
|
198 |
||
199 |
lemma all_comm: "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" by blast |
|
200 |
||
201 |
lemma ex_comm: "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" by blast |
|
202 |
||
9487 | 203 |
use "simpdata.ML" |
204 |
setup simpsetup |
|
205 |
setup "Simplifier.method_setup Splitter.split_modifiers" |
|
206 |
setup Splitter.setup |
|
207 |
setup Clasimp.setup |
|
18591 | 208 |
setup EqSubst.setup |
15481 | 209 |
|
210 |
||
14085 | 211 |
subsection {* Other simple lemmas *} |
212 |
||
213 |
lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)" |
|
214 |
by blast |
|
215 |
||
216 |
lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))" |
|
217 |
by blast |
|
218 |
||
219 |
lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)" |
|
220 |
by blast |
|
221 |
||
222 |
(** Monotonicity of implications **) |
|
223 |
||
224 |
lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)" |
|
225 |
by fast (*or (IntPr.fast_tac 1)*) |
|
226 |
||
227 |
lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)" |
|
228 |
by fast (*or (IntPr.fast_tac 1)*) |
|
229 |
||
230 |
lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)" |
|
231 |
by fast (*or (IntPr.fast_tac 1)*) |
|
232 |
||
233 |
lemma imp_refl: "P-->P" |
|
234 |
by (rule impI, assumption) |
|
235 |
||
236 |
(*The quantifier monotonicity rules are also intuitionistically valid*) |
|
237 |
lemma ex_mono: "(!!x. P(x) --> Q(x)) ==> (EX x. P(x)) --> (EX x. Q(x))" |
|
238 |
by blast |
|
239 |
||
240 |
lemma all_mono: "(!!x. P(x) --> Q(x)) ==> (ALL x. P(x)) --> (ALL x. Q(x))" |
|
241 |
by blast |
|
242 |
||
11678 | 243 |
|
244 |
subsection {* Proof by cases and induction *} |
|
245 |
||
246 |
text {* Proper handling of non-atomic rule statements. *} |
|
247 |
||
248 |
constdefs |
|
18456 | 249 |
induct_forall where "induct_forall(P) == \<forall>x. P(x)" |
250 |
induct_implies where "induct_implies(A, B) == A \<longrightarrow> B" |
|
251 |
induct_equal where "induct_equal(x, y) == x = y" |
|
252 |
induct_conj where "induct_conj(A, B) == A \<and> B" |
|
11678 | 253 |
|
254 |
lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))" |
|
18816 | 255 |
unfolding atomize_all induct_forall_def . |
11678 | 256 |
|
257 |
lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))" |
|
18816 | 258 |
unfolding atomize_imp induct_implies_def . |
11678 | 259 |
|
260 |
lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))" |
|
18816 | 261 |
unfolding atomize_eq induct_equal_def . |
11678 | 262 |
|
18456 | 263 |
lemma induct_conj_eq: |
264 |
includes meta_conjunction_syntax |
|
265 |
shows "(A && B) == Trueprop(induct_conj(A, B))" |
|
18816 | 266 |
unfolding atomize_conj induct_conj_def . |
11988 | 267 |
|
18456 | 268 |
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
269 |
lemmas induct_rulify [symmetric, standard] = induct_atomize |
|
270 |
lemmas induct_rulify_fallback = |
|
271 |
induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
|
11678 | 272 |
|
18456 | 273 |
hide const induct_forall induct_implies induct_equal induct_conj |
11678 | 274 |
|
275 |
||
276 |
text {* Method setup. *} |
|
277 |
||
278 |
ML {* |
|
279 |
structure InductMethod = InductMethodFun |
|
280 |
(struct |
|
281 |
val cases_default = thm "case_split"; |
|
282 |
val atomize = thms "induct_atomize"; |
|
18456 | 283 |
val rulify = thms "induct_rulify"; |
284 |
val rulify_fallback = thms "induct_rulify_fallback"; |
|
11678 | 285 |
end); |
286 |
*} |
|
287 |
||
288 |
setup InductMethod.setup |
|
289 |
||
4854 | 290 |
end |