renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
authorhaftmann
Sat Sep 10 10:29:24 2011 +0200 (2011-09-10)
changeset 4486056101fa00193
parent 44859 237ba63d6041
child 44861 329ced2615eb
child 44868 92be5b32ca71
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
src/HOL/Complete_Lattice.thy
src/HOL/Complete_Lattices.thy
src/HOL/Fun.thy
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Inductive.thy
src/HOL/IsaMakefile
src/HOL/Library/Executable_Set.thy
src/HOL/Library/Lattice_Syntax.thy
src/HOL/Main.thy
src/HOL/Quotient_Examples/Cset.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Sat Sep 10 00:44:25 2011 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,1259 +0,0 @@
     1.4 - (*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
     1.5 -
     1.6 -header {* Complete lattices *}
     1.7 -
     1.8 -theory Complete_Lattice
     1.9 -imports Set
    1.10 -begin
    1.11 -
    1.12 -notation
    1.13 -  less_eq (infix "\<sqsubseteq>" 50) and
    1.14 -  less (infix "\<sqsubset>" 50) and
    1.15 -  inf (infixl "\<sqinter>" 70) and
    1.16 -  sup (infixl "\<squnion>" 65) and
    1.17 -  top ("\<top>") and
    1.18 -  bot ("\<bottom>")
    1.19 -
    1.20 -
    1.21 -subsection {* Syntactic infimum and supremum operations *}
    1.22 -
    1.23 -class Inf =
    1.24 -  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    1.25 -
    1.26 -class Sup =
    1.27 -  fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.28 -
    1.29 -subsection {* Abstract complete lattices *}
    1.30 -
    1.31 -class complete_lattice = bounded_lattice + Inf + Sup +
    1.32 -  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    1.33 -     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.34 -  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    1.35 -     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
    1.36 -begin
    1.37 -
    1.38 -lemma dual_complete_lattice:
    1.39 -  "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
    1.40 -  by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
    1.41 -    (unfold_locales, (fact bot_least top_greatest
    1.42 -        Sup_upper Sup_least Inf_lower Inf_greatest)+)
    1.43 -
    1.44 -definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.45 -  INF_def: "INFI A f = \<Sqinter>(f ` A)"
    1.46 -
    1.47 -definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.48 -  SUP_def: "SUPR A f = \<Squnion>(f ` A)"
    1.49 -
    1.50 -text {*
    1.51 -  Note: must use names @{const INFI} and @{const SUPR} here instead of
    1.52 -  @{text INF} and @{text SUP} to allow the following syntax coexist
    1.53 -  with the plain constant names.
    1.54 -*}
    1.55 -
    1.56 -end
    1.57 -
    1.58 -syntax
    1.59 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
    1.60 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    1.61 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
    1.62 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    1.63 -
    1.64 -syntax (xsymbols)
    1.65 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.66 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.67 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    1.68 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    1.69 -
    1.70 -translations
    1.71 -  "INF x y. B"   == "INF x. INF y. B"
    1.72 -  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
    1.73 -  "INF x. B"     == "INF x:CONST UNIV. B"
    1.74 -  "INF x:A. B"   == "CONST INFI A (%x. B)"
    1.75 -  "SUP x y. B"   == "SUP x. SUP y. B"
    1.76 -  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
    1.77 -  "SUP x. B"     == "SUP x:CONST UNIV. B"
    1.78 -  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
    1.79 -
    1.80 -print_translation {*
    1.81 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
    1.82 -    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
    1.83 -*} -- {* to avoid eta-contraction of body *}
    1.84 -
    1.85 -context complete_lattice
    1.86 -begin
    1.87 -
    1.88 -lemma INF_foundation_dual [no_atp]:
    1.89 -  "complete_lattice.SUPR Inf = INFI"
    1.90 -proof (rule ext)+
    1.91 -  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
    1.92 -    by (fact dual_complete_lattice)
    1.93 -  fix f :: "'b \<Rightarrow> 'a" and A
    1.94 -  show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
    1.95 -    by (simp only: dual.SUP_def INF_def)
    1.96 -qed
    1.97 -
    1.98 -lemma SUP_foundation_dual [no_atp]:
    1.99 -  "complete_lattice.INFI Sup = SUPR"
   1.100 -proof (rule ext)+
   1.101 -  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
   1.102 -    by (fact dual_complete_lattice)
   1.103 -  fix f :: "'b \<Rightarrow> 'a" and A
   1.104 -  show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
   1.105 -    by (simp only: dual.INF_def SUP_def)
   1.106 -qed
   1.107 -
   1.108 -lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
   1.109 -  by (auto simp add: INF_def intro: Inf_lower)
   1.110 -
   1.111 -lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
   1.112 -  by (auto simp add: INF_def intro: Inf_greatest)
   1.113 -
   1.114 -lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
   1.115 -  by (auto simp add: SUP_def intro: Sup_upper)
   1.116 -
   1.117 -lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
   1.118 -  by (auto simp add: SUP_def intro: Sup_least)
   1.119 -
   1.120 -lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
   1.121 -  using Inf_lower [of u A] by auto
   1.122 -
   1.123 -lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
   1.124 -  using INF_lower [of i A f] by auto
   1.125 -
   1.126 -lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
   1.127 -  using Sup_upper [of u A] by auto
   1.128 -
   1.129 -lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
   1.130 -  using SUP_upper [of i A f] by auto
   1.131 -
   1.132 -lemma le_Inf_iff (*[simp]*): "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
   1.133 -  by (auto intro: Inf_greatest dest: Inf_lower)
   1.134 -
   1.135 -lemma le_INF_iff (*[simp]*): "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
   1.136 -  by (auto simp add: INF_def le_Inf_iff)
   1.137 -
   1.138 -lemma Sup_le_iff (*[simp]*): "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
   1.139 -  by (auto intro: Sup_least dest: Sup_upper)
   1.140 -
   1.141 -lemma SUP_le_iff (*[simp]*): "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
   1.142 -  by (auto simp add: SUP_def Sup_le_iff)
   1.143 -
   1.144 -lemma Inf_empty [simp]:
   1.145 -  "\<Sqinter>{} = \<top>"
   1.146 -  by (auto intro: antisym Inf_greatest)
   1.147 -
   1.148 -lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   1.149 -  by (simp add: INF_def)
   1.150 -
   1.151 -lemma Sup_empty [simp]:
   1.152 -  "\<Squnion>{} = \<bottom>"
   1.153 -  by (auto intro: antisym Sup_least)
   1.154 -
   1.155 -lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
   1.156 -  by (simp add: SUP_def)
   1.157 -
   1.158 -lemma Inf_UNIV [simp]:
   1.159 -  "\<Sqinter>UNIV = \<bottom>"
   1.160 -  by (auto intro!: antisym Inf_lower)
   1.161 -
   1.162 -lemma Sup_UNIV [simp]:
   1.163 -  "\<Squnion>UNIV = \<top>"
   1.164 -  by (auto intro!: antisym Sup_upper)
   1.165 -
   1.166 -lemma Inf_insert (*[simp]*): "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   1.167 -  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   1.168 -
   1.169 -lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
   1.170 -  by (simp add: INF_def Inf_insert)
   1.171 -
   1.172 -lemma Sup_insert (*[simp]*): "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   1.173 -  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
   1.174 -
   1.175 -lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   1.176 -  by (simp add: SUP_def Sup_insert)
   1.177 -
   1.178 -lemma INF_image (*[simp]*): "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
   1.179 -  by (simp add: INF_def image_image)
   1.180 -
   1.181 -lemma SUP_image (*[simp]*): "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
   1.182 -  by (simp add: SUP_def image_image)
   1.183 -
   1.184 -lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
   1.185 -  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   1.186 -
   1.187 -lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
   1.188 -  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   1.189 -
   1.190 -lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
   1.191 -  by (auto intro: Inf_greatest Inf_lower)
   1.192 -
   1.193 -lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
   1.194 -  by (auto intro: Sup_least Sup_upper)
   1.195 -
   1.196 -lemma INF_cong:
   1.197 -  "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)"
   1.198 -  by (simp add: INF_def image_def)
   1.199 -
   1.200 -lemma SUP_cong:
   1.201 -  "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)"
   1.202 -  by (simp add: SUP_def image_def)
   1.203 -
   1.204 -lemma Inf_mono:
   1.205 -  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
   1.206 -  shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
   1.207 -proof (rule Inf_greatest)
   1.208 -  fix b assume "b \<in> B"
   1.209 -  with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
   1.210 -  from `a \<in> A` have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
   1.211 -  with `a \<sqsubseteq> b` show "\<Sqinter>A \<sqsubseteq> b" by auto
   1.212 -qed
   1.213 -
   1.214 -lemma INF_mono:
   1.215 -  "(\<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)"
   1.216 -  by (force intro!: Inf_mono simp: INF_def)
   1.217 -
   1.218 -lemma Sup_mono:
   1.219 -  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
   1.220 -  shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
   1.221 -proof (rule Sup_least)
   1.222 -  fix a assume "a \<in> A"
   1.223 -  with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
   1.224 -  from `b \<in> B` have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
   1.225 -  with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
   1.226 -qed
   1.227 -
   1.228 -lemma SUP_mono:
   1.229 -  "(\<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)"
   1.230 -  by (force intro!: Sup_mono simp: SUP_def)
   1.231 -
   1.232 -lemma INF_superset_mono:
   1.233 -  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
   1.234 -  -- {* The last inclusion is POSITIVE! *}
   1.235 -  by (blast intro: INF_mono dest: subsetD)
   1.236 -
   1.237 -lemma SUP_subset_mono:
   1.238 -  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
   1.239 -  by (blast intro: SUP_mono dest: subsetD)
   1.240 -
   1.241 -lemma Inf_less_eq:
   1.242 -  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
   1.243 -    and "A \<noteq> {}"
   1.244 -  shows "\<Sqinter>A \<sqsubseteq> u"
   1.245 -proof -
   1.246 -  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
   1.247 -  moreover with assms have "v \<sqsubseteq> u" by blast
   1.248 -  ultimately show ?thesis by (rule Inf_lower2)
   1.249 -qed
   1.250 -
   1.251 -lemma less_eq_Sup:
   1.252 -  assumes "\<And>v. v \<in> A \<Longrightarrow> u \<sqsubseteq> v"
   1.253 -    and "A \<noteq> {}"
   1.254 -  shows "u \<sqsubseteq> \<Squnion>A"
   1.255 -proof -
   1.256 -  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
   1.257 -  moreover with assms have "u \<sqsubseteq> v" by blast
   1.258 -  ultimately show ?thesis by (rule Sup_upper2)
   1.259 -qed
   1.260 -
   1.261 -lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
   1.262 -  by (auto intro: Inf_greatest Inf_lower)
   1.263 -
   1.264 -lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
   1.265 -  by (auto intro: Sup_least Sup_upper)
   1.266 -
   1.267 -lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   1.268 -  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
   1.269 -
   1.270 -lemma INF_union:
   1.271 -  "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
   1.272 -  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
   1.273 -
   1.274 -lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
   1.275 -  by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
   1.276 -
   1.277 -lemma SUP_union:
   1.278 -  "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
   1.279 -  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
   1.280 -
   1.281 -lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)"
   1.282 -  by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
   1.283 -
   1.284 -lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)"
   1.285 -  by (rule antisym) (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono,
   1.286 -    rule SUP_least, auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
   1.287 -
   1.288 -lemma Inf_top_conv (*[simp]*) [no_atp]:
   1.289 -  "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
   1.290 -  "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
   1.291 -proof -
   1.292 -  show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
   1.293 -  proof
   1.294 -    assume "\<forall>x\<in>A. x = \<top>"
   1.295 -    then have "A = {} \<or> A = {\<top>}" by auto
   1.296 -    then show "\<Sqinter>A = \<top>" by (auto simp add: Inf_insert)
   1.297 -  next
   1.298 -    assume "\<Sqinter>A = \<top>"
   1.299 -    show "\<forall>x\<in>A. x = \<top>"
   1.300 -    proof (rule ccontr)
   1.301 -      assume "\<not> (\<forall>x\<in>A. x = \<top>)"
   1.302 -      then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
   1.303 -      then obtain B where "A = insert x B" by blast
   1.304 -      with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
   1.305 -    qed
   1.306 -  qed
   1.307 -  then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
   1.308 -qed
   1.309 -
   1.310 -lemma INF_top_conv (*[simp]*):
   1.311 - "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   1.312 - "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   1.313 -  by (auto simp add: INF_def Inf_top_conv)
   1.314 -
   1.315 -lemma Sup_bot_conv (*[simp]*) [no_atp]:
   1.316 -  "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
   1.317 -  "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
   1.318 -proof -
   1.319 -  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
   1.320 -    by (fact dual_complete_lattice)
   1.321 -  from dual.Inf_top_conv show ?P and ?Q by simp_all
   1.322 -qed
   1.323 -
   1.324 -lemma SUP_bot_conv (*[simp]*):
   1.325 - "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   1.326 - "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   1.327 -  by (auto simp add: SUP_def Sup_bot_conv)
   1.328 -
   1.329 -lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
   1.330 -  by (auto intro: antisym INF_lower INF_greatest)
   1.331 -
   1.332 -lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
   1.333 -  by (auto intro: antisym SUP_upper SUP_least)
   1.334 -
   1.335 -lemma INF_top (*[simp]*): "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   1.336 -  by (cases "A = {}") (simp_all add: INF_empty)
   1.337 -
   1.338 -lemma SUP_bot (*[simp]*): "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
   1.339 -  by (cases "A = {}") (simp_all add: SUP_empty)
   1.340 -
   1.341 -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)"
   1.342 -  by (iprover intro: INF_lower INF_greatest order_trans antisym)
   1.343 -
   1.344 -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)"
   1.345 -  by (iprover intro: SUP_upper SUP_least order_trans antisym)
   1.346 -
   1.347 -lemma INF_absorb:
   1.348 -  assumes "k \<in> I"
   1.349 -  shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
   1.350 -proof -
   1.351 -  from assms obtain J where "I = insert k J" by blast
   1.352 -  then show ?thesis by (simp add: INF_insert)
   1.353 -qed
   1.354 -
   1.355 -lemma SUP_absorb:
   1.356 -  assumes "k \<in> I"
   1.357 -  shows "A k \<squnion> (\<Squnion>i\<in>I. A i) = (\<Squnion>i\<in>I. A i)"
   1.358 -proof -
   1.359 -  from assms obtain J where "I = insert k J" by blast
   1.360 -  then show ?thesis by (simp add: SUP_insert)
   1.361 -qed
   1.362 -
   1.363 -lemma INF_constant:
   1.364 -  "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   1.365 -  by (simp add: INF_empty)
   1.366 -
   1.367 -lemma SUP_constant:
   1.368 -  "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
   1.369 -  by (simp add: SUP_empty)
   1.370 -
   1.371 -lemma less_INF_D:
   1.372 -  assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
   1.373 -proof -
   1.374 -  note `y < (\<Sqinter>i\<in>A. f i)`
   1.375 -  also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using `i \<in> A`
   1.376 -    by (rule INF_lower)
   1.377 -  finally show "y < f i" .
   1.378 -qed
   1.379 -
   1.380 -lemma SUP_lessD:
   1.381 -  assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
   1.382 -proof -
   1.383 -  have "f i \<le> (\<Squnion>i\<in>A. f i)" using `i \<in> A`
   1.384 -    by (rule SUP_upper)
   1.385 -  also note `(\<Squnion>i\<in>A. f i) < y`
   1.386 -  finally show "f i < y" .
   1.387 -qed
   1.388 -
   1.389 -lemma INF_UNIV_bool_expand:
   1.390 -  "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   1.391 -  by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
   1.392 -
   1.393 -lemma SUP_UNIV_bool_expand:
   1.394 -  "(\<Squnion>b. A b) = A True \<squnion> A False"
   1.395 -  by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
   1.396 -
   1.397 -end
   1.398 -
   1.399 -class complete_distrib_lattice = complete_lattice +
   1.400 -  assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   1.401 -  assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   1.402 -begin
   1.403 -
   1.404 -lemma sup_INF:
   1.405 -  "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   1.406 -  by (simp add: INF_def sup_Inf image_image)
   1.407 -
   1.408 -lemma inf_SUP:
   1.409 -  "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   1.410 -  by (simp add: SUP_def inf_Sup image_image)
   1.411 -
   1.412 -lemma dual_complete_distrib_lattice:
   1.413 -  "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   1.414 -  apply (rule class.complete_distrib_lattice.intro)
   1.415 -  apply (fact dual_complete_lattice)
   1.416 -  apply (rule class.complete_distrib_lattice_axioms.intro)
   1.417 -  apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf)
   1.418 -  done
   1.419 -
   1.420 -subclass distrib_lattice proof
   1.421 -  fix a b c
   1.422 -  from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
   1.423 -  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
   1.424 -qed
   1.425 -
   1.426 -lemma Inf_sup:
   1.427 -  "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
   1.428 -  by (simp add: sup_Inf sup_commute)
   1.429 -
   1.430 -lemma Sup_inf:
   1.431 -  "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
   1.432 -  by (simp add: inf_Sup inf_commute)
   1.433 -
   1.434 -lemma INF_sup: 
   1.435 -  "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
   1.436 -  by (simp add: sup_INF sup_commute)
   1.437 -
   1.438 -lemma SUP_inf:
   1.439 -  "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
   1.440 -  by (simp add: inf_SUP inf_commute)
   1.441 -
   1.442 -lemma Inf_sup_eq_top_iff:
   1.443 -  "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
   1.444 -  by (simp only: Inf_sup INF_top_conv)
   1.445 -
   1.446 -lemma Sup_inf_eq_bot_iff:
   1.447 -  "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
   1.448 -  by (simp only: Sup_inf SUP_bot_conv)
   1.449 -
   1.450 -lemma INF_sup_distrib2:
   1.451 -  "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)"
   1.452 -  by (subst INF_commute) (simp add: sup_INF INF_sup)
   1.453 -
   1.454 -lemma SUP_inf_distrib2:
   1.455 -  "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)"
   1.456 -  by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
   1.457 -
   1.458 -end
   1.459 -
   1.460 -class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice
   1.461 -begin
   1.462 -
   1.463 -lemma dual_complete_boolean_algebra:
   1.464 -  "class.complete_boolean_algebra Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
   1.465 -  by (rule class.complete_boolean_algebra.intro, rule dual_complete_distrib_lattice, rule dual_boolean_algebra)
   1.466 -
   1.467 -lemma uminus_Inf:
   1.468 -  "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
   1.469 -proof (rule antisym)
   1.470 -  show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
   1.471 -    by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
   1.472 -  show "\<Squnion>(uminus ` A) \<le> - \<Sqinter>A"
   1.473 -    by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto
   1.474 -qed
   1.475 -
   1.476 -lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
   1.477 -  by (simp add: INF_def SUP_def uminus_Inf image_image)
   1.478 -
   1.479 -lemma uminus_Sup:
   1.480 -  "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
   1.481 -proof -
   1.482 -  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_Inf)
   1.483 -  then show ?thesis by simp
   1.484 -qed
   1.485 -  
   1.486 -lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
   1.487 -  by (simp add: INF_def SUP_def uminus_Sup image_image)
   1.488 -
   1.489 -end
   1.490 -
   1.491 -class complete_linorder = linorder + complete_lattice
   1.492 -begin
   1.493 -
   1.494 -lemma dual_complete_linorder:
   1.495 -  "class.complete_linorder Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   1.496 -  by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
   1.497 -
   1.498 -lemma Inf_less_iff (*[simp]*):
   1.499 -  "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   1.500 -  unfolding not_le [symmetric] le_Inf_iff by auto
   1.501 -
   1.502 -lemma INF_less_iff (*[simp]*):
   1.503 -  "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   1.504 -  unfolding INF_def Inf_less_iff by auto
   1.505 -
   1.506 -lemma less_Sup_iff (*[simp]*):
   1.507 -  "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   1.508 -  unfolding not_le [symmetric] Sup_le_iff by auto
   1.509 -
   1.510 -lemma less_SUP_iff (*[simp]*):
   1.511 -  "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   1.512 -  unfolding SUP_def less_Sup_iff by auto
   1.513 -
   1.514 -lemma Sup_eq_top_iff (*[simp]*):
   1.515 -  "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   1.516 -proof
   1.517 -  assume *: "\<Squnion>A = \<top>"
   1.518 -  show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
   1.519 -  proof (intro allI impI)
   1.520 -    fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
   1.521 -      unfolding less_Sup_iff by auto
   1.522 -  qed
   1.523 -next
   1.524 -  assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i"
   1.525 -  show "\<Squnion>A = \<top>"
   1.526 -  proof (rule ccontr)
   1.527 -    assume "\<Squnion>A \<noteq> \<top>"
   1.528 -    with top_greatest [of "\<Squnion>A"]
   1.529 -    have "\<Squnion>A < \<top>" unfolding le_less by auto
   1.530 -    then have "\<Squnion>A < \<Squnion>A"
   1.531 -      using * unfolding less_Sup_iff by auto
   1.532 -    then show False by auto
   1.533 -  qed
   1.534 -qed
   1.535 -
   1.536 -lemma SUP_eq_top_iff (*[simp]*):
   1.537 -  "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
   1.538 -  unfolding SUP_def Sup_eq_top_iff by auto
   1.539 -
   1.540 -lemma Inf_eq_bot_iff (*[simp]*):
   1.541 -  "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
   1.542 -proof -
   1.543 -  interpret dual: complete_linorder Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
   1.544 -    by (fact dual_complete_linorder)
   1.545 -  from dual.Sup_eq_top_iff show ?thesis .
   1.546 -qed
   1.547 -
   1.548 -lemma INF_eq_bot_iff (*[simp]*):
   1.549 -  "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   1.550 -  unfolding INF_def Inf_eq_bot_iff by auto
   1.551 -
   1.552 -end
   1.553 -
   1.554 -
   1.555 -subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
   1.556 -
   1.557 -instantiation bool :: complete_lattice
   1.558 -begin
   1.559 -
   1.560 -definition
   1.561 -  [simp]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
   1.562 -
   1.563 -definition
   1.564 -  [simp]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
   1.565 -
   1.566 -instance proof
   1.567 -qed (auto intro: bool_induct)
   1.568 -
   1.569 -end
   1.570 -
   1.571 -lemma INF_bool_eq [simp]:
   1.572 -  "INFI = Ball"
   1.573 -proof (rule ext)+
   1.574 -  fix A :: "'a set"
   1.575 -  fix P :: "'a \<Rightarrow> bool"
   1.576 -  show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
   1.577 -    by (auto simp add: INF_def)
   1.578 -qed
   1.579 -
   1.580 -lemma SUP_bool_eq [simp]:
   1.581 -  "SUPR = Bex"
   1.582 -proof (rule ext)+
   1.583 -  fix A :: "'a set"
   1.584 -  fix P :: "'a \<Rightarrow> bool"
   1.585 -  show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
   1.586 -    by (auto simp add: SUP_def)
   1.587 -qed
   1.588 -
   1.589 -instance bool :: complete_boolean_algebra proof
   1.590 -qed (auto intro: bool_induct)
   1.591 -
   1.592 -instantiation "fun" :: (type, complete_lattice) complete_lattice
   1.593 -begin
   1.594 -
   1.595 -definition
   1.596 -  "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
   1.597 -
   1.598 -lemma Inf_apply:
   1.599 -  "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   1.600 -  by (simp add: Inf_fun_def)
   1.601 -
   1.602 -definition
   1.603 -  "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
   1.604 -
   1.605 -lemma Sup_apply:
   1.606 -  "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   1.607 -  by (simp add: Sup_fun_def)
   1.608 -
   1.609 -instance proof
   1.610 -qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_lower INF_greatest SUP_upper SUP_least)
   1.611 -
   1.612 -end
   1.613 -
   1.614 -lemma INF_apply:
   1.615 -  "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   1.616 -  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
   1.617 -
   1.618 -lemma SUP_apply:
   1.619 -  "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   1.620 -  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
   1.621 -
   1.622 -instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
   1.623 -qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image)
   1.624 -
   1.625 -instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
   1.626 -
   1.627 -
   1.628 -subsection {* Inter *}
   1.629 -
   1.630 -abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
   1.631 -  "Inter S \<equiv> \<Sqinter>S"
   1.632 -  
   1.633 -notation (xsymbols)
   1.634 -  Inter  ("\<Inter>_" [90] 90)
   1.635 -
   1.636 -lemma Inter_eq:
   1.637 -  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
   1.638 -proof (rule set_eqI)
   1.639 -  fix x
   1.640 -  have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
   1.641 -    by auto
   1.642 -  then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
   1.643 -    by (simp add: Inf_fun_def) (simp add: mem_def)
   1.644 -qed
   1.645 -
   1.646 -lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
   1.647 -  by (unfold Inter_eq) blast
   1.648 -
   1.649 -lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C"
   1.650 -  by (simp add: Inter_eq)
   1.651 -
   1.652 -text {*
   1.653 -  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
   1.654 -  contains @{term A} as an element, but @{prop "A \<in> X"} can hold when
   1.655 -  @{prop "X \<in> C"} does not!  This rule is analogous to @{text spec}.
   1.656 -*}
   1.657 -
   1.658 -lemma InterD [elim, Pure.elim]: "A \<in> \<Inter>C \<Longrightarrow> X \<in> C \<Longrightarrow> A \<in> X"
   1.659 -  by auto
   1.660 -
   1.661 -lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R"
   1.662 -  -- {* ``Classical'' elimination rule -- does not require proving
   1.663 -    @{prop "X \<in> C"}. *}
   1.664 -  by (unfold Inter_eq) blast
   1.665 -
   1.666 -lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
   1.667 -  by (fact Inf_lower)
   1.668 -
   1.669 -lemma Inter_subset:
   1.670 -  "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
   1.671 -  by (fact Inf_less_eq)
   1.672 -
   1.673 -lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
   1.674 -  by (fact Inf_greatest)
   1.675 -
   1.676 -lemma Inter_empty: "\<Inter>{} = UNIV"
   1.677 -  by (fact Inf_empty) (* already simp *)
   1.678 -
   1.679 -lemma Inter_UNIV: "\<Inter>UNIV = {}"
   1.680 -  by (fact Inf_UNIV) (* already simp *)
   1.681 -
   1.682 -lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
   1.683 -  by (fact Inf_insert)
   1.684 -
   1.685 -lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
   1.686 -  by (fact less_eq_Inf_inter)
   1.687 -
   1.688 -lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   1.689 -  by (fact Inf_union_distrib)
   1.690 -
   1.691 -lemma Inter_UNIV_conv [simp, no_atp]:
   1.692 -  "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   1.693 -  "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   1.694 -  by (fact Inf_top_conv)+
   1.695 -
   1.696 -lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
   1.697 -  by (fact Inf_superset_mono)
   1.698 -
   1.699 -
   1.700 -subsection {* Intersections of families *}
   1.701 -
   1.702 -abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   1.703 -  "INTER \<equiv> INFI"
   1.704 -
   1.705 -text {*
   1.706 -  Note: must use name @{const INTER} here instead of @{text INT}
   1.707 -  to allow the following syntax coexist with the plain constant name.
   1.708 -*}
   1.709 -
   1.710 -syntax
   1.711 -  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
   1.712 -  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
   1.713 -
   1.714 -syntax (xsymbols)
   1.715 -  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
   1.716 -  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
   1.717 -
   1.718 -syntax (latex output)
   1.719 -  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   1.720 -  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
   1.721 -
   1.722 -translations
   1.723 -  "INT x y. B"  == "INT x. INT y. B"
   1.724 -  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
   1.725 -  "INT x. B"    == "INT x:CONST UNIV. B"
   1.726 -  "INT x:A. B"  == "CONST INTER A (%x. B)"
   1.727 -
   1.728 -print_translation {*
   1.729 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
   1.730 -*} -- {* to avoid eta-contraction of body *}
   1.731 -
   1.732 -lemma INTER_eq:
   1.733 -  "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
   1.734 -  by (auto simp add: INF_def)
   1.735 -
   1.736 -lemma Inter_image_eq [simp]:
   1.737 -  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   1.738 -  by (rule sym) (fact INF_def)
   1.739 -
   1.740 -lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
   1.741 -  by (auto simp add: INF_def image_def)
   1.742 -
   1.743 -lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
   1.744 -  by (auto simp add: INF_def image_def)
   1.745 -
   1.746 -lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a"
   1.747 -  by auto
   1.748 -
   1.749 -lemma INT_E [elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> (b \<in> B a \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
   1.750 -  -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
   1.751 -  by (auto simp add: INF_def image_def)
   1.752 -
   1.753 -lemma INT_cong [cong]:
   1.754 -  "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)"
   1.755 -  by (fact INF_cong)
   1.756 -
   1.757 -lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
   1.758 -  by blast
   1.759 -
   1.760 -lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
   1.761 -  by blast
   1.762 -
   1.763 -lemma INT_lower: "a \<in> A \<Longrightarrow> (\<Inter>x\<in>A. B x) \<subseteq> B a"
   1.764 -  by (fact INF_lower)
   1.765 -
   1.766 -lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
   1.767 -  by (fact INF_greatest)
   1.768 -
   1.769 -lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV"
   1.770 -  by (fact INF_empty)
   1.771 -
   1.772 -lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
   1.773 -  by (fact INF_absorb)
   1.774 -
   1.775 -lemma INT_subset_iff: "B \<subseteq> (\<Inter>i\<in>I. A i) \<longleftrightarrow> (\<forall>i\<in>I. B \<subseteq> A i)"
   1.776 -  by (fact le_INF_iff)
   1.777 -
   1.778 -lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
   1.779 -  by (fact INF_insert)
   1.780 -
   1.781 -lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
   1.782 -  by (fact INF_union)
   1.783 -
   1.784 -lemma INT_insert_distrib:
   1.785 -  "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   1.786 -  by blast
   1.787 -
   1.788 -lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
   1.789 -  by (fact INF_constant)
   1.790 -
   1.791 -lemma INTER_UNIV_conv [simp]:
   1.792 - "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
   1.793 - "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
   1.794 -  by (fact INF_top_conv)+
   1.795 -
   1.796 -lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
   1.797 -  by (fact INF_UNIV_bool_expand)
   1.798 -
   1.799 -lemma INT_anti_mono:
   1.800 -  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
   1.801 -  -- {* The last inclusion is POSITIVE! *}
   1.802 -  by (fact INF_superset_mono)
   1.803 -
   1.804 -lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
   1.805 -  by blast
   1.806 -
   1.807 -lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)"
   1.808 -  by blast
   1.809 -
   1.810 -
   1.811 -subsection {* Union *}
   1.812 -
   1.813 -abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
   1.814 -  "Union S \<equiv> \<Squnion>S"
   1.815 -
   1.816 -notation (xsymbols)
   1.817 -  Union  ("\<Union>_" [90] 90)
   1.818 -
   1.819 -lemma Union_eq:
   1.820 -  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
   1.821 -proof (rule set_eqI)
   1.822 -  fix x
   1.823 -  have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
   1.824 -    by auto
   1.825 -  then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
   1.826 -    by (simp add: Sup_fun_def) (simp add: mem_def)
   1.827 -qed
   1.828 -
   1.829 -lemma Union_iff [simp, no_atp]:
   1.830 -  "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
   1.831 -  by (unfold Union_eq) blast
   1.832 -
   1.833 -lemma UnionI [intro]:
   1.834 -  "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
   1.835 -  -- {* The order of the premises presupposes that @{term C} is rigid;
   1.836 -    @{term A} may be flexible. *}
   1.837 -  by auto
   1.838 -
   1.839 -lemma UnionE [elim!]:
   1.840 -  "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R"
   1.841 -  by auto
   1.842 -
   1.843 -lemma Union_upper: "B \<in> A \<Longrightarrow> B \<subseteq> \<Union>A"
   1.844 -  by (fact Sup_upper)
   1.845 -
   1.846 -lemma Union_least: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> C) \<Longrightarrow> \<Union>A \<subseteq> C"
   1.847 -  by (fact Sup_least)
   1.848 -
   1.849 -lemma Union_empty [simp]: "\<Union>{} = {}"
   1.850 -  by (fact Sup_empty)
   1.851 -
   1.852 -lemma Union_UNIV [simp]: "\<Union>UNIV = UNIV"
   1.853 -  by (fact Sup_UNIV)
   1.854 -
   1.855 -lemma Union_insert [simp]: "\<Union>insert a B = a \<union> \<Union>B"
   1.856 -  by (fact Sup_insert)
   1.857 -
   1.858 -lemma Union_Un_distrib [simp]: "\<Union>(A \<union> B) = \<Union>A \<union> \<Union>B"
   1.859 -  by (fact Sup_union_distrib)
   1.860 -
   1.861 -lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   1.862 -  by (fact Sup_inter_less_eq)
   1.863 -
   1.864 -lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
   1.865 -  by (fact Sup_bot_conv)
   1.866 -
   1.867 -lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
   1.868 -  by (fact Sup_bot_conv)
   1.869 -
   1.870 -lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
   1.871 -  by blast
   1.872 -
   1.873 -lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
   1.874 -  by blast
   1.875 -
   1.876 -lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
   1.877 -  by (fact Sup_subset_mono)
   1.878 -
   1.879 -
   1.880 -subsection {* Unions of families *}
   1.881 -
   1.882 -abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   1.883 -  "UNION \<equiv> SUPR"
   1.884 -
   1.885 -text {*
   1.886 -  Note: must use name @{const UNION} here instead of @{text UN}
   1.887 -  to allow the following syntax coexist with the plain constant name.
   1.888 -*}
   1.889 -
   1.890 -syntax
   1.891 -  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   1.892 -  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
   1.893 -
   1.894 -syntax (xsymbols)
   1.895 -  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
   1.896 -  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
   1.897 -
   1.898 -syntax (latex output)
   1.899 -  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   1.900 -  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
   1.901 -
   1.902 -translations
   1.903 -  "UN x y. B"   == "UN x. UN y. B"
   1.904 -  "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"
   1.905 -  "UN x. B"     == "UN x:CONST UNIV. B"
   1.906 -  "UN x:A. B"   == "CONST UNION A (%x. B)"
   1.907 -
   1.908 -text {*
   1.909 -  Note the difference between ordinary xsymbol syntax of indexed
   1.910 -  unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
   1.911 -  and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
   1.912 -  former does not make the index expression a subscript of the
   1.913 -  union/intersection symbol because this leads to problems with nested
   1.914 -  subscripts in Proof General.
   1.915 -*}
   1.916 -
   1.917 -print_translation {*
   1.918 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
   1.919 -*} -- {* to avoid eta-contraction of body *}
   1.920 -
   1.921 -lemma UNION_eq [no_atp]:
   1.922 -  "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   1.923 -  by (auto simp add: SUP_def)
   1.924 -  
   1.925 -lemma Union_image_eq [simp]:
   1.926 -  "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   1.927 -  by (auto simp add: UNION_eq)
   1.928 -  
   1.929 -lemma UN_iff [simp]: "(b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)"
   1.930 -  by (auto simp add: SUP_def image_def)
   1.931 -
   1.932 -lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
   1.933 -  -- {* The order of the premises presupposes that @{term A} is rigid;
   1.934 -    @{term b} may be flexible. *}
   1.935 -  by auto
   1.936 -
   1.937 -lemma UN_E [elim!]: "b \<in> (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x\<in>A \<Longrightarrow> b \<in> B x \<Longrightarrow> R) \<Longrightarrow> R"
   1.938 -  by (auto simp add: SUP_def image_def)
   1.939 -
   1.940 -lemma UN_cong [cong]:
   1.941 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
   1.942 -  by (fact SUP_cong)
   1.943 -
   1.944 -lemma strong_UN_cong:
   1.945 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
   1.946 -  by (unfold simp_implies_def) (fact UN_cong)
   1.947 -
   1.948 -lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
   1.949 -  by blast
   1.950 -
   1.951 -lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
   1.952 -  by (fact SUP_upper)
   1.953 -
   1.954 -lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
   1.955 -  by (fact SUP_least)
   1.956 -
   1.957 -lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
   1.958 -  by blast
   1.959 -
   1.960 -lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
   1.961 -  by blast
   1.962 -
   1.963 -lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
   1.964 -  by (fact SUP_empty)
   1.965 -
   1.966 -lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
   1.967 -  by (fact SUP_bot)
   1.968 -
   1.969 -lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
   1.970 -  by (fact SUP_absorb)
   1.971 -
   1.972 -lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
   1.973 -  by (fact SUP_insert)
   1.974 -
   1.975 -lemma UN_Un [simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
   1.976 -  by (fact SUP_union)
   1.977 -
   1.978 -lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
   1.979 -  by blast
   1.980 -
   1.981 -lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
   1.982 -  by (fact SUP_le_iff)
   1.983 -
   1.984 -lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
   1.985 -  by (fact SUP_constant)
   1.986 -
   1.987 -lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
   1.988 -  by blast
   1.989 -
   1.990 -lemma UNION_empty_conv[simp]:
   1.991 -  "{} = (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
   1.992 -  "(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
   1.993 -  by (fact SUP_bot_conv)+
   1.994 -
   1.995 -lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   1.996 -  by blast
   1.997 -
   1.998 -lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
   1.999 -  by blast
  1.1000 -
  1.1001 -lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
  1.1002 -  by blast
  1.1003 -
  1.1004 -lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
  1.1005 -  by (auto simp add: split_if_mem2)
  1.1006 -
  1.1007 -lemma UN_bool_eq: "(\<Union>b. A b) = (A True \<union> A False)"
  1.1008 -  by (fact SUP_UNIV_bool_expand)
  1.1009 -
  1.1010 -lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
  1.1011 -  by blast
  1.1012 -
  1.1013 -lemma UN_mono:
  1.1014 -  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
  1.1015 -    (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
  1.1016 -  by (fact SUP_subset_mono)
  1.1017 -
  1.1018 -lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)"
  1.1019 -  by blast
  1.1020 -
  1.1021 -lemma vimage_UN: "f -` (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. f -` B x)"
  1.1022 -  by blast
  1.1023 -
  1.1024 -lemma vimage_eq_UN: "f -` B = (\<Union>y\<in>B. f -` {y})"
  1.1025 -  -- {* NOT suitable for rewriting *}
  1.1026 -  by blast
  1.1027 -
  1.1028 -lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
  1.1029 -  by blast
  1.1030 -
  1.1031 -
  1.1032 -subsection {* Distributive laws *}
  1.1033 -
  1.1034 -lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
  1.1035 -  by (fact inf_Sup)
  1.1036 -
  1.1037 -lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
  1.1038 -  by (fact sup_Inf)
  1.1039 -
  1.1040 -lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
  1.1041 -  by (fact Sup_inf)
  1.1042 -
  1.1043 -lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)"
  1.1044 -  by (rule sym) (rule INF_inf_distrib)
  1.1045 -
  1.1046 -lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
  1.1047 -  by (rule sym) (rule SUP_sup_distrib)
  1.1048 -
  1.1049 -lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"
  1.1050 -  by (simp only: INT_Int_distrib INF_def)
  1.1051 -
  1.1052 -lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"
  1.1053 -  -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
  1.1054 -  -- {* Union of a family of unions *}
  1.1055 -  by (simp only: UN_Un_distrib SUP_def)
  1.1056 -
  1.1057 -lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
  1.1058 -  by (fact sup_INF)
  1.1059 -
  1.1060 -lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"
  1.1061 -  -- {* Halmos, Naive Set Theory, page 35. *}
  1.1062 -  by (fact inf_SUP)
  1.1063 -
  1.1064 -lemma Int_UN_distrib2: "(\<Union>i\<in>I. A i) \<inter> (\<Union>j\<in>J. B j) = (\<Union>i\<in>I. \<Union>j\<in>J. A i \<inter> B j)"
  1.1065 -  by (fact SUP_inf_distrib2)
  1.1066 -
  1.1067 -lemma Un_INT_distrib2: "(\<Inter>i\<in>I. A i) \<union> (\<Inter>j\<in>J. B j) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A i \<union> B j)"
  1.1068 -  by (fact INF_sup_distrib2)
  1.1069 -
  1.1070 -lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
  1.1071 -  by (fact Sup_inf_eq_bot_iff)
  1.1072 -
  1.1073 -
  1.1074 -subsection {* Complement *}
  1.1075 -
  1.1076 -lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
  1.1077 -  by (fact uminus_INF)
  1.1078 -
  1.1079 -lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
  1.1080 -  by (fact uminus_SUP)
  1.1081 -
  1.1082 -
  1.1083 -subsection {* Miniscoping and maxiscoping *}
  1.1084 -
  1.1085 -text {* \medskip Miniscoping: pushing in quantifiers and big Unions
  1.1086 -           and Intersections. *}
  1.1087 -
  1.1088 -lemma UN_simps [simp]:
  1.1089 -  "\<And>a B C. (\<Union>x\<in>C. insert a (B x)) = (if C={} then {} else insert a (\<Union>x\<in>C. B x))"
  1.1090 -  "\<And>A B C. (\<Union>x\<in>C. A x \<union> B) = ((if C={} then {} else (\<Union>x\<in>C. A x) \<union> B))"
  1.1091 -  "\<And>A B C. (\<Union>x\<in>C. A \<union> B x) = ((if C={} then {} else A \<union> (\<Union>x\<in>C. B x)))"
  1.1092 -  "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter> B)"
  1.1093 -  "\<And>A B C. (\<Union>x\<in>C. A \<inter> B x) = (A \<inter>(\<Union>x\<in>C. B x))"
  1.1094 -  "\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
  1.1095 -  "\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
  1.1096 -  "\<And>A B. (\<Union>x\<in>\<Union>A. B x) = (\<Union>y\<in>A. \<Union>x\<in>y. B x)"
  1.1097 -  "\<And>A B C. (\<Union>z\<in>UNION A B. C z) = (\<Union>x\<in>A. \<Union>z\<in>B x. C z)"
  1.1098 -  "\<And>A B f. (\<Union>x\<in>f`A. B x) = (\<Union>a\<in>A. B (f a))"
  1.1099 -  by auto
  1.1100 -
  1.1101 -lemma INT_simps [simp]:
  1.1102 -  "\<And>A B C. (\<Inter>x\<in>C. A x \<inter> B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) \<inter> B)"
  1.1103 -  "\<And>A B C. (\<Inter>x\<in>C. A \<inter> B x) = (if C={} then UNIV else A \<inter>(\<Inter>x\<in>C. B x))"
  1.1104 -  "\<And>A B C. (\<Inter>x\<in>C. A x - B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)"
  1.1105 -  "\<And>A B C. (\<Inter>x\<in>C. A - B x) = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))"
  1.1106 -  "\<And>a B C. (\<Inter>x\<in>C. insert a (B x)) = insert a (\<Inter>x\<in>C. B x)"
  1.1107 -  "\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)"
  1.1108 -  "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))"
  1.1109 -  "\<And>A B. (\<Inter>x\<in>\<Union>A. B x) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B x)"
  1.1110 -  "\<And>A B C. (\<Inter>z\<in>UNION A B. C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
  1.1111 -  "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
  1.1112 -  by auto
  1.1113 -
  1.1114 -lemma UN_ball_bex_simps [simp, no_atp]:
  1.1115 -  "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
  1.1116 -  "\<And>A B P. (\<forall>x\<in>UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
  1.1117 -  "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
  1.1118 -  "\<And>A B P. (\<exists>x\<in>UNION A B. P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
  1.1119 -  by auto
  1.1120 -
  1.1121 -
  1.1122 -text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
  1.1123 -
  1.1124 -lemma UN_extend_simps:
  1.1125 -  "\<And>a B C. insert a (\<Union>x\<in>C. B x) = (if C={} then {a} else (\<Union>x\<in>C. insert a (B x)))"
  1.1126 -  "\<And>A B C. (\<Union>x\<in>C. A x) \<union> B = (if C={} then B else (\<Union>x\<in>C. A x \<union> B))"
  1.1127 -  "\<And>A B C. A \<union> (\<Union>x\<in>C. B x) = (if C={} then A else (\<Union>x\<in>C. A \<union> B x))"
  1.1128 -  "\<And>A B C. ((\<Union>x\<in>C. A x) \<inter> B) = (\<Union>x\<in>C. A x \<inter> B)"
  1.1129 -  "\<And>A B C. (A \<inter> (\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> B x)"
  1.1130 -  "\<And>A B C. ((\<Union>x\<in>C. A x) - B) = (\<Union>x\<in>C. A x - B)"
  1.1131 -  "\<And>A B C. (A - (\<Inter>x\<in>C. B x)) = (\<Union>x\<in>C. A - B x)"
  1.1132 -  "\<And>A B. (\<Union>y\<in>A. \<Union>x\<in>y. B x) = (\<Union>x\<in>\<Union>A. B x)"
  1.1133 -  "\<And>A B C. (\<Union>x\<in>A. \<Union>z\<in>B x. C z) = (\<Union>z\<in>UNION A B. C z)"
  1.1134 -  "\<And>A B f. (\<Union>a\<in>A. B (f a)) = (\<Union>x\<in>f`A. B x)"
  1.1135 -  by auto
  1.1136 -
  1.1137 -lemma INT_extend_simps:
  1.1138 -  "\<And>A B C. (\<Inter>x\<in>C. A x) \<inter> B = (if C={} then B else (\<Inter>x\<in>C. A x \<inter> B))"
  1.1139 -  "\<And>A B C. A \<inter> (\<Inter>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A \<inter> B x))"
  1.1140 -  "\<And>A B C. (\<Inter>x\<in>C. A x) - B = (if C={} then UNIV - B else (\<Inter>x\<in>C. A x - B))"
  1.1141 -  "\<And>A B C. A - (\<Union>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A - B x))"
  1.1142 -  "\<And>a B C. insert a (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. insert a (B x))"
  1.1143 -  "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)"
  1.1144 -  "\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)"
  1.1145 -  "\<And>A B. (\<Inter>y\<in>A. \<Inter>x\<in>y. B x) = (\<Inter>x\<in>\<Union>A. B x)"
  1.1146 -  "\<And>A B C. (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z) = (\<Inter>z\<in>UNION A B. C z)"
  1.1147 -  "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
  1.1148 -  by auto
  1.1149 -
  1.1150 -
  1.1151 -text {* Legacy names *}
  1.1152 -
  1.1153 -lemma (in complete_lattice) Inf_singleton [simp]:
  1.1154 -  "\<Sqinter>{a} = a"
  1.1155 -  by (simp add: Inf_insert)
  1.1156 -
  1.1157 -lemma (in complete_lattice) Sup_singleton [simp]:
  1.1158 -  "\<Squnion>{a} = a"
  1.1159 -  by (simp add: Sup_insert)
  1.1160 -
  1.1161 -lemma (in complete_lattice) Inf_binary:
  1.1162 -  "\<Sqinter>{a, b} = a \<sqinter> b"
  1.1163 -  by (simp add: Inf_insert)
  1.1164 -
  1.1165 -lemma (in complete_lattice) Sup_binary:
  1.1166 -  "\<Squnion>{a, b} = a \<squnion> b"
  1.1167 -  by (simp add: Sup_insert)
  1.1168 -
  1.1169 -lemmas (in complete_lattice) INFI_def = INF_def
  1.1170 -lemmas (in complete_lattice) SUPR_def = SUP_def
  1.1171 -lemmas (in complete_lattice) INF_leI = INF_lower
  1.1172 -lemmas (in complete_lattice) INF_leI2 = INF_lower2
  1.1173 -lemmas (in complete_lattice) le_INFI = INF_greatest
  1.1174 -lemmas (in complete_lattice) le_SUPI = SUP_upper
  1.1175 -lemmas (in complete_lattice) le_SUPI2 = SUP_upper2
  1.1176 -lemmas (in complete_lattice) SUP_leI = SUP_least
  1.1177 -lemmas (in complete_lattice) less_INFD = less_INF_D
  1.1178 -
  1.1179 -lemmas INFI_apply = INF_apply
  1.1180 -lemmas SUPR_apply = SUP_apply
  1.1181 -
  1.1182 -text {* Grep and put to news from here *}
  1.1183 -
  1.1184 -lemma (in complete_lattice) INF_eq:
  1.1185 -  "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
  1.1186 -  by (simp add: INF_def image_def)
  1.1187 -
  1.1188 -lemma (in complete_lattice) SUP_eq:
  1.1189 -  "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
  1.1190 -  by (simp add: SUP_def image_def)
  1.1191 -
  1.1192 -lemma (in complete_lattice) INF_subset:
  1.1193 -  "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
  1.1194 -  by (rule INF_superset_mono) auto
  1.1195 -
  1.1196 -lemma (in complete_lattice) INF_UNIV_range:
  1.1197 -  "(\<Sqinter>x. f x) = \<Sqinter>range f"
  1.1198 -  by (fact INF_def)
  1.1199 -
  1.1200 -lemma (in complete_lattice) SUP_UNIV_range:
  1.1201 -  "(\<Squnion>x. f x) = \<Squnion>range f"
  1.1202 -  by (fact SUP_def)
  1.1203 -
  1.1204 -lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
  1.1205 -  by (simp add: Inf_insert)
  1.1206 -
  1.1207 -lemma INTER_eq_Inter_image:
  1.1208 -  "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
  1.1209 -  by (fact INF_def)
  1.1210 -  
  1.1211 -lemma Inter_def:
  1.1212 -  "\<Inter>S = (\<Inter>x\<in>S. x)"
  1.1213 -  by (simp add: INTER_eq_Inter_image image_def)
  1.1214 -
  1.1215 -lemmas INTER_def = INTER_eq
  1.1216 -lemmas UNION_def = UNION_eq
  1.1217 -
  1.1218 -lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
  1.1219 -  by (fact INF_eq)
  1.1220 -
  1.1221 -lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
  1.1222 -  by blast
  1.1223 -
  1.1224 -lemma UNION_eq_Union_image:
  1.1225 -  "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
  1.1226 -  by (fact SUP_def)
  1.1227 -
  1.1228 -lemma Union_def:
  1.1229 -  "\<Union>S = (\<Union>x\<in>S. x)"
  1.1230 -  by (simp add: UNION_eq_Union_image image_def)
  1.1231 -
  1.1232 -lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
  1.1233 -  by blast
  1.1234 -
  1.1235 -lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
  1.1236 -  by (fact SUP_eq)
  1.1237 -
  1.1238 -
  1.1239 -text {* Finally *}
  1.1240 -
  1.1241 -no_notation
  1.1242 -  less_eq  (infix "\<sqsubseteq>" 50) and
  1.1243 -  less (infix "\<sqsubset>" 50) and
  1.1244 -  bot ("\<bottom>") and
  1.1245 -  top ("\<top>") and
  1.1246 -  inf  (infixl "\<sqinter>" 70) and
  1.1247 -  sup  (infixl "\<squnion>" 65) and
  1.1248 -  Inf  ("\<Sqinter>_" [900] 900) and
  1.1249 -  Sup  ("\<Squnion>_" [900] 900)
  1.1250 -
  1.1251 -no_syntax (xsymbols)
  1.1252 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
  1.1253 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
  1.1254 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
  1.1255 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
  1.1256 -
  1.1257 -lemmas mem_simps =
  1.1258 -  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
  1.1259 -  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
  1.1260 -  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
  1.1261 -
  1.1262 -end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Sat Sep 10 10:29:24 2011 +0200
     2.3 @@ -0,0 +1,1259 @@
     2.4 + (*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
     2.5 +
     2.6 +header {* Complete lattices *}
     2.7 +
     2.8 +theory Complete_Lattices
     2.9 +imports Set
    2.10 +begin
    2.11 +
    2.12 +notation
    2.13 +  less_eq (infix "\<sqsubseteq>" 50) and
    2.14 +  less (infix "\<sqsubset>" 50) and
    2.15 +  inf (infixl "\<sqinter>" 70) and
    2.16 +  sup (infixl "\<squnion>" 65) and
    2.17 +  top ("\<top>") and
    2.18 +  bot ("\<bottom>")
    2.19 +
    2.20 +
    2.21 +subsection {* Syntactic infimum and supremum operations *}
    2.22 +
    2.23 +class Inf =
    2.24 +  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    2.25 +
    2.26 +class Sup =
    2.27 +  fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    2.28 +
    2.29 +subsection {* Abstract complete lattices *}
    2.30 +
    2.31 +class complete_lattice = bounded_lattice + Inf + Sup +
    2.32 +  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    2.33 +     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    2.34 +  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    2.35 +     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
    2.36 +begin
    2.37 +
    2.38 +lemma dual_complete_lattice:
    2.39 +  "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
    2.40 +  by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
    2.41 +    (unfold_locales, (fact bot_least top_greatest
    2.42 +        Sup_upper Sup_least Inf_lower Inf_greatest)+)
    2.43 +
    2.44 +definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.45 +  INF_def: "INFI A f = \<Sqinter>(f ` A)"
    2.46 +
    2.47 +definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.48 +  SUP_def: "SUPR A f = \<Squnion>(f ` A)"
    2.49 +
    2.50 +text {*
    2.51 +  Note: must use names @{const INFI} and @{const SUPR} here instead of
    2.52 +  @{text INF} and @{text SUP} to allow the following syntax coexist
    2.53 +  with the plain constant names.
    2.54 +*}
    2.55 +
    2.56 +end
    2.57 +
    2.58 +syntax
    2.59 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
    2.60 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    2.61 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
    2.62 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    2.63 +
    2.64 +syntax (xsymbols)
    2.65 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    2.66 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    2.67 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    2.68 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    2.69 +
    2.70 +translations
    2.71 +  "INF x y. B"   == "INF x. INF y. B"
    2.72 +  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
    2.73 +  "INF x. B"     == "INF x:CONST UNIV. B"
    2.74 +  "INF x:A. B"   == "CONST INFI A (%x. B)"
    2.75 +  "SUP x y. B"   == "SUP x. SUP y. B"
    2.76 +  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
    2.77 +  "SUP x. B"     == "SUP x:CONST UNIV. B"
    2.78 +  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
    2.79 +
    2.80 +print_translation {*
    2.81 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
    2.82 +    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
    2.83 +*} -- {* to avoid eta-contraction of body *}
    2.84 +
    2.85 +context complete_lattice
    2.86 +begin
    2.87 +
    2.88 +lemma INF_foundation_dual [no_atp]:
    2.89 +  "complete_lattice.SUPR Inf = INFI"
    2.90 +proof (rule ext)+
    2.91 +  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
    2.92 +    by (fact dual_complete_lattice)
    2.93 +  fix f :: "'b \<Rightarrow> 'a" and A
    2.94 +  show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
    2.95 +    by (simp only: dual.SUP_def INF_def)
    2.96 +qed
    2.97 +
    2.98 +lemma SUP_foundation_dual [no_atp]:
    2.99 +  "complete_lattice.INFI Sup = SUPR"
   2.100 +proof (rule ext)+
   2.101 +  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
   2.102 +    by (fact dual_complete_lattice)
   2.103 +  fix f :: "'b \<Rightarrow> 'a" and A
   2.104 +  show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
   2.105 +    by (simp only: dual.INF_def SUP_def)
   2.106 +qed
   2.107 +
   2.108 +lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
   2.109 +  by (auto simp add: INF_def intro: Inf_lower)
   2.110 +
   2.111 +lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
   2.112 +  by (auto simp add: INF_def intro: Inf_greatest)
   2.113 +
   2.114 +lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
   2.115 +  by (auto simp add: SUP_def intro: Sup_upper)
   2.116 +
   2.117 +lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
   2.118 +  by (auto simp add: SUP_def intro: Sup_least)
   2.119 +
   2.120 +lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
   2.121 +  using Inf_lower [of u A] by auto
   2.122 +
   2.123 +lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
   2.124 +  using INF_lower [of i A f] by auto
   2.125 +
   2.126 +lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
   2.127 +  using Sup_upper [of u A] by auto
   2.128 +
   2.129 +lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
   2.130 +  using SUP_upper [of i A f] by auto
   2.131 +
   2.132 +lemma le_Inf_iff (*[simp]*): "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
   2.133 +  by (auto intro: Inf_greatest dest: Inf_lower)
   2.134 +
   2.135 +lemma le_INF_iff (*[simp]*): "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
   2.136 +  by (auto simp add: INF_def le_Inf_iff)
   2.137 +
   2.138 +lemma Sup_le_iff (*[simp]*): "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
   2.139 +  by (auto intro: Sup_least dest: Sup_upper)
   2.140 +
   2.141 +lemma SUP_le_iff (*[simp]*): "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
   2.142 +  by (auto simp add: SUP_def Sup_le_iff)
   2.143 +
   2.144 +lemma Inf_empty [simp]:
   2.145 +  "\<Sqinter>{} = \<top>"
   2.146 +  by (auto intro: antisym Inf_greatest)
   2.147 +
   2.148 +lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   2.149 +  by (simp add: INF_def)
   2.150 +
   2.151 +lemma Sup_empty [simp]:
   2.152 +  "\<Squnion>{} = \<bottom>"
   2.153 +  by (auto intro: antisym Sup_least)
   2.154 +
   2.155 +lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
   2.156 +  by (simp add: SUP_def)
   2.157 +
   2.158 +lemma Inf_UNIV [simp]:
   2.159 +  "\<Sqinter>UNIV = \<bottom>"
   2.160 +  by (auto intro!: antisym Inf_lower)
   2.161 +
   2.162 +lemma Sup_UNIV [simp]:
   2.163 +  "\<Squnion>UNIV = \<top>"
   2.164 +  by (auto intro!: antisym Sup_upper)
   2.165 +
   2.166 +lemma Inf_insert (*[simp]*): "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   2.167 +  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   2.168 +
   2.169 +lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
   2.170 +  by (simp add: INF_def Inf_insert)
   2.171 +
   2.172 +lemma Sup_insert (*[simp]*): "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   2.173 +  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
   2.174 +
   2.175 +lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   2.176 +  by (simp add: SUP_def Sup_insert)
   2.177 +
   2.178 +lemma INF_image (*[simp]*): "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
   2.179 +  by (simp add: INF_def image_image)
   2.180 +
   2.181 +lemma SUP_image (*[simp]*): "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
   2.182 +  by (simp add: SUP_def image_image)
   2.183 +
   2.184 +lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
   2.185 +  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   2.186 +
   2.187 +lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
   2.188 +  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   2.189 +
   2.190 +lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
   2.191 +  by (auto intro: Inf_greatest Inf_lower)
   2.192 +
   2.193 +lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
   2.194 +  by (auto intro: Sup_least Sup_upper)
   2.195 +
   2.196 +lemma INF_cong:
   2.197 +  "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)"
   2.198 +  by (simp add: INF_def image_def)
   2.199 +
   2.200 +lemma SUP_cong:
   2.201 +  "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)"
   2.202 +  by (simp add: SUP_def image_def)
   2.203 +
   2.204 +lemma Inf_mono:
   2.205 +  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
   2.206 +  shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
   2.207 +proof (rule Inf_greatest)
   2.208 +  fix b assume "b \<in> B"
   2.209 +  with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
   2.210 +  from `a \<in> A` have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
   2.211 +  with `a \<sqsubseteq> b` show "\<Sqinter>A \<sqsubseteq> b" by auto
   2.212 +qed
   2.213 +
   2.214 +lemma INF_mono:
   2.215 +  "(\<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)"
   2.216 +  by (force intro!: Inf_mono simp: INF_def)
   2.217 +
   2.218 +lemma Sup_mono:
   2.219 +  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
   2.220 +  shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
   2.221 +proof (rule Sup_least)
   2.222 +  fix a assume "a \<in> A"
   2.223 +  with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
   2.224 +  from `b \<in> B` have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
   2.225 +  with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
   2.226 +qed
   2.227 +
   2.228 +lemma SUP_mono:
   2.229 +  "(\<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)"
   2.230 +  by (force intro!: Sup_mono simp: SUP_def)
   2.231 +
   2.232 +lemma INF_superset_mono:
   2.233 +  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
   2.234 +  -- {* The last inclusion is POSITIVE! *}
   2.235 +  by (blast intro: INF_mono dest: subsetD)
   2.236 +
   2.237 +lemma SUP_subset_mono:
   2.238 +  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
   2.239 +  by (blast intro: SUP_mono dest: subsetD)
   2.240 +
   2.241 +lemma Inf_less_eq:
   2.242 +  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
   2.243 +    and "A \<noteq> {}"
   2.244 +  shows "\<Sqinter>A \<sqsubseteq> u"
   2.245 +proof -
   2.246 +  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
   2.247 +  moreover with assms have "v \<sqsubseteq> u" by blast
   2.248 +  ultimately show ?thesis by (rule Inf_lower2)
   2.249 +qed
   2.250 +
   2.251 +lemma less_eq_Sup:
   2.252 +  assumes "\<And>v. v \<in> A \<Longrightarrow> u \<sqsubseteq> v"
   2.253 +    and "A \<noteq> {}"
   2.254 +  shows "u \<sqsubseteq> \<Squnion>A"
   2.255 +proof -
   2.256 +  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
   2.257 +  moreover with assms have "u \<sqsubseteq> v" by blast
   2.258 +  ultimately show ?thesis by (rule Sup_upper2)
   2.259 +qed
   2.260 +
   2.261 +lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
   2.262 +  by (auto intro: Inf_greatest Inf_lower)
   2.263 +
   2.264 +lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
   2.265 +  by (auto intro: Sup_least Sup_upper)
   2.266 +
   2.267 +lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   2.268 +  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
   2.269 +
   2.270 +lemma INF_union:
   2.271 +  "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
   2.272 +  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
   2.273 +
   2.274 +lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
   2.275 +  by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
   2.276 +
   2.277 +lemma SUP_union:
   2.278 +  "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
   2.279 +  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
   2.280 +
   2.281 +lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)"
   2.282 +  by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
   2.283 +
   2.284 +lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)"
   2.285 +  by (rule antisym) (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono,
   2.286 +    rule SUP_least, auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
   2.287 +
   2.288 +lemma Inf_top_conv (*[simp]*) [no_atp]:
   2.289 +  "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
   2.290 +  "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
   2.291 +proof -
   2.292 +  show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
   2.293 +  proof
   2.294 +    assume "\<forall>x\<in>A. x = \<top>"
   2.295 +    then have "A = {} \<or> A = {\<top>}" by auto
   2.296 +    then show "\<Sqinter>A = \<top>" by (auto simp add: Inf_insert)
   2.297 +  next
   2.298 +    assume "\<Sqinter>A = \<top>"
   2.299 +    show "\<forall>x\<in>A. x = \<top>"
   2.300 +    proof (rule ccontr)
   2.301 +      assume "\<not> (\<forall>x\<in>A. x = \<top>)"
   2.302 +      then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
   2.303 +      then obtain B where "A = insert x B" by blast
   2.304 +      with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
   2.305 +    qed
   2.306 +  qed
   2.307 +  then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
   2.308 +qed
   2.309 +
   2.310 +lemma INF_top_conv (*[simp]*):
   2.311 + "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   2.312 + "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   2.313 +  by (auto simp add: INF_def Inf_top_conv)
   2.314 +
   2.315 +lemma Sup_bot_conv (*[simp]*) [no_atp]:
   2.316 +  "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
   2.317 +  "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
   2.318 +proof -
   2.319 +  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
   2.320 +    by (fact dual_complete_lattice)
   2.321 +  from dual.Inf_top_conv show ?P and ?Q by simp_all
   2.322 +qed
   2.323 +
   2.324 +lemma SUP_bot_conv (*[simp]*):
   2.325 + "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   2.326 + "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   2.327 +  by (auto simp add: SUP_def Sup_bot_conv)
   2.328 +
   2.329 +lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
   2.330 +  by (auto intro: antisym INF_lower INF_greatest)
   2.331 +
   2.332 +lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
   2.333 +  by (auto intro: antisym SUP_upper SUP_least)
   2.334 +
   2.335 +lemma INF_top (*[simp]*): "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   2.336 +  by (cases "A = {}") (simp_all add: INF_empty)
   2.337 +
   2.338 +lemma SUP_bot (*[simp]*): "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
   2.339 +  by (cases "A = {}") (simp_all add: SUP_empty)
   2.340 +
   2.341 +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)"
   2.342 +  by (iprover intro: INF_lower INF_greatest order_trans antisym)
   2.343 +
   2.344 +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)"
   2.345 +  by (iprover intro: SUP_upper SUP_least order_trans antisym)
   2.346 +
   2.347 +lemma INF_absorb:
   2.348 +  assumes "k \<in> I"
   2.349 +  shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
   2.350 +proof -
   2.351 +  from assms obtain J where "I = insert k J" by blast
   2.352 +  then show ?thesis by (simp add: INF_insert)
   2.353 +qed
   2.354 +
   2.355 +lemma SUP_absorb:
   2.356 +  assumes "k \<in> I"
   2.357 +  shows "A k \<squnion> (\<Squnion>i\<in>I. A i) = (\<Squnion>i\<in>I. A i)"
   2.358 +proof -
   2.359 +  from assms obtain J where "I = insert k J" by blast
   2.360 +  then show ?thesis by (simp add: SUP_insert)
   2.361 +qed
   2.362 +
   2.363 +lemma INF_constant:
   2.364 +  "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   2.365 +  by (simp add: INF_empty)
   2.366 +
   2.367 +lemma SUP_constant:
   2.368 +  "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
   2.369 +  by (simp add: SUP_empty)
   2.370 +
   2.371 +lemma less_INF_D:
   2.372 +  assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
   2.373 +proof -
   2.374 +  note `y < (\<Sqinter>i\<in>A. f i)`
   2.375 +  also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using `i \<in> A`
   2.376 +    by (rule INF_lower)
   2.377 +  finally show "y < f i" .
   2.378 +qed
   2.379 +
   2.380 +lemma SUP_lessD:
   2.381 +  assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
   2.382 +proof -
   2.383 +  have "f i \<le> (\<Squnion>i\<in>A. f i)" using `i \<in> A`
   2.384 +    by (rule SUP_upper)
   2.385 +  also note `(\<Squnion>i\<in>A. f i) < y`
   2.386 +  finally show "f i < y" .
   2.387 +qed
   2.388 +
   2.389 +lemma INF_UNIV_bool_expand:
   2.390 +  "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   2.391 +  by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
   2.392 +
   2.393 +lemma SUP_UNIV_bool_expand:
   2.394 +  "(\<Squnion>b. A b) = A True \<squnion> A False"
   2.395 +  by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
   2.396 +
   2.397 +end
   2.398 +
   2.399 +class complete_distrib_lattice = complete_lattice +
   2.400 +  assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   2.401 +  assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   2.402 +begin
   2.403 +
   2.404 +lemma sup_INF:
   2.405 +  "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   2.406 +  by (simp add: INF_def sup_Inf image_image)
   2.407 +
   2.408 +lemma inf_SUP:
   2.409 +  "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   2.410 +  by (simp add: SUP_def inf_Sup image_image)
   2.411 +
   2.412 +lemma dual_complete_distrib_lattice:
   2.413 +  "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   2.414 +  apply (rule class.complete_distrib_lattice.intro)
   2.415 +  apply (fact dual_complete_lattice)
   2.416 +  apply (rule class.complete_distrib_lattice_axioms.intro)
   2.417 +  apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf)
   2.418 +  done
   2.419 +
   2.420 +subclass distrib_lattice proof
   2.421 +  fix a b c
   2.422 +  from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
   2.423 +  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
   2.424 +qed
   2.425 +
   2.426 +lemma Inf_sup:
   2.427 +  "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
   2.428 +  by (simp add: sup_Inf sup_commute)
   2.429 +
   2.430 +lemma Sup_inf:
   2.431 +  "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
   2.432 +  by (simp add: inf_Sup inf_commute)
   2.433 +
   2.434 +lemma INF_sup: 
   2.435 +  "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
   2.436 +  by (simp add: sup_INF sup_commute)
   2.437 +
   2.438 +lemma SUP_inf:
   2.439 +  "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
   2.440 +  by (simp add: inf_SUP inf_commute)
   2.441 +
   2.442 +lemma Inf_sup_eq_top_iff:
   2.443 +  "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
   2.444 +  by (simp only: Inf_sup INF_top_conv)
   2.445 +
   2.446 +lemma Sup_inf_eq_bot_iff:
   2.447 +  "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
   2.448 +  by (simp only: Sup_inf SUP_bot_conv)
   2.449 +
   2.450 +lemma INF_sup_distrib2:
   2.451 +  "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)"
   2.452 +  by (subst INF_commute) (simp add: sup_INF INF_sup)
   2.453 +
   2.454 +lemma SUP_inf_distrib2:
   2.455 +  "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)"
   2.456 +  by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
   2.457 +
   2.458 +end
   2.459 +
   2.460 +class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice
   2.461 +begin
   2.462 +
   2.463 +lemma dual_complete_boolean_algebra:
   2.464 +  "class.complete_boolean_algebra Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
   2.465 +  by (rule class.complete_boolean_algebra.intro, rule dual_complete_distrib_lattice, rule dual_boolean_algebra)
   2.466 +
   2.467 +lemma uminus_Inf:
   2.468 +  "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
   2.469 +proof (rule antisym)
   2.470 +  show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
   2.471 +    by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
   2.472 +  show "\<Squnion>(uminus ` A) \<le> - \<Sqinter>A"
   2.473 +    by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto
   2.474 +qed
   2.475 +
   2.476 +lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
   2.477 +  by (simp add: INF_def SUP_def uminus_Inf image_image)
   2.478 +
   2.479 +lemma uminus_Sup:
   2.480 +  "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
   2.481 +proof -
   2.482 +  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_Inf)
   2.483 +  then show ?thesis by simp
   2.484 +qed
   2.485 +  
   2.486 +lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
   2.487 +  by (simp add: INF_def SUP_def uminus_Sup image_image)
   2.488 +
   2.489 +end
   2.490 +
   2.491 +class complete_linorder = linorder + complete_lattice
   2.492 +begin
   2.493 +
   2.494 +lemma dual_complete_linorder:
   2.495 +  "class.complete_linorder Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   2.496 +  by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
   2.497 +
   2.498 +lemma Inf_less_iff (*[simp]*):
   2.499 +  "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   2.500 +  unfolding not_le [symmetric] le_Inf_iff by auto
   2.501 +
   2.502 +lemma INF_less_iff (*[simp]*):
   2.503 +  "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   2.504 +  unfolding INF_def Inf_less_iff by auto
   2.505 +
   2.506 +lemma less_Sup_iff (*[simp]*):
   2.507 +  "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   2.508 +  unfolding not_le [symmetric] Sup_le_iff by auto
   2.509 +
   2.510 +lemma less_SUP_iff (*[simp]*):
   2.511 +  "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   2.512 +  unfolding SUP_def less_Sup_iff by auto
   2.513 +
   2.514 +lemma Sup_eq_top_iff (*[simp]*):
   2.515 +  "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   2.516 +proof
   2.517 +  assume *: "\<Squnion>A = \<top>"
   2.518 +  show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
   2.519 +  proof (intro allI impI)
   2.520 +    fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
   2.521 +      unfolding less_Sup_iff by auto
   2.522 +  qed
   2.523 +next
   2.524 +  assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i"
   2.525 +  show "\<Squnion>A = \<top>"
   2.526 +  proof (rule ccontr)
   2.527 +    assume "\<Squnion>A \<noteq> \<top>"
   2.528 +    with top_greatest [of "\<Squnion>A"]
   2.529 +    have "\<Squnion>A < \<top>" unfolding le_less by auto
   2.530 +    then have "\<Squnion>A < \<Squnion>A"
   2.531 +      using * unfolding less_Sup_iff by auto
   2.532 +    then show False by auto
   2.533 +  qed
   2.534 +qed
   2.535 +
   2.536 +lemma SUP_eq_top_iff (*[simp]*):
   2.537 +  "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
   2.538 +  unfolding SUP_def Sup_eq_top_iff by auto
   2.539 +
   2.540 +lemma Inf_eq_bot_iff (*[simp]*):
   2.541 +  "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
   2.542 +proof -
   2.543 +  interpret dual: complete_linorder Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
   2.544 +    by (fact dual_complete_linorder)
   2.545 +  from dual.Sup_eq_top_iff show ?thesis .
   2.546 +qed
   2.547 +
   2.548 +lemma INF_eq_bot_iff (*[simp]*):
   2.549 +  "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   2.550 +  unfolding INF_def Inf_eq_bot_iff by auto
   2.551 +
   2.552 +end
   2.553 +
   2.554 +
   2.555 +subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
   2.556 +
   2.557 +instantiation bool :: complete_lattice
   2.558 +begin
   2.559 +
   2.560 +definition
   2.561 +  [simp]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
   2.562 +
   2.563 +definition
   2.564 +  [simp]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
   2.565 +
   2.566 +instance proof
   2.567 +qed (auto intro: bool_induct)
   2.568 +
   2.569 +end
   2.570 +
   2.571 +lemma INF_bool_eq [simp]:
   2.572 +  "INFI = Ball"
   2.573 +proof (rule ext)+
   2.574 +  fix A :: "'a set"
   2.575 +  fix P :: "'a \<Rightarrow> bool"
   2.576 +  show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
   2.577 +    by (auto simp add: INF_def)
   2.578 +qed
   2.579 +
   2.580 +lemma SUP_bool_eq [simp]:
   2.581 +  "SUPR = Bex"
   2.582 +proof (rule ext)+
   2.583 +  fix A :: "'a set"
   2.584 +  fix P :: "'a \<Rightarrow> bool"
   2.585 +  show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
   2.586 +    by (auto simp add: SUP_def)
   2.587 +qed
   2.588 +
   2.589 +instance bool :: complete_boolean_algebra proof
   2.590 +qed (auto intro: bool_induct)
   2.591 +
   2.592 +instantiation "fun" :: (type, complete_lattice) complete_lattice
   2.593 +begin
   2.594 +
   2.595 +definition
   2.596 +  "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
   2.597 +
   2.598 +lemma Inf_apply:
   2.599 +  "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   2.600 +  by (simp add: Inf_fun_def)
   2.601 +
   2.602 +definition
   2.603 +  "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
   2.604 +
   2.605 +lemma Sup_apply:
   2.606 +  "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   2.607 +  by (simp add: Sup_fun_def)
   2.608 +
   2.609 +instance proof
   2.610 +qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_lower INF_greatest SUP_upper SUP_least)
   2.611 +
   2.612 +end
   2.613 +
   2.614 +lemma INF_apply:
   2.615 +  "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   2.616 +  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
   2.617 +
   2.618 +lemma SUP_apply:
   2.619 +  "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   2.620 +  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
   2.621 +
   2.622 +instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
   2.623 +qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image)
   2.624 +
   2.625 +instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
   2.626 +
   2.627 +
   2.628 +subsection {* Inter *}
   2.629 +
   2.630 +abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
   2.631 +  "Inter S \<equiv> \<Sqinter>S"
   2.632 +  
   2.633 +notation (xsymbols)
   2.634 +  Inter  ("\<Inter>_" [90] 90)
   2.635 +
   2.636 +lemma Inter_eq:
   2.637 +  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
   2.638 +proof (rule set_eqI)
   2.639 +  fix x
   2.640 +  have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
   2.641 +    by auto
   2.642 +  then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
   2.643 +    by (simp add: Inf_fun_def) (simp add: mem_def)
   2.644 +qed
   2.645 +
   2.646 +lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
   2.647 +  by (unfold Inter_eq) blast
   2.648 +
   2.649 +lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C"
   2.650 +  by (simp add: Inter_eq)
   2.651 +
   2.652 +text {*
   2.653 +  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
   2.654 +  contains @{term A} as an element, but @{prop "A \<in> X"} can hold when
   2.655 +  @{prop "X \<in> C"} does not!  This rule is analogous to @{text spec}.
   2.656 +*}
   2.657 +
   2.658 +lemma InterD [elim, Pure.elim]: "A \<in> \<Inter>C \<Longrightarrow> X \<in> C \<Longrightarrow> A \<in> X"
   2.659 +  by auto
   2.660 +
   2.661 +lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R"
   2.662 +  -- {* ``Classical'' elimination rule -- does not require proving
   2.663 +    @{prop "X \<in> C"}. *}
   2.664 +  by (unfold Inter_eq) blast
   2.665 +
   2.666 +lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
   2.667 +  by (fact Inf_lower)
   2.668 +
   2.669 +lemma Inter_subset:
   2.670 +  "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
   2.671 +  by (fact Inf_less_eq)
   2.672 +
   2.673 +lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
   2.674 +  by (fact Inf_greatest)
   2.675 +
   2.676 +lemma Inter_empty: "\<Inter>{} = UNIV"
   2.677 +  by (fact Inf_empty) (* already simp *)
   2.678 +
   2.679 +lemma Inter_UNIV: "\<Inter>UNIV = {}"
   2.680 +  by (fact Inf_UNIV) (* already simp *)
   2.681 +
   2.682 +lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
   2.683 +  by (fact Inf_insert)
   2.684 +
   2.685 +lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
   2.686 +  by (fact less_eq_Inf_inter)
   2.687 +
   2.688 +lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   2.689 +  by (fact Inf_union_distrib)
   2.690 +
   2.691 +lemma Inter_UNIV_conv [simp, no_atp]:
   2.692 +  "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   2.693 +  "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   2.694 +  by (fact Inf_top_conv)+
   2.695 +
   2.696 +lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
   2.697 +  by (fact Inf_superset_mono)
   2.698 +
   2.699 +
   2.700 +subsection {* Intersections of families *}
   2.701 +
   2.702 +abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   2.703 +  "INTER \<equiv> INFI"
   2.704 +
   2.705 +text {*
   2.706 +  Note: must use name @{const INTER} here instead of @{text INT}
   2.707 +  to allow the following syntax coexist with the plain constant name.
   2.708 +*}
   2.709 +
   2.710 +syntax
   2.711 +  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
   2.712 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
   2.713 +
   2.714 +syntax (xsymbols)
   2.715 +  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
   2.716 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
   2.717 +
   2.718 +syntax (latex output)
   2.719 +  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   2.720 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
   2.721 +
   2.722 +translations
   2.723 +  "INT x y. B"  == "INT x. INT y. B"
   2.724 +  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
   2.725 +  "INT x. B"    == "INT x:CONST UNIV. B"
   2.726 +  "INT x:A. B"  == "CONST INTER A (%x. B)"
   2.727 +
   2.728 +print_translation {*
   2.729 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
   2.730 +*} -- {* to avoid eta-contraction of body *}
   2.731 +
   2.732 +lemma INTER_eq:
   2.733 +  "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
   2.734 +  by (auto simp add: INF_def)
   2.735 +
   2.736 +lemma Inter_image_eq [simp]:
   2.737 +  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   2.738 +  by (rule sym) (fact INF_def)
   2.739 +
   2.740 +lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
   2.741 +  by (auto simp add: INF_def image_def)
   2.742 +
   2.743 +lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
   2.744 +  by (auto simp add: INF_def image_def)
   2.745 +
   2.746 +lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a"
   2.747 +  by auto
   2.748 +
   2.749 +lemma INT_E [elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> (b \<in> B a \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
   2.750 +  -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
   2.751 +  by (auto simp add: INF_def image_def)
   2.752 +
   2.753 +lemma INT_cong [cong]:
   2.754 +  "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)"
   2.755 +  by (fact INF_cong)
   2.756 +
   2.757 +lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
   2.758 +  by blast
   2.759 +
   2.760 +lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
   2.761 +  by blast
   2.762 +
   2.763 +lemma INT_lower: "a \<in> A \<Longrightarrow> (\<Inter>x\<in>A. B x) \<subseteq> B a"
   2.764 +  by (fact INF_lower)
   2.765 +
   2.766 +lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
   2.767 +  by (fact INF_greatest)
   2.768 +
   2.769 +lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV"
   2.770 +  by (fact INF_empty)
   2.771 +
   2.772 +lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
   2.773 +  by (fact INF_absorb)
   2.774 +
   2.775 +lemma INT_subset_iff: "B \<subseteq> (\<Inter>i\<in>I. A i) \<longleftrightarrow> (\<forall>i\<in>I. B \<subseteq> A i)"
   2.776 +  by (fact le_INF_iff)
   2.777 +
   2.778 +lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
   2.779 +  by (fact INF_insert)
   2.780 +
   2.781 +lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
   2.782 +  by (fact INF_union)
   2.783 +
   2.784 +lemma INT_insert_distrib:
   2.785 +  "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   2.786 +  by blast
   2.787 +
   2.788 +lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
   2.789 +  by (fact INF_constant)
   2.790 +
   2.791 +lemma INTER_UNIV_conv [simp]:
   2.792 + "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
   2.793 + "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
   2.794 +  by (fact INF_top_conv)+
   2.795 +
   2.796 +lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
   2.797 +  by (fact INF_UNIV_bool_expand)
   2.798 +
   2.799 +lemma INT_anti_mono:
   2.800 +  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
   2.801 +  -- {* The last inclusion is POSITIVE! *}
   2.802 +  by (fact INF_superset_mono)
   2.803 +
   2.804 +lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
   2.805 +  by blast
   2.806 +
   2.807 +lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)"
   2.808 +  by blast
   2.809 +
   2.810 +
   2.811 +subsection {* Union *}
   2.812 +
   2.813 +abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
   2.814 +  "Union S \<equiv> \<Squnion>S"
   2.815 +
   2.816 +notation (xsymbols)
   2.817 +  Union  ("\<Union>_" [90] 90)
   2.818 +
   2.819 +lemma Union_eq:
   2.820 +  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
   2.821 +proof (rule set_eqI)
   2.822 +  fix x
   2.823 +  have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
   2.824 +    by auto
   2.825 +  then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
   2.826 +    by (simp add: Sup_fun_def) (simp add: mem_def)
   2.827 +qed
   2.828 +
   2.829 +lemma Union_iff [simp, no_atp]:
   2.830 +  "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
   2.831 +  by (unfold Union_eq) blast
   2.832 +
   2.833 +lemma UnionI [intro]:
   2.834 +  "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
   2.835 +  -- {* The order of the premises presupposes that @{term C} is rigid;
   2.836 +    @{term A} may be flexible. *}
   2.837 +  by auto
   2.838 +
   2.839 +lemma UnionE [elim!]:
   2.840 +  "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R"
   2.841 +  by auto
   2.842 +
   2.843 +lemma Union_upper: "B \<in> A \<Longrightarrow> B \<subseteq> \<Union>A"
   2.844 +  by (fact Sup_upper)
   2.845 +
   2.846 +lemma Union_least: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> C) \<Longrightarrow> \<Union>A \<subseteq> C"
   2.847 +  by (fact Sup_least)
   2.848 +
   2.849 +lemma Union_empty [simp]: "\<Union>{} = {}"
   2.850 +  by (fact Sup_empty)
   2.851 +
   2.852 +lemma Union_UNIV [simp]: "\<Union>UNIV = UNIV"
   2.853 +  by (fact Sup_UNIV)
   2.854 +
   2.855 +lemma Union_insert [simp]: "\<Union>insert a B = a \<union> \<Union>B"
   2.856 +  by (fact Sup_insert)
   2.857 +
   2.858 +lemma Union_Un_distrib [simp]: "\<Union>(A \<union> B) = \<Union>A \<union> \<Union>B"
   2.859 +  by (fact Sup_union_distrib)
   2.860 +
   2.861 +lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   2.862 +  by (fact Sup_inter_less_eq)
   2.863 +
   2.864 +lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
   2.865 +  by (fact Sup_bot_conv)
   2.866 +
   2.867 +lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
   2.868 +  by (fact Sup_bot_conv)
   2.869 +
   2.870 +lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
   2.871 +  by blast
   2.872 +
   2.873 +lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
   2.874 +  by blast
   2.875 +
   2.876 +lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
   2.877 +  by (fact Sup_subset_mono)
   2.878 +
   2.879 +
   2.880 +subsection {* Unions of families *}
   2.881 +
   2.882 +abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   2.883 +  "UNION \<equiv> SUPR"
   2.884 +
   2.885 +text {*
   2.886 +  Note: must use name @{const UNION} here instead of @{text UN}
   2.887 +  to allow the following syntax coexist with the plain constant name.
   2.888 +*}
   2.889 +
   2.890 +syntax
   2.891 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   2.892 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
   2.893 +
   2.894 +syntax (xsymbols)
   2.895 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
   2.896 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
   2.897 +
   2.898 +syntax (latex output)
   2.899 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   2.900 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
   2.901 +
   2.902 +translations
   2.903 +  "UN x y. B"   == "UN x. UN y. B"
   2.904 +  "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"
   2.905 +  "UN x. B"     == "UN x:CONST UNIV. B"
   2.906 +  "UN x:A. B"   == "CONST UNION A (%x. B)"
   2.907 +
   2.908 +text {*
   2.909 +  Note the difference between ordinary xsymbol syntax of indexed
   2.910 +  unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
   2.911 +  and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
   2.912 +  former does not make the index expression a subscript of the
   2.913 +  union/intersection symbol because this leads to problems with nested
   2.914 +  subscripts in Proof General.
   2.915 +*}
   2.916 +
   2.917 +print_translation {*
   2.918 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
   2.919 +*} -- {* to avoid eta-contraction of body *}
   2.920 +
   2.921 +lemma UNION_eq [no_atp]:
   2.922 +  "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   2.923 +  by (auto simp add: SUP_def)
   2.924 +  
   2.925 +lemma Union_image_eq [simp]:
   2.926 +  "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   2.927 +  by (auto simp add: UNION_eq)
   2.928 +  
   2.929 +lemma UN_iff [simp]: "(b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)"
   2.930 +  by (auto simp add: SUP_def image_def)
   2.931 +
   2.932 +lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
   2.933 +  -- {* The order of the premises presupposes that @{term A} is rigid;
   2.934 +    @{term b} may be flexible. *}
   2.935 +  by auto
   2.936 +
   2.937 +lemma UN_E [elim!]: "b \<in> (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x\<in>A \<Longrightarrow> b \<in> B x \<Longrightarrow> R) \<Longrightarrow> R"
   2.938 +  by (auto simp add: SUP_def image_def)
   2.939 +
   2.940 +lemma UN_cong [cong]:
   2.941 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
   2.942 +  by (fact SUP_cong)
   2.943 +
   2.944 +lemma strong_UN_cong:
   2.945 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
   2.946 +  by (unfold simp_implies_def) (fact UN_cong)
   2.947 +
   2.948 +lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
   2.949 +  by blast
   2.950 +
   2.951 +lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
   2.952 +  by (fact SUP_upper)
   2.953 +
   2.954 +lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
   2.955 +  by (fact SUP_least)
   2.956 +
   2.957 +lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
   2.958 +  by blast
   2.959 +
   2.960 +lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
   2.961 +  by blast
   2.962 +
   2.963 +lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
   2.964 +  by (fact SUP_empty)
   2.965 +
   2.966 +lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
   2.967 +  by (fact SUP_bot)
   2.968 +
   2.969 +lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
   2.970 +  by (fact SUP_absorb)
   2.971 +
   2.972 +lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
   2.973 +  by (fact SUP_insert)
   2.974 +
   2.975 +lemma UN_Un [simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
   2.976 +  by (fact SUP_union)
   2.977 +
   2.978 +lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
   2.979 +  by blast
   2.980 +
   2.981 +lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
   2.982 +  by (fact SUP_le_iff)
   2.983 +
   2.984 +lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
   2.985 +  by (fact SUP_constant)
   2.986 +
   2.987 +lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
   2.988 +  by blast
   2.989 +
   2.990 +lemma UNION_empty_conv[simp]:
   2.991 +  "{} = (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
   2.992 +  "(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
   2.993 +  by (fact SUP_bot_conv)+
   2.994 +
   2.995 +lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   2.996 +  by blast
   2.997 +
   2.998 +lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
   2.999 +  by blast
  2.1000 +
  2.1001 +lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
  2.1002 +  by blast
  2.1003 +
  2.1004 +lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
  2.1005 +  by (auto simp add: split_if_mem2)
  2.1006 +
  2.1007 +lemma UN_bool_eq: "(\<Union>b. A b) = (A True \<union> A False)"
  2.1008 +  by (fact SUP_UNIV_bool_expand)
  2.1009 +
  2.1010 +lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
  2.1011 +  by blast
  2.1012 +
  2.1013 +lemma UN_mono:
  2.1014 +  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
  2.1015 +    (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
  2.1016 +  by (fact SUP_subset_mono)
  2.1017 +
  2.1018 +lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)"
  2.1019 +  by blast
  2.1020 +
  2.1021 +lemma vimage_UN: "f -` (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. f -` B x)"
  2.1022 +  by blast
  2.1023 +
  2.1024 +lemma vimage_eq_UN: "f -` B = (\<Union>y\<in>B. f -` {y})"
  2.1025 +  -- {* NOT suitable for rewriting *}
  2.1026 +  by blast
  2.1027 +
  2.1028 +lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
  2.1029 +  by blast
  2.1030 +
  2.1031 +
  2.1032 +subsection {* Distributive laws *}
  2.1033 +
  2.1034 +lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
  2.1035 +  by (fact inf_Sup)
  2.1036 +
  2.1037 +lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
  2.1038 +  by (fact sup_Inf)
  2.1039 +
  2.1040 +lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
  2.1041 +  by (fact Sup_inf)
  2.1042 +
  2.1043 +lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)"
  2.1044 +  by (rule sym) (rule INF_inf_distrib)
  2.1045 +
  2.1046 +lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
  2.1047 +  by (rule sym) (rule SUP_sup_distrib)
  2.1048 +
  2.1049 +lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"
  2.1050 +  by (simp only: INT_Int_distrib INF_def)
  2.1051 +
  2.1052 +lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"
  2.1053 +  -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
  2.1054 +  -- {* Union of a family of unions *}
  2.1055 +  by (simp only: UN_Un_distrib SUP_def)
  2.1056 +
  2.1057 +lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
  2.1058 +  by (fact sup_INF)
  2.1059 +
  2.1060 +lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"
  2.1061 +  -- {* Halmos, Naive Set Theory, page 35. *}
  2.1062 +  by (fact inf_SUP)
  2.1063 +
  2.1064 +lemma Int_UN_distrib2: "(\<Union>i\<in>I. A i) \<inter> (\<Union>j\<in>J. B j) = (\<Union>i\<in>I. \<Union>j\<in>J. A i \<inter> B j)"
  2.1065 +  by (fact SUP_inf_distrib2)
  2.1066 +
  2.1067 +lemma Un_INT_distrib2: "(\<Inter>i\<in>I. A i) \<union> (\<Inter>j\<in>J. B j) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A i \<union> B j)"
  2.1068 +  by (fact INF_sup_distrib2)
  2.1069 +
  2.1070 +lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
  2.1071 +  by (fact Sup_inf_eq_bot_iff)
  2.1072 +
  2.1073 +
  2.1074 +subsection {* Complement *}
  2.1075 +
  2.1076 +lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
  2.1077 +  by (fact uminus_INF)
  2.1078 +
  2.1079 +lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
  2.1080 +  by (fact uminus_SUP)
  2.1081 +
  2.1082 +
  2.1083 +subsection {* Miniscoping and maxiscoping *}
  2.1084 +
  2.1085 +text {* \medskip Miniscoping: pushing in quantifiers and big Unions
  2.1086 +           and Intersections. *}
  2.1087 +
  2.1088 +lemma UN_simps [simp]:
  2.1089 +  "\<And>a B C. (\<Union>x\<in>C. insert a (B x)) = (if C={} then {} else insert a (\<Union>x\<in>C. B x))"
  2.1090 +  "\<And>A B C. (\<Union>x\<in>C. A x \<union> B) = ((if C={} then {} else (\<Union>x\<in>C. A x) \<union> B))"
  2.1091 +  "\<And>A B C. (\<Union>x\<in>C. A \<union> B x) = ((if C={} then {} else A \<union> (\<Union>x\<in>C. B x)))"
  2.1092 +  "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter> B)"
  2.1093 +  "\<And>A B C. (\<Union>x\<in>C. A \<inter> B x) = (A \<inter>(\<Union>x\<in>C. B x))"
  2.1094 +  "\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
  2.1095 +  "\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
  2.1096 +  "\<And>A B. (\<Union>x\<in>\<Union>A. B x) = (\<Union>y\<in>A. \<Union>x\<in>y. B x)"
  2.1097 +  "\<And>A B C. (\<Union>z\<in>UNION A B. C z) = (\<Union>x\<in>A. \<Union>z\<in>B x. C z)"
  2.1098 +  "\<And>A B f. (\<Union>x\<in>f`A. B x) = (\<Union>a\<in>A. B (f a))"
  2.1099 +  by auto
  2.1100 +
  2.1101 +lemma INT_simps [simp]:
  2.1102 +  "\<And>A B C. (\<Inter>x\<in>C. A x \<inter> B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) \<inter> B)"
  2.1103 +  "\<And>A B C. (\<Inter>x\<in>C. A \<inter> B x) = (if C={} then UNIV else A \<inter>(\<Inter>x\<in>C. B x))"
  2.1104 +  "\<And>A B C. (\<Inter>x\<in>C. A x - B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)"
  2.1105 +  "\<And>A B C. (\<Inter>x\<in>C. A - B x) = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))"
  2.1106 +  "\<And>a B C. (\<Inter>x\<in>C. insert a (B x)) = insert a (\<Inter>x\<in>C. B x)"
  2.1107 +  "\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)"
  2.1108 +  "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))"
  2.1109 +  "\<And>A B. (\<Inter>x\<in>\<Union>A. B x) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B x)"
  2.1110 +  "\<And>A B C. (\<Inter>z\<in>UNION A B. C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
  2.1111 +  "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
  2.1112 +  by auto
  2.1113 +
  2.1114 +lemma UN_ball_bex_simps [simp, no_atp]:
  2.1115 +  "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
  2.1116 +  "\<And>A B P. (\<forall>x\<in>UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
  2.1117 +  "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
  2.1118 +  "\<And>A B P. (\<exists>x\<in>UNION A B. P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
  2.1119 +  by auto
  2.1120 +
  2.1121 +
  2.1122 +text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
  2.1123 +
  2.1124 +lemma UN_extend_simps:
  2.1125 +  "\<And>a B C. insert a (\<Union>x\<in>C. B x) = (if C={} then {a} else (\<Union>x\<in>C. insert a (B x)))"
  2.1126 +  "\<And>A B C. (\<Union>x\<in>C. A x) \<union> B = (if C={} then B else (\<Union>x\<in>C. A x \<union> B))"
  2.1127 +  "\<And>A B C. A \<union> (\<Union>x\<in>C. B x) = (if C={} then A else (\<Union>x\<in>C. A \<union> B x))"
  2.1128 +  "\<And>A B C. ((\<Union>x\<in>C. A x) \<inter> B) = (\<Union>x\<in>C. A x \<inter> B)"
  2.1129 +  "\<And>A B C. (A \<inter> (\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> B x)"
  2.1130 +  "\<And>A B C. ((\<Union>x\<in>C. A x) - B) = (\<Union>x\<in>C. A x - B)"
  2.1131 +  "\<And>A B C. (A - (\<Inter>x\<in>C. B x)) = (\<Union>x\<in>C. A - B x)"
  2.1132 +  "\<And>A B. (\<Union>y\<in>A. \<Union>x\<in>y. B x) = (\<Union>x\<in>\<Union>A. B x)"
  2.1133 +  "\<And>A B C. (\<Union>x\<in>A. \<Union>z\<in>B x. C z) = (\<Union>z\<in>UNION A B. C z)"
  2.1134 +  "\<And>A B f. (\<Union>a\<in>A. B (f a)) = (\<Union>x\<in>f`A. B x)"
  2.1135 +  by auto
  2.1136 +
  2.1137 +lemma INT_extend_simps:
  2.1138 +  "\<And>A B C. (\<Inter>x\<in>C. A x) \<inter> B = (if C={} then B else (\<Inter>x\<in>C. A x \<inter> B))"
  2.1139 +  "\<And>A B C. A \<inter> (\<Inter>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A \<inter> B x))"
  2.1140 +  "\<And>A B C. (\<Inter>x\<in>C. A x) - B = (if C={} then UNIV - B else (\<Inter>x\<in>C. A x - B))"
  2.1141 +  "\<And>A B C. A - (\<Union>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A - B x))"
  2.1142 +  "\<And>a B C. insert a (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. insert a (B x))"
  2.1143 +  "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)"
  2.1144 +  "\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)"
  2.1145 +  "\<And>A B. (\<Inter>y\<in>A. \<Inter>x\<in>y. B x) = (\<Inter>x\<in>\<Union>A. B x)"
  2.1146 +  "\<And>A B C. (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z) = (\<Inter>z\<in>UNION A B. C z)"
  2.1147 +  "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
  2.1148 +  by auto
  2.1149 +
  2.1150 +
  2.1151 +text {* Legacy names *}
  2.1152 +
  2.1153 +lemma (in complete_lattice) Inf_singleton [simp]:
  2.1154 +  "\<Sqinter>{a} = a"
  2.1155 +  by (simp add: Inf_insert)
  2.1156 +
  2.1157 +lemma (in complete_lattice) Sup_singleton [simp]:
  2.1158 +  "\<Squnion>{a} = a"
  2.1159 +  by (simp add: Sup_insert)
  2.1160 +
  2.1161 +lemma (in complete_lattice) Inf_binary:
  2.1162 +  "\<Sqinter>{a, b} = a \<sqinter> b"
  2.1163 +  by (simp add: Inf_insert)
  2.1164 +
  2.1165 +lemma (in complete_lattice) Sup_binary:
  2.1166 +  "\<Squnion>{a, b} = a \<squnion> b"
  2.1167 +  by (simp add: Sup_insert)
  2.1168 +
  2.1169 +lemmas (in complete_lattice) INFI_def = INF_def
  2.1170 +lemmas (in complete_lattice) SUPR_def = SUP_def
  2.1171 +lemmas (in complete_lattice) INF_leI = INF_lower
  2.1172 +lemmas (in complete_lattice) INF_leI2 = INF_lower2
  2.1173 +lemmas (in complete_lattice) le_INFI = INF_greatest
  2.1174 +lemmas (in complete_lattice) le_SUPI = SUP_upper
  2.1175 +lemmas (in complete_lattice) le_SUPI2 = SUP_upper2
  2.1176 +lemmas (in complete_lattice) SUP_leI = SUP_least
  2.1177 +lemmas (in complete_lattice) less_INFD = less_INF_D
  2.1178 +
  2.1179 +lemmas INFI_apply = INF_apply
  2.1180 +lemmas SUPR_apply = SUP_apply
  2.1181 +
  2.1182 +text {* Grep and put to news from here *}
  2.1183 +
  2.1184 +lemma (in complete_lattice) INF_eq:
  2.1185 +  "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
  2.1186 +  by (simp add: INF_def image_def)
  2.1187 +
  2.1188 +lemma (in complete_lattice) SUP_eq:
  2.1189 +  "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
  2.1190 +  by (simp add: SUP_def image_def)
  2.1191 +
  2.1192 +lemma (in complete_lattice) INF_subset:
  2.1193 +  "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
  2.1194 +  by (rule INF_superset_mono) auto
  2.1195 +
  2.1196 +lemma (in complete_lattice) INF_UNIV_range:
  2.1197 +  "(\<Sqinter>x. f x) = \<Sqinter>range f"
  2.1198 +  by (fact INF_def)
  2.1199 +
  2.1200 +lemma (in complete_lattice) SUP_UNIV_range:
  2.1201 +  "(\<Squnion>x. f x) = \<Squnion>range f"
  2.1202 +  by (fact SUP_def)
  2.1203 +
  2.1204 +lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
  2.1205 +  by (simp add: Inf_insert)
  2.1206 +
  2.1207 +lemma INTER_eq_Inter_image:
  2.1208 +  "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
  2.1209 +  by (fact INF_def)
  2.1210 +  
  2.1211 +lemma Inter_def:
  2.1212 +  "\<Inter>S = (\<Inter>x\<in>S. x)"
  2.1213 +  by (simp add: INTER_eq_Inter_image image_def)
  2.1214 +
  2.1215 +lemmas INTER_def = INTER_eq
  2.1216 +lemmas UNION_def = UNION_eq
  2.1217 +
  2.1218 +lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
  2.1219 +  by (fact INF_eq)
  2.1220 +
  2.1221 +lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
  2.1222 +  by blast
  2.1223 +
  2.1224 +lemma UNION_eq_Union_image:
  2.1225 +  "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
  2.1226 +  by (fact SUP_def)
  2.1227 +
  2.1228 +lemma Union_def:
  2.1229 +  "\<Union>S = (\<Union>x\<in>S. x)"
  2.1230 +  by (simp add: UNION_eq_Union_image image_def)
  2.1231 +
  2.1232 +lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
  2.1233 +  by blast
  2.1234 +
  2.1235 +lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
  2.1236 +  by (fact SUP_eq)
  2.1237 +
  2.1238 +
  2.1239 +text {* Finally *}
  2.1240 +
  2.1241 +no_notation
  2.1242 +  less_eq  (infix "\<sqsubseteq>" 50) and
  2.1243 +  less (infix "\<sqsubset>" 50) and
  2.1244 +  bot ("\<bottom>") and
  2.1245 +  top ("\<top>") and
  2.1246 +  inf  (infixl "\<sqinter>" 70) and
  2.1247 +  sup  (infixl "\<squnion>" 65) and
  2.1248 +  Inf  ("\<Sqinter>_" [900] 900) and
  2.1249 +  Sup  ("\<Squnion>_" [900] 900)
  2.1250 +
  2.1251 +no_syntax (xsymbols)
  2.1252 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
  2.1253 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
  2.1254 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
  2.1255 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
  2.1256 +
  2.1257 +lemmas mem_simps =
  2.1258 +  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
  2.1259 +  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
  2.1260 +  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
  2.1261 +
  2.1262 +end
     3.1 --- a/src/HOL/Fun.thy	Sat Sep 10 00:44:25 2011 +0200
     3.2 +++ b/src/HOL/Fun.thy	Sat Sep 10 10:29:24 2011 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Notions about functions *}
     3.5  
     3.6  theory Fun
     3.7 -imports Complete_Lattice
     3.8 +imports Complete_Lattices
     3.9  uses ("Tools/enriched_type.ML")
    3.10  begin
    3.11  
     4.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Sep 10 00:44:25 2011 +0200
     4.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Sep 10 10:29:24 2011 +0200
     4.3 @@ -146,9 +146,9 @@
     4.4    GSPEC > Set.Collect
     4.5    SETSPEC > HOLLightCompat.SETSPEC
     4.6    UNION > Lattices.sup_class.sup :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
     4.7 -  UNIONS > Complete_Lattice.Sup_class.Sup :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
     4.8 +  UNIONS > Complete_Lattices.Sup_class.Sup :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
     4.9    INTER > Lattices.inf_class.inf :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    4.10 -  INTERS > Complete_Lattice.Inf_class.Inf :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    4.11 +  INTERS > Complete_Lattices.Inf_class.Inf :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    4.12    DIFF > Groups.minus_class.minus :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    4.13    SUBSET > Orderings.ord_class.less_eq :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    4.14    PSUBSET > Orderings.ord_class.less :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
     5.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Sat Sep 10 00:44:25 2011 +0200
     5.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Sat Sep 10 10:29:24 2011 +0200
     5.3 @@ -266,7 +266,7 @@
     5.4    "ZBOT" > "HOLLight.hollight.ZBOT"
     5.5    "WF" > "Wellfounded.wfP"
     5.6    "UNIV" > "Orderings.top_class.top" :: "'a => bool"
     5.7 -  "UNIONS" > "Complete_Lattice.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
     5.8 +  "UNIONS" > "Complete_Lattices.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
     5.9    "UNION" > "Lattices.sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
    5.10    "UNCURRY" > "HOLLight.hollight.UNCURRY"
    5.11    "TL" > "List.tl"
    5.12 @@ -316,7 +316,7 @@
    5.13    "ITLIST2" > "HOLLightList.fold2"
    5.14    "ITLIST" > "List.foldr"
    5.15    "ISO" > "HOLLight.hollight.ISO"
    5.16 -  "INTERS" > "Complete_Lattice.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
    5.17 +  "INTERS" > "Complete_Lattices.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
    5.18    "INTER" > "Lattices.inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
    5.19    "INSERT" > "Set.insert"
    5.20    "INR" > "Sum_Type.Inr"
    5.21 @@ -584,15 +584,15 @@
    5.22    "UNION_COMM" > "Lattices.lattice_class.inf_sup_aci_5"
    5.23    "UNION_ASSOC" > "Lattices.lattice_class.inf_sup_aci_6"
    5.24    "UNION_ACI" > "HOLLight.hollight.UNION_ACI"
    5.25 -  "UNIONS_UNION" > "Complete_Lattice.Union_Un_distrib"
    5.26 +  "UNIONS_UNION" > "Complete_Lattices.Union_Un_distrib"
    5.27    "UNIONS_SUBSET" > "HOLLight.hollight.UNIONS_SUBSET"
    5.28    "UNIONS_INTERS" > "HOLLight.hollight.UNIONS_INTERS"
    5.29 -  "UNIONS_INSERT" > "Complete_Lattice.Union_insert"
    5.30 +  "UNIONS_INSERT" > "Complete_Lattices.Union_insert"
    5.31    "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
    5.32    "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
    5.33 -  "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
    5.34 -  "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
    5.35 -  "UNIONS_0" > "Complete_Lattice.Union_empty"
    5.36 +  "UNIONS_2" > "Complete_Lattices.Un_eq_Union"
    5.37 +  "UNIONS_1" > "Complete_Lattices.complete_lattice_class.Sup_singleton"
    5.38 +  "UNIONS_0" > "Complete_Lattices.Union_empty"
    5.39    "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
    5.40    "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
    5.41    "TYDEF_real" > "HOLLight.hollight.TYDEF_real"
    5.42 @@ -779,7 +779,7 @@
    5.43    "SUB_0" > "HOLLight.hollight.SUB_0"
    5.44    "SUBSET_UNIV" > "Orderings.top_class.top_greatest"
    5.45    "SUBSET_UNION_ABSORPTION" > "Lattices.semilattice_sup_class.le_iff_sup"
    5.46 -  "SUBSET_UNIONS" > "Complete_Lattice.Union_mono"
    5.47 +  "SUBSET_UNIONS" > "Complete_Lattices.Union_mono"
    5.48    "SUBSET_UNION" > "HOLLight.hollight.SUBSET_UNION"
    5.49    "SUBSET_TRANS" > "Orderings.order_trans_rules_23"
    5.50    "SUBSET_RESTRICT" > "HOLLight.hollight.SUBSET_RESTRICT"
    5.51 @@ -1544,7 +1544,7 @@
    5.52    "ISO_FUN" > "HOLLight.hollight.ISO_FUN"
    5.53    "IN_UNIV" > "Set.UNIV_I"
    5.54    "IN_UNIONS" > "HOLLight.hollight.IN_UNIONS"
    5.55 -  "IN_UNION" > "Complete_Lattice.mem_simps_3"
    5.56 +  "IN_UNION" > "Complete_Lattices.mem_simps_3"
    5.57    "IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
    5.58    "IN_SING" > "Set.singleton_iff"
    5.59    "IN_SET_OF_LIST" > "HOLLightList.IN_SET_OF_LIST"
    5.60 @@ -1552,13 +1552,13 @@
    5.61    "IN_NUMSEG_0" > "HOLLight.hollight.IN_NUMSEG_0"
    5.62    "IN_NUMSEG" > "SetInterval.ord_class.atLeastAtMost_iff"
    5.63    "IN_INTERS" > "HOLLight.hollight.IN_INTERS"
    5.64 -  "IN_INTER" > "Complete_Lattice.mem_simps_4"
    5.65 -  "IN_INSERT" > "Complete_Lattice.mem_simps_1"
    5.66 +  "IN_INTER" > "Complete_Lattices.mem_simps_4"
    5.67 +  "IN_INSERT" > "Complete_Lattices.mem_simps_1"
    5.68    "IN_IMAGE" > "HOLLight.hollight.IN_IMAGE"
    5.69    "IN_ELIM_THM" > "HOLLight.hollight.IN_ELIM_THM"
    5.70    "IN_ELIM_PAIR_THM" > "HOLLight.hollight.IN_ELIM_PAIR_THM"
    5.71    "IN_DISJOINT" > "HOLLight.hollight.IN_DISJOINT"
    5.72 -  "IN_DIFF" > "Complete_Lattice.mem_simps_6"
    5.73 +  "IN_DIFF" > "Complete_Lattices.mem_simps_6"
    5.74    "IN_DELETE_EQ" > "HOLLight.hollight.IN_DELETE_EQ"
    5.75    "IN_DELETE" > "HOLLight.hollight.IN_DELETE"
    5.76    "IN_CROSS" > "HOLLight.hollight.IN_CROSS"
    5.77 @@ -1594,12 +1594,12 @@
    5.78    "INTER_ASSOC" > "Lattices.lattice_class.inf_sup_aci_2"
    5.79    "INTER_ACI" > "HOLLight.hollight.INTER_ACI"
    5.80    "INTERS_UNIONS" > "HOLLight.hollight.INTERS_UNIONS"
    5.81 -  "INTERS_INSERT" > "Complete_Lattice.Inter_insert"
    5.82 +  "INTERS_INSERT" > "Complete_Lattices.Inter_insert"
    5.83    "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
    5.84    "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
    5.85 -  "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
    5.86 -  "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
    5.87 -  "INTERS_0" > "Complete_Lattice.Inter_empty"
    5.88 +  "INTERS_2" > "Complete_Lattices.Int_eq_Inter"
    5.89 +  "INTERS_1" > "Complete_Lattices.complete_lattice_class.Inf_singleton"
    5.90 +  "INTERS_0" > "Complete_Lattices.Inter_empty"
    5.91    "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
    5.92    "INSERT_UNION_EQ" > "Set.Un_insert_left"
    5.93    "INSERT_UNION" > "HOLLight.hollight.INSERT_UNION"
     6.1 --- a/src/HOL/Inductive.thy	Sat Sep 10 00:44:25 2011 +0200
     6.2 +++ b/src/HOL/Inductive.thy	Sat Sep 10 10:29:24 2011 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
     6.5  
     6.6  theory Inductive 
     6.7 -imports Complete_Lattice
     6.8 +imports Complete_Lattices
     6.9  uses
    6.10    ("Tools/inductive.ML")
    6.11    "Tools/dseq.ML"
     7.1 --- a/src/HOL/IsaMakefile	Sat Sep 10 00:44:25 2011 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Sat Sep 10 10:29:24 2011 +0200
     7.3 @@ -171,7 +171,7 @@
     7.4    $(SRC)/Tools/Metis/metis.ML \
     7.5    $(SRC)/Tools/rat.ML \
     7.6    ATP.thy \
     7.7 -  Complete_Lattice.thy \
     7.8 +  Complete_Lattices.thy \
     7.9    Complete_Partial_Order.thy \
    7.10    Datatype.thy \
    7.11    Extraction.thy \
     8.1 --- a/src/HOL/Library/Executable_Set.thy	Sat Sep 10 00:44:25 2011 +0200
     8.2 +++ b/src/HOL/Library/Executable_Set.thy	Sat Sep 10 10:29:24 2011 +0200
     8.3 @@ -199,17 +199,17 @@
     8.4    by simp
     8.5  
     8.6  definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
     8.7 -  [simp]: "Inf = Complete_Lattice.Inf"
     8.8 +  [simp]: "Inf = Complete_Lattices.Inf"
     8.9  
    8.10  lemma [code_unfold]:
    8.11 -  "Complete_Lattice.Inf = Inf"
    8.12 +  "Complete_Lattices.Inf = Inf"
    8.13    by simp
    8.14  
    8.15  definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
    8.16 -  [simp]: "Sup = Complete_Lattice.Sup"
    8.17 +  [simp]: "Sup = Complete_Lattices.Sup"
    8.18  
    8.19  lemma [code_unfold]:
    8.20 -  "Complete_Lattice.Sup = Sup"
    8.21 +  "Complete_Lattices.Sup = Sup"
    8.22    by simp
    8.23  
    8.24  definition Inter :: "'a set set \<Rightarrow> 'a set" where
     9.1 --- a/src/HOL/Library/Lattice_Syntax.thy	Sat Sep 10 00:44:25 2011 +0200
     9.2 +++ b/src/HOL/Library/Lattice_Syntax.thy	Sat Sep 10 10:29:24 2011 +0200
     9.3 @@ -3,7 +3,7 @@
     9.4  header {* Pretty syntax for lattice operations *}
     9.5  
     9.6  theory Lattice_Syntax
     9.7 -imports Complete_Lattice
     9.8 +imports Complete_Lattices
     9.9  begin
    9.10  
    9.11  notation
    10.1 --- a/src/HOL/Main.thy	Sat Sep 10 00:44:25 2011 +0200
    10.2 +++ b/src/HOL/Main.thy	Sat Sep 10 10:29:24 2011 +0200
    10.3 @@ -21,7 +21,7 @@
    10.4    "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    10.5    by auto
    10.6  
    10.7 -declare Complete_Lattice.Inf_bool_def [simp del]
    10.8 -declare Complete_Lattice.Sup_bool_def [simp del]
    10.9 +declare Complete_Lattices.Inf_bool_def [simp del]
   10.10 +declare Complete_Lattices.Sup_bool_def [simp del]
   10.11  
   10.12  end
    11.1 --- a/src/HOL/Quotient_Examples/Cset.thy	Sat Sep 10 00:44:25 2011 +0200
    11.2 +++ b/src/HOL/Quotient_Examples/Cset.thy	Sat Sep 10 10:29:24 2011 +0200
    11.3 @@ -89,7 +89,7 @@
    11.4  quotient_definition Sup where "Sup :: ('a :: Sup) Cset.set \<Rightarrow> 'a"
    11.5  is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a"
    11.6  quotient_definition UNION where "UNION :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
    11.7 -is "Complete_Lattice.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    11.8 +is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    11.9  
   11.10  hide_const (open) is_empty insert remove map filter forall exists card
   11.11    set subset psubset inter union empty UNIV uminus minus Inf Sup UNION