# HG changeset patch
# User haftmann
# Date 1310927019 -7200
# Node ID 58be172c6ca4f3ca45f899a9813071d24adfd8b9
# Parent  58a7b3fdc193cab136b1f01c5858ace8873c2084# Parent  9684251c7ec1d5511342d9782b7e77c2c4a68110
merged

diff -r 58a7b3fdc193 -r 58be172c6ca4 NEWS
--- a/NEWS	Sun Jul 17 14:21:19 2011 +0200
+++ b/NEWS	Sun Jul 17 20:23:39 2011 +0200
@@ -63,6 +63,11 @@
 * Classes bot and top require underlying partial order rather than preorder:
 uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
 
+* Class 'complete_lattice': generalized a couple of lemmas from sets;
+generalized theorems INF_cong and SUP_cong.  More consistent names: TBD.
+
+INCOMPATIBILITY.
+
 * Archimedian_Field.thy:
     floor now is defined as parameter of a separate type class floor_ceiling.
  
diff -r 58a7b3fdc193 -r 58be172c6ca4 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 14:21:19 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:23:39 2011 +0200
@@ -33,7 +33,7 @@
 begin
 
 lemma dual_complete_lattice:
-  "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  "class.complete_lattice Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
   by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
     (unfold_locales, (fact bot_least top_greatest
         Sup_upper Sup_least Inf_lower Inf_greatest)+)
@@ -109,10 +109,79 @@
 qed
 
 lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
-  using Sup_upper[of u A] by auto
+  using Sup_upper [of u A] by auto
 
 lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
-  using Inf_lower[of u A] by auto
+  using Inf_lower [of u A] by auto
+
+lemma Inf_less_eq:
+  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
+    and "A \<noteq> {}"
+  shows "\<Sqinter>A \<sqsubseteq> u"
+proof -
+  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
+  moreover with assms have "v \<sqsubseteq> u" by blast
+  ultimately show ?thesis by (rule Inf_lower2)
+qed
+
+lemma less_eq_Sup:
+  assumes "\<And>v. v \<in> A \<Longrightarrow> u \<sqsubseteq> v"
+    and "A \<noteq> {}"
+  shows "u \<sqsubseteq> \<Squnion>A"
+proof -
+  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
+  moreover with assms have "u \<sqsubseteq> v" by blast
+  ultimately show ?thesis by (rule Sup_upper2)
+qed
+
+lemma Inf_inter_less_eq: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
+  by (auto intro: Inf_greatest Inf_lower)
+
+lemma Sup_inter_greater_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
+  by (auto intro: Sup_least Sup_upper)
+
+lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
+  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
+
+lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
+  by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
+
+lemma Inf_top_conv [no_atp]:
+  "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
+  "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
+proof -
+  show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
+  proof
+    assume "\<forall>x\<in>A. x = \<top>"
+    then have "A = {} \<or> A = {\<top>}" by auto
+    then show "\<Sqinter>A = \<top>" by auto
+  next
+    assume "\<Sqinter>A = \<top>"
+    show "\<forall>x\<in>A. x = \<top>"
+    proof (rule ccontr)
+      assume "\<not> (\<forall>x\<in>A. x = \<top>)"
+      then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
+      then obtain B where "A = insert x B" by blast
+      with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
+    qed
+  qed
+  then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
+qed
+
+lemma Sup_bot_conv [no_atp]:
+  "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
+  "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
+proof -
+  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+    by (fact dual_complete_lattice)
+  from dual.Inf_top_conv show ?P and ?Q by simp_all
+qed
+
+lemma Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
+  by (auto intro: Inf_greatest Inf_lower)
+
+lemma Sup_anti_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
+  by (auto intro: Sup_least Sup_upper)
 
 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "INFI A f = \<Sqinter> (f ` A)"
@@ -152,66 +221,116 @@
 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 INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
+  by (simp add: INFI_def)
 
-lemma le_SUPI: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
-  by (auto simp add: SUPR_def intro: Sup_upper)
+lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
+  by (simp add: INFI_def Inf_insert)
 
-lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
-  using le_SUPI[of i A M] by auto
-
-lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. M i) \<sqsubseteq> u"
-  by (auto simp add: SUPR_def intro: Sup_least)
-
-lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> M i"
+lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
   by (auto simp add: INFI_def intro: Inf_lower)
 
-lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> u"
-  using INF_leI[of i A M] by auto
+lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
+  using INF_leI [of i A f] by auto
 
-lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. M i)"
+lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
   by (auto simp add: INFI_def intro: Inf_greatest)
 
-lemma SUP_le_iff: "(\<Squnion>i\<in>A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
-  unfolding SUPR_def by (auto simp add: Sup_le_iff)
+lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
+  by (auto simp add: INFI_def le_Inf_iff)
 
-lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
-  unfolding INFI_def by (auto simp add: le_Inf_iff)
-
-lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. M) = M"
+lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
   by (auto intro: antisym INF_leI le_INFI)
 
-lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. M) = M"
-  by (auto intro: antisym SUP_leI le_SUPI)
+lemma INF_cong:
+  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Sqinter>x\<in>A. C x) = (\<Sqinter>x\<in>B. D x)"
+  by (simp add: INFI_def image_def)
 
 lemma INF_mono:
   "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
   by (force intro!: Inf_mono simp: INFI_def)
 
+lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
+  by (intro INF_mono) auto
+
+lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
+  by (iprover intro: INF_leI le_INFI order_trans antisym)
+
+lemma (in complete_lattice) INFI_empty:
+  "(\<Sqinter>x\<in>{}. B x) = \<top>"
+  by (simp add: INFI_def)
+
+lemma (in complete_lattice) INFI_absorb:
+  assumes "k \<in> I"
+  shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
+proof -
+  from assms obtain J where "I = insert k J" by blast
+  then show ?thesis by (simp add: INF_insert)
+qed
+
+lemma (in complete_lattice) INF_union:
+  "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
+  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INFI INF_leI)
+
+lemma (in complete_lattice) INF_constant:
+  "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
+  by (simp add: INF_empty)
+
+lemma (in complete_lattice) INF_eq:
+  "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
+  by (simp add: INFI_def image_def)
+
+lemma (in complete_lattice) INF_top_conv:
+ "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
+ "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
+  by (auto simp add: INFI_def Inf_top_conv)
+
+lemma (in complete_lattice) INFI_UNIV_range:
+  "(\<Sqinter>x\<in>UNIV. f x) = \<Sqinter>range f"
+  by (simp add: INFI_def)
+
+lemma (in complete_lattice) INF_bool_eq:
+  "(\<Sqinter>b. A b) = A True \<sqinter> A False"
+  by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
+
+lemma (in complete_lattice) INF_anti_mono:
+  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>B. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
+  -- {* The last inclusion is POSITIVE! *}
+  by (blast intro: INF_mono dest: subsetD)
+
+lemma SUP_cong:
+  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Squnion>x\<in>A. C x) = (\<Squnion>x\<in>B. D x)"
+  by (simp add: SUPR_def image_def)
+
+lemma le_SUPI: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+  by (auto simp add: SUPR_def intro: Sup_upper)
+
+lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+  using le_SUPI [of i A f] by auto
+
+lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
+  by (auto simp add: SUPR_def intro: Sup_least)
+
+lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
+  unfolding SUPR_def by (auto simp add: Sup_le_iff)
+
+lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
+  by (auto intro: antisym SUP_leI le_SUPI)
+
 lemma SUP_mono:
   "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
   by (force intro!: Sup_mono simp: SUPR_def)
 
-lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
-  by (intro INF_mono) auto
-
 lemma SUP_subset:  "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
   by (intro SUP_mono) auto
 
-lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
-  by (iprover intro: INF_leI le_INFI order_trans antisym)
-
 lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
   by (iprover intro: SUP_leI le_SUPI order_trans antisym)
 
-lemma INFI_insert: "(\<Sqinter>x\<in>insert a A. B x) = B a \<sqinter> INFI A B"
-  by (simp add: INFI_def Inf_insert)
+lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
+  by (simp add: SUPR_def)
 
-lemma SUPR_insert: "(\<Squnion>x\<in>insert a A. B x) = B a \<squnion> SUPR A B"
+lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   by (simp add: SUPR_def Sup_insert)
 
 end
@@ -221,16 +340,16 @@
   shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   unfolding not_le [symmetric] le_Inf_iff by auto
 
+lemma INF_less_iff:
+  fixes a :: "'a::{complete_lattice,linorder}"
+  shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
+  unfolding INFI_def Inf_less_iff by auto
+
 lemma less_Sup_iff:
   fixes a :: "'a\<Colon>{complete_lattice,linorder}"
   shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   unfolding not_le [symmetric] Sup_le_iff by auto
 
-lemma INF_less_iff:
-  fixes a :: "'a::{complete_lattice,linorder}"
-  shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
-  unfolding INFI_def Inf_less_iff by auto
-
 lemma less_SUP_iff:
   fixes a :: "'a::{complete_lattice,linorder}"
   shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
@@ -343,16 +462,6 @@
 lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
   by (fact Inf_lower)
 
-lemma (in complete_lattice) Inf_less_eq:
-  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
-    and "A \<noteq> {}"
-  shows "\<Sqinter>A \<sqsubseteq> u"
-proof -
-  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
-  moreover with assms have "v \<sqsubseteq> u" by blast
-  ultimately show ?thesis by (rule Inf_lower2)
-qed
-
 lemma Inter_subset:
   "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
   by (fact Inf_less_eq)
@@ -372,48 +481,17 @@
 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
   by (fact Inf_insert)
 
-lemma (in complete_lattice) Inf_inter_less: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
-  by (auto intro: Inf_greatest Inf_lower)
-
 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
-  by (fact Inf_inter_less)
-
-lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
-  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
+  by (fact Inf_inter_less_eq)
 
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   by (fact Inf_union_distrib)
 
-lemma (in complete_lattice) Inf_top_conv [no_atp]:
-  "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
-  "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
-proof -
-  show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
-  proof
-    assume "\<forall>x\<in>A. x = \<top>"
-    then have "A = {} \<or> A = {\<top>}" by auto
-    then show "\<Sqinter>A = \<top>" by auto
-  next
-    assume "\<Sqinter>A = \<top>"
-    show "\<forall>x\<in>A. x = \<top>"
-    proof (rule ccontr)
-      assume "\<not> (\<forall>x\<in>A. x = \<top>)"
-      then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
-      then obtain B where "A = insert x B" by blast
-      with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
-    qed
-  qed
-  then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
-qed
-
-lemma Inter_UNIV_conv [simp,no_atp]:
+lemma Inter_UNIV_conv [simp, no_atp]:
   "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   by (fact Inf_top_conv)+
 
-lemma (in complete_lattice) Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
-  by (auto intro: Inf_greatest Inf_lower)
-
 lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
   by (fact Inf_anti_mono)
 
@@ -474,13 +552,9 @@
   -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
   by (unfold INTER_def) blast
 
-lemma (in complete_lattice) INFI_cong:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Sqinter>x\<in>A. C x) = (\<Sqinter>x\<in>B. D x)"
-  by (simp add: INFI_def image_def)
-
 lemma INT_cong [cong]:
   "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Inter>x\<in>A. C x) = (\<Inter>x\<in>B. D x)"
-  by (fact INFI_cong)
+  by (fact INF_cong)
 
 lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
   by blast
@@ -494,21 +568,9 @@
 lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
   by (fact le_INFI)
 
-lemma (in complete_lattice) INFI_empty:
-  "(\<Sqinter>x\<in>{}. B x) = \<top>"
-  by (simp add: INFI_def)
-
 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
   by (fact INFI_empty)
 
-lemma (in complete_lattice) INFI_absorb:
-  assumes "k \<in> I"
-  shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
-proof -
-  from assms obtain J where "I = insert k J" by blast
-  then show ?thesis by (simp add: INFI_insert)
-qed
-
 lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
   by (fact INFI_absorb)
 
@@ -516,41 +578,38 @@
   by (fact le_INF_iff)
 
 lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
-  by (fact INFI_insert)
-
--- {* continue generalization from here *}
+  by (fact INF_insert)
 
 lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
-  by blast
+  by (fact INF_union)
 
 lemma INT_insert_distrib:
-    "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
+  "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   by blast
 
 lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
-  by auto
+  by (fact INF_constant)
 
 lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
   -- {* Look: it has an \emph{existential} quantifier *}
-  by blast
+  by (fact INF_eq)
 
 lemma INTER_UNIV_conv [simp]:
  "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
  "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
-  by blast+
+  by (fact INF_top_conv)+
+
+lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
+  by (fact INF_bool_eq)
 
-lemma INT_bool_eq: "(\<Inter>b. A b) = (A True \<inter> A False)"
-  by (auto intro: bool_induct)
+lemma INT_anti_mono:
+  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>B. g x)"
+  -- {* The last inclusion is POSITIVE! *}
+  by (fact INF_anti_mono)
 
 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
   by blast
 
-lemma INT_anti_mono:
-  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
-    (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
-  -- {* The last inclusion is POSITIVE! *}
-  by (blast dest: subsetD)
-
 lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)"
   by blast
 
diff -r 58a7b3fdc193 -r 58be172c6ca4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Jul 17 14:21:19 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Jul 17 20:23:39 2011 +0200
@@ -477,20 +477,14 @@
 lemma finite [simp]: "finite (A \<Colon> 'a set)"
   by (rule subset_UNIV finite_UNIV finite_subset)+
 
-lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
+lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True"
   by simp
 
 end
 
-lemma UNIV_unit [no_atp]:
-  "UNIV = {()}" by auto
-
 instance unit :: finite proof
 qed (simp add: UNIV_unit)
 
-lemma UNIV_bool [no_atp]:
-  "UNIV = {False, True}" by auto
-
 instance bool :: finite proof
 qed (simp add: UNIV_bool)
 
diff -r 58a7b3fdc193 -r 58be172c6ca4 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Jul 17 14:21:19 2011 +0200
+++ b/src/HOL/Product_Type.thy	Sun Jul 17 20:23:39 2011 +0200
@@ -84,9 +84,12 @@
   f} rather than by @{term [source] "%u. f ()"}.
 *}
 
-lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp, no_atp]: "(%u::unit. f ()) = f"
   by (rule ext) simp
 
+lemma UNIV_unit [no_atp]:
+  "UNIV = {()}" by auto
+
 instantiation unit :: default
 begin
 
diff -r 58a7b3fdc193 -r 58be172c6ca4 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Jul 17 14:21:19 2011 +0200
+++ b/src/HOL/Set.thy	Sun Jul 17 20:23:39 2011 +0200
@@ -1487,6 +1487,9 @@
 lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
   by (auto intro: bool_contrapos)
 
+lemma UNIV_bool [no_atp]: "UNIV = {False, True}"
+  by (auto intro: bool_induct)
+
 text {* \medskip @{text Pow} *}
 
 lemma Pow_empty [simp]: "Pow {} = {{}}"