src/HOL/Complete_Lattices.thy

--- a/src/HOL/Complete_Lattices.thy	Mon Feb 20 21:04:00 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy	Tue Feb 21 08:15:42 2012 +0100
@@ -536,7 +536,7 @@
 end
 
 
-subsection {* @{typ bool} as complete lattice *}
+subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
 
 instantiation bool :: complete_lattice
 begin
@@ -573,9 +573,6 @@
 instance bool :: complete_boolean_algebra proof
 qed (auto intro: bool_induct)
 
-
-subsection {* @{typ "_ \<Rightarrow> _"} as complete lattice *}
-
 instantiation "fun" :: (type, complete_lattice) complete_lattice
 begin
 
@@ -611,54 +608,6 @@
 
 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
 
-
-subsection {* Unary and binary predicates as complete lattice *}
-
-lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
-  by (simp add: INF_apply)
-
-lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
-  by (simp add: INF_apply)
-
-lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
-  by (auto simp add: INF_apply)
-
-lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
-  by (auto simp add: INF_apply)
-
-lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
-  by (auto simp add: INF_apply)
-
-lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
-  by (auto simp add: INF_apply)
-
-lemma INF1_E [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: INF_apply)
-
-lemma INF2_E [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: INF_apply)
-
-lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
-  by (simp add: SUP_apply)
-
-lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
-  by (simp add: SUP_apply)
-
-lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
-  by (auto simp add: SUP_apply)
-
-lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
-  by (auto simp add: SUP_apply)
-
-lemma SUP1_E [elim!]: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: SUP_apply)
-
-lemma SUP2_E [elim!]: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: SUP_apply)
-
-
-subsection {* @{typ "_ set"} as complete lattice *}
-
 instantiation "set" :: (type) complete_lattice
 begin
 
@@ -678,7 +627,7 @@
 qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)
   
 
-subsubsection {* Inter *}
+subsection {* Inter *}
 
 abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
   "Inter S \<equiv> \<Sqinter>S"
@@ -750,7 +699,7 @@
   by (fact Inf_superset_mono)
 
 
-subsubsection {* Intersections of families *}
+subsection {* Intersections of families *}
 
 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   "INTER \<equiv> INFI"
@@ -861,7 +810,7 @@
   by blast
 
 
-subsubsection {* Union *}
+subsection {* Union *}
 
 abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
   "Union S \<equiv> \<Squnion>S"
@@ -930,7 +879,7 @@
   by (fact Sup_subset_mono)
 
 
-subsubsection {* Unions of families *}
+subsection {* Unions of families *}
 
 abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   "UNION \<equiv> SUPR"
@@ -1093,7 +1042,7 @@
   by blast
 
 
-subsubsection {* Distributive laws *}
+subsection {* Distributive laws *}
 
 lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
   by (fact inf_Sup)
@@ -1135,7 +1084,7 @@
   by (fact Sup_inf_eq_bot_iff)
 
 
-subsubsection {* Complement *}
+subsection {* Complement *}
 
 lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
   by (fact uminus_INF)
@@ -1144,7 +1093,7 @@
   by (fact uminus_SUP)
 
 
-subsubsection {* Miniscoping and maxiscoping *}
+subsection {* Miniscoping and maxiscoping *}
 
 text {* \medskip Miniscoping: pushing in quantifiers and big Unions
            and Intersections. *}