# HG changeset patch
# User hoelzl
# Date 1300109856 -3600
# Node ID a54e8e95fe962311c31b22ab26a8d802681562a0
# Parent  47d6e13d17108c2489cb94a5ab19890b5c754513
add lemmas for SUP and INF

diff -r 47d6e13d1710 -r a54e8e95fe96 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Mar 14 14:37:35 2011 +0100
+++ b/src/HOL/Complete_Lattice.thy	Mon Mar 14 14:37:36 2011 +0100
@@ -89,25 +89,45 @@
   by (auto intro: Sup_least dest: Sup_upper)
 
 lemma Inf_mono:
-  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
-  shows "Inf A \<le> Inf B"
+  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
+  shows "Inf A \<sqsubseteq> Inf B"
 proof (rule Inf_greatest)
   fix b assume "b \<in> B"
-  with assms obtain a where "a \<in> A" and "a \<le> b" by blast
-  from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower)
-  with `a \<le> b` show "Inf A \<le> b" by auto
+  with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
+  from `a \<in> A` have "Inf A \<sqsubseteq> a" by (rule Inf_lower)
+  with `a \<sqsubseteq> b` show "Inf A \<sqsubseteq> b" by auto
 qed
 
 lemma Sup_mono:
-  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
-  shows "Sup A \<le> Sup B"
+  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
+  shows "Sup A \<sqsubseteq> Sup B"
 proof (rule Sup_least)
   fix a assume "a \<in> A"
-  with assms obtain b where "b \<in> B" and "a \<le> b" by blast
-  from `b \<in> B` have "b \<le> Sup B" by (rule Sup_upper)
-  with `a \<le> b` show "a \<le> Sup B" by auto
+  with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
+  from `b \<in> B` have "b \<sqsubseteq> Sup B" by (rule Sup_upper)
+  with `a \<sqsubseteq> b` show "a \<sqsubseteq> Sup B" by auto
 qed
 
+lemma top_le:
+  "top \<sqsubseteq> x \<Longrightarrow> x = top"
+  by (rule antisym) auto
+
+lemma le_bot:
+  "x \<sqsubseteq> bot \<Longrightarrow> x = bot"
+  by (rule antisym) auto
+
+lemma not_less_bot[simp]: "\<not> (x \<sqsubset> bot)"
+  using bot_least[of x] by (auto simp: le_less)
+
+lemma not_top_less[simp]: "\<not> (top \<sqsubset> x)"
+  using top_greatest[of x] by (auto simp: le_less)
+
+lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> Sup A"
+  using Sup_upper[of u A] by auto
+
+lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> Inf A \<sqsubseteq> v"
+  using Inf_lower[of u A] by auto
+
 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "INFI A f = \<Sqinter> (f ` A)"
 
@@ -146,15 +166,27 @@
 context complete_lattice
 begin
 
+lemma SUP_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> SUPR A f = SUPR A g"
+  by (simp add: SUPR_def cong: image_cong)
+
+lemma INF_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> INFI A f = INFI A g"
+  by (simp add: INFI_def cong: image_cong)
+
 lemma le_SUPI: "i : A \<Longrightarrow> M i \<sqsubseteq> (SUP i:A. M i)"
   by (auto simp add: SUPR_def intro: Sup_upper)
 
+lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (SUP i:A. M i)"
+  using le_SUPI[of i A M] by auto
+
 lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (SUP i:A. M i) \<sqsubseteq> u"
   by (auto simp add: SUPR_def intro: Sup_least)
 
 lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> M i"
   by (auto simp add: INFI_def intro: Inf_lower)
 
+lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> u"
+  using INF_leI[of i A M] by auto
+
 lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
   by (auto simp add: INFI_def intro: Inf_greatest)