src/HOL/SupInf.thy
changeset 33609 059cd49e4b1e
parent 33271 7be66dee1a5a
child 33657 a4179bf442d1
     1.1 --- a/src/HOL/SupInf.thy	Wed Nov 11 09:02:37 2009 +0100
     1.2 +++ b/src/HOL/SupInf.thy	Wed Nov 11 14:04:56 2009 +0000
     1.3 @@ -88,6 +88,12 @@
     1.4    finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
     1.5  qed
     1.6  
     1.7 +lemma less_SupE:
     1.8 +  fixes y :: real
     1.9 +  assumes "y < Sup X" "X \<noteq> {}"
    1.10 +  obtains x where "x\<in>X" "y < x"
    1.11 +by (metis SupInf.Sup_least assms linorder_not_less that)
    1.12 +
    1.13  lemma Sup_singleton [simp]: "Sup {x::real} = x"
    1.14    by (force intro: Least_equality simp add: Sup_real_def)
    1.15   
    1.16 @@ -459,4 +465,36 @@
    1.17    ultimately show ?thesis by arith
    1.18  qed
    1.19  
    1.20 +lemma reals_complete_interval:
    1.21 +  fixes a::real and b::real
    1.22 +  assumes "a < b" and "P a" and "~P b"
    1.23 +  shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c --> P x) &
    1.24 +             (\<forall>d. (\<forall>x. a \<le> x & x < d --> P x) --> d \<le> c)"
    1.25 +proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
    1.26 +  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
    1.27 +    by (rule SupInf.Sup_upper [where z=b], auto)
    1.28 +       (metis prems real_le_linear real_less_def) 
    1.29 +next
    1.30 +  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
    1.31 +    apply (rule SupInf.Sup_least) 
    1.32 +    apply (auto simp add: )
    1.33 +    apply (metis less_le_not_le)
    1.34 +    apply (metis `a<b` `~ P b` real_le_linear real_less_def) 
    1.35 +    done
    1.36 +next
    1.37 +  fix x
    1.38 +  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
    1.39 +  show "P x"
    1.40 +    apply (rule less_SupE [OF lt], auto)
    1.41 +    apply (metis less_le_not_le)
    1.42 +    apply (metis x) 
    1.43 +    done
    1.44 +next
    1.45 +  fix d
    1.46 +    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
    1.47 +    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
    1.48 +      by (rule_tac z="b" in SupInf.Sup_upper, auto) 
    1.49 +         (metis `a<b` `~ P b` real_le_linear real_less_def) 
    1.50 +qed
    1.51 +
    1.52  end