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