# Theory Hilbert_Classical

Up to index of Isabelle/HOL-Proofs/HOL-Proofs-ex

theory Hilbert_Classical
imports Main
`(*  Title:      HOL/Proofs/ex/Hilbert_Classical.thy    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen*)header {* Hilbert's choice and classical logic *}theory Hilbert_Classicalimports Mainbegintext {*  Derivation of the classical law of tertium-non-datur by means of  Hilbert's choice operator (due to M. J. Beeson and J. Harrison).*}subsection {* Proof text *}theorem tnd: "A ∨ ¬ A"proof -  let ?P = "λX. X = False ∨ X = True ∧ A"  let ?Q = "λX. X = False ∧ A ∨ X = True"  have a: "?P (Eps ?P)"  proof (rule someI)    have "False = False" ..    thus "?P False" ..  qed  have b: "?Q (Eps ?Q)"  proof (rule someI)    have "True = True" ..    thus "?Q True" ..  qed  from a show ?thesis  proof    assume "Eps ?P = True ∧ A"    hence A ..    thus ?thesis ..  next    assume P: "Eps ?P = False"    from b show ?thesis    proof      assume "Eps ?Q = False ∧ A"      hence A ..      thus ?thesis ..    next      assume Q: "Eps ?Q = True"      have neq: "?P ≠ ?Q"      proof        assume "?P = ?Q"        hence "Eps ?P = Eps ?Q" by (rule arg_cong)        also note P        also note Q        finally show False by (rule False_neq_True)      qed      have "¬ A"      proof        assume a: A        have "?P = ?Q"        proof (rule ext)          fix x show "?P x = ?Q x"          proof            assume "?P x"            thus "?Q x"            proof              assume "x = False"              from this and a have "x = False ∧ A" ..              thus "?Q x" ..            next              assume "x = True ∧ A"              hence "x = True" ..              thus "?Q x" ..            qed          next            assume "?Q x"            thus "?P x"            proof              assume "x = False ∧ A"              hence "x = False" ..              thus "?P x" ..            next              assume "x = True"              from this and a have "x = True ∧ A" ..              thus "?P x" ..            qed          qed        qed        with neq show False by contradiction      qed      thus ?thesis ..    qed  qedqedsubsection {* Proof term of text *}prf tndsubsection {* Proof script *}theorem tnd': "A ∨ ¬ A"  apply (subgoal_tac    "(((SOME x. x = False ∨ x = True ∧ A) = False) ∨      ((SOME x. x = False ∨ x = True ∧ A) = True) ∧ A) ∧     (((SOME x. x = False ∧ A ∨ x = True) = False) ∧ A ∨      ((SOME x. x = False ∧ A ∨ x = True) = True))")  prefer 2  apply (rule conjI)  apply (rule someI)  apply (rule disjI1)  apply (rule refl)  apply (rule someI)  apply (rule disjI2)  apply (rule refl)  apply (erule conjE)  apply (erule disjE)  apply (erule disjE)  apply (erule conjE)  apply (erule disjI1)  prefer 2  apply (erule conjE)  apply (erule disjI1)  apply (subgoal_tac    "(λx. (x = False) ∨ (x = True) ∧ A) ≠     (λx. (x = False) ∧ A ∨ (x = True))")  prefer 2  apply (rule notI)  apply (drule_tac f = "λy. SOME x. y x" in arg_cong)  apply (drule trans, assumption)  apply (drule sym)  apply (drule trans, assumption)  apply (erule False_neq_True)  apply (rule disjI2)  apply (rule notI)  apply (erule notE)  apply (rule ext)  apply (rule iffI)  apply (erule disjE)  apply (rule disjI1)  apply (erule conjI)  apply assumption  apply (erule conjE)  apply (erule disjI2)  apply (erule disjE)  apply (erule conjE)  apply (erule disjI1)  apply (rule disjI2)  apply (erule conjI)  apply assumption  donesubsection {* Proof term of script *}prf tnd'end`