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