src/HOL/Complete_Lattices.thy
 changeset 46553 50a7e97fe653 parent 46154 5115e47a7752 child 46557 ae926869a311
```--- a/src/HOL/Complete_Lattices.thy	Mon Feb 20 15:17:03 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy	Sun Feb 19 15:30:35 2012 +0100
@@ -536,7 +536,7 @@
end

-subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
+subsection {* @{typ bool} as complete lattice *}

instantiation bool :: complete_lattice
begin
@@ -573,6 +573,9 @@
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

@@ -608,6 +611,54 @@

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)"
+
+lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
+
+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)"
+
+lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
+
+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

@@ -627,7 +678,7 @@
qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)

-subsection {* Inter *}
+subsubsection {* Inter *}

abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
"Inter S \<equiv> \<Sqinter>S"
@@ -699,7 +750,7 @@
by (fact Inf_superset_mono)

-subsection {* Intersections of families *}
+subsubsection {* Intersections of families *}

abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
"INTER \<equiv> INFI"
@@ -810,7 +861,7 @@
by blast

-subsection {* Union *}
+subsubsection {* Union *}

abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
"Union S \<equiv> \<Squnion>S"
@@ -879,7 +930,7 @@
by (fact Sup_subset_mono)

-subsection {* Unions of families *}
+subsubsection {* Unions of families *}

abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
"UNION \<equiv> SUPR"
@@ -1042,7 +1093,7 @@
by blast

-subsection {* Distributive laws *}
+subsubsection {* Distributive laws *}

lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
by (fact inf_Sup)
@@ -1084,7 +1135,7 @@
by (fact Sup_inf_eq_bot_iff)

-subsection {* Complement *}
+subsubsection {* Complement *}

lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
by (fact uminus_INF)
@@ -1093,7 +1144,7 @@
by (fact uminus_SUP)

-subsection {* Miniscoping and maxiscoping *}
+subsubsection {* Miniscoping and maxiscoping *}

text {* \medskip Miniscoping: pushing in quantifiers and big Unions
and Intersections. *}```