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