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