src/HOL/ex/Higher_Order_Logic.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 14981 e73f8140af78
child 19380 b808efaa5828
permissions -rw-r--r--
migrated theory headers to new format
wenzelm@12360
     1
(*  Title:      HOL/ex/Higher_Order_Logic.thy
wenzelm@12360
     2
    ID:         $Id$
wenzelm@12360
     3
    Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
wenzelm@12360
     4
*)
wenzelm@12360
     5
wenzelm@12360
     6
header {* Foundations of HOL *}
wenzelm@12360
     7
haftmann@16417
     8
theory Higher_Order_Logic imports CPure begin
wenzelm@12360
     9
wenzelm@12360
    10
text {*
wenzelm@12360
    11
  The following theory development demonstrates Higher-Order Logic
wenzelm@12360
    12
  itself, represented directly within the Pure framework of Isabelle.
wenzelm@12360
    13
  The ``HOL'' logic given here is essentially that of Gordon
wenzelm@12360
    14
  \cite{Gordon:1985:HOL}, although we prefer to present basic concepts
wenzelm@12360
    15
  in a slightly more conventional manner oriented towards plain
wenzelm@12360
    16
  Natural Deduction.
wenzelm@12360
    17
*}
wenzelm@12360
    18
wenzelm@12360
    19
wenzelm@12360
    20
subsection {* Pure Logic *}
wenzelm@12360
    21
wenzelm@14854
    22
classes type
wenzelm@12360
    23
defaultsort type
wenzelm@12360
    24
wenzelm@12360
    25
typedecl o
wenzelm@12360
    26
arities
wenzelm@12360
    27
  o :: type
wenzelm@12360
    28
  fun :: (type, type) type
wenzelm@12360
    29
wenzelm@12360
    30
wenzelm@12360
    31
subsubsection {* Basic logical connectives *}
wenzelm@12360
    32
wenzelm@12360
    33
judgment
wenzelm@12360
    34
  Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
wenzelm@12360
    35
wenzelm@12360
    36
consts
wenzelm@12360
    37
  imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25)
wenzelm@12360
    38
  All :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<forall>" 10)
wenzelm@12360
    39
wenzelm@12360
    40
axioms
wenzelm@12360
    41
  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
wenzelm@12360
    42
  impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@12360
    43
  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
wenzelm@12360
    44
  allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
wenzelm@12360
    45
wenzelm@12360
    46
wenzelm@12360
    47
subsubsection {* Extensional equality *}
wenzelm@12360
    48
wenzelm@12360
    49
consts
wenzelm@12360
    50
  equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
wenzelm@12360
    51
wenzelm@12360
    52
axioms
wenzelm@12360
    53
  refl [intro]: "x = x"
wenzelm@12360
    54
  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
wenzelm@12360
    55
  ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
wenzelm@12360
    56
  iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
wenzelm@12360
    57
wenzelm@12394
    58
theorem sym [sym]: "x = y \<Longrightarrow> y = x"
wenzelm@12360
    59
proof -
wenzelm@12360
    60
  assume "x = y"
wenzelm@12360
    61
  thus "y = x" by (rule subst) (rule refl)
wenzelm@12360
    62
qed
wenzelm@12360
    63
wenzelm@12360
    64
lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
wenzelm@12360
    65
  by (rule subst) (rule sym)
wenzelm@12360
    66
wenzelm@12360
    67
lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"
wenzelm@12360
    68
  by (rule subst)
wenzelm@12360
    69
wenzelm@12360
    70
theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
wenzelm@12360
    71
  by (rule subst)
wenzelm@12360
    72
wenzelm@12360
    73
theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@12360
    74
  by (rule subst)
wenzelm@12360
    75
wenzelm@12360
    76
theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A"
wenzelm@12360
    77
  by (rule subst) (rule sym)
wenzelm@12360
    78
wenzelm@12360
    79
wenzelm@12360
    80
subsubsection {* Derived connectives *}
wenzelm@12360
    81
wenzelm@12360
    82
constdefs
wenzelm@12360
    83
  false :: o    ("\<bottom>")
wenzelm@12360
    84
  "\<bottom> \<equiv> \<forall>A. A"
wenzelm@12360
    85
  true :: o    ("\<top>")
wenzelm@12360
    86
  "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
wenzelm@12360
    87
  not :: "o \<Rightarrow> o"     ("\<not> _" [40] 40)
wenzelm@12360
    88
  "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
wenzelm@12360
    89
  conj :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<and>" 35)
wenzelm@12360
    90
  "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
    91
  disj :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<or>" 30)
wenzelm@12360
    92
  "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
    93
  Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<exists>" 10)
wenzelm@12360
    94
  "Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
    95
wenzelm@12360
    96
syntax
wenzelm@12360
    97
  "_not_equal" :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
wenzelm@12360
    98
translations
wenzelm@12360
    99
  "x \<noteq> y"  \<rightleftharpoons>  "\<not> (x = y)"
wenzelm@12360
   100
wenzelm@12360
   101
theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
wenzelm@12360
   102
proof (unfold false_def)
wenzelm@12360
   103
  assume "\<forall>A. A"
wenzelm@12360
   104
  thus A ..
wenzelm@12360
   105
qed
wenzelm@12360
   106
wenzelm@12360
   107
theorem trueI [intro]: \<top>
wenzelm@12360
   108
proof (unfold true_def)
wenzelm@12360
   109
  show "\<bottom> \<longrightarrow> \<bottom>" ..
wenzelm@12360
   110
qed
wenzelm@12360
   111
wenzelm@12360
   112
theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
wenzelm@12360
   113
proof (unfold not_def)
wenzelm@12360
   114
  assume "A \<Longrightarrow> \<bottom>"
wenzelm@12360
   115
  thus "A \<longrightarrow> \<bottom>" ..
wenzelm@12360
   116
qed
wenzelm@12360
   117
wenzelm@12360
   118
theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@12360
   119
proof (unfold not_def)
wenzelm@12360
   120
  assume "A \<longrightarrow> \<bottom>"
wenzelm@12360
   121
  also assume A
wenzelm@12360
   122
  finally have \<bottom> ..
wenzelm@12360
   123
  thus B ..
wenzelm@12360
   124
qed
wenzelm@12360
   125
wenzelm@12360
   126
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
wenzelm@12360
   127
  by (rule notE)
wenzelm@12360
   128
wenzelm@12360
   129
lemmas contradiction = notE notE'  -- {* proof by contradiction in any order *}
wenzelm@12360
   130
wenzelm@12360
   131
theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
wenzelm@12360
   132
proof (unfold conj_def)
wenzelm@12360
   133
  assume A and B
wenzelm@12360
   134
  show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   135
  proof
wenzelm@12360
   136
    fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   137
    proof
wenzelm@12360
   138
      assume "A \<longrightarrow> B \<longrightarrow> C"
wenzelm@12360
   139
      also have A .
wenzelm@12360
   140
      also have B .
wenzelm@12360
   141
      finally show C .
wenzelm@12360
   142
    qed
wenzelm@12360
   143
  qed
wenzelm@12360
   144
qed
wenzelm@12360
   145
wenzelm@12360
   146
theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@12360
   147
proof (unfold conj_def)
wenzelm@12360
   148
  assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   149
  assume "A \<Longrightarrow> B \<Longrightarrow> C"
wenzelm@12360
   150
  moreover {
wenzelm@12360
   151
    from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
wenzelm@12360
   152
    also have "A \<longrightarrow> B \<longrightarrow> A"
wenzelm@12360
   153
    proof
wenzelm@12360
   154
      assume A
wenzelm@12360
   155
      thus "B \<longrightarrow> A" ..
wenzelm@12360
   156
    qed
wenzelm@12360
   157
    finally have A .
wenzelm@12360
   158
  } moreover {
wenzelm@12360
   159
    from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
wenzelm@12360
   160
    also have "A \<longrightarrow> B \<longrightarrow> B"
wenzelm@12360
   161
    proof
wenzelm@12360
   162
      show "B \<longrightarrow> B" ..
wenzelm@12360
   163
    qed
wenzelm@12360
   164
    finally have B .
wenzelm@12360
   165
  } ultimately show C .
wenzelm@12360
   166
qed
wenzelm@12360
   167
wenzelm@12360
   168
theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
wenzelm@12360
   169
proof (unfold disj_def)
wenzelm@12360
   170
  assume A
wenzelm@12360
   171
  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   172
  proof
wenzelm@12360
   173
    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   174
    proof
wenzelm@12360
   175
      assume "A \<longrightarrow> C"
wenzelm@12360
   176
      also have A .
wenzelm@12360
   177
      finally have C .
wenzelm@12360
   178
      thus "(B \<longrightarrow> C) \<longrightarrow> C" ..
wenzelm@12360
   179
    qed
wenzelm@12360
   180
  qed
wenzelm@12360
   181
qed
wenzelm@12360
   182
wenzelm@12360
   183
theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
wenzelm@12360
   184
proof (unfold disj_def)
wenzelm@12360
   185
  assume B
wenzelm@12360
   186
  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   187
  proof
wenzelm@12360
   188
    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   189
    proof
wenzelm@12360
   190
      show "(B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   191
      proof
wenzelm@12360
   192
        assume "B \<longrightarrow> C"
wenzelm@12360
   193
        also have B .
wenzelm@12360
   194
        finally show C .
wenzelm@12360
   195
      qed
wenzelm@12360
   196
    qed
wenzelm@12360
   197
  qed
wenzelm@12360
   198
qed
wenzelm@12360
   199
wenzelm@12360
   200
theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@12360
   201
proof (unfold disj_def)
wenzelm@12360
   202
  assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   203
  assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
wenzelm@12360
   204
  from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
wenzelm@12360
   205
  also have "A \<longrightarrow> C"
wenzelm@12360
   206
  proof
wenzelm@12360
   207
    assume A thus C by (rule r1)
wenzelm@12360
   208
  qed
wenzelm@12360
   209
  also have "B \<longrightarrow> C"
wenzelm@12360
   210
  proof
wenzelm@12360
   211
    assume B thus C by (rule r2)
wenzelm@12360
   212
  qed
wenzelm@12360
   213
  finally show C .
wenzelm@12360
   214
qed
wenzelm@12360
   215
wenzelm@12360
   216
theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
wenzelm@12360
   217
proof (unfold Ex_def)
wenzelm@12360
   218
  assume "P a"
wenzelm@12360
   219
  show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   220
  proof
wenzelm@12360
   221
    fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   222
    proof
wenzelm@12360
   223
      assume "\<forall>x. P x \<longrightarrow> C"
wenzelm@12360
   224
      hence "P a \<longrightarrow> C" ..
wenzelm@12360
   225
      also have "P a" .
wenzelm@12360
   226
      finally show C .
wenzelm@12360
   227
    qed
wenzelm@12360
   228
  qed
wenzelm@12360
   229
qed
wenzelm@12360
   230
wenzelm@12360
   231
theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@12360
   232
proof (unfold Ex_def)
wenzelm@12360
   233
  assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   234
  assume r: "\<And>x. P x \<Longrightarrow> C"
wenzelm@12360
   235
  from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
wenzelm@12360
   236
  also have "\<forall>x. P x \<longrightarrow> C"
wenzelm@12360
   237
  proof
wenzelm@12360
   238
    fix x show "P x \<longrightarrow> C"
wenzelm@12360
   239
    proof
wenzelm@12360
   240
      assume "P x"
wenzelm@12360
   241
      thus C by (rule r)
wenzelm@12360
   242
    qed
wenzelm@12360
   243
  qed
wenzelm@12360
   244
  finally show C .
wenzelm@12360
   245
qed
wenzelm@12360
   246
wenzelm@12360
   247
wenzelm@12360
   248
subsection {* Classical logic *}
wenzelm@12360
   249
wenzelm@12360
   250
locale classical =
wenzelm@12360
   251
  assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
wenzelm@12360
   252
wenzelm@12360
   253
theorem (in classical)
wenzelm@12360
   254
  Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
wenzelm@12360
   255
proof
wenzelm@12360
   256
  assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
wenzelm@12360
   257
  show A
wenzelm@12360
   258
  proof (rule classical)
wenzelm@12360
   259
    assume "\<not> A"
wenzelm@12360
   260
    have "A \<longrightarrow> B"
wenzelm@12360
   261
    proof
wenzelm@12360
   262
      assume A
wenzelm@12360
   263
      thus B by (rule contradiction)
wenzelm@12360
   264
    qed
wenzelm@12360
   265
    with a show A ..
wenzelm@12360
   266
  qed
wenzelm@12360
   267
qed
wenzelm@12360
   268
wenzelm@12360
   269
theorem (in classical)
wenzelm@12360
   270
  double_negation: "\<not> \<not> A \<Longrightarrow> A"
wenzelm@12360
   271
proof -
wenzelm@12360
   272
  assume "\<not> \<not> A"
wenzelm@12360
   273
  show A
wenzelm@12360
   274
  proof (rule classical)
wenzelm@12360
   275
    assume "\<not> A"
wenzelm@12360
   276
    thus ?thesis by (rule contradiction)
wenzelm@12360
   277
  qed
wenzelm@12360
   278
qed
wenzelm@12360
   279
wenzelm@12360
   280
theorem (in classical)
wenzelm@12360
   281
  tertium_non_datur: "A \<or> \<not> A"
wenzelm@12360
   282
proof (rule double_negation)
wenzelm@12360
   283
  show "\<not> \<not> (A \<or> \<not> A)"
wenzelm@12360
   284
  proof
wenzelm@12360
   285
    assume "\<not> (A \<or> \<not> A)"
wenzelm@12360
   286
    have "\<not> A"
wenzelm@12360
   287
    proof
wenzelm@12360
   288
      assume A hence "A \<or> \<not> A" ..
wenzelm@12360
   289
      thus \<bottom> by (rule contradiction)
wenzelm@12360
   290
    qed
wenzelm@12360
   291
    hence "A \<or> \<not> A" ..
wenzelm@12360
   292
    thus \<bottom> by (rule contradiction)
wenzelm@12360
   293
  qed
wenzelm@12360
   294
qed
wenzelm@12360
   295
wenzelm@12360
   296
theorem (in classical)
wenzelm@12360
   297
  classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@12360
   298
proof -
wenzelm@12360
   299
  assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
wenzelm@12360
   300
  from tertium_non_datur show C
wenzelm@12360
   301
  proof
wenzelm@12360
   302
    assume A
wenzelm@12360
   303
    thus ?thesis by (rule r1)
wenzelm@12360
   304
  next
wenzelm@12360
   305
    assume "\<not> A"
wenzelm@12360
   306
    thus ?thesis by (rule r2)
wenzelm@12360
   307
  qed
wenzelm@12360
   308
qed
wenzelm@12360
   309
wenzelm@12573
   310
lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
wenzelm@12573
   311
proof -
wenzelm@12573
   312
  assume r: "\<not> A \<Longrightarrow> A"
wenzelm@12573
   313
  show A
wenzelm@12573
   314
  proof (rule classical_cases)
wenzelm@12573
   315
    assume A thus A .
wenzelm@12573
   316
  next
wenzelm@12573
   317
    assume "\<not> A" thus A by (rule r)
wenzelm@12573
   318
  qed
wenzelm@12573
   319
qed
wenzelm@12573
   320
wenzelm@12360
   321
end