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