src/HOL/ex/Hilbert_Classical.thy
author wenzelm
Thu Sep 27 15:41:48 2001 +0200 (2001-09-27)
changeset 11584 c8e98b9498b4
child 11590 14ae6a86813d
permissions -rw-r--r--
derive tertium-non-datur by means of Hilbert's choice operator;
wenzelm@11584
     1
(*  Title:      HOL/ex/Hilbert_Classical.thy
wenzelm@11584
     2
    ID:         $Id$
wenzelm@11584
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
wenzelm@11584
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@11584
     5
*)
wenzelm@11584
     6
wenzelm@11584
     7
header {* Hilbert's choice and classical logic *}
wenzelm@11584
     8
wenzelm@11584
     9
theory Hilbert_Classical = Main:
wenzelm@11584
    10
wenzelm@11584
    11
text {*
wenzelm@11584
    12
  Derivation of the classical law of tertium-non-datur by means of
wenzelm@11584
    13
  Hilbert's choice operator (due to M. J. Beeson and J. Harrison).
wenzelm@11584
    14
*}
wenzelm@11584
    15
wenzelm@11584
    16
wenzelm@11584
    17
subsection {* Proof text *}
wenzelm@11584
    18
wenzelm@11584
    19
theorem tnd: "P \<or> \<not> P"
wenzelm@11584
    20
proof -
wenzelm@11584
    21
  let ?A = "\<lambda>x. x = False \<or> x = True \<and> P"
wenzelm@11584
    22
  let ?B = "\<lambda>x. x = False \<and> P \<or> x = True"
wenzelm@11584
    23
  let ?f = "\<lambda>R. SOME y. R y"
wenzelm@11584
    24
wenzelm@11584
    25
  have a: "?A (?f ?A)"
wenzelm@11584
    26
  proof (rule someI)
wenzelm@11584
    27
    have "False = False" ..
wenzelm@11584
    28
    thus "?A False" ..
wenzelm@11584
    29
  qed
wenzelm@11584
    30
  have b: "?B (?f ?B)"
wenzelm@11584
    31
  proof (rule someI)
wenzelm@11584
    32
    have "True = True" ..
wenzelm@11584
    33
    thus "?B True" ..
wenzelm@11584
    34
  qed
wenzelm@11584
    35
wenzelm@11584
    36
  from a show ?thesis
wenzelm@11584
    37
  proof
wenzelm@11584
    38
    assume fa: "?f ?A = False"
wenzelm@11584
    39
    from b show ?thesis
wenzelm@11584
    40
    proof
wenzelm@11584
    41
      assume "?f ?B = False \<and> P"
wenzelm@11584
    42
      hence P ..
wenzelm@11584
    43
      thus ?thesis ..
wenzelm@11584
    44
    next
wenzelm@11584
    45
      assume fb: "?f ?B = True"
wenzelm@11584
    46
      have neq: "?A \<noteq> ?B"
wenzelm@11584
    47
      proof
wenzelm@11584
    48
	assume "?A = ?B" hence eq: "?f ?A = ?f ?B" by (rule arg_cong)
wenzelm@11584
    49
	from fa have "False = ?f ?A" ..
wenzelm@11584
    50
	also note eq
wenzelm@11584
    51
	also note fb
wenzelm@11584
    52
	finally have "False = True" .
wenzelm@11584
    53
	thus False by (rule False_neq_True)
wenzelm@11584
    54
      qed
wenzelm@11584
    55
      have "\<not> P"
wenzelm@11584
    56
      proof
wenzelm@11584
    57
	assume p: P
wenzelm@11584
    58
	have "?A = ?B"
wenzelm@11584
    59
	proof
wenzelm@11584
    60
	  fix x
wenzelm@11584
    61
	  show "?A x = ?B x"
wenzelm@11584
    62
	  proof
wenzelm@11584
    63
	    assume "?A x"
wenzelm@11584
    64
	    thus "?B x"
wenzelm@11584
    65
	    proof
wenzelm@11584
    66
	      assume "x = False"
wenzelm@11584
    67
	      from this and p
wenzelm@11584
    68
	      have "x = False \<and> P" ..
wenzelm@11584
    69
	      thus "?B x" ..
wenzelm@11584
    70
	    next
wenzelm@11584
    71
	      assume "x = True \<and> P"
wenzelm@11584
    72
	      hence "x = True" ..
wenzelm@11584
    73
	      thus "?B x" ..
wenzelm@11584
    74
	    qed
wenzelm@11584
    75
	  next
wenzelm@11584
    76
	    assume "?B x"
wenzelm@11584
    77
	    thus "?A x"
wenzelm@11584
    78
	    proof
wenzelm@11584
    79
	      assume "x = False \<and> P"
wenzelm@11584
    80
	      hence "x = False" ..
wenzelm@11584
    81
	      thus "?A x" ..
wenzelm@11584
    82
	    next
wenzelm@11584
    83
	      assume "x = True"
wenzelm@11584
    84
	      from this and p
wenzelm@11584
    85
	      have "x = True \<and> P" ..
wenzelm@11584
    86
	      thus "?A x" ..
wenzelm@11584
    87
	    qed
wenzelm@11584
    88
	  qed
wenzelm@11584
    89
	qed
wenzelm@11584
    90
	with neq show False by contradiction
wenzelm@11584
    91
      qed
wenzelm@11584
    92
      thus ?thesis ..
wenzelm@11584
    93
    qed
wenzelm@11584
    94
  next
wenzelm@11584
    95
    assume "?f ?A = True \<and> P" hence P ..
wenzelm@11584
    96
    thus ?thesis ..
wenzelm@11584
    97
  qed
wenzelm@11584
    98
qed
wenzelm@11584
    99
wenzelm@11584
   100
wenzelm@11584
   101
subsection {* Proof script *}
wenzelm@11584
   102
wenzelm@11584
   103
theorem tnd': "P \<or> \<not> P"
wenzelm@11584
   104
  apply (subgoal_tac
wenzelm@11584
   105
    "(((SOME x. x = False \<or> x = True \<and> P) = False) \<or>
wenzelm@11584
   106
      ((SOME x. x = False \<or> x = True \<and> P) = True) \<and> P) \<and>
wenzelm@11584
   107
     (((SOME x. x = False \<and> P \<or> x = True) = False) \<and> P \<or>
wenzelm@11584
   108
      ((SOME x. x = False \<and> P \<or> x = True) = True))")
wenzelm@11584
   109
  prefer 2
wenzelm@11584
   110
  apply (rule conjI)
wenzelm@11584
   111
  apply (rule someI)
wenzelm@11584
   112
  apply (rule disjI1)
wenzelm@11584
   113
  apply (rule refl)
wenzelm@11584
   114
  apply (rule someI)
wenzelm@11584
   115
  apply (rule disjI2)
wenzelm@11584
   116
  apply (rule refl)
wenzelm@11584
   117
  apply (erule conjE)
wenzelm@11584
   118
  apply (erule disjE)
wenzelm@11584
   119
  apply (erule disjE)
wenzelm@11584
   120
  apply (erule conjE)
wenzelm@11584
   121
  apply (erule disjI1)
wenzelm@11584
   122
  prefer 2
wenzelm@11584
   123
  apply (erule conjE)
wenzelm@11584
   124
  apply (erule disjI1)
wenzelm@11584
   125
  apply (subgoal_tac
wenzelm@11584
   126
    "(\<lambda>x. (x = False) \<or> (x = True) \<and> P) \<noteq>
wenzelm@11584
   127
     (\<lambda>x. (x = False) \<and> P \<or> (x = True))")
wenzelm@11584
   128
  prefer 2
wenzelm@11584
   129
  apply (rule notI)
wenzelm@11584
   130
  apply (drule_tac f="\<lambda>y. SOME x. y x" in arg_cong)
wenzelm@11584
   131
  apply (drule trans, assumption)
wenzelm@11584
   132
  apply (drule sym)
wenzelm@11584
   133
  apply (drule trans, assumption)
wenzelm@11584
   134
  apply (erule False_neq_True)
wenzelm@11584
   135
  apply (rule disjI2)
wenzelm@11584
   136
  apply (rule notI)
wenzelm@11584
   137
  apply (erule notE)
wenzelm@11584
   138
  apply (rule ext)
wenzelm@11584
   139
  apply (rule iffI)
wenzelm@11584
   140
  apply (erule disjE)
wenzelm@11584
   141
  apply (rule disjI1)
wenzelm@11584
   142
  apply (erule conjI)
wenzelm@11584
   143
  apply assumption
wenzelm@11584
   144
  apply (erule conjE)
wenzelm@11584
   145
  apply (erule disjI2)
wenzelm@11584
   146
  apply (erule disjE)
wenzelm@11584
   147
  apply (erule conjE)
wenzelm@11584
   148
  apply (erule disjI1)
wenzelm@11584
   149
  apply (rule disjI2)
wenzelm@11584
   150
  apply (erule conjI)
wenzelm@11584
   151
  apply assumption
wenzelm@11584
   152
  done
wenzelm@11584
   153
wenzelm@11584
   154
wenzelm@11584
   155
subsection {* Proof term of text *}
wenzelm@11584
   156
wenzelm@11584
   157
text {*
wenzelm@11584
   158
  @{prf [display] tnd}
wenzelm@11584
   159
*}
wenzelm@11584
   160
wenzelm@11584
   161
wenzelm@11584
   162
subsection {* Proof term of script *}
wenzelm@11584
   163
wenzelm@11584
   164
text {*
wenzelm@11584
   165
  @{prf [display] tnd'}
wenzelm@11584
   166
*}
wenzelm@11584
   167
wenzelm@11584
   168
end