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
```