src/HOL/Conditionally_Complete_Lattices.thy
changeset 53215 5e47c31c6f7c
parent 52265 bb907eba5902
child 53216 ad2e09c30aa8
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Aug 26 23:39:53 2013 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Aug 27 14:37:56 2013 +0200
     1.3 @@ -283,22 +283,22 @@
     1.4  lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
     1.5    using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
     1.6  
     1.7 -lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
     1.8 +lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
     1.9    by (auto intro!: cSup_eq_non_empty intro: dense_le)
    1.10  
    1.11 -lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
    1.12 +lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
    1.13    by (auto intro!: cSup_eq intro: dense_le_bounded)
    1.14  
    1.15 -lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
    1.16 +lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
    1.17    by (auto intro!: cSup_eq intro: dense_le_bounded)
    1.18  
    1.19 -lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, dense_linorder} <..} = x"
    1.20 +lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, unbounded_dense_linorder} <..} = x"
    1.21    by (auto intro!: cInf_eq intro: dense_ge)
    1.22  
    1.23 -lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
    1.24 +lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
    1.25    by (auto intro!: cInf_eq intro: dense_ge_bounded)
    1.26  
    1.27 -lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
    1.28 +lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
    1.29    by (auto intro!: cInf_eq intro: dense_ge_bounded)
    1.30  
    1.31  end