src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 54263 c4159fe6fa46 parent 54230 b1d955791529 child 54489 03ff4d1e6784
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.36  subsection {* Fundamental theorem of algebra *}