1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Conditionally-complete Lattices *}
     1.5  
     1.6  theory Conditionally_Complete_Lattices
     1.7 -imports Main Lubs
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
    1.12 @@ -28,6 +28,12 @@
    1.13  lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A"
    1.14    by (auto simp: bdd_below_def)
    1.15  
    1.16 +lemma bdd_aboveI2: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> bdd_above (f`A)"
    1.17 +  by force
    1.18 +
    1.19 +lemma bdd_belowI2: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> bdd_below (f`A)"
    1.20 +  by force
    1.21 +
    1.22  lemma bdd_above_empty [simp, intro]: "bdd_above {}"
    1.23    unfolding bdd_above_def by auto
    1.24  
    1.25 @@ -298,6 +304,12 @@
    1.26  lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
    1.27    by (metis cSUP_least cSUP_upper assms order_trans)
    1.28  
    1.29 +lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
    1.30 +  by (metis cINF_lower less_le_trans)
    1.31 +
    1.32 +lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (SUP i:A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y"
    1.33 +  by (metis cSUP_upper le_less_trans)
    1.34 +
    1.35  lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
    1.36    by (metis INF_def cInf_insert assms empty_is_image image_insert)
    1.37  
    1.38 @@ -347,11 +359,6 @@
    1.39  instance complete_lattice \<subseteq> conditionally_complete_lattice
    1.40    by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
    1.41  
    1.42 -lemma isLub_cSup: 
    1.43 -  "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
    1.44 -  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
    1.45 -            intro!: setgeI cSup_upper cSup_least)
    1.46 -
    1.47  lemma cSup_eq:
    1.48    fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
    1.49    assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
    1.50 @@ -370,12 +377,6 @@
    1.51    assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
    1.52  qed (intro cInf_eq_non_empty assms)
    1.53  
    1.54 -lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
    1.55 -  by (metis cSup_least setle_def)
    1.56 -
    1.57 -lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
    1.58 -  by (metis cInf_greatest setge_def)
    1.59 -
    1.60  class conditionally_complete_linorder = conditionally_complete_lattice + linorder
    1.61  begin
    1.62  
    1.63 @@ -386,6 +387,12 @@
    1.64  lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
    1.65    by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
    1.66  
    1.67 +lemma cINF_less_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
    1.68 +  unfolding INF_def using cInf_less_iff[of "f`A"] by auto
    1.69 +
    1.70 +lemma less_cSUP_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
    1.71 +  unfolding SUP_def using less_cSup_iff[of "f`A"] by auto
    1.72 +
    1.73  lemma less_cSupE:
    1.74    assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
    1.75    by (metis cSup_least assms not_le that)
    1.76 @@ -437,27 +444,6 @@
    1.77  lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
    1.78    using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
    1.79  
    1.80 -lemma cSup_bounds:
    1.81 -  fixes S :: "'a :: conditionally_complete_lattice set"
    1.82 -  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
    1.83 -  shows "a \<le> Sup S \<and> Sup S \<le> b"
    1.84 -proof-
    1.85 -  from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
    1.86 -  hence b: "Sup S \<le> b" using u 
    1.87 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
    1.88 -  from Se obtain y where y: "y \<in> S" by blast
    1.89 -  from lub l have "a \<le> Sup S"
    1.90 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
    1.91 -       (metis le_iff_sup le_sup_iff y)
    1.92 -  with b show ?thesis by blast
    1.93 -qed
    1.94 -
    1.95 -lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
    1.96 -  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
    1.97 -
    1.98 -lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
    1.99 -  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
   1.100 -
   1.101  lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
   1.102    by (auto intro!: cSup_eq_non_empty intro: dense_le)
   1.103