src/HOL/Conditionally_Complete_Lattices.thy
changeset 57447 87429bdecad5
parent 57275 0ddb5b755cdc
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Jun 30 15:45:03 2014 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon Jun 30 15:45:21 2014 +0200
     1.3 @@ -354,6 +354,10 @@
     1.4    by (intro antisym le_supI cSUP_least cSUP_upper2)
     1.5       (auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI)
     1.6  
     1.7 +lemma cInf_le_cSup:
     1.8 +  "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below A \<Longrightarrow> Inf A \<le> Sup A"
     1.9 +  by (auto intro!: cSup_upper2[of "SOME a. a \<in> A"] intro: someI cInf_lower)
    1.10 +
    1.11  end
    1.12  
    1.13  instance complete_lattice \<subseteq> conditionally_complete_lattice
    1.14 @@ -447,20 +451,20 @@
    1.15  lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
    1.16    by (auto intro!: cSup_eq_non_empty intro: dense_le)
    1.17  
    1.18 -lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
    1.19 -  by (auto intro!: cSup_eq intro: dense_le_bounded)
    1.20 +lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
    1.21 +  by (auto intro!: cSup_eq_non_empty intro: dense_le_bounded)
    1.22  
    1.23 -lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
    1.24 -  by (auto intro!: cSup_eq intro: dense_le_bounded)
    1.25 +lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
    1.26 +  by (auto intro!: cSup_eq_non_empty intro: dense_le_bounded)
    1.27  
    1.28  lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, no_top, dense_linorder} <..} = x"
    1.29 -  by (auto intro!: cInf_eq intro: dense_ge)
    1.30 +  by (auto intro!: cInf_eq_non_empty intro: dense_ge)
    1.31  
    1.32 -lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y"
    1.33 -  by (auto intro!: cInf_eq intro: dense_ge_bounded)
    1.34 +lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
    1.35 +  by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)
    1.36  
    1.37 -lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y"
    1.38 -  by (auto intro!: cInf_eq intro: dense_ge_bounded)
    1.39 +lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
    1.40 +  by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)
    1.41  
    1.42  class linear_continuum = conditionally_complete_linorder + dense_linorder +
    1.43    assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"