src/HOL/Hilbert_Choice.thy
changeset 64591 240a39af9ec4
parent 63981 6f7db4f8df4c
child 65815 416aa3b00cbe
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Dec 17 15:22:13 2016 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Dec 17 15:22:13 2016 +0100
     1.3 @@ -657,6 +657,12 @@
     1.4    for x :: nat
     1.5    unfolding Greatest_def by (rule GreatestM_nat_le) auto
     1.6  
     1.7 +lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
     1.8 +  apply (erule exE)
     1.9 +  apply (rule GreatestI)
    1.10 +   apply assumption+
    1.11 +  done
    1.12 +
    1.13  
    1.14  subsection \<open>An aside: bounded accessible part\<close>
    1.15