src/HOL/ex/Hilbert_Classical.thy
author wenzelm
Fri Sep 28 20:08:05 2001 +0200 (2001-09-28)
changeset 11635 fd242f857508
parent 11591 4b171ad4ff65
child 14981 e73f8140af78
permissions -rw-r--r--
tuned;
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@11591
    19
theorem tnd: "A \<or> \<not> A"
wenzelm@11584
    20
proof -
wenzelm@11590
    21
  let ?P = "\<lambda>X. X = False \<or> X = True \<and> A"
wenzelm@11590
    22
  let ?Q = "\<lambda>X. X = False \<and> A \<or> X = True"
wenzelm@11584
    23
wenzelm@11590
    24
  have a: "?P (Eps ?P)"
wenzelm@11584
    25
  proof (rule someI)
wenzelm@11584
    26
    have "False = False" ..
wenzelm@11590
    27
    thus "?P False" ..
wenzelm@11584
    28
  qed
wenzelm@11590
    29
  have b: "?Q (Eps ?Q)"
wenzelm@11584
    30
  proof (rule someI)
wenzelm@11584
    31
    have "True = True" ..
wenzelm@11590
    32
    thus "?Q True" ..
wenzelm@11584
    33
  qed
wenzelm@11584
    34
wenzelm@11584
    35
  from a show ?thesis
wenzelm@11584
    36
  proof
wenzelm@11590
    37
    assume "Eps ?P = True \<and> A"
wenzelm@11590
    38
    hence A ..
wenzelm@11590
    39
    thus ?thesis ..
wenzelm@11590
    40
  next
wenzelm@11590
    41
    assume P: "Eps ?P = False"
wenzelm@11584
    42
    from b show ?thesis
wenzelm@11584
    43
    proof
wenzelm@11590
    44
      assume "Eps ?Q = False \<and> A"
wenzelm@11590
    45
      hence A ..
wenzelm@11584
    46
      thus ?thesis ..
wenzelm@11584
    47
    next
wenzelm@11590
    48
      assume Q: "Eps ?Q = True"
wenzelm@11590
    49
      have neq: "?P \<noteq> ?Q"
wenzelm@11584
    50
      proof
wenzelm@11590
    51
	assume "?P = ?Q"
wenzelm@11590
    52
	hence "Eps ?P = Eps ?Q" by (rule arg_cong)
wenzelm@11590
    53
	also note P
wenzelm@11590
    54
	also note Q
wenzelm@11635
    55
	finally show False by (rule False_neq_True)
wenzelm@11584
    56
      qed
wenzelm@11590
    57
      have "\<not> A"
wenzelm@11584
    58
      proof
wenzelm@11590
    59
	assume a: A
wenzelm@11590
    60
	have "?P = ?Q"
wenzelm@11584
    61
	proof
wenzelm@11590
    62
	  fix x show "?P x = ?Q x"
wenzelm@11584
    63
	  proof
wenzelm@11590
    64
	    assume "?P x"
wenzelm@11590
    65
	    thus "?Q x"
wenzelm@11584
    66
	    proof
wenzelm@11584
    67
	      assume "x = False"
wenzelm@11590
    68
	      from this and a have "x = False \<and> A" ..
wenzelm@11590
    69
	      thus "?Q x" ..
wenzelm@11584
    70
	    next
wenzelm@11590
    71
	      assume "x = True \<and> A"
wenzelm@11584
    72
	      hence "x = True" ..
wenzelm@11590
    73
	      thus "?Q x" ..
wenzelm@11584
    74
	    qed
wenzelm@11584
    75
	  next
wenzelm@11590
    76
	    assume "?Q x"
wenzelm@11590
    77
	    thus "?P x"
wenzelm@11584
    78
	    proof
wenzelm@11590
    79
	      assume "x = False \<and> A"
wenzelm@11584
    80
	      hence "x = False" ..
wenzelm@11590
    81
	      thus "?P x" ..
wenzelm@11584
    82
	    next
wenzelm@11584
    83
	      assume "x = True"
wenzelm@11590
    84
	      from this and a have "x = True \<and> A" ..
wenzelm@11590
    85
	      thus "?P x" ..
wenzelm@11584
    86
	    qed
wenzelm@11584
    87
	  qed
wenzelm@11584
    88
	qed
wenzelm@11584
    89
	with neq show False by contradiction
wenzelm@11584
    90
      qed
wenzelm@11584
    91
      thus ?thesis ..
wenzelm@11584
    92
    qed
wenzelm@11584
    93
  qed
wenzelm@11584
    94
qed
wenzelm@11584
    95
wenzelm@11584
    96
wenzelm@11591
    97
subsection {* Proof term of text *}
wenzelm@11591
    98
wenzelm@11591
    99
text {*
wenzelm@11591
   100
  {\small @{prf [display, margin = 80] tnd}}
wenzelm@11591
   101
*}
wenzelm@11591
   102
wenzelm@11591
   103
wenzelm@11584
   104
subsection {* Proof script *}
wenzelm@11584
   105
wenzelm@11590
   106
theorem tnd': "A \<or> \<not> A"
wenzelm@11584
   107
  apply (subgoal_tac
wenzelm@11590
   108
    "(((SOME x. x = False \<or> x = True \<and> A) = False) \<or>
wenzelm@11590
   109
      ((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and>
wenzelm@11590
   110
     (((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or>
wenzelm@11590
   111
      ((SOME x. x = False \<and> A \<or> x = True) = True))")
wenzelm@11584
   112
  prefer 2
wenzelm@11584
   113
  apply (rule conjI)
wenzelm@11584
   114
  apply (rule someI)
wenzelm@11584
   115
  apply (rule disjI1)
wenzelm@11584
   116
  apply (rule refl)
wenzelm@11584
   117
  apply (rule someI)
wenzelm@11584
   118
  apply (rule disjI2)
wenzelm@11584
   119
  apply (rule refl)
wenzelm@11584
   120
  apply (erule conjE)
wenzelm@11584
   121
  apply (erule disjE)
wenzelm@11584
   122
  apply (erule disjE)
wenzelm@11584
   123
  apply (erule conjE)
wenzelm@11584
   124
  apply (erule disjI1)
wenzelm@11584
   125
  prefer 2
wenzelm@11584
   126
  apply (erule conjE)
wenzelm@11584
   127
  apply (erule disjI1)
wenzelm@11584
   128
  apply (subgoal_tac
wenzelm@11590
   129
    "(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq>
wenzelm@11590
   130
     (\<lambda>x. (x = False) \<and> A \<or> (x = True))")
wenzelm@11584
   131
  prefer 2
wenzelm@11584
   132
  apply (rule notI)
wenzelm@11590
   133
  apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong)
wenzelm@11584
   134
  apply (drule trans, assumption)
wenzelm@11584
   135
  apply (drule sym)
wenzelm@11584
   136
  apply (drule trans, assumption)
wenzelm@11584
   137
  apply (erule False_neq_True)
wenzelm@11584
   138
  apply (rule disjI2)
wenzelm@11584
   139
  apply (rule notI)
wenzelm@11584
   140
  apply (erule notE)
wenzelm@11584
   141
  apply (rule ext)
wenzelm@11584
   142
  apply (rule iffI)
wenzelm@11584
   143
  apply (erule disjE)
wenzelm@11584
   144
  apply (rule disjI1)
wenzelm@11584
   145
  apply (erule conjI)
wenzelm@11584
   146
  apply assumption
wenzelm@11584
   147
  apply (erule conjE)
wenzelm@11584
   148
  apply (erule disjI2)
wenzelm@11584
   149
  apply (erule disjE)
wenzelm@11584
   150
  apply (erule conjE)
wenzelm@11584
   151
  apply (erule disjI1)
wenzelm@11584
   152
  apply (rule disjI2)
wenzelm@11584
   153
  apply (erule conjI)
wenzelm@11584
   154
  apply assumption
wenzelm@11584
   155
  done
wenzelm@11584
   156
wenzelm@11584
   157
wenzelm@11584
   158
subsection {* Proof term of script *}
wenzelm@11584
   159
wenzelm@11584
   160
text {*
wenzelm@11591
   161
  {\small @{prf [display, margin = 80] tnd'}}
wenzelm@11584
   162
*}
wenzelm@11584
   163
wenzelm@11584
   164
end