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