# HG changeset patch
# User paulson
# Date 1257948296 0
# Node ID 059cd49e4b1e7b739c3ea24cf21faed8e39f765f
# Parent  5c0024338ceff4063eafd58621ec48dc9b14cc2e
Added two new lemmas

diff -r 5c0024338cef -r 059cd49e4b1e src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/SupInf.thy	Wed Nov 11 14:04:56 2009 +0000
@@ -88,6 +88,12 @@
   finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
 qed
 
+lemma less_SupE:
+  fixes y :: real
+  assumes "y < Sup X" "X \<noteq> {}"
+  obtains x where "x\<in>X" "y < x"
+by (metis SupInf.Sup_least assms linorder_not_less that)
+
 lemma Sup_singleton [simp]: "Sup {x::real} = x"
   by (force intro: Least_equality simp add: Sup_real_def)
  
@@ -459,4 +465,36 @@
   ultimately show ?thesis by arith
 qed
 
+lemma reals_complete_interval:
+  fixes a::real and b::real
+  assumes "a < b" and "P a" and "~P b"
+  shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c --> P x) &
+             (\<forall>d. (\<forall>x. a \<le> x & x < d --> P x) --> d \<le> c)"
+proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
+  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+    by (rule SupInf.Sup_upper [where z=b], auto)
+       (metis prems real_le_linear real_less_def) 
+next
+  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
+    apply (rule SupInf.Sup_least) 
+    apply (auto simp add: )
+    apply (metis less_le_not_le)
+    apply (metis `a<b` `~ P b` real_le_linear real_less_def) 
+    done
+next
+  fix x
+  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+  show "P x"
+    apply (rule less_SupE [OF lt], auto)
+    apply (metis less_le_not_le)
+    apply (metis x) 
+    done
+next
+  fix d
+    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
+    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+      by (rule_tac z="b" in SupInf.Sup_upper, auto) 
+         (metis `a<b` `~ P b` real_le_linear real_less_def) 
+qed
+
 end