src/HOL/Hilbert_Choice.thy
 changeset 39943 0ef551d47783 parent 39900 549c00e0e89b child 39950 f3c4849868b8
equal inserted replaced
39942:1ae333bfef14 39943:0ef551d47783
5
5
6 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
6 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
7
7
8 theory Hilbert_Choice
8 theory Hilbert_Choice
9 imports Nat Wellfounded Plain
9 imports Nat Wellfounded Plain
10 uses ("Tools/meson.ML")
10 uses ("Tools/choice_specification.ML")
11      ("Tools/choice_specification.ML")

12 begin
11 begin
13
12
14 subsection {* Hilbert's epsilon *}
13 subsection {* Hilbert's epsilon *}
15
14
16 axiomatization Eps :: "('a => bool) => 'a" where
15 axiomatization Eps :: "('a => bool) => 'a" where
78 apply (erule sym)
77 apply (erule sym)
79 done
78 done
80
79
81
80
82 subsection{*Axiom of Choice, Proved Using the Description Operator*}
81 subsection{*Axiom of Choice, Proved Using the Description Operator*}
93
82
94 lemma choice [meson_choice]: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
83 lemma choice [meson_choice]: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
95 by (fast elim: someI)
84 by (fast elim: someI)
96
85
97 lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
86 lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
450   apply (rule GreatestM_nat_le, auto)
439   apply (rule GreatestM_nat_le, auto)
451   done
440   done
452
441
453
442
576 subsection {* Specification package -- Hilbertized version *}
443 subsection {* Specification package -- Hilbertized version *}
577
444
578 lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
445 lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
579   by (simp only: someI_ex)
446   by (simp only: someI_ex)
580
447
581 use "Tools/choice_specification.ML"
448 use "Tools/choice_specification.ML"
582
449
584 end
450 end