src/HOL/SupInf.thy
changeset 35581 a25e51e2d64d
parent 35216 7641e8d831d2
child 35823 bd26885af9f4
     1.1 --- a/src/HOL/SupInf.thy	Thu Mar 04 19:43:51 2010 +0100
     1.2 +++ b/src/HOL/SupInf.thy	Thu Mar 04 19:50:45 2010 +0100
     1.3 @@ -228,6 +228,24 @@
     1.4      by  (auto simp add: setge_def setle_def)
     1.5  qed
     1.6  
     1.7 +lemma Sup_lessThan[simp]: "Sup {..<x} = (x::real)"
     1.8 +  by (auto intro!: Sup_eq intro: dense_le)
     1.9 +
    1.10 +lemma Sup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x} = (x::real)"
    1.11 +  by (auto intro!: Sup_eq intro: dense_le_bounded)
    1.12 +
    1.13 +lemma Sup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x} = (x::real)"
    1.14 +  by (auto intro!: Sup_eq intro: dense_le_bounded)
    1.15 +
    1.16 +lemma Sup_atMost[simp]: "Sup {..x} = (x::real)"
    1.17 +  by (auto intro!: Sup_eq_maximum)
    1.18 +
    1.19 +lemma Sup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = (x::real)"
    1.20 +  by (auto intro!: Sup_eq_maximum)
    1.21 +
    1.22 +lemma Sup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = (x::real)"
    1.23 +  by (auto intro!: Sup_eq_maximum)
    1.24 +
    1.25  
    1.26  subsection{*Infimum of a set of reals*}
    1.27  
    1.28 @@ -406,6 +424,21 @@
    1.29      by (simp add: Inf_real_def)
    1.30  qed
    1.31  
    1.32 +lemma Inf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x} = (y::real)"
    1.33 +  by (simp add: Inf_real_def)
    1.34 +
    1.35 +lemma Inf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = (y::real)"
    1.36 +  by (simp add: Inf_real_def)
    1.37 +
    1.38 +lemma Inf_atLeast[simp]: "Inf {x..} = (x::real)"
    1.39 +  by (simp add: Inf_real_def)
    1.40 +
    1.41 +lemma Inf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x} = (y::real)"
    1.42 +  by (simp add: Inf_real_def)
    1.43 +
    1.44 +lemma Inf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = (y::real)"
    1.45 +  by (simp add: Inf_real_def)
    1.46 +
    1.47  subsection{*Relate max and min to Sup and Inf.*}
    1.48  
    1.49  lemma real_max_Sup: