1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -156,28 +156,11 @@
     1.4  text{* An alternative useful formulation of completeness of the reals *}
     1.5  lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
     1.6    shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
     1.7 -proof-
     1.8 -  from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y"  by blast
     1.9 -  from ex have thx:"\<exists>x. x \<in> Collect P" by blast
    1.10 -  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y"
    1.11 -    by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
    1.12 -  from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
    1.13 -    by blast
    1.14 -  from Y[OF x] have xY: "x < Y" .
    1.15 -  from L have L': "\<forall>x. P x \<longrightarrow> x \<le> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
    1.16 -  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y"
    1.17 -    apply (clarsimp, atomize (full)) by auto
    1.18 -  from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
    1.19 -  {fix y
    1.20 -    {fix z assume z: "P z" "y < z"
    1.21 -      from L' z have "y < L" by auto }
    1.22 -    moreover
    1.23 -    {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
    1.24 -      hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
    1.25 -      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
    1.26 -      with yL(1) have False  by arith}
    1.27 -    ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
    1.28 -  thus ?thesis by blast
    1.29 +proof
    1.30 +  from bz have "bdd_above (Collect P)"
    1.31 +    by (force intro: less_imp_le)
    1.32 +  then show "\<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < Sup (Collect P)"
    1.33 +    using ex bz by (subst less_cSup_iff) auto
    1.34  qed
    1.35  
    1.36  subsection {* Fundamental theorem of algebra *}