src/HOL/ex/Hilbert_Classical.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 16417 9bc16273c2d4 child 26828 60d1fa8e0831 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     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
```
```    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
```