src/HOL/ex/Hilbert_Classical.thy
author wenzelm
Thu Sep 27 16:43:46 2001 +0200 (2001-09-27)
changeset 11591 4b171ad4ff65
parent 11590 14ae6a86813d
child 11635 fd242f857508
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@11590
    55
	finally have "False = True" .	
wenzelm@11584
    56
	thus False by (rule False_neq_True)
wenzelm@11584
    57
      qed
wenzelm@11590
    58
      have "\<not> A"
wenzelm@11584
    59
      proof
wenzelm@11590
    60
	assume a: A
wenzelm@11590
    61
	have "?P = ?Q"
wenzelm@11584
    62
	proof
wenzelm@11590
    63
	  fix x show "?P x = ?Q x"
wenzelm@11584
    64
	  proof
wenzelm@11590
    65
	    assume "?P x"
wenzelm@11590
    66
	    thus "?Q x"
wenzelm@11584
    67
	    proof
wenzelm@11584
    68
	      assume "x = False"
wenzelm@11590
    69
	      from this and a have "x = False \<and> A" ..
wenzelm@11590
    70
	      thus "?Q x" ..
wenzelm@11584
    71
	    next
wenzelm@11590
    72
	      assume "x = True \<and> A"
wenzelm@11584
    73
	      hence "x = True" ..
wenzelm@11590
    74
	      thus "?Q x" ..
wenzelm@11584
    75
	    qed
wenzelm@11584
    76
	  next
wenzelm@11590
    77
	    assume "?Q x"
wenzelm@11590
    78
	    thus "?P x"
wenzelm@11584
    79
	    proof
wenzelm@11590
    80
	      assume "x = False \<and> A"
wenzelm@11584
    81
	      hence "x = False" ..
wenzelm@11590
    82
	      thus "?P x" ..
wenzelm@11584
    83
	    next
wenzelm@11584
    84
	      assume "x = True"
wenzelm@11590
    85
	      from this and a have "x = True \<and> A" ..
wenzelm@11590
    86
	      thus "?P 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
  qed
wenzelm@11584
    95
qed
wenzelm@11584
    96
wenzelm@11584
    97
wenzelm@11591
    98
subsection {* Proof term of text *}
wenzelm@11591
    99
wenzelm@11591
   100
text {*
wenzelm@11591
   101
  {\small @{prf [display, margin = 80] tnd}}
wenzelm@11591
   102
*}
wenzelm@11591
   103
wenzelm@11591
   104
wenzelm@11584
   105
subsection {* Proof script *}
wenzelm@11584
   106
wenzelm@11590
   107
theorem tnd': "A \<or> \<not> A"
wenzelm@11584
   108
  apply (subgoal_tac
wenzelm@11590
   109
    "(((SOME x. x = False \<or> x = True \<and> A) = False) \<or>
wenzelm@11590
   110
      ((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and>
wenzelm@11590
   111
     (((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or>
wenzelm@11590
   112
      ((SOME x. x = False \<and> A \<or> x = True) = True))")
wenzelm@11584
   113
  prefer 2
wenzelm@11584
   114
  apply (rule conjI)
wenzelm@11584
   115
  apply (rule someI)
wenzelm@11584
   116
  apply (rule disjI1)
wenzelm@11584
   117
  apply (rule refl)
wenzelm@11584
   118
  apply (rule someI)
wenzelm@11584
   119
  apply (rule disjI2)
wenzelm@11584
   120
  apply (rule refl)
wenzelm@11584
   121
  apply (erule conjE)
wenzelm@11584
   122
  apply (erule disjE)
wenzelm@11584
   123
  apply (erule disjE)
wenzelm@11584
   124
  apply (erule conjE)
wenzelm@11584
   125
  apply (erule disjI1)
wenzelm@11584
   126
  prefer 2
wenzelm@11584
   127
  apply (erule conjE)
wenzelm@11584
   128
  apply (erule disjI1)
wenzelm@11584
   129
  apply (subgoal_tac
wenzelm@11590
   130
    "(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq>
wenzelm@11590
   131
     (\<lambda>x. (x = False) \<and> A \<or> (x = True))")
wenzelm@11584
   132
  prefer 2
wenzelm@11584
   133
  apply (rule notI)
wenzelm@11590
   134
  apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong)
wenzelm@11584
   135
  apply (drule trans, assumption)
wenzelm@11584
   136
  apply (drule sym)
wenzelm@11584
   137
  apply (drule trans, assumption)
wenzelm@11584
   138
  apply (erule False_neq_True)
wenzelm@11584
   139
  apply (rule disjI2)
wenzelm@11584
   140
  apply (rule notI)
wenzelm@11584
   141
  apply (erule notE)
wenzelm@11584
   142
  apply (rule ext)
wenzelm@11584
   143
  apply (rule iffI)
wenzelm@11584
   144
  apply (erule disjE)
wenzelm@11584
   145
  apply (rule disjI1)
wenzelm@11584
   146
  apply (erule conjI)
wenzelm@11584
   147
  apply assumption
wenzelm@11584
   148
  apply (erule conjE)
wenzelm@11584
   149
  apply (erule disjI2)
wenzelm@11584
   150
  apply (erule disjE)
wenzelm@11584
   151
  apply (erule conjE)
wenzelm@11584
   152
  apply (erule disjI1)
wenzelm@11584
   153
  apply (rule disjI2)
wenzelm@11584
   154
  apply (erule conjI)
wenzelm@11584
   155
  apply assumption
wenzelm@11584
   156
  done
wenzelm@11584
   157
wenzelm@11584
   158
wenzelm@11584
   159
subsection {* Proof term of script *}
wenzelm@11584
   160
wenzelm@11584
   161
text {*
wenzelm@11591
   162
  {\small @{prf [display, margin = 80] tnd'}}
wenzelm@11584
   163
*}
wenzelm@11584
   164
wenzelm@11584
   165
end