1.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Tue Dec 30 08:18:54 2008 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,82 +0,0 @@
     1.4 -(*  Title:      HOL/Real/HahnBanach/Bounds.thy
     1.5 -    Author:     Gertrud Bauer, TU Munich
     1.6 -*)
     1.7 -
     1.8 -header {* Bounds *}
     1.9 -
    1.10 -theory Bounds
    1.11 -imports Main ContNotDenum
    1.12 -begin
    1.13 -
    1.14 -locale lub =
    1.15 -  fixes A and x
    1.16 -  assumes least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<le> b) \<Longrightarrow> x \<le> b"
    1.17 -    and upper [intro?]: "a \<in> A \<Longrightarrow> a \<le> x"
    1.18 -
    1.19 -lemmas [elim?] = lub.least lub.upper
    1.20 -
    1.21 -definition
    1.22 -  the_lub :: "'a::order set \<Rightarrow> 'a" where
    1.23 -  "the_lub A = The (lub A)"
    1.24 -
    1.25 -notation (xsymbols)
    1.26 -  the_lub  ("\<Squnion>_" [90] 90)
    1.27 -
    1.28 -lemma the_lub_equality [elim?]:
    1.29 -  assumes "lub A x"
    1.30 -  shows "\<Squnion>A = (x::'a::order)"
    1.31 -proof -
    1.32 -  interpret lub A x by fact
    1.33 -  show ?thesis
    1.34 -  proof (unfold the_lub_def)
    1.35 -    from `lub A x` show "The (lub A) = x"
    1.36 -    proof
    1.37 -      fix x' assume lub': "lub A x'"
    1.38 -      show "x' = x"
    1.39 -      proof (rule order_antisym)
    1.40 -	from lub' show "x' \<le> x"
    1.41 -	proof
    1.42 -          fix a assume "a \<in> A"
    1.43 -          then show "a \<le> x" ..
    1.44 -	qed
    1.45 -	show "x \<le> x'"
    1.46 -	proof
    1.47 -          fix a assume "a \<in> A"
    1.48 -          with lub' show "a \<le> x'" ..
    1.49 -	qed
    1.50 -      qed
    1.51 -    qed
    1.52 -  qed
    1.53 -qed
    1.54 -
    1.55 -lemma the_lubI_ex:
    1.56 -  assumes ex: "\<exists>x. lub A x"
    1.57 -  shows "lub A (\<Squnion>A)"
    1.58 -proof -
    1.59 -  from ex obtain x where x: "lub A x" ..
    1.60 -  also from x have [symmetric]: "\<Squnion>A = x" ..
    1.61 -  finally show ?thesis .
    1.62 -qed
    1.63 -
    1.64 -lemma lub_compat: "lub A x = isLub UNIV A x"
    1.65 -proof -
    1.66 -  have "isUb UNIV A = (\<lambda>x. A *<= x \<and> x \<in> UNIV)"
    1.67 -    by (rule ext) (simp only: isUb_def)
    1.68 -  then show ?thesis
    1.69 -    by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast
    1.70 -qed
    1.71 -
    1.72 -lemma real_complete:
    1.73 -  fixes A :: "real set"
    1.74 -  assumes nonempty: "\<exists>a. a \<in> A"
    1.75 -    and ex_upper: "\<exists>y. \<forall>a \<in> A. a \<le> y"
    1.76 -  shows "\<exists>x. lub A x"
    1.77 -proof -
    1.78 -  from ex_upper have "\<exists>y. isUb UNIV A y"
    1.79 -    unfolding isUb_def setle_def by blast
    1.80 -  with nonempty have "\<exists>x. isLub UNIV A x"
    1.81 -    by (rule reals_complete)
    1.82 -  then show ?thesis by (simp only: lub_compat)
    1.83 -qed
    1.84 -
    1.85 -end