merged
authorhaftmann
Tue Aug 09 07:44:17 2011 +0200 (2011-08-09)
changeset 44086c0847967a25a
parent 44081 730f7cced3a6
parent 44085 a65e26f1427b
child 44087 8e491cb8841c
child 44103 cedaca00789f
merged
NEWS
     1.1 --- a/NEWS	Mon Aug 08 19:26:53 2011 -0700
     1.2 +++ b/NEWS	Tue Aug 09 07:44:17 2011 +0200
     1.3 @@ -68,6 +68,8 @@
     1.4  boolean algebras and complete linear orders.  Lemmas Inf_less_iff,
     1.5  less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
     1.6  Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
     1.7 +Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary and Sup_binary have
     1.8 +been discarded.
     1.9  More consistent and less misunderstandable names:
    1.10    INFI_def ~> INF_def
    1.11    SUPR_def ~> SUP_def
     2.1 --- a/src/HOL/Complete_Lattice.thy	Mon Aug 08 19:26:53 2011 -0700
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Tue Aug 09 07:44:17 2011 +0200
     2.3 @@ -126,16 +126,16 @@
     2.4  lemma le_SUP_I2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
     2.5    using le_SUP_I [of i A f] by auto
     2.6  
     2.7 -lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     2.8 +lemma le_Inf_iff (*[simp]*): "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     2.9    by (auto intro: Inf_greatest dest: Inf_lower)
    2.10  
    2.11 -lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
    2.12 +lemma le_INF_iff (*[simp]*): "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
    2.13    by (auto simp add: INF_def le_Inf_iff)
    2.14  
    2.15 -lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    2.16 +lemma Sup_le_iff (*[simp]*): "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    2.17    by (auto intro: Sup_least dest: Sup_upper)
    2.18  
    2.19 -lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
    2.20 +lemma SUP_le_iff (*[simp]*): "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
    2.21    by (auto simp add: SUP_def Sup_le_iff)
    2.22  
    2.23  lemma Inf_empty [simp]:
    2.24 @@ -160,22 +160,22 @@
    2.25    "\<Squnion>UNIV = \<top>"
    2.26    by (auto intro!: antisym Sup_upper)
    2.27  
    2.28 -lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    2.29 +lemma Inf_insert (*[simp]*): "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    2.30    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
    2.31  
    2.32  lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
    2.33    by (simp add: INF_def Inf_insert)
    2.34  
    2.35 -lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    2.36 +lemma Sup_insert (*[simp]*): "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    2.37    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
    2.38  
    2.39  lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
    2.40    by (simp add: SUP_def Sup_insert)
    2.41  
    2.42 -lemma INF_image: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
    2.43 +lemma INF_image (*[simp]*): "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
    2.44    by (simp add: INF_def image_image)
    2.45  
    2.46 -lemma SUP_image: "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
    2.47 +lemma SUP_image (*[simp]*): "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
    2.48    by (simp add: SUP_def image_image)
    2.49  
    2.50  lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
    2.51 @@ -184,22 +184,6 @@
    2.52  lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
    2.53    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
    2.54  
    2.55 -lemma Inf_singleton [simp]:
    2.56 -  "\<Sqinter>{a} = a"
    2.57 -  by (auto intro: antisym Inf_lower Inf_greatest)
    2.58 -
    2.59 -lemma Sup_singleton [simp]:
    2.60 -  "\<Squnion>{a} = a"
    2.61 -  by (auto intro: antisym Sup_upper Sup_least)
    2.62 -
    2.63 -lemma Inf_binary:
    2.64 -  "\<Sqinter>{a, b} = a \<sqinter> b"
    2.65 -  by (simp add: Inf_insert)
    2.66 -
    2.67 -lemma Sup_binary:
    2.68 -  "\<Squnion>{a, b} = a \<squnion> b"
    2.69 -  by (simp add: Sup_insert)
    2.70 -
    2.71  lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
    2.72    by (auto intro: Inf_greatest Inf_lower)
    2.73  
    2.74 @@ -298,7 +282,7 @@
    2.75    by (rule antisym) (auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono,
    2.76      rule SUP_leI, auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono)
    2.77  
    2.78 -lemma Inf_top_conv [no_atp]:
    2.79 +lemma Inf_top_conv (*[simp]*) [no_atp]:
    2.80    "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
    2.81    "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
    2.82  proof -
    2.83 @@ -306,7 +290,7 @@
    2.84    proof
    2.85      assume "\<forall>x\<in>A. x = \<top>"
    2.86      then have "A = {} \<or> A = {\<top>}" by auto
    2.87 -    then show "\<Sqinter>A = \<top>" by auto
    2.88 +    then show "\<Sqinter>A = \<top>" by (auto simp add: Inf_insert)
    2.89    next
    2.90      assume "\<Sqinter>A = \<top>"
    2.91      show "\<forall>x\<in>A. x = \<top>"
    2.92 @@ -320,12 +304,12 @@
    2.93    then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
    2.94  qed
    2.95  
    2.96 -lemma INF_top_conv:
    2.97 +lemma INF_top_conv (*[simp]*):
    2.98   "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
    2.99   "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   2.100    by (auto simp add: INF_def Inf_top_conv)
   2.101  
   2.102 -lemma Sup_bot_conv [no_atp]:
   2.103 +lemma Sup_bot_conv (*[simp]*) [no_atp]:
   2.104    "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
   2.105    "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
   2.106  proof -
   2.107 @@ -334,7 +318,7 @@
   2.108    from dual.Inf_top_conv show ?P and ?Q by simp_all
   2.109  qed
   2.110  
   2.111 -lemma SUP_bot_conv:
   2.112 +lemma SUP_bot_conv (*[simp]*):
   2.113   "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   2.114   "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   2.115    by (auto simp add: SUP_def Sup_bot_conv)
   2.116 @@ -345,10 +329,10 @@
   2.117  lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
   2.118    by (auto intro: antisym SUP_leI le_SUP_I)
   2.119  
   2.120 -lemma INF_top: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   2.121 +lemma INF_top (*[simp]*): "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   2.122    by (cases "A = {}") (simp_all add: INF_empty)
   2.123  
   2.124 -lemma SUP_bot: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
   2.125 +lemma SUP_bot (*[simp]*): "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
   2.126    by (cases "A = {}") (simp_all add: SUP_empty)
   2.127  
   2.128  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.129 @@ -381,14 +365,6 @@
   2.130    "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
   2.131    by (simp add: SUP_empty)
   2.132  
   2.133 -lemma INF_eq:
   2.134 -  "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
   2.135 -  by (simp add: INF_def image_def)
   2.136 -
   2.137 -lemma SUP_eq:
   2.138 -  "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
   2.139 -  by (simp add: SUP_def image_def)
   2.140 -
   2.141  lemma less_INF_D:
   2.142    assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
   2.143  proof -
   2.144 @@ -407,14 +383,6 @@
   2.145    finally show "f i < y" .
   2.146  qed
   2.147  
   2.148 -lemma INF_UNIV_range:
   2.149 -  "(\<Sqinter>x. f x) = \<Sqinter>range f"
   2.150 -  by (fact INF_def)
   2.151 -
   2.152 -lemma SUP_UNIV_range:
   2.153 -  "(\<Squnion>x. f x) = \<Squnion>range f"
   2.154 -  by (fact SUP_def)
   2.155 -
   2.156  lemma INF_UNIV_bool_expand:
   2.157    "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   2.158    by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
   2.159 @@ -450,7 +418,7 @@
   2.160    and prove @{text inf_Sup} and @{text sup_Inf} from that? *}
   2.161    fix a b c
   2.162    from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
   2.163 -  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary)
   2.164 +  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
   2.165  qed
   2.166  
   2.167  lemma Inf_sup:
   2.168 @@ -525,23 +493,23 @@
   2.169    "class.complete_linorder Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
   2.170    by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
   2.171  
   2.172 -lemma Inf_less_iff:
   2.173 +lemma Inf_less_iff (*[simp]*):
   2.174    "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   2.175    unfolding not_le [symmetric] le_Inf_iff by auto
   2.176  
   2.177 -lemma INF_less_iff:
   2.178 +lemma INF_less_iff (*[simp]*):
   2.179    "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   2.180    unfolding INF_def Inf_less_iff by auto
   2.181  
   2.182 -lemma less_Sup_iff:
   2.183 +lemma less_Sup_iff (*[simp]*):
   2.184    "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   2.185    unfolding not_le [symmetric] Sup_le_iff by auto
   2.186  
   2.187 -lemma less_SUP_iff:
   2.188 +lemma less_SUP_iff (*[simp]*):
   2.189    "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   2.190    unfolding SUP_def less_Sup_iff by auto
   2.191  
   2.192 -lemma Sup_eq_top_iff:
   2.193 +lemma Sup_eq_top_iff (*[simp]*):
   2.194    "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   2.195  proof
   2.196    assume *: "\<Squnion>A = \<top>"
   2.197 @@ -563,11 +531,11 @@
   2.198    qed
   2.199  qed
   2.200  
   2.201 -lemma SUP_eq_top_iff:
   2.202 +lemma SUP_eq_top_iff (*[simp]*):
   2.203    "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
   2.204    unfolding SUP_def Sup_eq_top_iff by auto
   2.205  
   2.206 -lemma Inf_eq_bot_iff:
   2.207 +lemma Inf_eq_bot_iff (*[simp]*):
   2.208    "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
   2.209  proof -
   2.210    interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
   2.211 @@ -575,7 +543,7 @@
   2.212    from dual.Sup_eq_top_iff show ?thesis .
   2.213  qed
   2.214  
   2.215 -lemma INF_eq_bot_iff:
   2.216 +lemma INF_eq_bot_iff (*[simp]*):
   2.217    "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   2.218    unfolding INF_def Inf_eq_bot_iff by auto
   2.219  
   2.220 @@ -703,9 +671,6 @@
   2.221  lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
   2.222    by (fact Inf_greatest)
   2.223  
   2.224 -lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
   2.225 -  by (fact Inf_binary [symmetric])
   2.226 -
   2.227  lemma Inter_empty: "\<Inter>{} = UNIV"
   2.228    by (fact Inf_empty) (* already simp *)
   2.229  
   2.230 @@ -762,34 +727,26 @@
   2.231    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
   2.232  *} -- {* to avoid eta-contraction of body *}
   2.233  
   2.234 -lemma INTER_eq_Inter_image:
   2.235 -  "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
   2.236 -  by (fact INF_def)
   2.237 -  
   2.238 -lemma Inter_def:
   2.239 -  "\<Inter>S = (\<Inter>x\<in>S. x)"
   2.240 -  by (simp add: INTER_eq_Inter_image image_def)
   2.241 -
   2.242 -lemma INTER_def:
   2.243 +lemma INTER_eq:
   2.244    "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
   2.245 -  by (auto simp add: INTER_eq_Inter_image Inter_eq)
   2.246 +  by (auto simp add: INF_def)
   2.247  
   2.248  lemma Inter_image_eq [simp]:
   2.249    "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   2.250    by (rule sym) (fact INF_def)
   2.251  
   2.252  lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
   2.253 -  by (unfold INTER_def) blast
   2.254 +  by (auto simp add: INF_def image_def)
   2.255  
   2.256  lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
   2.257 -  by (unfold INTER_def) blast
   2.258 +  by (auto simp add: INF_def image_def)
   2.259  
   2.260  lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a"
   2.261    by auto
   2.262  
   2.263  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.264    -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
   2.265 -  by (unfold INTER_def) blast
   2.266 +  by (auto simp add: INF_def image_def)
   2.267  
   2.268  lemma INT_cong [cong]:
   2.269    "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.270 @@ -808,7 +765,7 @@
   2.271    by (fact le_INF_I)
   2.272  
   2.273  lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV"
   2.274 -  by (fact INF_empty) (* already simp *)
   2.275 +  by (fact INF_empty)
   2.276  
   2.277  lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
   2.278    by (fact INF_absorb)
   2.279 @@ -829,10 +786,6 @@
   2.280  lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
   2.281    by (fact INF_constant)
   2.282  
   2.283 -lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
   2.284 -  -- {* Look: it has an \emph{existential} quantifier *}
   2.285 -  by (fact INF_eq)
   2.286 -
   2.287  lemma INTER_UNIV_conv [simp]:
   2.288   "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
   2.289   "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
   2.290 @@ -891,9 +844,6 @@
   2.291  lemma Union_least: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> C) \<Longrightarrow> \<Union>A \<subseteq> C"
   2.292    by (fact Sup_least)
   2.293  
   2.294 -lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
   2.295 -  by blast
   2.296 -
   2.297  lemma Union_empty [simp]: "\<Union>{} = {}"
   2.298    by (fact Sup_empty)
   2.299  
   2.300 @@ -966,24 +916,16 @@
   2.301    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
   2.302  *} -- {* to avoid eta-contraction of body *}
   2.303  
   2.304 -lemma UNION_eq_Union_image:
   2.305 -  "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
   2.306 -  by (fact SUP_def)
   2.307 -
   2.308 -lemma Union_def:
   2.309 -  "\<Union>S = (\<Union>x\<in>S. x)"
   2.310 -  by (simp add: UNION_eq_Union_image image_def)
   2.311 -
   2.312 -lemma UNION_def [no_atp]:
   2.313 +lemma UNION_eq [no_atp]:
   2.314    "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   2.315 -  by (auto simp add: UNION_eq_Union_image Union_eq)
   2.316 +  by (auto simp add: SUP_def)
   2.317    
   2.318  lemma Union_image_eq [simp]:
   2.319    "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   2.320 -  by (rule sym) (fact UNION_eq_Union_image)
   2.321 +  by (auto simp add: UNION_eq)
   2.322    
   2.323  lemma UN_iff [simp]: "(b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)"
   2.324 -  by (unfold UNION_def) blast
   2.325 +  by (auto simp add: SUP_def image_def)
   2.326  
   2.327  lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
   2.328    -- {* The order of the premises presupposes that @{term A} is rigid;
   2.329 @@ -991,7 +933,7 @@
   2.330    by auto
   2.331  
   2.332  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.333 -  by (unfold UNION_def) blast
   2.334 +  by (auto simp add: SUP_def image_def)
   2.335  
   2.336  lemma UN_cong [cong]:
   2.337    "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.338 @@ -1017,21 +959,18 @@
   2.339    by blast
   2.340  
   2.341  lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
   2.342 -  by (fact SUP_empty) (* already simp *)
   2.343 +  by (fact SUP_empty)
   2.344  
   2.345  lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
   2.346    by (fact SUP_bot)
   2.347  
   2.348 -lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
   2.349 -  by blast
   2.350 -
   2.351  lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
   2.352    by (fact SUP_absorb)
   2.353  
   2.354  lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
   2.355    by (fact SUP_insert)
   2.356  
   2.357 -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.358 +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.359    by (fact SUP_union)
   2.360  
   2.361  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.362 @@ -1043,9 +982,6 @@
   2.363  lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
   2.364    by (fact SUP_constant)
   2.365  
   2.366 -lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
   2.367 -  by (fact SUP_eq)
   2.368 -
   2.369  lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
   2.370    by blast
   2.371  
   2.372 @@ -1212,6 +1148,22 @@
   2.373  
   2.374  text {* Legacy names *}
   2.375  
   2.376 +lemma (in complete_lattice) Inf_singleton [simp]:
   2.377 +  "\<Sqinter>{a} = a"
   2.378 +  by (simp add: Inf_insert)
   2.379 +
   2.380 +lemma (in complete_lattice) Sup_singleton [simp]:
   2.381 +  "\<Squnion>{a} = a"
   2.382 +  by (simp add: Sup_insert)
   2.383 +
   2.384 +lemma (in complete_lattice) Inf_binary:
   2.385 +  "\<Sqinter>{a, b} = a \<sqinter> b"
   2.386 +  by (simp add: Inf_insert)
   2.387 +
   2.388 +lemma (in complete_lattice) Sup_binary:
   2.389 +  "\<Squnion>{a, b} = a \<squnion> b"
   2.390 +  by (simp add: Sup_insert)
   2.391 +
   2.392  lemmas (in complete_lattice) INFI_def = INF_def
   2.393  lemmas (in complete_lattice) SUPR_def = SUP_def
   2.394  lemmas (in complete_lattice) le_SUPI = le_SUP_I
   2.395 @@ -1219,12 +1171,65 @@
   2.396  lemmas (in complete_lattice) le_INFI = le_INF_I
   2.397  lemmas (in complete_lattice) less_INFD = less_INF_D
   2.398  
   2.399 +lemmas INFI_apply = INF_apply
   2.400 +lemmas SUPR_apply = SUP_apply
   2.401 +
   2.402 +text {* Grep and put to news from here *}
   2.403 +
   2.404 +lemma (in complete_lattice) INF_eq:
   2.405 +  "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
   2.406 +  by (simp add: INF_def image_def)
   2.407 +
   2.408 +lemma (in complete_lattice) SUP_eq:
   2.409 +  "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
   2.410 +  by (simp add: SUP_def image_def)
   2.411 +
   2.412  lemma (in complete_lattice) INF_subset:
   2.413    "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
   2.414    by (rule INF_superset_mono) auto
   2.415  
   2.416 -lemmas INFI_apply = INF_apply
   2.417 -lemmas SUPR_apply = SUP_apply
   2.418 +lemma (in complete_lattice) INF_UNIV_range:
   2.419 +  "(\<Sqinter>x. f x) = \<Sqinter>range f"
   2.420 +  by (fact INF_def)
   2.421 +
   2.422 +lemma (in complete_lattice) SUP_UNIV_range:
   2.423 +  "(\<Squnion>x. f x) = \<Squnion>range f"
   2.424 +  by (fact SUP_def)
   2.425 +
   2.426 +lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
   2.427 +  by (simp add: Inf_insert)
   2.428 +
   2.429 +lemma INTER_eq_Inter_image:
   2.430 +  "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
   2.431 +  by (fact INF_def)
   2.432 +  
   2.433 +lemma Inter_def:
   2.434 +  "\<Inter>S = (\<Inter>x\<in>S. x)"
   2.435 +  by (simp add: INTER_eq_Inter_image image_def)
   2.436 +
   2.437 +lemmas INTER_def = INTER_eq
   2.438 +lemmas UNION_def = UNION_eq
   2.439 +
   2.440 +lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
   2.441 +  by (fact INF_eq)
   2.442 +
   2.443 +lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
   2.444 +  by blast
   2.445 +
   2.446 +lemma UNION_eq_Union_image:
   2.447 +  "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
   2.448 +  by (fact SUP_def)
   2.449 +
   2.450 +lemma Union_def:
   2.451 +  "\<Union>S = (\<Union>x\<in>S. x)"
   2.452 +  by (simp add: UNION_eq_Union_image image_def)
   2.453 +
   2.454 +lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
   2.455 +  by blast
   2.456 +
   2.457 +lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
   2.458 +  by (fact SUP_eq)
   2.459 +
   2.460  
   2.461  text {* Finally *}
   2.462  
     3.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Mon Aug 08 19:26:53 2011 -0700
     3.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Tue Aug 09 07:44:17 2011 +0200
     3.3 @@ -591,7 +591,6 @@
     3.4    "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
     3.5    "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
     3.6    "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
     3.7 -  "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
     3.8    "UNIONS_0" > "Complete_Lattice.Union_empty"
     3.9    "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
    3.10    "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
    3.11 @@ -1598,7 +1597,6 @@
    3.12    "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
    3.13    "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
    3.14    "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
    3.15 -  "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
    3.16    "INTERS_0" > "Complete_Lattice.Inter_empty"
    3.17    "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
    3.18    "INSERT_UNION_EQ" > "Set.Un_insert_left"
     4.1 --- a/src/HOL/Lattices.thy	Mon Aug 08 19:26:53 2011 -0700
     4.2 +++ b/src/HOL/Lattices.thy	Tue Aug 09 07:44:17 2011 +0200
     4.3 @@ -177,10 +177,10 @@
     4.4  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
     4.5    by (fact inf.left_commute)
     4.6  
     4.7 -lemma inf_idem: "x \<sqinter> x = x"
     4.8 +lemma inf_idem (*[simp]*): "x \<sqinter> x = x"
     4.9    by (fact inf.idem)
    4.10  
    4.11 -lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    4.12 +lemma inf_left_idem (*[simp]*): "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    4.13    by (fact inf.left_idem)
    4.14  
    4.15  lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    4.16 @@ -216,10 +216,10 @@
    4.17  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    4.18    by (fact sup.left_commute)
    4.19  
    4.20 -lemma sup_idem: "x \<squnion> x = x"
    4.21 +lemma sup_idem (*[simp]*): "x \<squnion> x = x"
    4.22    by (fact sup.idem)
    4.23  
    4.24 -lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    4.25 +lemma sup_left_idem (*[simp]*): "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    4.26    by (fact sup.left_idem)
    4.27  
    4.28  lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    4.29 @@ -240,10 +240,10 @@
    4.30    by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
    4.31      (unfold_locales, auto)
    4.32  
    4.33 -lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
    4.34 +lemma inf_sup_absorb (*[simp]*): "x \<sqinter> (x \<squnion> y) = x"
    4.35    by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
    4.36  
    4.37 -lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
    4.38 +lemma sup_inf_absorb (*[simp]*): "x \<squnion> (x \<sqinter> y) = x"
    4.39    by (blast intro: antisym sup_ge1 sup_least inf_le1)
    4.40  
    4.41  lemmas inf_sup_aci = inf_aci sup_aci
    4.42 @@ -436,11 +436,11 @@
    4.43    by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    4.44      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    4.45  
    4.46 -lemma compl_inf_bot:
    4.47 +lemma compl_inf_bot (*[simp]*):
    4.48    "- x \<sqinter> x = \<bottom>"
    4.49    by (simp add: inf_commute inf_compl_bot)
    4.50  
    4.51 -lemma compl_sup_top:
    4.52 +lemma compl_sup_top (*[simp]*):
    4.53    "- x \<squnion> x = \<top>"
    4.54    by (simp add: sup_commute sup_compl_top)
    4.55  
    4.56 @@ -522,7 +522,7 @@
    4.57    then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
    4.58  qed
    4.59  
    4.60 -lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
    4.61 +lemma compl_le_compl_iff (*[simp]*):
    4.62    "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
    4.63    by (auto dest: compl_mono)
    4.64