# HG changeset patch
# User hoelzl
# Date 1267728645 -3600
# Node ID a25e51e2d64db37cd25bb1020d39bbce6757284d
# Parent  0f74806cab224a6c363db69566bf5ce89424c5bf
Supremum and Infimum on real intervals

diff -r 0f74806cab22 -r a25e51e2d64d src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Thu Mar 04 19:43:51 2010 +0100
+++ b/src/HOL/SupInf.thy	Thu Mar 04 19:50:45 2010 +0100
@@ -228,6 +228,24 @@
     by  (auto simp add: setge_def setle_def)
 qed
 
+lemma Sup_lessThan[simp]: "Sup {..<x} = (x::real)"
+  by (auto intro!: Sup_eq intro: dense_le)
+
+lemma Sup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x} = (x::real)"
+  by (auto intro!: Sup_eq intro: dense_le_bounded)
+
+lemma Sup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x} = (x::real)"
+  by (auto intro!: Sup_eq intro: dense_le_bounded)
+
+lemma Sup_atMost[simp]: "Sup {..x} = (x::real)"
+  by (auto intro!: Sup_eq_maximum)
+
+lemma Sup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = (x::real)"
+  by (auto intro!: Sup_eq_maximum)
+
+lemma Sup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = (x::real)"
+  by (auto intro!: Sup_eq_maximum)
+
 
 subsection{*Infimum of a set of reals*}
 
@@ -406,6 +424,21 @@
     by (simp add: Inf_real_def)
 qed
 
+lemma Inf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x} = (y::real)"
+  by (simp add: Inf_real_def)
+
+lemma Inf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = (y::real)"
+  by (simp add: Inf_real_def)
+
+lemma Inf_atLeast[simp]: "Inf {x..} = (x::real)"
+  by (simp add: Inf_real_def)
+
+lemma Inf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x} = (y::real)"
+  by (simp add: Inf_real_def)
+
+lemma Inf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = (y::real)"
+  by (simp add: Inf_real_def)
+
 subsection{*Relate max and min to Sup and Inf.*}
 
 lemma real_max_Sup: