1(*  Title:      FOL/FOL.thy
2    Author:     Lawrence C Paulson and Markus Wenzel
3*)
4
5section \<open>Classical first-order logic\<close>
6
7theory FOL
8imports IFOL
9keywords "print_claset" "print_induct_rules" :: diag
10begin
11
12ML_file \<open>~~/src/Provers/classical.ML\<close>
13ML_file \<open>~~/src/Provers/blast.ML\<close>
14ML_file \<open>~~/src/Provers/clasimp.ML\<close>
15
16
17subsection \<open>The classical axiom\<close>
18
19axiomatization where
20  classical: \<open>(\<not> P \<Longrightarrow> P) \<Longrightarrow> P\<close>
21
22
23subsection \<open>Lemmas and proof tools\<close>
24
25lemma ccontr: \<open>(\<not> P \<Longrightarrow> False) \<Longrightarrow> P\<close>
26  by (erule FalseE [THEN classical])
27
28
29subsubsection \<open>Classical introduction rules for \<open>\<or>\<close> and \<open>\<exists>\<close>\<close>
30
31lemma disjCI: \<open>(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q\<close>
32  apply (rule classical)
33  apply (assumption | erule meta_mp | rule disjI1 notI)+
34  apply (erule notE disjI2)+
35  done
36
37text \<open>Introduction rule involving only \<open>\<exists>\<close>\<close>
38lemma ex_classical:
39  assumes r: \<open>\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)\<close>
40  shows \<open>\<exists>x. P(x)\<close>
41  apply (rule classical)
42  apply (rule exI, erule r)
43  done
44
45text \<open>Version of above, simplifying \<open>\<not>\<exists>\<close> to \<open>\<forall>\<not>\<close>.\<close>
46lemma exCI:
47  assumes r: \<open>\<forall>x. \<not> P(x) \<Longrightarrow> P(a)\<close>
48  shows \<open>\<exists>x. P(x)\<close>
49  apply (rule ex_classical)
50  apply (rule notI [THEN allI, THEN r])
51  apply (erule notE)
52  apply (erule exI)
53  done
54
55lemma excluded_middle: \<open>\<not> P \<or> P\<close>
56  apply (rule disjCI)
57  apply assumption
58  done
59
60lemma case_split [case_names True False]:
61  assumes r1: \<open>P \<Longrightarrow> Q\<close>
62    and r2: \<open>\<not> P \<Longrightarrow> Q\<close>
63  shows \<open>Q\<close>
64  apply (rule excluded_middle [THEN disjE])
65  apply (erule r2)
66  apply (erule r1)
67  done
68
69ML \<open>
70  fun case_tac ctxt a fixes =
71    Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split};
72\<close>
73
74method_setup case_tac = \<open>
75  Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
76    (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
77\<close> "case_tac emulation (dynamic instantiation!)"
78
79
80subsection \<open>Special elimination rules\<close>
81
82text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
83lemma impCE:
84  assumes major: \<open>P \<longrightarrow> Q\<close>
85    and r1: \<open>\<not> P \<Longrightarrow> R\<close>
86    and r2: \<open>Q \<Longrightarrow> R\<close>
87  shows \<open>R\<close>
88  apply (rule excluded_middle [THEN disjE])
89   apply (erule r1)
90  apply (rule r2)
91  apply (erule major [THEN mp])
92  done
93
94text \<open>
95  This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for those cases in which P holds ``almost everywhere''.
96  Can't install as default: would break old proofs.
97\<close>
98lemma impCE':
99  assumes major: \<open>P \<longrightarrow> Q\<close>
100    and r1: \<open>Q \<Longrightarrow> R\<close>
101    and r2: \<open>\<not> P \<Longrightarrow> R\<close>
102  shows \<open>R\<close>
103  apply (rule excluded_middle [THEN disjE])
104   apply (erule r2)
105  apply (rule r1)
106  apply (erule major [THEN mp])
107  done
108
109text \<open>Double negation law.\<close>
110lemma notnotD: \<open>\<not> \<not> P \<Longrightarrow> P\<close>
111  apply (rule classical)
112  apply (erule notE)
113  apply assumption
114  done
115
116lemma contrapos2:  \<open>\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P\<close>
117  apply (rule classical)
118  apply (drule (1) meta_mp)
119  apply (erule (1) notE)
120  done
121
122
123subsubsection \<open>Tactics for implication and contradiction\<close>
124
125text \<open>
126  Classical \<open>\<longleftrightarrow>\<close> elimination. Proof substitutes \<open>P = Q\<close> in
127  \<open>\<not> P \<Longrightarrow> \<not> Q\<close> and \<open>P \<Longrightarrow> Q\<close>.
128\<close>
129lemma iffCE:
130  assumes major: \<open>P \<longleftrightarrow> Q\<close>
131    and r1: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close>
132    and r2: \<open>\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R\<close>
133  shows \<open>R\<close>
134  apply (rule major [unfolded iff_def, THEN conjE])
135  apply (elim impCE)
136     apply (erule (1) r2)
137    apply (erule (1) notE)+
138  apply (erule (1) r1)
139  done
140
141
142(*Better for fast_tac: needs no quantifier duplication!*)
143lemma alt_ex1E:
144  assumes major: \<open>\<exists>! x. P(x)\<close>
145    and r: \<open>\<And>x. \<lbrakk>P(x);  \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R\<close>
146  shows \<open>R\<close>
147  using major
148proof (rule ex1E)
149  fix x
150  assume * : \<open>\<forall>y. P(y) \<longrightarrow> y = x\<close>
151  assume \<open>P(x)\<close>
152  then show \<open>R\<close>
153  proof (rule r)
154    {
155      fix y y'
156      assume \<open>P(y)\<close> and \<open>P(y')\<close>
157      with * have \<open>x = y\<close> and \<open>x = y'\<close>
158        by - (tactic "IntPr.fast_tac \<^context> 1")+
159      then have \<open>y = y'\<close> by (rule subst)
160    } note r' = this
161    show \<open>\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<close>
162      by (intro strip, elim conjE) (rule r')
163  qed
164qed
165
166lemma imp_elim: \<open>P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R\<close>
167  by (rule classical) iprover
168
169lemma swap: \<open>\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R\<close>
170  by (rule classical) iprover
171
172
173section \<open>Classical Reasoner\<close>
174
175ML \<open>
176structure Cla = Classical
177(
178  val imp_elim = @{thm imp_elim}
179  val not_elim = @{thm notE}
180  val swap = @{thm swap}
181  val classical = @{thm classical}
182  val sizef = size_of_thm
183  val hyp_subst_tacs = [hyp_subst_tac]
184);
185
186structure Basic_Classical: BASIC_CLASSICAL = Cla;
187open Basic_Classical;
188\<close>
189
190(*Propositional rules*)
191lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
192  and [elim!] = conjE disjE impCE FalseE iffCE
193ML \<open>val prop_cs = claset_of \<^context>\<close>
194
195(*Quantifier rules*)
196lemmas [intro!] = allI ex_ex1I
197  and [intro] = exI
198  and [elim!] = exE alt_ex1E
199  and [elim] = allE
200ML \<open>val FOL_cs = claset_of \<^context>\<close>
201
202ML \<open>
203  structure Blast = Blast
204  (
205    structure Classical = Cla
206    val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
207    val equality_name = \<^const_name>\<open>eq\<close>
208    val not_name = \<^const_name>\<open>Not\<close>
209    val notE = @{thm notE}
210    val ccontr = @{thm ccontr}
211    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
212  );
213  val blast_tac = Blast.blast_tac;
214\<close>
215
216
217lemma ex1_functional: \<open>\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c\<close>
218  by blast
219
220text \<open>Elimination of \<open>True\<close> from assumptions:\<close>
221lemma True_implies_equals: \<open>(True \<Longrightarrow> PROP P) \<equiv> PROP P\<close>
222proof
223  assume \<open>True \<Longrightarrow> PROP P\<close>
224  from this and TrueI show \<open>PROP P\<close> .
225next
226  assume \<open>PROP P\<close>
227  then show \<open>PROP P\<close> .
228qed
229
230lemma uncurry: \<open>P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R\<close>
231  by blast
232
233lemma iff_allI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))\<close>
234  by blast
235
236lemma iff_exI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))\<close>
237  by blast
238
239lemma all_comm: \<open>(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))\<close>
240  by blast
241
242lemma ex_comm: \<open>(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))\<close>
243  by blast
244
245
246
247subsection \<open>Classical simplification rules\<close>
248
249text \<open>
250  Avoids duplication of subgoals after \<open>expand_if\<close>, when the true and
251  false cases boil down to the same thing.
252\<close>
253
254lemma cases_simp: \<open>(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q\<close>
255  by blast
256
257
258subsubsection \<open>Miniscoping: pushing quantifiers in\<close>
259
260text \<open>
261  We do NOT distribute of \<open>\<forall>\<close> over \<open>\<and>\<close>, or dually that of
262  \<open>\<exists>\<close> over \<open>\<or>\<close>.
263
264  Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that
265  this step can increase proof length!
266\<close>
267
268text \<open>Existential miniscoping.\<close>
269lemma int_ex_simps:
270  \<open>\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q\<close>
271  \<open>\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))\<close>
272  \<open>\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q\<close>
273  \<open>\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))\<close>
274  by iprover+
275
276text \<open>Classical rules.\<close>
277lemma cla_ex_simps:
278  \<open>\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q\<close>
279  \<open>\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))\<close>
280  by blast+
281
282lemmas ex_simps = int_ex_simps cla_ex_simps
283
284text \<open>Universal miniscoping.\<close>
285lemma int_all_simps:
286  \<open>\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q\<close>
287  \<open>\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))\<close>
288  \<open>\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q\<close>
289  \<open>\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))\<close>
290  by iprover+
291
292text \<open>Classical rules.\<close>
293lemma cla_all_simps:
294  \<open>\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q\<close>
295  \<open>\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))\<close>
296  by blast+
297
298lemmas all_simps = int_all_simps cla_all_simps
299
300
301subsubsection \<open>Named rewrite rules proved for IFOL\<close>
302
303lemma imp_disj1: \<open>(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast
304lemma imp_disj2: \<open>Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast
305
306lemma de_Morgan_conj: \<open>(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)\<close> by blast
307
308lemma not_imp: \<open>\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)\<close> by blast
309lemma not_iff: \<open>\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)\<close> by blast
310
311lemma not_all: \<open>(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))\<close> by blast
312lemma imp_all: \<open>((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)\<close> by blast
313
314
315lemmas meta_simps =
316  triv_forall_equality  \<comment> \<open>prunes params\<close>
317  True_implies_equals  \<comment> \<open>prune asms \<open>True\<close>\<close>
318
319lemmas IFOL_simps =
320  refl [THEN P_iff_T] conj_simps disj_simps not_simps
321  imp_simps iff_simps quant_simps
322
323lemma notFalseI: \<open>\<not> False\<close> by iprover
324
325lemma cla_simps_misc:
326  \<open>\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q\<close>
327  \<open>P \<or> \<not> P\<close>
328  \<open>\<not> P \<or> P\<close>
329  \<open>\<not> \<not> P \<longleftrightarrow> P\<close>
330  \<open>(\<not> P \<longrightarrow> P) \<longleftrightarrow> P\<close>
331  \<open>(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)\<close> by blast+
332
333lemmas cla_simps =
334  de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
335  not_imp not_all not_ex cases_simp cla_simps_misc
336
337
338ML_file \<open>simpdata.ML\<close>
339
340simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_ex\<close>
341simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_all\<close>
342
343ML \<open>
344(*intuitionistic simprules only*)
345val IFOL_ss =
346  put_simpset FOL_basic_ss \<^context>
347  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
348  addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>]
349  |> Simplifier.add_cong @{thm imp_cong}
350  |> simpset_of;
351
352(*classical simprules too*)
353val FOL_ss =
354  put_simpset IFOL_ss \<^context>
355  addsimps @{thms cla_simps cla_ex_simps cla_all_simps}
356  |> simpset_of;
357\<close>
358
359setup \<open>
360  map_theory_simpset (put_simpset FOL_ss) #>
361  Simplifier.method_setup Splitter.split_modifiers
362\<close>
363
364ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
365
366
367subsection \<open>Other simple lemmas\<close>
368
369lemma [simp]: \<open>((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)\<close>
370  by blast
371
372lemma [simp]: \<open>((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))\<close>
373  by blast
374
375lemma not_disj_iff_imp: \<open>\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)\<close>
376  by blast
377
378
379subsubsection \<open>Monotonicity of implications\<close>
380
381lemma conj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)\<close>
382  by fast (*or (IntPr.fast_tac 1)*)
383
384lemma disj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)\<close>
385  by fast (*or (IntPr.fast_tac 1)*)
386
387lemma imp_mono: \<open>\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)\<close>
388  by fast (*or (IntPr.fast_tac 1)*)
389
390lemma imp_refl: \<open>P \<longrightarrow> P\<close>
391  by (rule impI)
392
393text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close>
394lemma ex_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))\<close>
395  by blast
396
397lemma all_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))\<close>
398  by blast
399
400
401subsection \<open>Proof by cases and induction\<close>
402
403text \<open>Proper handling of non-atomic rule statements.\<close>
404
405context
406begin
407
408qualified definition \<open>induct_forall(P) \<equiv> \<forall>x. P(x)\<close>
409qualified definition \<open>induct_implies(A, B) \<equiv> A \<longrightarrow> B\<close>
410qualified definition \<open>induct_equal(x, y) \<equiv> x = y\<close>
411qualified definition \<open>induct_conj(A, B) \<equiv> A \<and> B\<close>
412
413lemma induct_forall_eq: \<open>(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))\<close>
414  unfolding atomize_all induct_forall_def .
415
416lemma induct_implies_eq: \<open>(A \<Longrightarrow> B) \<equiv> Trueprop(induct_implies(A, B))\<close>
417  unfolding atomize_imp induct_implies_def .
418
419lemma induct_equal_eq: \<open>(x \<equiv> y) \<equiv> Trueprop(induct_equal(x, y))\<close>
420  unfolding atomize_eq induct_equal_def .
421
422lemma induct_conj_eq: \<open>(A &&& B) \<equiv> Trueprop(induct_conj(A, B))\<close>
423  unfolding atomize_conj induct_conj_def .
424
425lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
426lemmas induct_rulify [symmetric] = induct_atomize
427lemmas induct_rulify_fallback =
428  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
429
430text \<open>Method setup.\<close>
431
432ML_file \<open>~~/src/Tools/induct.ML\<close>
433ML \<open>
434  structure Induct = Induct
435  (
436    val cases_default = @{thm case_split}
437    val atomize = @{thms induct_atomize}
438    val rulify = @{thms induct_rulify}
439    val rulify_fallback = @{thms induct_rulify_fallback}
440    val equal_def = @{thm induct_equal_def}
441    fun dest_def _ = NONE
442    fun trivial_tac _ _ = no_tac
443  );
444\<close>
445
446declare case_split [cases type: o]
447
448end
449
450ML_file \<open>~~/src/Tools/case_product.ML\<close>
451
452
453hide_const (open) eq
454
455end
456