src/HOL/Isar_Examples/Higher_Order_Logic.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 64908 f94ad67a0f6e
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned;
wenzelm@61935
     1
(*  Title:      HOL/Isar_Examples/Higher_Order_Logic.thy
wenzelm@61759
     2
    Author:     Makarius
wenzelm@12360
     3
*)
wenzelm@12360
     4
wenzelm@59031
     5
section \<open>Foundations of HOL\<close>
wenzelm@12360
     6
wenzelm@60769
     7
theory Higher_Order_Logic
wenzelm@63585
     8
  imports Pure
wenzelm@60769
     9
begin
wenzelm@12360
    10
wenzelm@59031
    11
text \<open>
wenzelm@64907
    12
  The following theory development illustrates the foundations of Higher-Order
wenzelm@64907
    13
  Logic. The ``HOL'' logic that is given here resembles @{cite
wenzelm@64907
    14
  "Gordon:1985:HOL"} and its predecessor @{cite "church40"}, but the order of
wenzelm@64907
    15
  axiomatizations and defined connectives has be adapted to modern
wenzelm@64907
    16
  presentations of \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus it fits
wenzelm@64907
    17
  nicely to the underlying Natural Deduction framework of Isabelle/Pure and
wenzelm@64907
    18
  Isabelle/Isar.
wenzelm@59031
    19
\<close>
wenzelm@12360
    20
wenzelm@12360
    21
wenzelm@64907
    22
section \<open>HOL syntax within Pure\<close>
wenzelm@12360
    23
wenzelm@55380
    24
class type
wenzelm@36452
    25
default_sort type
wenzelm@12360
    26
wenzelm@12360
    27
typedecl o
wenzelm@55380
    28
instance o :: type ..
wenzelm@55380
    29
instance "fun" :: (type, type) type ..
wenzelm@12360
    30
wenzelm@64907
    31
judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
wenzelm@12360
    32
wenzelm@12360
    33
wenzelm@64907
    34
section \<open>Minimal logic (axiomatization)\<close>
wenzelm@12360
    35
wenzelm@61759
    36
axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
wenzelm@61759
    37
  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
wenzelm@61759
    38
    and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@61759
    39
wenzelm@61759
    40
axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
wenzelm@61759
    41
  where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
wenzelm@61759
    42
    and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
wenzelm@12360
    43
wenzelm@64907
    44
lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
wenzelm@64907
    45
  by standard (fact impI, fact impE)
wenzelm@12360
    46
wenzelm@64907
    47
lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
wenzelm@64907
    48
  by standard (fact allI, fact allE)
wenzelm@12360
    49
wenzelm@12360
    50
wenzelm@59031
    51
subsubsection \<open>Derived connectives\<close>
wenzelm@12360
    52
wenzelm@64907
    53
definition False :: o
wenzelm@64907
    54
  where "False \<equiv> \<forall>A. A"
wenzelm@21404
    55
wenzelm@64907
    56
lemma FalseE [elim]:
wenzelm@64907
    57
  assumes "False"
wenzelm@61759
    58
  shows A
wenzelm@61759
    59
proof -
wenzelm@64907
    60
  from \<open>False\<close> have "\<forall>A. A" by (simp only: False_def)
wenzelm@61759
    61
  then show A ..
wenzelm@61759
    62
qed
wenzelm@61759
    63
wenzelm@61759
    64
wenzelm@64907
    65
definition True :: o
wenzelm@64907
    66
  where "True \<equiv> False \<longrightarrow> False"
wenzelm@21404
    67
wenzelm@64907
    68
lemma TrueI [intro]: True
wenzelm@64907
    69
  unfolding True_def ..
wenzelm@61759
    70
wenzelm@61759
    71
wenzelm@59031
    72
definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
wenzelm@64907
    73
  where "not \<equiv> \<lambda>A. A \<longrightarrow> False"
wenzelm@21404
    74
wenzelm@64907
    75
lemma notI [intro]:
wenzelm@64907
    76
  assumes "A \<Longrightarrow> False"
wenzelm@61759
    77
  shows "\<not> A"
wenzelm@61759
    78
  using assms unfolding not_def ..
wenzelm@12360
    79
wenzelm@64907
    80
lemma notE [elim]:
wenzelm@61759
    81
  assumes "\<not> A" and A
wenzelm@61759
    82
  shows B
wenzelm@61759
    83
proof -
wenzelm@64907
    84
  from \<open>\<not> A\<close> have "A \<longrightarrow> False" by (simp only: not_def)
wenzelm@64907
    85
  from this and \<open>A\<close> have "False" ..
wenzelm@23373
    86
  then show B ..
wenzelm@12360
    87
qed
wenzelm@12360
    88
wenzelm@12360
    89
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
wenzelm@12360
    90
  by (rule notE)
wenzelm@12360
    91
wenzelm@61759
    92
lemmas contradiction = notE notE'  \<comment> \<open>proof by contradiction in any order\<close>
wenzelm@61759
    93
wenzelm@61759
    94
wenzelm@61759
    95
definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
wenzelm@64907
    96
  where "A \<and> B \<equiv> \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
    97
wenzelm@64907
    98
lemma conjI [intro]:
wenzelm@61759
    99
  assumes A and B
wenzelm@61759
   100
  shows "A \<and> B"
wenzelm@61759
   101
  unfolding conj_def
wenzelm@61759
   102
proof
wenzelm@61759
   103
  fix C
wenzelm@61759
   104
  show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   105
  proof
wenzelm@61759
   106
    assume "A \<longrightarrow> B \<longrightarrow> C"
wenzelm@61759
   107
    also note \<open>A\<close>
wenzelm@61759
   108
    also note \<open>B\<close>
wenzelm@61759
   109
    finally show C .
wenzelm@12360
   110
  qed
wenzelm@12360
   111
qed
wenzelm@12360
   112
wenzelm@64907
   113
lemma conjE [elim]:
wenzelm@61759
   114
  assumes "A \<and> B"
wenzelm@61759
   115
  obtains A and B
wenzelm@61759
   116
proof
wenzelm@61759
   117
  from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
wenzelm@61759
   118
    unfolding conj_def ..
wenzelm@61759
   119
  show A
wenzelm@61759
   120
  proof -
wenzelm@61759
   121
    note * [of A]
wenzelm@12360
   122
    also have "A \<longrightarrow> B \<longrightarrow> A"
wenzelm@12360
   123
    proof
wenzelm@12360
   124
      assume A
wenzelm@23373
   125
      then show "B \<longrightarrow> A" ..
wenzelm@12360
   126
    qed
wenzelm@61759
   127
    finally show ?thesis .
wenzelm@61759
   128
  qed
wenzelm@61759
   129
  show B
wenzelm@61759
   130
  proof -
wenzelm@61759
   131
    note * [of B]
wenzelm@12360
   132
    also have "A \<longrightarrow> B \<longrightarrow> B"
wenzelm@12360
   133
    proof
wenzelm@12360
   134
      show "B \<longrightarrow> B" ..
wenzelm@12360
   135
    qed
wenzelm@61759
   136
    finally show ?thesis .
wenzelm@12360
   137
  qed
wenzelm@12360
   138
qed
wenzelm@12360
   139
wenzelm@61759
   140
wenzelm@61759
   141
definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
wenzelm@64907
   142
  where "A \<or> B \<equiv> \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@61759
   143
wenzelm@64907
   144
lemma disjI1 [intro]:
wenzelm@61759
   145
  assumes A
wenzelm@61759
   146
  shows "A \<or> B"
wenzelm@61759
   147
  unfolding disj_def
wenzelm@61759
   148
proof
wenzelm@61759
   149
  fix C
wenzelm@61759
   150
  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   151
  proof
wenzelm@61759
   152
    assume "A \<longrightarrow> C"
wenzelm@61759
   153
    from this and \<open>A\<close> have C ..
wenzelm@61759
   154
    then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
wenzelm@61759
   155
  qed
wenzelm@61759
   156
qed
wenzelm@61759
   157
wenzelm@64907
   158
lemma disjI2 [intro]:
wenzelm@61759
   159
  assumes B
wenzelm@61759
   160
  shows "A \<or> B"
wenzelm@61759
   161
  unfolding disj_def
wenzelm@61759
   162
proof
wenzelm@61759
   163
  fix C
wenzelm@61759
   164
  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@61759
   165
  proof
wenzelm@61759
   166
    show "(B \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   167
    proof
wenzelm@61759
   168
      assume "B \<longrightarrow> C"
wenzelm@61759
   169
      from this and \<open>B\<close> show C ..
wenzelm@12360
   170
    qed
wenzelm@12360
   171
  qed
wenzelm@12360
   172
qed
wenzelm@12360
   173
wenzelm@64907
   174
lemma disjE [elim]:
wenzelm@61759
   175
  assumes "A \<or> B"
wenzelm@61759
   176
  obtains (a) A | (b) B
wenzelm@61759
   177
proof -
wenzelm@61759
   178
  from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
wenzelm@61759
   179
    unfolding disj_def ..
wenzelm@61759
   180
  also have "A \<longrightarrow> thesis"
wenzelm@12360
   181
  proof
wenzelm@60769
   182
    assume A
wenzelm@61759
   183
    then show thesis by (rule a)
wenzelm@12360
   184
  qed
wenzelm@61759
   185
  also have "B \<longrightarrow> thesis"
wenzelm@12360
   186
  proof
wenzelm@60769
   187
    assume B
wenzelm@61759
   188
    then show thesis by (rule b)
wenzelm@12360
   189
  qed
wenzelm@61759
   190
  finally show thesis .
wenzelm@12360
   191
qed
wenzelm@12360
   192
wenzelm@61759
   193
wenzelm@61759
   194
definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
wenzelm@61759
   195
  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@61759
   196
wenzelm@64907
   197
lemma exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
wenzelm@61759
   198
  unfolding Ex_def
wenzelm@61759
   199
proof
wenzelm@61759
   200
  fix C
wenzelm@12360
   201
  assume "P a"
wenzelm@61759
   202
  show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
wenzelm@12360
   203
  proof
wenzelm@61759
   204
    assume "\<forall>x. P x \<longrightarrow> C"
wenzelm@61759
   205
    then have "P a \<longrightarrow> C" ..
wenzelm@61759
   206
    from this and \<open>P a\<close> show C ..
wenzelm@12360
   207
  qed
wenzelm@12360
   208
qed
wenzelm@12360
   209
wenzelm@64907
   210
lemma exE [elim]:
wenzelm@61759
   211
  assumes "\<exists>x. P x"
wenzelm@61759
   212
  obtains (that) x where "P x"
wenzelm@61759
   213
proof -
wenzelm@61759
   214
  from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
wenzelm@61759
   215
    unfolding Ex_def ..
wenzelm@61759
   216
  also have "\<forall>x. P x \<longrightarrow> thesis"
wenzelm@12360
   217
  proof
wenzelm@61759
   218
    fix x
wenzelm@61759
   219
    show "P x \<longrightarrow> thesis"
wenzelm@12360
   220
    proof
wenzelm@12360
   221
      assume "P x"
wenzelm@61759
   222
      then show thesis by (rule that)
wenzelm@12360
   223
    qed
wenzelm@12360
   224
  qed
wenzelm@61759
   225
  finally show thesis .
wenzelm@12360
   226
qed
wenzelm@12360
   227
wenzelm@12360
   228
wenzelm@64907
   229
subsubsection \<open>Extensional equality\<close>
wenzelm@64907
   230
wenzelm@64907
   231
axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "=" 50)
wenzelm@64907
   232
  where refl [intro]: "x = x"
wenzelm@64907
   233
    and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
wenzelm@64907
   234
wenzelm@64907
   235
abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
wenzelm@64907
   236
  where "x \<noteq> y \<equiv> \<not> (x = y)"
wenzelm@64907
   237
wenzelm@64907
   238
abbreviation iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25)
wenzelm@64907
   239
  where "A \<longleftrightarrow> B \<equiv> A = B"
wenzelm@64907
   240
wenzelm@64907
   241
axiomatization
wenzelm@64907
   242
  where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
wenzelm@64907
   243
    and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"
wenzelm@64907
   244
wenzelm@64907
   245
lemma sym [sym]: "y = x" if "x = y"
wenzelm@64907
   246
  using that by (rule subst) (rule refl)
wenzelm@64907
   247
wenzelm@64907
   248
lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
wenzelm@64907
   249
  by (rule subst) (rule sym)
wenzelm@64907
   250
wenzelm@64907
   251
lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"
wenzelm@64907
   252
  by (rule subst)
wenzelm@64907
   253
wenzelm@64907
   254
lemma arg_cong: "f x = f y" if "x = y"
wenzelm@64907
   255
  using that by (rule subst) (rule refl)
wenzelm@64907
   256
wenzelm@64907
   257
lemma fun_cong: "f x = g x" if "f = g"
wenzelm@64907
   258
  using that by (rule subst) (rule refl)
wenzelm@64907
   259
wenzelm@64907
   260
lemma trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
wenzelm@64907
   261
  by (rule subst)
wenzelm@64907
   262
wenzelm@64907
   263
lemma iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
wenzelm@64907
   264
  by (rule subst)
wenzelm@64907
   265
wenzelm@64907
   266
lemma iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
wenzelm@64907
   267
  by (rule subst) (rule sym)
wenzelm@64907
   268
wenzelm@64907
   269
wenzelm@61936
   270
subsection \<open>Cantor's Theorem\<close>
wenzelm@61936
   271
wenzelm@61936
   272
text \<open>
wenzelm@61936
   273
  Cantor's Theorem states that there is no surjection from a set to its
wenzelm@61936
   274
  powerset. The subsequent formulation uses elementary \<open>\<lambda>\<close>-calculus and
wenzelm@61936
   275
  predicate logic, with standard introduction and elimination rules.
wenzelm@61936
   276
\<close>
wenzelm@61936
   277
wenzelm@61936
   278
lemma iff_contradiction:
wenzelm@61936
   279
  assumes *: "\<not> A \<longleftrightarrow> A"
wenzelm@61936
   280
  shows C
wenzelm@61936
   281
proof (rule notE)
wenzelm@61936
   282
  show "\<not> A"
wenzelm@61936
   283
  proof
wenzelm@61936
   284
    assume A
wenzelm@61936
   285
    with * have "\<not> A" ..
wenzelm@64907
   286
    from this and \<open>A\<close> show False ..
wenzelm@61936
   287
  qed
wenzelm@61936
   288
  with * show A ..
wenzelm@61936
   289
qed
wenzelm@61936
   290
wenzelm@62038
   291
theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x)"
wenzelm@61936
   292
proof
wenzelm@61936
   293
  assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x"
wenzelm@61936
   294
  then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> o" where *: "\<forall>A. \<exists>x. A = f x" ..
wenzelm@61936
   295
  let ?D = "\<lambda>x. \<not> f x x"
wenzelm@61936
   296
  from * have "\<exists>x. ?D = f x" ..
wenzelm@61936
   297
  then obtain a where "?D = f a" ..
wenzelm@61936
   298
  then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst)
wenzelm@62266
   299
  then have "\<not> f a a \<longleftrightarrow> f a a" .
wenzelm@64907
   300
  then show False by (rule iff_contradiction)
wenzelm@61936
   301
qed
wenzelm@61936
   302
wenzelm@61936
   303
wenzelm@64907
   304
subsection \<open>Characterization of Classical Logic\<close>
wenzelm@12360
   305
wenzelm@61759
   306
text \<open>
wenzelm@61759
   307
  The subsequent rules of classical reasoning are all equivalent.
wenzelm@61759
   308
\<close>
wenzelm@61759
   309
wenzelm@12360
   310
locale classical =
wenzelm@12360
   311
  assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
wenzelm@64907
   312
  \<comment> \<open>predicate definition and hypothetical context\<close>
wenzelm@64907
   313
begin
wenzelm@12360
   314
wenzelm@64908
   315
lemma classical_contradiction:
wenzelm@64908
   316
  assumes "\<not> A \<Longrightarrow> False"
wenzelm@64908
   317
  shows A
wenzelm@64908
   318
proof (rule classical)
wenzelm@64908
   319
  assume "\<not> A"
wenzelm@64908
   320
  then have False by (rule assms)
wenzelm@64908
   321
  then show A ..
wenzelm@12360
   322
qed
wenzelm@12360
   323
wenzelm@64907
   324
lemma double_negation:
wenzelm@61759
   325
  assumes "\<not> \<not> A"
wenzelm@61759
   326
  shows A
wenzelm@64908
   327
proof (rule classical_contradiction)
wenzelm@61759
   328
  assume "\<not> A"
wenzelm@64908
   329
  with \<open>\<not> \<not> A\<close> show False by (rule contradiction)
wenzelm@12360
   330
qed
wenzelm@12360
   331
wenzelm@64907
   332
lemma tertium_non_datur: "A \<or> \<not> A"
wenzelm@12360
   333
proof (rule double_negation)
wenzelm@12360
   334
  show "\<not> \<not> (A \<or> \<not> A)"
wenzelm@12360
   335
  proof
wenzelm@12360
   336
    assume "\<not> (A \<or> \<not> A)"
wenzelm@12360
   337
    have "\<not> A"
wenzelm@12360
   338
    proof
wenzelm@23373
   339
      assume A then have "A \<or> \<not> A" ..
wenzelm@64907
   340
      with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
wenzelm@12360
   341
    qed
wenzelm@23373
   342
    then have "A \<or> \<not> A" ..
wenzelm@64907
   343
    with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
wenzelm@12360
   344
  qed
wenzelm@12360
   345
qed
wenzelm@12360
   346
wenzelm@64907
   347
lemma classical_cases:
wenzelm@61759
   348
  obtains A | "\<not> A"
wenzelm@61759
   349
  using tertium_non_datur
wenzelm@61759
   350
proof
wenzelm@61759
   351
  assume A
wenzelm@61759
   352
  then show thesis ..
wenzelm@61759
   353
next
wenzelm@61759
   354
  assume "\<not> A"
wenzelm@61759
   355
  then show thesis ..
wenzelm@61759
   356
qed
wenzelm@61759
   357
wenzelm@64907
   358
end
wenzelm@64907
   359
wenzelm@64907
   360
lemma classical_if_cases: classical
wenzelm@64907
   361
  if cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@61759
   362
proof
wenzelm@61759
   363
  fix A
wenzelm@61759
   364
  assume *: "\<not> A \<Longrightarrow> A"
wenzelm@61759
   365
  show A
wenzelm@64907
   366
  proof (rule cases)
wenzelm@12360
   367
    assume A
wenzelm@61759
   368
    then show A .
wenzelm@12360
   369
  next
wenzelm@12360
   370
    assume "\<not> A"
wenzelm@61759
   371
    then show A by (rule *)
wenzelm@12573
   372
  qed
wenzelm@12573
   373
qed
wenzelm@12573
   374
wenzelm@64907
   375
wenzelm@64908
   376
section \<open>Peirce's Law\<close>
wenzelm@64908
   377
wenzelm@64908
   378
text \<open>
wenzelm@64908
   379
  Peirce's Law is another characterization of classical reasoning. Its
wenzelm@64908
   380
  statement only requires implication.
wenzelm@64908
   381
\<close>
wenzelm@64908
   382
wenzelm@64908
   383
theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
wenzelm@64908
   384
proof
wenzelm@64908
   385
  assume *: "(A \<longrightarrow> B) \<longrightarrow> A"
wenzelm@64908
   386
  show A
wenzelm@64908
   387
  proof (rule classical)
wenzelm@64908
   388
    assume "\<not> A"
wenzelm@64908
   389
    have "A \<longrightarrow> B"
wenzelm@64908
   390
    proof
wenzelm@64908
   391
      assume A
wenzelm@64908
   392
      with \<open>\<not> A\<close> show B by (rule contradiction)
wenzelm@64908
   393
    qed
wenzelm@64908
   394
    with * show A ..
wenzelm@64908
   395
  qed
wenzelm@64908
   396
qed
wenzelm@64908
   397
wenzelm@64908
   398
wenzelm@64907
   399
section \<open>Hilbert's choice operator (axiomatization)\<close>
wenzelm@64907
   400
wenzelm@64907
   401
axiomatization Eps :: "('a \<Rightarrow> o) \<Rightarrow> 'a"
wenzelm@64907
   402
  where someI: "P x \<Longrightarrow> P (Eps P)"
wenzelm@64907
   403
wenzelm@64907
   404
syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a"  ("(3SOME _./ _)" [0, 10] 10)
wenzelm@64907
   405
translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
wenzelm@64907
   406
wenzelm@64907
   407
text \<open>
wenzelm@64907
   408
  \<^medskip>
wenzelm@64907
   409
  It follows a derivation of the classical law of tertium-non-datur by
wenzelm@64907
   410
  means of Hilbert's choice operator (due to Berghofer, Beeson, Harrison,
wenzelm@64907
   411
  based on a proof by Diaconescu).
wenzelm@64907
   412
  \<^medskip>
wenzelm@64907
   413
\<close>
wenzelm@64907
   414
wenzelm@64907
   415
theorem Diaconescu: "A \<or> \<not> A"
wenzelm@64907
   416
proof -
wenzelm@64907
   417
  let ?P = "\<lambda>x. (A \<and> x) \<or> \<not> x"
wenzelm@64907
   418
  let ?Q = "\<lambda>x. (A \<and> \<not> x) \<or> x"
wenzelm@64907
   419
wenzelm@64907
   420
  have a: "?P (Eps ?P)"
wenzelm@64907
   421
  proof (rule someI)
wenzelm@64907
   422
    have "\<not> False" ..
wenzelm@64907
   423
    then show "?P False" ..
wenzelm@64907
   424
  qed
wenzelm@64907
   425
  have b: "?Q (Eps ?Q)"
wenzelm@64907
   426
  proof (rule someI)
wenzelm@64907
   427
    have True ..
wenzelm@64907
   428
    then show "?Q True" ..
wenzelm@64907
   429
  qed
wenzelm@64907
   430
wenzelm@64907
   431
  from a show ?thesis
wenzelm@64907
   432
  proof
wenzelm@64907
   433
    assume "A \<and> Eps ?P"
wenzelm@64907
   434
    then have A ..
wenzelm@64907
   435
    then show ?thesis ..
wenzelm@64907
   436
  next
wenzelm@64907
   437
    assume "\<not> Eps ?P"
wenzelm@64907
   438
    from b show ?thesis
wenzelm@64907
   439
    proof
wenzelm@64907
   440
      assume "A \<and> \<not> Eps ?Q"
wenzelm@64907
   441
      then have A ..
wenzelm@64907
   442
      then show ?thesis ..
wenzelm@64907
   443
    next
wenzelm@64907
   444
      assume "Eps ?Q"
wenzelm@64907
   445
      have neq: "?P \<noteq> ?Q"
wenzelm@64907
   446
      proof
wenzelm@64907
   447
        assume "?P = ?Q"
wenzelm@64907
   448
        then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong)
wenzelm@64907
   449
        also note \<open>Eps ?Q\<close>
wenzelm@64907
   450
        finally have "Eps ?P" .
wenzelm@64907
   451
        with \<open>\<not> Eps ?P\<close> show False by (rule contradiction)
wenzelm@64907
   452
      qed
wenzelm@64907
   453
      have "\<not> A"
wenzelm@64907
   454
      proof
wenzelm@64907
   455
        assume A
wenzelm@64907
   456
        have "?P = ?Q"
wenzelm@64907
   457
        proof (rule ext)
wenzelm@64907
   458
          show "?P x \<longleftrightarrow> ?Q x" for x
wenzelm@64907
   459
          proof
wenzelm@64907
   460
            assume "?P x"
wenzelm@64907
   461
            then show "?Q x"
wenzelm@64907
   462
            proof
wenzelm@64907
   463
              assume "\<not> x"
wenzelm@64907
   464
              with \<open>A\<close> have "A \<and> \<not> x" ..
wenzelm@64907
   465
              then show ?thesis ..
wenzelm@64907
   466
            next
wenzelm@64907
   467
              assume "A \<and> x"
wenzelm@64907
   468
              then have x ..
wenzelm@64907
   469
              then show ?thesis ..
wenzelm@64907
   470
            qed
wenzelm@64907
   471
          next
wenzelm@64907
   472
            assume "?Q x"
wenzelm@64907
   473
            then show "?P x"
wenzelm@64907
   474
            proof
wenzelm@64907
   475
              assume "A \<and> \<not> x"
wenzelm@64907
   476
              then have "\<not> x" ..
wenzelm@64907
   477
              then show ?thesis ..
wenzelm@64907
   478
            next
wenzelm@64907
   479
              assume x
wenzelm@64907
   480
              with \<open>A\<close> have "A \<and> x" ..
wenzelm@64907
   481
              then show ?thesis ..
wenzelm@64907
   482
            qed
wenzelm@64907
   483
          qed
wenzelm@64907
   484
        qed
wenzelm@64907
   485
        with neq show False by (rule contradiction)
wenzelm@64907
   486
      qed
wenzelm@64907
   487
      then show ?thesis ..
wenzelm@64907
   488
    qed
wenzelm@64907
   489
  qed
wenzelm@64907
   490
qed
wenzelm@64907
   491
wenzelm@64907
   492
text \<open>
wenzelm@64907
   493
  This means, the hypothetical predicate @{const classical} always holds
wenzelm@64907
   494
  unconditionally (with all consequences).
wenzelm@64907
   495
\<close>
wenzelm@64907
   496
wenzelm@64907
   497
interpretation classical
wenzelm@64907
   498
proof (rule classical_if_cases)
wenzelm@64907
   499
  fix A C
wenzelm@64907
   500
  assume *: "A \<Longrightarrow> C"
wenzelm@64907
   501
    and **: "\<not> A \<Longrightarrow> C"
wenzelm@64907
   502
  from Diaconescu [of A] show C
wenzelm@64907
   503
  proof
wenzelm@64907
   504
    assume A
wenzelm@64907
   505
    then show C by (rule *)
wenzelm@64907
   506
  next
wenzelm@64907
   507
    assume "\<not> A"
wenzelm@64907
   508
    then show C by (rule **)
wenzelm@64907
   509
  qed
wenzelm@64907
   510
qed
wenzelm@64907
   511
wenzelm@64907
   512
thm classical
wenzelm@64908
   513
  classical_contradiction
wenzelm@64907
   514
  double_negation
wenzelm@64907
   515
  tertium_non_datur
wenzelm@64907
   516
  classical_cases
wenzelm@64908
   517
  Peirce's_Law
wenzelm@64907
   518
wenzelm@12360
   519
end