# HG changeset patch # User huffman # Date 1267891710 28800 # Node ID 57f1a5e93b6b8600a6e85b7221915c45100192bd # Parent 0f2c634c8ab7395c1854810282a6116ecca660f0 add some lemmas about complete lattices diff -r 0f2c634c8ab7 -r 57f1a5e93b6b src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Sat Mar 06 11:21:09 2010 +0100 +++ b/src/HOL/Complete_Lattice.thy Sat Mar 06 08:08:30 2010 -0800 @@ -82,6 +82,12 @@ "\UNIV = top" by (simp add: Inf_Sup Inf_empty [symmetric]) +lemma Sup_le_iff: "Sup A \ b \ (\a\A. a \ b)" + by (auto intro: Sup_least dest: Sup_upper) + +lemma le_Inf_iff: "b \ Inf A \ (\a\A. b \ a)" + by (auto intro: Inf_greatest dest: Inf_lower) + definition SUPR :: "'b set \ ('b \ 'a) \ 'a" where "SUPR A f = \ (f ` A)" @@ -126,6 +132,12 @@ lemma le_INFI: "(\i. i : A \ u \ M i) \ u \ (INF i:A. M i)" by (auto simp add: INFI_def intro: Inf_greatest) +lemma SUP_le_iff: "(SUP i:A. M i) \ u \ (\i \ A. M i \ u)" + unfolding SUPR_def by (auto simp add: Sup_le_iff) + +lemma le_INF_iff: "u \ (INF i:A. M i) \ (\i \ A. u \ M i)" + unfolding INFI_def by (auto simp add: le_Inf_iff) + lemma SUP_const[simp]: "A \ {} \ (SUP i:A. M) = M" by (auto intro: antisym SUP_leI le_SUPI) @@ -384,7 +396,7 @@ by blast lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)" - by blast + by (fact SUP_le_iff) lemma image_Union: "f ` \S = (\x\S. f ` x)" by blast @@ -591,7 +603,7 @@ by blast lemma INT_subset_iff: "(B \ (\i\I. A i)) = (\i\I. B \ A i)" - by blast + by (fact le_INF_iff) lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ INTER A B" by blast