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