move legacy candiates to bottom; marked candidates for default simp rules
authorhaftmann
Mon Aug 08 22:33:36 2011 +0200 (2011-08-08)
changeset 44085a65e26f1427b
parent 44084 caac24afcadb
child 44086 c0847967a25a
move legacy candiates to bottom; marked candidates for default simp rules
src/HOL/Complete_Lattice.thy
src/HOL/Lattices.thy
     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