src/HOL/Real.thy
changeset 54281 b01057e72233
parent 54263 c4159fe6fa46
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Real.thy	Wed Nov 06 14:50:50 2013 +0100
     1.2 +++ b/src/HOL/Real.thy	Tue Nov 05 21:23:42 2013 +0100
     1.3 @@ -924,11 +924,8 @@
     1.4  
     1.5  subsection{*Supremum of a set of reals*}
     1.6  
     1.7 -definition
     1.8 -  Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
     1.9 -
    1.10 -definition
    1.11 -  Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
    1.12 +definition "Sup X = (LEAST z::real. \<forall>x\<in>X. x \<le> z)"
    1.13 +definition "Inf (X::real set) = - Sup (uminus ` X)"
    1.14  
    1.15  instance
    1.16  proof
    1.17 @@ -951,20 +948,10 @@
    1.18      finally show "Sup X \<le> z" . }
    1.19    note Sup_least = this
    1.20  
    1.21 -  { fix x z :: real and X :: "real set"
    1.22 -    assume x: "x \<in> X" and [simp]: "bdd_below X"
    1.23 -    have "-x \<le> Sup (uminus ` X)"
    1.24 -      by (rule Sup_upper) (auto simp add: image_iff x)
    1.25 -    then show "Inf X \<le> x" 
    1.26 -      by (auto simp add: Inf_real_def) }
    1.27 -
    1.28 -  { fix z :: real and X :: "real set"
    1.29 -    assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
    1.30 -    have "Sup (uminus ` X) \<le> -z"
    1.31 -      using x z by (force intro: Sup_least)
    1.32 -    then show "z \<le> Inf X" 
    1.33 -        by (auto simp add: Inf_real_def) }
    1.34 -
    1.35 +  { fix x :: real and X :: "real set" assume x: "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
    1.36 +      using Sup_upper[of "-x" "uminus ` X"] by (auto simp: Inf_real_def) }
    1.37 +  { fix z :: real and X :: "real set" assume "X \<noteq> {}" "\<And>x. x \<in> X \<Longrightarrow> z \<le> x" then show "z \<le> Inf X"
    1.38 +      using Sup_least[of "uminus ` X" "- z"] by (force simp: Inf_real_def) }
    1.39    show "\<exists>a b::real. a \<noteq> b"
    1.40      using zero_neq_one by blast
    1.41  qed