src/FOL/FOL.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 58826 2ed2eaabe3df child 58957 c9e744ea8a38 permissions -rw-r--r--
1 (*  Title:      FOL/FOL.thy
2     Author:     Lawrence C Paulson and Markus Wenzel
3 *)
5 section {* Classical first-order logic *}
7 theory FOL
8 imports IFOL
9 keywords "print_claset" "print_induct_rules" :: diag
10 begin
12 ML_file "~~/src/Provers/classical.ML"
13 ML_file "~~/src/Provers/blast.ML"
14 ML_file "~~/src/Provers/clasimp.ML"
17 subsection {* The classical axiom *}
19 axiomatization where
20   classical: "(~P ==> P) ==> P"
23 subsection {* Lemmas and proof tools *}
25 lemma ccontr: "(\<not> P \<Longrightarrow> False) \<Longrightarrow> P"
26   by (erule FalseE [THEN classical])
28 (*** Classical introduction rules for | and EX ***)
30 lemma disjCI: "(~Q ==> P) ==> P|Q"
31   apply (rule classical)
32   apply (assumption | erule meta_mp | rule disjI1 notI)+
33   apply (erule notE disjI2)+
34   done
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
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
54 lemma excluded_middle: "~P | P"
55   apply (rule disjCI)
56   apply assumption
57   done
59 lemma case_split [case_names True False]:
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
68 ML {*
69   fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
70 *}
72 method_setup case_tac = {*
73   Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
74     (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
75 *} "case_tac emulation (dynamic instantiation!)"
78 (*** Special elimination rules *)
81 (*Classical implies (-->) elimination. *)
82 lemma impCE:
83   assumes major: "P-->Q"
84     and r1: "~P ==> R"
85     and r2: "Q ==> R"
86   shows R
87   apply (rule excluded_middle [THEN disjE])
88    apply (erule r1)
89   apply (rule r2)
90   apply (erule major [THEN mp])
91   done
93 (*This version of --> elimination works on Q before P.  It works best for
94   those cases in which P holds "almost everywhere".  Can't install as
95   default: would break old proofs.*)
96 lemma impCE':
97   assumes major: "P-->Q"
98     and r1: "Q ==> R"
99     and r2: "~P ==> R"
100   shows R
101   apply (rule excluded_middle [THEN disjE])
102    apply (erule r2)
103   apply (rule r1)
104   apply (erule major [THEN mp])
105   done
107 (*Double negation law*)
108 lemma notnotD: "~~P ==> P"
109   apply (rule classical)
110   apply (erule notE)
111   apply assumption
112   done
114 lemma contrapos2:  "[| Q; ~ P ==> ~ Q |] ==> P"
115   apply (rule classical)
116   apply (drule (1) meta_mp)
117   apply (erule (1) notE)
118   done
120 (*** Tactics for implication and contradiction ***)
122 (*Classical <-> elimination.  Proof substitutes P=Q in
123     ~P ==> ~Q    and    P ==> Q  *)
124 lemma iffCE:
125   assumes major: "P<->Q"
126     and r1: "[| P; Q |] ==> R"
127     and r2: "[| ~P; ~Q |] ==> R"
128   shows R
129   apply (rule major [unfolded iff_def, THEN conjE])
130   apply (elim impCE)
131      apply (erule (1) r2)
132     apply (erule (1) notE)+
133   apply (erule (1) r1)
134   done
137 (*Better for fast_tac: needs no quantifier duplication!*)
138 lemma alt_ex1E:
139   assumes major: "EX! x. P(x)"
140     and r: "!!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R"
141   shows R
142   using major
143 proof (rule ex1E)
144   fix x
145   assume * : "\<forall>y. P(y) \<longrightarrow> y = x"
146   assume "P(x)"
147   then show R
148   proof (rule r)
149     { fix y y'
150       assume "P(y)" and "P(y')"
151       with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac @{context} 1")+
152       then have "y = y'" by (rule subst)
153     } note r' = this
154     show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r')
155   qed
156 qed
158 lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
159   by (rule classical) iprover
161 lemma swap: "~ P ==> (~ R ==> P) ==> R"
162   by (rule classical) iprover
165 section {* Classical Reasoner *}
167 ML {*
168 structure Cla = Classical
169 (
170   val imp_elim = @{thm imp_elim}
171   val not_elim = @{thm notE}
172   val swap = @{thm swap}
173   val classical = @{thm classical}
174   val sizef = size_of_thm
175   val hyp_subst_tacs = [hyp_subst_tac]
176 );
178 structure Basic_Classical: BASIC_CLASSICAL = Cla;
179 open Basic_Classical;
180 *}
182 (*Propositional rules*)
183 lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
184   and [elim!] = conjE disjE impCE FalseE iffCE
185 ML {* val prop_cs = claset_of @{context} *}
187 (*Quantifier rules*)
188 lemmas [intro!] = allI ex_ex1I
189   and [intro] = exI
190   and [elim!] = exE alt_ex1E
191   and [elim] = allE
192 ML {* val FOL_cs = claset_of @{context} *}
194 ML {*
195   structure Blast = Blast
196   (
197     structure Classical = Cla
198     val Trueprop_const = dest_Const @{const Trueprop}
199     val equality_name = @{const_name eq}
200     val not_name = @{const_name Not}
201     val notE = @{thm notE}
202     val ccontr = @{thm ccontr}
203     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
204   );
205   val blast_tac = Blast.blast_tac;
206 *}
209 lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
210   by blast
212 (* Elimination of True from asumptions: *)
213 lemma True_implies_equals: "(True ==> PROP P) == PROP P"
214 proof
215   assume "True \<Longrightarrow> PROP P"
216   from this and TrueI show "PROP P" .
217 next
218   assume "PROP P"
219   then show "PROP P" .
220 qed
222 lemma uncurry: "P --> Q --> R ==> P & Q --> R"
223   by blast
225 lemma iff_allI: "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
226   by blast
228 lemma iff_exI: "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
229   by blast
231 lemma all_comm: "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" by blast
233 lemma ex_comm: "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" by blast
237 (*** Classical simplification rules ***)
239 (*Avoids duplication of subgoals after expand_if, when the true and false
240   cases boil down to the same thing.*)
241 lemma cases_simp: "(P --> Q) & (~P --> Q) <-> Q" by blast
244 (*** Miniscoping: pushing quantifiers in
245      We do NOT distribute of ALL over &, or dually that of EX over |
246      Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
247      show that this step can increase proof length!
248 ***)
250 (*existential miniscoping*)
251 lemma int_ex_simps:
252   "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
253   "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
254   "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
255   "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
256   by iprover+
258 (*classical rules*)
259 lemma cla_ex_simps:
260   "!!P Q. (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
261   "!!P Q. (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
262   by blast+
264 lemmas ex_simps = int_ex_simps cla_ex_simps
266 (*universal miniscoping*)
267 lemma int_all_simps:
268   "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
269   "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
270   "!!P Q. (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
271   "!!P Q. (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
272   by iprover+
274 (*classical rules*)
275 lemma cla_all_simps:
276   "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
277   "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
278   by blast+
280 lemmas all_simps = int_all_simps cla_all_simps
283 (*** Named rewrite rules proved for IFOL ***)
285 lemma imp_disj1: "(P-->Q) | R <-> (P-->Q | R)" by blast
286 lemma imp_disj2: "Q | (P-->R) <-> (P-->Q | R)" by blast
288 lemma de_Morgan_conj: "(~(P & Q)) <-> (~P | ~Q)" by blast
290 lemma not_imp: "~(P --> Q) <-> (P & ~Q)" by blast
291 lemma not_iff: "~(P <-> Q) <-> (P <-> ~Q)" by blast
293 lemma not_all: "(~ (ALL x. P(x))) <-> (EX x.~P(x))" by blast
294 lemma imp_all: "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)" by blast
297 lemmas meta_simps =
298   triv_forall_equality (* prunes params *)
299   True_implies_equals  (* prune asms `True' *)
301 lemmas IFOL_simps =
302   refl [THEN P_iff_T] conj_simps disj_simps not_simps
303   imp_simps iff_simps quant_simps
305 lemma notFalseI: "~False" by iprover
307 lemma cla_simps_misc:
308   "~(P&Q) <-> ~P | ~Q"
309   "P | ~P"
310   "~P | P"
311   "~ ~ P <-> P"
312   "(~P --> P) <-> P"
313   "(~P <-> ~Q) <-> (P<->Q)" by blast+
315 lemmas cla_simps =
316   de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
317   not_imp not_all not_ex cases_simp cla_simps_misc
320 ML_file "simpdata.ML"
322 simproc_setup defined_Ex ("EX x. P(x)") = {* fn _ => Quantifier1.rearrange_ex *}
323 simproc_setup defined_All ("ALL x. P(x)") = {* fn _ => Quantifier1.rearrange_all *}
325 ML {*
326 (*intuitionistic simprules only*)
327 val IFOL_ss =
328   put_simpset FOL_basic_ss @{context}
329   addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
330   addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
332   |> simpset_of;
334 (*classical simprules too*)
335 val FOL_ss =
336   put_simpset IFOL_ss @{context}
337   addsimps @{thms cla_simps cla_ex_simps cla_all_simps}
338   |> simpset_of;
339 *}
341 setup {*
342   map_theory_simpset (put_simpset FOL_ss) #>
343   Simplifier.method_setup Splitter.split_modifiers
344 *}
346 ML_file "~~/src/Tools/eqsubst.ML"
349 subsection {* Other simple lemmas *}
351 lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)"
352 by blast
354 lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
355 by blast
357 lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
358 by blast
360 (** Monotonicity of implications **)
362 lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
363 by fast (*or (IntPr.fast_tac 1)*)
365 lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
366 by fast (*or (IntPr.fast_tac 1)*)
368 lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
369 by fast (*or (IntPr.fast_tac 1)*)
371 lemma imp_refl: "P-->P"
372 by (rule impI, assumption)
374 (*The quantifier monotonicity rules are also intuitionistically valid*)
375 lemma ex_mono: "(!!x. P(x) --> Q(x)) ==> (EX x. P(x)) --> (EX x. Q(x))"
376 by blast
378 lemma all_mono: "(!!x. P(x) --> Q(x)) ==> (ALL x. P(x)) --> (ALL x. Q(x))"
379 by blast
382 subsection {* Proof by cases and induction *}
384 text {* Proper handling of non-atomic rule statements. *}
386 definition "induct_forall(P) == \<forall>x. P(x)"
387 definition "induct_implies(A, B) == A \<longrightarrow> B"
388 definition "induct_equal(x, y) == x = y"
389 definition "induct_conj(A, B) == A \<and> B"
391 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
392   unfolding atomize_all induct_forall_def .
394 lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))"
395   unfolding atomize_imp induct_implies_def .
397 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
398   unfolding atomize_eq induct_equal_def .
400 lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))"
401   unfolding atomize_conj induct_conj_def .
403 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
404 lemmas induct_rulify [symmetric] = induct_atomize
405 lemmas induct_rulify_fallback =
406   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
408 hide_const induct_forall induct_implies induct_equal induct_conj
411 text {* Method setup. *}
413 ML_file "~~/src/Tools/induct.ML"
414 ML {*
415   structure Induct = Induct
416   (
417     val cases_default = @{thm case_split}
418     val atomize = @{thms induct_atomize}
419     val rulify = @{thms induct_rulify}
420     val rulify_fallback = @{thms induct_rulify_fallback}
421     val equal_def = @{thm induct_equal_def}
422     fun dest_def _ = NONE
423     fun trivial_tac _ = no_tac
424   );
425 *}
427 declare case_split [cases type: o]
429 ML_file "~~/src/Tools/case_product.ML"
432 hide_const (open) eq
434 end