1.1 --- a/src/HOL/Complete_Lattice.thy Mon Aug 08 22:11:00 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy Mon Aug 08 22:33:36 2011 +0200
1.3 @@ -126,16 +126,16 @@
1.4 lemma le_SUP_I2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
1.5 using le_SUP_I [of i A f] by auto
1.6
1.7 -lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
1.8 +lemma le_Inf_iff (*[simp]*): "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
1.9 by (auto intro: Inf_greatest dest: Inf_lower)
1.10
1.11 -lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
1.12 +lemma le_INF_iff (*[simp]*): "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
1.13 by (auto simp add: INF_def le_Inf_iff)
1.14
1.15 -lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
1.16 +lemma Sup_le_iff (*[simp]*): "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
1.17 by (auto intro: Sup_least dest: Sup_upper)
1.18
1.19 -lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
1.20 +lemma SUP_le_iff (*[simp]*): "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
1.21 by (auto simp add: SUP_def Sup_le_iff)
1.22
1.23 lemma Inf_empty [simp]:
1.24 @@ -172,10 +172,10 @@
1.25 lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
1.26 by (simp add: SUP_def Sup_insert)
1.27
1.28 -lemma INF_image: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
1.29 +lemma INF_image (*[simp]*): "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
1.30 by (simp add: INF_def image_image)
1.31
1.32 -lemma SUP_image: "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
1.33 +lemma SUP_image (*[simp]*): "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
1.34 by (simp add: SUP_def image_image)
1.35
1.36 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
1.37 @@ -282,7 +282,7 @@
1.38 by (rule antisym) (auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono,
1.39 rule SUP_leI, auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono)
1.40
1.41 -lemma Inf_top_conv [no_atp]:
1.42 +lemma Inf_top_conv (*[simp]*) [no_atp]:
1.43 "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
1.44 "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
1.45 proof -
1.46 @@ -304,12 +304,12 @@
1.47 then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
1.48 qed
1.49
1.50 -lemma INF_top_conv:
1.51 +lemma INF_top_conv (*[simp]*):
1.52 "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
1.53 "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
1.54 by (auto simp add: INF_def Inf_top_conv)
1.55
1.56 -lemma Sup_bot_conv [no_atp]:
1.57 +lemma Sup_bot_conv (*[simp]*) [no_atp]:
1.58 "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
1.59 "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
1.60 proof -
1.61 @@ -318,7 +318,7 @@
1.62 from dual.Inf_top_conv show ?P and ?Q by simp_all
1.63 qed
1.64
1.65 -lemma SUP_bot_conv:
1.66 +lemma SUP_bot_conv (*[simp]*):
1.67 "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
1.68 "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
1.69 by (auto simp add: SUP_def Sup_bot_conv)
1.70 @@ -329,10 +329,10 @@
1.71 lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
1.72 by (auto intro: antisym SUP_leI le_SUP_I)
1.73
1.74 -lemma INF_top: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
1.75 +lemma INF_top (*[simp]*): "(\<Sqinter>x\<in>A. \<top>) = \<top>"
1.76 by (cases "A = {}") (simp_all add: INF_empty)
1.77
1.78 -lemma SUP_bot: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
1.79 +lemma SUP_bot (*[simp]*): "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
1.80 by (cases "A = {}") (simp_all add: SUP_empty)
1.81
1.82 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.83 @@ -365,14 +365,6 @@
1.84 "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
1.85 by (simp add: SUP_empty)
1.86
1.87 -lemma INF_eq:
1.88 - "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
1.89 - by (simp add: INF_def image_def)
1.90 -
1.91 -lemma SUP_eq:
1.92 - "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
1.93 - by (simp add: SUP_def image_def)
1.94 -
1.95 lemma less_INF_D:
1.96 assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
1.97 proof -
1.98 @@ -391,14 +383,6 @@
1.99 finally show "f i < y" .
1.100 qed
1.101
1.102 -lemma INF_UNIV_range:
1.103 - "(\<Sqinter>x. f x) = \<Sqinter>range f"
1.104 - by (fact INF_def)
1.105 -
1.106 -lemma SUP_UNIV_range:
1.107 - "(\<Squnion>x. f x) = \<Squnion>range f"
1.108 - by (fact SUP_def)
1.109 -
1.110 lemma INF_UNIV_bool_expand:
1.111 "(\<Sqinter>b. A b) = A True \<sqinter> A False"
1.112 by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
1.113 @@ -509,23 +493,23 @@
1.114 "class.complete_linorder Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
1.115 by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
1.116
1.117 -lemma Inf_less_iff:
1.118 +lemma Inf_less_iff (*[simp]*):
1.119 "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
1.120 unfolding not_le [symmetric] le_Inf_iff by auto
1.121
1.122 -lemma INF_less_iff:
1.123 +lemma INF_less_iff (*[simp]*):
1.124 "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
1.125 unfolding INF_def Inf_less_iff by auto
1.126
1.127 -lemma less_Sup_iff:
1.128 +lemma less_Sup_iff (*[simp]*):
1.129 "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
1.130 unfolding not_le [symmetric] Sup_le_iff by auto
1.131
1.132 -lemma less_SUP_iff:
1.133 +lemma less_SUP_iff (*[simp]*):
1.134 "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
1.135 unfolding SUP_def less_Sup_iff by auto
1.136
1.137 -lemma Sup_eq_top_iff:
1.138 +lemma Sup_eq_top_iff (*[simp]*):
1.139 "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
1.140 proof
1.141 assume *: "\<Squnion>A = \<top>"
1.142 @@ -547,11 +531,11 @@
1.143 qed
1.144 qed
1.145
1.146 -lemma SUP_eq_top_iff:
1.147 +lemma SUP_eq_top_iff (*[simp]*):
1.148 "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
1.149 unfolding SUP_def Sup_eq_top_iff by auto
1.150
1.151 -lemma Inf_eq_bot_iff:
1.152 +lemma Inf_eq_bot_iff (*[simp]*):
1.153 "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
1.154 proof -
1.155 interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
1.156 @@ -559,7 +543,7 @@
1.157 from dual.Sup_eq_top_iff show ?thesis .
1.158 qed
1.159
1.160 -lemma INF_eq_bot_iff:
1.161 +lemma INF_eq_bot_iff (*[simp]*):
1.162 "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
1.163 unfolding INF_def Inf_eq_bot_iff by auto
1.164
1.165 @@ -687,9 +671,6 @@
1.166 lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
1.167 by (fact Inf_greatest)
1.168
1.169 -lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
1.170 - by (simp add: Inf_insert)
1.171 -
1.172 lemma Inter_empty: "\<Inter>{} = UNIV"
1.173 by (fact Inf_empty) (* already simp *)
1.174
1.175 @@ -746,34 +727,26 @@
1.176 [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
1.177 *} -- {* to avoid eta-contraction of body *}
1.178
1.179 -lemma INTER_eq_Inter_image:
1.180 - "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
1.181 - by (fact INF_def)
1.182 -
1.183 -lemma Inter_def:
1.184 - "\<Inter>S = (\<Inter>x\<in>S. x)"
1.185 - by (simp add: INTER_eq_Inter_image image_def)
1.186 -
1.187 -lemma INTER_def:
1.188 +lemma INTER_eq:
1.189 "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
1.190 - by (auto simp add: INTER_eq_Inter_image Inter_eq)
1.191 + by (auto simp add: INF_def)
1.192
1.193 lemma Inter_image_eq [simp]:
1.194 "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
1.195 by (rule sym) (fact INF_def)
1.196
1.197 lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
1.198 - by (unfold INTER_def) blast
1.199 + by (auto simp add: INF_def image_def)
1.200
1.201 lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
1.202 - by (unfold INTER_def) blast
1.203 + by (auto simp add: INF_def image_def)
1.204
1.205 lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a"
1.206 by auto
1.207
1.208 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.209 -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
1.210 - by (unfold INTER_def) blast
1.211 + by (auto simp add: INF_def image_def)
1.212
1.213 lemma INT_cong [cong]:
1.214 "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.215 @@ -792,7 +765,7 @@
1.216 by (fact le_INF_I)
1.217
1.218 lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV"
1.219 - by (fact INF_empty) (* already simp *)
1.220 + by (fact INF_empty)
1.221
1.222 lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
1.223 by (fact INF_absorb)
1.224 @@ -813,10 +786,6 @@
1.225 lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
1.226 by (fact INF_constant)
1.227
1.228 -lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
1.229 - -- {* Look: it has an \emph{existential} quantifier *}
1.230 - by (fact INF_eq)
1.231 -
1.232 lemma INTER_UNIV_conv [simp]:
1.233 "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
1.234 "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
1.235 @@ -875,9 +844,6 @@
1.236 lemma Union_least: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> C) \<Longrightarrow> \<Union>A \<subseteq> C"
1.237 by (fact Sup_least)
1.238
1.239 -lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
1.240 - by blast
1.241 -
1.242 lemma Union_empty [simp]: "\<Union>{} = {}"
1.243 by (fact Sup_empty)
1.244
1.245 @@ -950,24 +916,16 @@
1.246 [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
1.247 *} -- {* to avoid eta-contraction of body *}
1.248
1.249 -lemma UNION_eq_Union_image:
1.250 - "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
1.251 - by (fact SUP_def)
1.252 -
1.253 -lemma Union_def:
1.254 - "\<Union>S = (\<Union>x\<in>S. x)"
1.255 - by (simp add: UNION_eq_Union_image image_def)
1.256 -
1.257 -lemma UNION_def [no_atp]:
1.258 +lemma UNION_eq [no_atp]:
1.259 "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
1.260 - by (auto simp add: UNION_eq_Union_image Union_eq)
1.261 + by (auto simp add: SUP_def)
1.262
1.263 lemma Union_image_eq [simp]:
1.264 "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
1.265 - by (rule sym) (fact UNION_eq_Union_image)
1.266 + by (auto simp add: UNION_eq)
1.267
1.268 lemma UN_iff [simp]: "(b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)"
1.269 - by (unfold UNION_def) blast
1.270 + by (auto simp add: SUP_def image_def)
1.271
1.272 lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
1.273 -- {* The order of the premises presupposes that @{term A} is rigid;
1.274 @@ -975,7 +933,7 @@
1.275 by auto
1.276
1.277 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.278 - by (unfold UNION_def) blast
1.279 + by (auto simp add: SUP_def image_def)
1.280
1.281 lemma UN_cong [cong]:
1.282 "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.283 @@ -1001,21 +959,18 @@
1.284 by blast
1.285
1.286 lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
1.287 - by (fact SUP_empty) (* already simp *)
1.288 + by (fact SUP_empty)
1.289
1.290 lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
1.291 by (fact SUP_bot)
1.292
1.293 -lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
1.294 - by blast
1.295 -
1.296 lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
1.297 by (fact SUP_absorb)
1.298
1.299 lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
1.300 by (fact SUP_insert)
1.301
1.302 -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.303 +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.304 by (fact SUP_union)
1.305
1.306 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.307 @@ -1027,9 +982,6 @@
1.308 lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
1.309 by (fact SUP_constant)
1.310
1.311 -lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
1.312 - by (fact SUP_eq)
1.313 -
1.314 lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
1.315 by blast
1.316
1.317 @@ -1219,12 +1171,65 @@
1.318 lemmas (in complete_lattice) le_INFI = le_INF_I
1.319 lemmas (in complete_lattice) less_INFD = less_INF_D
1.320
1.321 +lemmas INFI_apply = INF_apply
1.322 +lemmas SUPR_apply = SUP_apply
1.323 +
1.324 +text {* Grep and put to news from here *}
1.325 +
1.326 +lemma (in complete_lattice) INF_eq:
1.327 + "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
1.328 + by (simp add: INF_def image_def)
1.329 +
1.330 +lemma (in complete_lattice) SUP_eq:
1.331 + "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
1.332 + by (simp add: SUP_def image_def)
1.333 +
1.334 lemma (in complete_lattice) INF_subset:
1.335 "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
1.336 by (rule INF_superset_mono) auto
1.337
1.338 -lemmas INFI_apply = INF_apply
1.339 -lemmas SUPR_apply = SUP_apply
1.340 +lemma (in complete_lattice) INF_UNIV_range:
1.341 + "(\<Sqinter>x. f x) = \<Sqinter>range f"
1.342 + by (fact INF_def)
1.343 +
1.344 +lemma (in complete_lattice) SUP_UNIV_range:
1.345 + "(\<Squnion>x. f x) = \<Squnion>range f"
1.346 + by (fact SUP_def)
1.347 +
1.348 +lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
1.349 + by (simp add: Inf_insert)
1.350 +
1.351 +lemma INTER_eq_Inter_image:
1.352 + "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
1.353 + by (fact INF_def)
1.354 +
1.355 +lemma Inter_def:
1.356 + "\<Inter>S = (\<Inter>x\<in>S. x)"
1.357 + by (simp add: INTER_eq_Inter_image image_def)
1.358 +
1.359 +lemmas INTER_def = INTER_eq
1.360 +lemmas UNION_def = UNION_eq
1.361 +
1.362 +lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
1.363 + by (fact INF_eq)
1.364 +
1.365 +lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
1.366 + by blast
1.367 +
1.368 +lemma UNION_eq_Union_image:
1.369 + "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
1.370 + by (fact SUP_def)
1.371 +
1.372 +lemma Union_def:
1.373 + "\<Union>S = (\<Union>x\<in>S. x)"
1.374 + by (simp add: UNION_eq_Union_image image_def)
1.375 +
1.376 +lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
1.377 + by blast
1.378 +
1.379 +lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
1.380 + by (fact SUP_eq)
1.381 +
1.382
1.383 text {* Finally *}
1.384
2.1 --- a/src/HOL/Lattices.thy Mon Aug 08 22:11:00 2011 +0200
2.2 +++ b/src/HOL/Lattices.thy Mon Aug 08 22:33:36 2011 +0200
2.3 @@ -177,10 +177,10 @@
2.4 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
2.5 by (fact inf.left_commute)
2.6
2.7 -lemma inf_idem: "x \<sqinter> x = x"
2.8 +lemma inf_idem (*[simp]*): "x \<sqinter> x = x"
2.9 by (fact inf.idem)
2.10
2.11 -lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
2.12 +lemma inf_left_idem (*[simp]*): "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
2.13 by (fact inf.left_idem)
2.14
2.15 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
2.16 @@ -216,10 +216,10 @@
2.17 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
2.18 by (fact sup.left_commute)
2.19
2.20 -lemma sup_idem: "x \<squnion> x = x"
2.21 +lemma sup_idem (*[simp]*): "x \<squnion> x = x"
2.22 by (fact sup.idem)
2.23
2.24 -lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
2.25 +lemma sup_left_idem (*[simp]*): "x \<squnion> (x \<squnion> y) = x \<squnion> y"
2.26 by (fact sup.left_idem)
2.27
2.28 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
2.29 @@ -240,10 +240,10 @@
2.30 by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
2.31 (unfold_locales, auto)
2.32
2.33 -lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
2.34 +lemma inf_sup_absorb (*[simp]*): "x \<sqinter> (x \<squnion> y) = x"
2.35 by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
2.36
2.37 -lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
2.38 +lemma sup_inf_absorb (*[simp]*): "x \<squnion> (x \<sqinter> y) = x"
2.39 by (blast intro: antisym sup_ge1 sup_least inf_le1)
2.40
2.41 lemmas inf_sup_aci = inf_aci sup_aci
2.42 @@ -436,11 +436,11 @@
2.43 by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
2.44 (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
2.45
2.46 -lemma compl_inf_bot:
2.47 +lemma compl_inf_bot (*[simp]*):
2.48 "- x \<sqinter> x = \<bottom>"
2.49 by (simp add: inf_commute inf_compl_bot)
2.50
2.51 -lemma compl_sup_top:
2.52 +lemma compl_sup_top (*[simp]*):
2.53 "- x \<squnion> x = \<top>"
2.54 by (simp add: sup_commute sup_compl_top)
2.55
2.56 @@ -522,7 +522,7 @@
2.57 then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
2.58 qed
2.59
2.60 -lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
2.61 +lemma compl_le_compl_iff (*[simp]*):
2.62 "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
2.63 by (auto dest: compl_mono)
2.64