diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 09:45:00 2013 +0100 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 09:45:02 2013 +0100 @@ -7,7 +7,7 @@ header {* Conditionally-complete Lattices *} theory Conditionally_Complete_Lattices -imports Main Lubs +imports Main begin lemma (in linorder) Sup_fin_eq_Max: "finite X \ X \ {} \ Sup_fin X = Max X" @@ -28,6 +28,12 @@ lemma bdd_belowI[intro]: "(\x. x \ A \ m \ x) \ bdd_below A" by (auto simp: bdd_below_def) +lemma bdd_aboveI2: "(\x. x \ A \ f x \ M) \ bdd_above (f`A)" + by force + +lemma bdd_belowI2: "(\x. x \ A \ m \ f x) \ bdd_below (f`A)" + by force + lemma bdd_above_empty [simp, intro]: "bdd_above {}" unfolding bdd_above_def by auto @@ -298,6 +304,12 @@ lemma cSUP_le_iff: "A \ {} \ bdd_above (f ` A) \ SUPR A f \ u \ (\x\A. f x \ u)" by (metis cSUP_least cSUP_upper assms order_trans) +lemma less_cINF_D: "bdd_below (f`A) \ y < (INF i:A. f i) \ i \ A \ y < f i" + by (metis cINF_lower less_le_trans) + +lemma cSUP_lessD: "bdd_above (f`A) \ (SUP i:A. f i) < y \ i \ A \ f i < y" + by (metis cSUP_upper le_less_trans) + lemma cINF_insert: "A \ {} \ bdd_below (f ` A) \ INFI (insert a A) f = inf (f a) (INFI A f)" by (metis INF_def cInf_insert assms empty_is_image image_insert) @@ -347,11 +359,6 @@ instance complete_lattice \ conditionally_complete_lattice by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) -lemma isLub_cSup: - "(S::'a :: conditionally_complete_lattice set) \ {} \ (\b. S *<= b) \ isLub UNIV S (Sup S)" - by (auto simp add: isLub_def setle_def leastP_def isUb_def - intro!: setgeI cSup_upper cSup_least) - lemma cSup_eq: fixes a :: "'a :: {conditionally_complete_lattice, no_bot}" assumes upper: "\x. x \ X \ x \ a" @@ -370,12 +377,6 @@ assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le) qed (intro cInf_eq_non_empty assms) -lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \ {} \ S *<= b \ Sup S \ b" - by (metis cSup_least setle_def) - -lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \ {} \ b <=* S \ Inf S \ b" - by (metis cInf_greatest setge_def) - class conditionally_complete_linorder = conditionally_complete_lattice + linorder begin @@ -386,6 +387,12 @@ lemma cInf_less_iff: "X \ {} \ bdd_below X \ Inf X < y \ (\x\X. x < y)" by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans) +lemma cINF_less_iff: "A \ {} \ bdd_below (f`A) \ (INF i:A. f i) < a \ (\x\A. f x < a)" + unfolding INF_def using cInf_less_iff[of "f`A"] by auto + +lemma less_cSUP_iff: "A \ {} \ bdd_above (f`A) \ a < (SUP i:A. f i) \ (\x\A. a < f x)" + unfolding SUP_def using less_cSup_iff[of "f`A"] by auto + lemma less_cSupE: assumes "y < Sup X" "X \ {}" obtains x where "x \ X" "y < x" by (metis cSup_least assms not_le that) @@ -437,27 +444,6 @@ lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \ X \ {} \ Inf X = Min X" using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp -lemma cSup_bounds: - fixes S :: "'a :: conditionally_complete_lattice set" - assumes Se: "S \ {}" and l: "a <=* S" and u: "S *<= b" - shows "a \ Sup S \ Sup S \ b" -proof- - from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast - hence b: "Sup S \ b" using u - by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) - from Se obtain y where y: "y \ S" by blast - from lub l have "a \ Sup S" - by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) - (metis le_iff_sup le_sup_iff y) - with b show ?thesis by blast -qed - -lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \ (\b'x\S. b' < x) \ Sup S = b" - by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def) - -lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \ (\b'>b. \x\S. b' > x) \ Inf S = b" - by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def) - lemma cSup_lessThan[simp]: "Sup {..