(* Title: HOL/Proofs/ex/Hilbert_Classical.thy Author: Stefan Berghofer Author: Makarius Wenzel *) section ‹Hilbert's choice and classical logic› theory Hilbert_Classical imports Main begin text ‹ 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 tertium_non_datur: "A ∨ ¬ A" proof - let ?P = "λx. (A ∧ x) ∨ ¬ x" let ?Q = "λx. (A ∧ ¬ x) ∨ x" have a: "?P (Eps ?P)" proof (rule someI) have "¬ False" .. then show "?P False" .. qed have b: "?Q (Eps ?Q)" proof (rule someI) have True .. then show "?Q True" .. qed from a show ?thesis proof assume "A ∧ Eps ?P" then have A .. then show ?thesis .. next assume "¬ Eps ?P" from b show ?thesis proof assume "A ∧ ¬ Eps ?Q" then have A .. then show ?thesis .. next assume "Eps ?Q" have neq: "?P ≠ ?Q" proof assume "?P = ?Q" then have "Eps ?P ⟷ Eps ?Q" by (rule arg_cong) also note ‹Eps ?Q› finally have "Eps ?P" . with ‹¬ Eps ?P› show False by contradiction qed have "¬ A" proof assume A have "?P = ?Q" proof (rule ext) show "?P x ⟷ ?Q x" for x proof assume "?P x" then show "?Q x" proof assume "¬ x" with ‹A› have "A ∧ ¬ x" .. then show ?thesis .. next assume "A ∧ x" then have x .. then show ?thesis .. qed next assume "?Q x" then show "?P x" proof assume "A ∧ ¬ x" then have "¬ x" .. then show ?thesis .. next assume x with ‹A› have "A ∧ x" .. then show ?thesis .. qed qed qed with neq show False by contradiction qed then show ?thesis .. qed qed qed subsection ‹Old proof text› theorem tertium_non_datur1: "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) show "?P False" using refl .. qed have b: "?Q (Eps ?Q)" proof (rule someI) show "?Q True" using refl .. qed from a show ?thesis proof assume "(Eps ?P ⟷ True) ∧ A" then have A .. then show ?thesis .. next assume P: "Eps ?P ⟷ False" from b show ?thesis proof assume "(Eps ?Q ⟷ False) ∧ A" then have A .. then show ?thesis .. next assume Q: "Eps ?Q ⟷ True" have neq: "?P ≠ ?Q" proof assume "?P = ?Q" then have "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 have "?P = ?Q" proof (rule ext) show "?P x ⟷ ?Q x" for x proof assume "?P x" then show "?Q x" proof assume "x ⟷ False" from this and ‹A› have "(x ⟷ False) ∧ A" .. then show ?thesis .. next assume "(x ⟷ True) ∧ A" then have "x ⟷ True" .. then show ?thesis .. qed next assume "?Q x" then show "?P x" proof assume "(x ⟷ False) ∧ A" then have "x ⟷ False" .. then show ?thesis .. next assume "x ⟷ True" from this and ‹A› have "(x ⟷ True) ∧ A" .. then show ?thesis .. qed qed qed with neq show False by contradiction qed then show ?thesis .. qed qed qed subsection ‹Old proof script› theorem tertium_non_datur2: "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 done subsection ‹Proof terms› prf tertium_non_datur prf tertium_non_datur1 prf tertium_non_datur2 end