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)"`
`   449   apply (simp add: Greatest_def)`
`   438   apply (simp add: Greatest_def)`
`   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`