src/HOL/Complete_Lattices.thy
 changeset 46557 ae926869a311 parent 46553 50a7e97fe653 child 46631 2c5c003cee35
```     1.1 --- a/src/HOL/Complete_Lattices.thy	Mon Feb 20 21:04:00 2012 +0100
1.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Feb 21 08:15:42 2012 +0100
1.3 @@ -536,7 +536,7 @@
1.4  end
1.5
1.6
1.7 -subsection {* @{typ bool} as complete lattice *}
1.8 +subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
1.9
1.10  instantiation bool :: complete_lattice
1.11  begin
1.12 @@ -573,9 +573,6 @@
1.13  instance bool :: complete_boolean_algebra proof
1.14  qed (auto intro: bool_induct)
1.15
1.16 -
1.17 -subsection {* @{typ "_ \<Rightarrow> _"} as complete lattice *}
1.18 -
1.19  instantiation "fun" :: (type, complete_lattice) complete_lattice
1.20  begin
1.21
1.22 @@ -611,54 +608,6 @@
1.23
1.24  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
1.25
1.26 -
1.27 -subsection {* Unary and binary predicates as complete lattice *}
1.28 -
1.29 -lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
1.30 -  by (simp add: INF_apply)
1.31 -
1.32 -lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
1.33 -  by (simp add: INF_apply)
1.34 -
1.35 -lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
1.36 -  by (auto simp add: INF_apply)
1.37 -
1.38 -lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
1.39 -  by (auto simp add: INF_apply)
1.40 -
1.41 -lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
1.42 -  by (auto simp add: INF_apply)
1.43 -
1.44 -lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
1.45 -  by (auto simp add: INF_apply)
1.46 -
1.47 -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"
1.48 -  by (auto simp add: INF_apply)
1.49 -
1.50 -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"
1.51 -  by (auto simp add: INF_apply)
1.52 -
1.53 -lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
1.54 -  by (simp add: SUP_apply)
1.55 -
1.56 -lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
1.57 -  by (simp add: SUP_apply)
1.58 -
1.59 -lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
1.60 -  by (auto simp add: SUP_apply)
1.61 -
1.62 -lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
1.63 -  by (auto simp add: SUP_apply)
1.64 -
1.65 -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"
1.66 -  by (auto simp add: SUP_apply)
1.67 -
1.68 -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"
1.69 -  by (auto simp add: SUP_apply)
1.70 -
1.71 -
1.72 -subsection {* @{typ "_ set"} as complete lattice *}
1.73 -
1.74  instantiation "set" :: (type) complete_lattice
1.75  begin
1.76
1.77 @@ -678,7 +627,7 @@
1.78  qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)
1.79
1.80
1.81 -subsubsection {* Inter *}
1.82 +subsection {* Inter *}
1.83
1.84  abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
1.85    "Inter S \<equiv> \<Sqinter>S"
1.86 @@ -750,7 +699,7 @@
1.87    by (fact Inf_superset_mono)
1.88
1.89
1.90 -subsubsection {* Intersections of families *}
1.91 +subsection {* Intersections of families *}
1.92
1.93  abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.94    "INTER \<equiv> INFI"
1.95 @@ -861,7 +810,7 @@
1.96    by blast
1.97
1.98
1.99 -subsubsection {* Union *}
1.100 +subsection {* Union *}
1.101
1.102  abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
1.103    "Union S \<equiv> \<Squnion>S"
1.104 @@ -930,7 +879,7 @@
1.105    by (fact Sup_subset_mono)
1.106
1.107
1.108 -subsubsection {* Unions of families *}
1.109 +subsection {* Unions of families *}
1.110
1.111  abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.112    "UNION \<equiv> SUPR"
1.113 @@ -1093,7 +1042,7 @@
1.114    by blast
1.115
1.116
1.117 -subsubsection {* Distributive laws *}
1.118 +subsection {* Distributive laws *}
1.119
1.120  lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
1.121    by (fact inf_Sup)
1.122 @@ -1135,7 +1084,7 @@
1.123    by (fact Sup_inf_eq_bot_iff)
1.124
1.125
1.126 -subsubsection {* Complement *}
1.127 +subsection {* Complement *}
1.128
1.129  lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
1.130    by (fact uminus_INF)
1.131 @@ -1144,7 +1093,7 @@
1.132    by (fact uminus_SUP)
1.133
1.134
1.135 -subsubsection {* Miniscoping and maxiscoping *}
1.136 +subsection {* Miniscoping and maxiscoping *}
1.137
1.138  text {* \medskip Miniscoping: pushing in quantifiers and big Unions
1.139             and Intersections. *}
```