src/FOL/FOL.thy
author haftmann
Thu Nov 23 17:03:27 2017 +0000 (20 months ago)
changeset 67087 733017b19de9
parent 63120 629a4c5e953e
child 69590 e65314985426
permissions -rw-r--r--
generalized more lemmas
     1 (*  Title:      FOL/FOL.thy
     2     Author:     Lawrence C Paulson and Markus Wenzel
     3 *)
     4 
     5 section \<open>Classical first-order logic\<close>
     6 
     7 theory FOL
     8 imports IFOL
     9 keywords "print_claset" "print_induct_rules" :: diag
    10 begin
    11 
    12 ML_file "~~/src/Provers/classical.ML"
    13 ML_file "~~/src/Provers/blast.ML"
    14 ML_file "~~/src/Provers/clasimp.ML"
    15 
    16 
    17 subsection \<open>The classical axiom\<close>
    18 
    19 axiomatization where
    20   classical: "(\<not> P \<Longrightarrow> P) \<Longrightarrow> P"
    21 
    22 
    23 subsection \<open>Lemmas and proof tools\<close>
    24 
    25 lemma ccontr: "(\<not> P \<Longrightarrow> False) \<Longrightarrow> P"
    26   by (erule FalseE [THEN classical])
    27 
    28 
    29 subsubsection \<open>Classical introduction rules for \<open>\<or>\<close> and \<open>\<exists>\<close>\<close>
    30 
    31 lemma disjCI: "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"
    32   apply (rule classical)
    33   apply (assumption | erule meta_mp | rule disjI1 notI)+
    34   apply (erule notE disjI2)+
    35   done
    36 
    37 text \<open>Introduction rule involving only \<open>\<exists>\<close>\<close>
    38 lemma ex_classical:
    39   assumes r: "\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)"
    40   shows "\<exists>x. P(x)"
    41   apply (rule classical)
    42   apply (rule exI, erule r)
    43   done
    44 
    45 text \<open>Version of above, simplifying \<open>\<not>\<exists>\<close> to \<open>\<forall>\<not>\<close>.\<close>
    46 lemma exCI:
    47   assumes r: "\<forall>x. \<not> P(x) \<Longrightarrow> P(a)"
    48   shows "\<exists>x. P(x)"
    49   apply (rule ex_classical)
    50   apply (rule notI [THEN allI, THEN r])
    51   apply (erule notE)
    52   apply (erule exI)
    53   done
    54 
    55 lemma excluded_middle: "\<not> P \<or> P"
    56   apply (rule disjCI)
    57   apply assumption
    58   done
    59 
    60 lemma case_split [case_names True False]:
    61   assumes r1: "P \<Longrightarrow> Q"
    62     and r2: "\<not> P \<Longrightarrow> Q"
    63   shows Q
    64   apply (rule excluded_middle [THEN disjE])
    65   apply (erule r2)
    66   apply (erule r1)
    67   done
    68 
    69 ML \<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 
    74 method_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 
    80 subsection \<open>Special elimination rules\<close>
    81 
    82 text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
    83 lemma impCE:
    84   assumes major: "P \<longrightarrow> Q"
    85     and r1: "\<not> P \<Longrightarrow> R"
    86     and r2: "Q \<Longrightarrow> R"
    87   shows R
    88   apply (rule excluded_middle [THEN disjE])
    89    apply (erule r1)
    90   apply (rule r2)
    91   apply (erule major [THEN mp])
    92   done
    93 
    94 text \<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>
    98 lemma impCE':
    99   assumes major: "P \<longrightarrow> Q"
   100     and r1: "Q \<Longrightarrow> R"
   101     and r2: "\<not> P \<Longrightarrow> 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 text \<open>Double negation law.\<close>
   110 lemma notnotD: "\<not> \<not> P \<Longrightarrow> P"
   111   apply (rule classical)
   112   apply (erule notE)
   113   apply assumption
   114   done
   115 
   116 lemma contrapos2:  "\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P"
   117   apply (rule classical)
   118   apply (drule (1) meta_mp)
   119   apply (erule (1) notE)
   120   done
   121 
   122 
   123 subsubsection \<open>Tactics for implication and contradiction\<close>
   124 
   125 text \<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>
   129 lemma iffCE:
   130   assumes major: "P \<longleftrightarrow> Q"
   131     and r1: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   132     and r2: "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
   133   shows R
   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!*)
   143 lemma alt_ex1E:
   144   assumes major: "\<exists>! x. P(x)"
   145     and r: "\<And>x. \<lbrakk>P(x);  \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
   146   shows R
   147   using major
   148 proof (rule ex1E)
   149   fix x
   150   assume * : "\<forall>y. P(y) \<longrightarrow> y = x"
   151   assume "P(x)"
   152   then show R
   153   proof (rule r)
   154     {
   155       fix y y'
   156       assume "P(y)" and "P(y')"
   157       with * have "x = y" and "x = y'"
   158         by - (tactic "IntPr.fast_tac @{context} 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'"
   162       by (intro strip, elim conjE) (rule r')
   163   qed
   164 qed
   165 
   166 lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   167   by (rule classical) iprover
   168 
   169 lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
   170   by (rule classical) iprover
   171 
   172 
   173 section \<open>Classical Reasoner\<close>
   174 
   175 ML \<open>
   176 structure 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 
   186 structure Basic_Classical: BASIC_CLASSICAL = Cla;
   187 open Basic_Classical;
   188 \<close>
   189 
   190 (*Propositional rules*)
   191 lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
   192   and [elim!] = conjE disjE impCE FalseE iffCE
   193 ML \<open>val prop_cs = claset_of @{context}\<close>
   194 
   195 (*Quantifier rules*)
   196 lemmas [intro!] = allI ex_ex1I
   197   and [intro] = exI
   198   and [elim!] = exE alt_ex1E
   199   and [elim] = allE
   200 ML \<open>val FOL_cs = claset_of @{context}\<close>
   201 
   202 ML \<open>
   203   structure Blast = Blast
   204   (
   205     structure Classical = Cla
   206     val Trueprop_const = dest_Const @{const Trueprop}
   207     val equality_name = @{const_name eq}
   208     val not_name = @{const_name Not}
   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 
   217 lemma ex1_functional: "\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c"
   218   by blast
   219 
   220 text \<open>Elimination of \<open>True\<close> from assumptions:\<close>
   221 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   222 proof
   223   assume "True \<Longrightarrow> PROP P"
   224   from this and TrueI show "PROP P" .
   225 next
   226   assume "PROP P"
   227   then show "PROP P" .
   228 qed
   229 
   230 lemma uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
   231   by blast
   232 
   233 lemma iff_allI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))"
   234   by blast
   235 
   236 lemma iff_exI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))"
   237   by blast
   238 
   239 lemma all_comm: "(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
   240   by blast
   241 
   242 lemma ex_comm: "(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
   243   by blast
   244 
   245 
   246 
   247 subsection \<open>Classical simplification rules\<close>
   248 
   249 text \<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 
   254 lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
   255   by blast
   256 
   257 
   258 subsubsection \<open>Miniscoping: pushing quantifiers in\<close>
   259 
   260 text \<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 
   268 text \<open>Existential miniscoping.\<close>
   269 lemma int_ex_simps:
   270   "\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
   271   "\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
   272   "\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
   273   "\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
   274   by iprover+
   275 
   276 text \<open>Classical rules.\<close>
   277 lemma cla_ex_simps:
   278   "\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
   279   "\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))"
   280   by blast+
   281 
   282 lemmas ex_simps = int_ex_simps cla_ex_simps
   283 
   284 text \<open>Universal miniscoping.\<close>
   285 lemma int_all_simps:
   286   "\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
   287   "\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
   288   "\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q"
   289   "\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))"
   290   by iprover+
   291 
   292 text \<open>Classical rules.\<close>
   293 lemma cla_all_simps:
   294   "\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
   295   "\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
   296   by blast+
   297 
   298 lemmas all_simps = int_all_simps cla_all_simps
   299 
   300 
   301 subsubsection \<open>Named rewrite rules proved for IFOL\<close>
   302 
   303 lemma imp_disj1: "(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
   304 lemma imp_disj2: "Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
   305 
   306 lemma de_Morgan_conj: "(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)" by blast
   307 
   308 lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)" by blast
   309 lemma not_iff: "\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
   310 
   311 lemma not_all: "(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))" by blast
   312 lemma imp_all: "((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)" by blast
   313 
   314 
   315 lemmas meta_simps =
   316   triv_forall_equality  \<comment> \<open>prunes params\<close>
   317   True_implies_equals  \<comment> \<open>prune asms \<open>True\<close>\<close>
   318 
   319 lemmas IFOL_simps =
   320   refl [THEN P_iff_T] conj_simps disj_simps not_simps
   321   imp_simps iff_simps quant_simps
   322 
   323 lemma notFalseI: "\<not> False" by iprover
   324 
   325 lemma cla_simps_misc:
   326   "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
   327   "P \<or> \<not> P"
   328   "\<not> P \<or> P"
   329   "\<not> \<not> P \<longleftrightarrow> P"
   330   "(\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
   331   "(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)" by blast+
   332 
   333 lemmas 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 
   338 ML_file "simpdata.ML"
   339 
   340 simproc_setup defined_Ex ("\<exists>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
   341 simproc_setup defined_All ("\<forall>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_all\<close>
   342 
   343 ML \<open>
   344 (*intuitionistic simprules only*)
   345 val 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 defined_All}, @{simproc defined_Ex}]
   349   |> Simplifier.add_cong @{thm imp_cong}
   350   |> simpset_of;
   351 
   352 (*classical simprules too*)
   353 val 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 
   359 setup \<open>
   360   map_theory_simpset (put_simpset FOL_ss) #>
   361   Simplifier.method_setup Splitter.split_modifiers
   362 \<close>
   363 
   364 ML_file "~~/src/Tools/eqsubst.ML"
   365 
   366 
   367 subsection \<open>Other simple lemmas\<close>
   368 
   369 lemma [simp]: "((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)"
   370   by blast
   371 
   372 lemma [simp]: "((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))"
   373   by blast
   374 
   375 lemma not_disj_iff_imp: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)"
   376   by blast
   377 
   378 
   379 subsubsection \<open>Monotonicity of implications\<close>
   380 
   381 lemma conj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)"
   382   by fast (*or (IntPr.fast_tac 1)*)
   383 
   384 lemma disj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)"
   385   by fast (*or (IntPr.fast_tac 1)*)
   386 
   387 lemma imp_mono: "\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)"
   388   by fast (*or (IntPr.fast_tac 1)*)
   389 
   390 lemma imp_refl: "P \<longrightarrow> P"
   391   by (rule impI)
   392 
   393 text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close>
   394 lemma ex_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
   395   by blast
   396 
   397 lemma all_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))"
   398   by blast
   399 
   400 
   401 subsection \<open>Proof by cases and induction\<close>
   402 
   403 text \<open>Proper handling of non-atomic rule statements.\<close>
   404 
   405 context
   406 begin
   407 
   408 qualified definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
   409 qualified definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
   410 qualified definition "induct_equal(x, y) \<equiv> x = y"
   411 qualified definition "induct_conj(A, B) \<equiv> A \<and> B"
   412 
   413 lemma induct_forall_eq: "(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))"
   414   unfolding atomize_all induct_forall_def .
   415 
   416 lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop(induct_implies(A, B))"
   417   unfolding atomize_imp induct_implies_def .
   418 
   419 lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop(induct_equal(x, y))"
   420   unfolding atomize_eq induct_equal_def .
   421 
   422 lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop(induct_conj(A, B))"
   423   unfolding atomize_conj induct_conj_def .
   424 
   425 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
   426 lemmas induct_rulify [symmetric] = induct_atomize
   427 lemmas induct_rulify_fallback =
   428   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   429 
   430 text \<open>Method setup.\<close>
   431 
   432 ML_file "~~/src/Tools/induct.ML"
   433 ML \<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 
   446 declare case_split [cases type: o]
   447 
   448 end
   449 
   450 ML_file "~~/src/Tools/case_product.ML"
   451 
   452 
   453 hide_const (open) eq
   454 
   455 end