src/HOL/Complete_Lattices.thy
changeset 56166 9a241bc276cd
parent 56076 e52fc7c37ed3
child 56212 3253aaf73a01
     1.1 --- a/src/HOL/Complete_Lattices.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 - (*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
     1.5 +(*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
     1.6  
     1.7  header {* Complete lattices *}
     1.8  
     1.9 @@ -20,10 +20,24 @@
    1.10  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.11    INF_def: "INFI A f = \<Sqinter>(f ` A)"
    1.12  
    1.13 -lemma INF_image [simp]: "INFI (f`A) g = INFI A (\<lambda>x. g (f x))"
    1.14 -  by (simp add: INF_def image_image)
    1.15 +lemma Inf_image_eq [simp]:
    1.16 +  "\<Sqinter>(f ` A) = INFI A f"
    1.17 +  by (simp add: INF_def)
    1.18 +
    1.19 +lemma INF_image [simp]:
    1.20 +  "INFI (f ` A) g = INFI A (g \<circ> f)"
    1.21 +  by (simp only: INF_def image_comp)
    1.22  
    1.23 -lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
    1.24 +lemma INF_identity_eq [simp]:
    1.25 +  "INFI A (\<lambda>x. x) = \<Sqinter>A"
    1.26 +  by (simp add: INF_def)
    1.27 +
    1.28 +lemma INF_id_eq [simp]:
    1.29 +  "INFI A id = \<Sqinter>A"
    1.30 +  by (simp add: id_def)
    1.31 +
    1.32 +lemma INF_cong:
    1.33 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
    1.34    by (simp add: INF_def image_def)
    1.35  
    1.36  end
    1.37 @@ -35,10 +49,24 @@
    1.38  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.39    SUP_def: "SUPR A f = \<Squnion>(f ` A)"
    1.40  
    1.41 -lemma SUP_image [simp]: "SUPR (f`A) g = SUPR A (%x. g (f x))"
    1.42 -  by (simp add: SUP_def image_image)
    1.43 +lemma Sup_image_eq [simp]:
    1.44 +  "\<Squnion>(f ` A) = SUPR A f"
    1.45 +  by (simp add: SUP_def)
    1.46 +
    1.47 +lemma SUP_image [simp]:
    1.48 +  "SUPR (f ` A) g = SUPR A (g \<circ> f)"
    1.49 +  by (simp only: SUP_def image_comp)
    1.50  
    1.51 -lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
    1.52 +lemma SUP_identity_eq [simp]:
    1.53 +  "SUPR A (\<lambda>x. x) = \<Squnion>A"
    1.54 +  by (simp add: SUP_def)
    1.55 +
    1.56 +lemma SUP_id_eq [simp]:
    1.57 +  "SUPR A id = \<Squnion>A"
    1.58 +  by (simp add: id_def)
    1.59 +
    1.60 +lemma SUP_cong:
    1.61 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
    1.62    by (simp add: SUP_def image_def)
    1.63  
    1.64  end
    1.65 @@ -112,10 +140,11 @@
    1.66  
    1.67  lemma INF_foundation_dual:
    1.68    "Sup.SUPR Inf = INFI"
    1.69 -  by (simp add: fun_eq_iff INF_def Sup.SUP_def)
    1.70 +  by (simp add: fun_eq_iff Sup.SUP_def)
    1.71  
    1.72  lemma SUP_foundation_dual:
    1.73 -  "Inf.INFI Sup = SUPR" by (simp add: fun_eq_iff SUP_def Inf.INF_def)
    1.74 +  "Inf.INFI Sup = SUPR"
    1.75 +  by (simp add: fun_eq_iff Inf.INF_def)
    1.76  
    1.77  lemma Sup_eqI:
    1.78    "(\<And>y. y \<in> A \<Longrightarrow> y \<le> x) \<Longrightarrow> (\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> \<Squnion>A = x"
    1.79 @@ -127,23 +156,23 @@
    1.80  
    1.81  lemma SUP_eqI:
    1.82    "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (\<Squnion>i\<in>A. f i) = x"
    1.83 -  unfolding SUP_def by (rule Sup_eqI) auto
    1.84 +  using Sup_eqI [of "f ` A" x] by auto
    1.85  
    1.86  lemma INF_eqI:
    1.87    "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (\<Sqinter>i\<in>A. f i) = x"
    1.88 -  unfolding INF_def by (rule Inf_eqI) auto
    1.89 +  using Inf_eqI [of "f ` A" x] by auto
    1.90  
    1.91  lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
    1.92 -  by (auto simp add: INF_def intro: Inf_lower)
    1.93 +  using Inf_lower [of _ "f ` A"] by simp
    1.94  
    1.95  lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
    1.96 -  by (auto simp add: INF_def intro: Inf_greatest)
    1.97 +  using Inf_greatest [of "f ` A"] by auto
    1.98  
    1.99  lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
   1.100 -  by (auto simp add: SUP_def intro: Sup_upper)
   1.101 +  using Sup_upper [of _ "f ` A"] by simp
   1.102  
   1.103  lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
   1.104 -  by (auto simp add: SUP_def intro: Sup_least)
   1.105 +  using Sup_least [of "f ` A"] by auto
   1.106  
   1.107  lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
   1.108    using Inf_lower [of u A] by auto
   1.109 @@ -161,25 +190,25 @@
   1.110    by (auto intro: Inf_greatest dest: Inf_lower)
   1.111  
   1.112  lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
   1.113 -  by (auto simp add: INF_def le_Inf_iff)
   1.114 +  using le_Inf_iff [of _ "f ` A"] by simp
   1.115  
   1.116  lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
   1.117    by (auto intro: Sup_least dest: Sup_upper)
   1.118  
   1.119  lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
   1.120 -  by (auto simp add: SUP_def Sup_le_iff)
   1.121 +  using Sup_le_iff [of "f ` A"] by simp
   1.122  
   1.123  lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   1.124    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   1.125  
   1.126 -lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
   1.127 -  by (simp add: INF_def)
   1.128 +lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
   1.129 +  unfolding INF_def Inf_insert by simp
   1.130  
   1.131  lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   1.132    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
   1.133  
   1.134 -lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   1.135 -  by (simp add: SUP_def)
   1.136 +lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   1.137 +  unfolding SUP_def Sup_insert by simp
   1.138  
   1.139  lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   1.140    by (simp add: INF_def)
   1.141 @@ -219,7 +248,7 @@
   1.142  
   1.143  lemma INF_mono:
   1.144    "(\<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.145 -  unfolding INF_def by (rule Inf_mono) fast
   1.146 +  using Inf_mono [of "g ` B" "f ` A"] by auto
   1.147  
   1.148  lemma Sup_mono:
   1.149    assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
   1.150 @@ -233,7 +262,7 @@
   1.151  
   1.152  lemma SUP_mono:
   1.153    "(\<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.154 -  unfolding SUP_def by (rule Sup_mono) fast
   1.155 +  using Sup_mono [of "f ` A" "g ` B"] by auto
   1.156  
   1.157  lemma INF_superset_mono:
   1.158    "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.159 @@ -267,13 +296,13 @@
   1.160  lemma SUPR_eq:
   1.161    assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
   1.162    assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
   1.163 -  shows "(SUP i:A. f i) = (SUP j:B. g j)"
   1.164 +  shows "(\<Squnion>i\<in>A. f i) = (\<Squnion>j\<in>B. g j)"
   1.165    by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
   1.166  
   1.167  lemma INFI_eq:
   1.168    assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
   1.169    assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
   1.170 -  shows "(INF i:A. f i) = (INF j:B. g j)"
   1.171 +  shows "(\<Sqinter>i\<in>A. f i) = (\<Sqinter>j\<in>B. g j)"
   1.172    by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
   1.173  
   1.174  lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
   1.175 @@ -329,9 +358,9 @@
   1.176  qed
   1.177  
   1.178  lemma INF_top_conv [simp]:
   1.179 - "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   1.180 - "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   1.181 -  by (auto simp add: INF_def)
   1.182 +  "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   1.183 +  "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   1.184 +  using Inf_top_conv [of "B ` A"] by simp_all
   1.185  
   1.186  lemma Sup_bot_conv [simp]:
   1.187    "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
   1.188 @@ -342,7 +371,7 @@
   1.189  lemma SUP_bot_conv [simp]:
   1.190   "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   1.191   "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   1.192 -  by (auto simp add: SUP_def)
   1.193 +  using Sup_bot_conv [of "B ` A"] by simp_all
   1.194  
   1.195  lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
   1.196    by (auto intro: antisym INF_lower INF_greatest)
   1.197 @@ -367,7 +396,7 @@
   1.198    shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
   1.199  proof -
   1.200    from assms obtain J where "I = insert k J" by blast
   1.201 -  then show ?thesis by (simp add: INF_insert)
   1.202 +  then show ?thesis by simp
   1.203  qed
   1.204  
   1.205  lemma SUP_absorb:
   1.206 @@ -375,7 +404,7 @@
   1.207    shows "A k \<squnion> (\<Squnion>i\<in>I. A i) = (\<Squnion>i\<in>I. A i)"
   1.208  proof -
   1.209    from assms obtain J where "I = insert k J" by blast
   1.210 -  then show ?thesis by (simp add: SUP_insert)
   1.211 +  then show ?thesis by simp
   1.212  qed
   1.213  
   1.214  lemma INF_constant:
   1.215 @@ -406,17 +435,17 @@
   1.216  
   1.217  lemma INF_UNIV_bool_expand:
   1.218    "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   1.219 -  by (simp add: UNIV_bool INF_insert inf_commute)
   1.220 +  by (simp add: UNIV_bool inf_commute)
   1.221  
   1.222  lemma SUP_UNIV_bool_expand:
   1.223    "(\<Squnion>b. A b) = A True \<squnion> A False"
   1.224 -  by (simp add: UNIV_bool SUP_insert sup_commute)
   1.225 +  by (simp add: UNIV_bool sup_commute)
   1.226  
   1.227  lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
   1.228    by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
   1.229  
   1.230  lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
   1.231 -  unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
   1.232 +  using Inf_le_Sup [of "f ` A"] by simp
   1.233  
   1.234  lemma SUP_eq_const:
   1.235    "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPR I f = x"
   1.236 @@ -443,11 +472,11 @@
   1.237  
   1.238  lemma sup_INF:
   1.239    "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   1.240 -  by (simp add: INF_def sup_Inf image_image)
   1.241 +  by (simp only: INF_def sup_Inf image_image)
   1.242  
   1.243  lemma inf_SUP:
   1.244    "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   1.245 -  by (simp add: SUP_def inf_Sup image_image)
   1.246 +  by (simp only: SUP_def inf_Sup image_image)
   1.247  
   1.248  lemma dual_complete_distrib_lattice:
   1.249    "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   1.250 @@ -529,17 +558,17 @@
   1.251  qed
   1.252  
   1.253  lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
   1.254 -  by (simp add: INF_def SUP_def uminus_Inf image_image)
   1.255 +  by (simp only: INF_def SUP_def uminus_Inf image_image)
   1.256  
   1.257  lemma uminus_Sup:
   1.258    "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
   1.259  proof -
   1.260 -  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_Inf)
   1.261 +  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_INF)
   1.262    then show ?thesis by simp
   1.263  qed
   1.264    
   1.265  lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
   1.266 -  by (simp add: INF_def SUP_def uminus_Sup image_image)
   1.267 +  by (simp only: INF_def SUP_def uminus_Sup image_image)
   1.268  
   1.269  end
   1.270  
   1.271 @@ -562,7 +591,7 @@
   1.272  
   1.273  lemma INF_less_iff:
   1.274    "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   1.275 -  unfolding INF_def Inf_less_iff by auto
   1.276 +  using Inf_less_iff [of "f ` A"] by simp
   1.277  
   1.278  lemma less_Sup_iff:
   1.279    "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   1.280 @@ -570,7 +599,7 @@
   1.281  
   1.282  lemma less_SUP_iff:
   1.283    "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   1.284 -  unfolding SUP_def less_Sup_iff by auto
   1.285 +  using less_Sup_iff [of _ "f ` A"] by simp
   1.286  
   1.287  lemma Sup_eq_top_iff [simp]:
   1.288    "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   1.289 @@ -596,7 +625,7 @@
   1.290  
   1.291  lemma SUP_eq_top_iff [simp]:
   1.292    "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
   1.293 -  unfolding SUP_def by auto
   1.294 +  using Sup_eq_top_iff [of "f ` A"] by simp
   1.295  
   1.296  lemma Inf_eq_bot_iff [simp]:
   1.297    "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
   1.298 @@ -605,18 +634,7 @@
   1.299  
   1.300  lemma INF_eq_bot_iff [simp]:
   1.301    "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   1.302 -  unfolding INF_def by auto
   1.303 -
   1.304 -lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
   1.305 -proof safe
   1.306 -  fix y assume "x \<le> \<Squnion>A" "y < x"
   1.307 -  then have "y < \<Squnion>A" by auto
   1.308 -  then show "\<exists>a\<in>A. y < a"
   1.309 -    unfolding less_Sup_iff .
   1.310 -qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
   1.311 -
   1.312 -lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
   1.313 -  unfolding le_Sup_iff SUP_def by simp
   1.314 +  using Inf_eq_bot_iff [of "f ` A"] by simp
   1.315  
   1.316  lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
   1.317  proof safe
   1.318 @@ -628,7 +646,18 @@
   1.319  
   1.320  lemma INF_le_iff:
   1.321    "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   1.322 -  unfolding Inf_le_iff INF_def by simp
   1.323 +  using Inf_le_iff [of "f ` A"] by simp
   1.324 +
   1.325 +lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
   1.326 +proof safe
   1.327 +  fix y assume "x \<le> \<Squnion>A" "y < x"
   1.328 +  then have "y < \<Squnion>A" by auto
   1.329 +  then show "\<exists>a\<in>A. y < a"
   1.330 +    unfolding less_Sup_iff .
   1.331 +qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
   1.332 +
   1.333 +lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
   1.334 +  using le_Sup_iff [of _ "f ` A"] by simp
   1.335  
   1.336  subclass complete_distrib_lattice
   1.337  proof
   1.338 @@ -704,14 +733,15 @@
   1.339  
   1.340  lemma INF_apply [simp]:
   1.341    "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   1.342 -  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def)
   1.343 +  using Inf_apply [of "f ` A"] by (simp add: comp_def)
   1.344  
   1.345  lemma SUP_apply [simp]:
   1.346    "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   1.347 -  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def)
   1.348 +  using Sup_apply [of "f ` A"] by (simp add: comp_def)
   1.349  
   1.350  instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
   1.351 -qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf image_image)
   1.352 +qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf fun_eq_iff image_image
   1.353 +  simp del: Inf_image_eq Sup_image_eq)
   1.354  
   1.355  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
   1.356  
   1.357 @@ -888,14 +918,14 @@
   1.358  
   1.359  lemma INTER_eq:
   1.360    "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
   1.361 -  by (auto simp add: INF_def)
   1.362 +  by (auto intro!: INF_eqI)
   1.363  
   1.364 -lemma Inter_image_eq [simp]:
   1.365 -  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   1.366 -  by (rule sym) (fact INF_def)
   1.367 +lemma Inter_image_eq:
   1.368 +  "\<Inter>(B ` A) = (\<Inter>x\<in>A. B x)"
   1.369 +  by (fact Inf_image_eq)
   1.370  
   1.371  lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
   1.372 -  by (auto simp add: INF_def image_def)
   1.373 +  using Inter_iff [of _ "B ` A"] by simp
   1.374  
   1.375  lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
   1.376    by (auto simp add: INF_def image_def)
   1.377 @@ -1077,7 +1107,7 @@
   1.378  
   1.379  lemma UNION_eq:
   1.380    "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   1.381 -  by (auto simp add: SUP_def)
   1.382 +  by (auto intro!: SUP_eqI)
   1.383  
   1.384  lemma bind_UNION [code]:
   1.385    "Set.bind A f = UNION A f"
   1.386 @@ -1087,12 +1117,12 @@
   1.387    "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
   1.388    by (simp add: bind_UNION)
   1.389  
   1.390 -lemma Union_image_eq [simp]:
   1.391 +lemma Union_image_eq:
   1.392    "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   1.393 -  by (rule sym) (fact SUP_def)
   1.394 +  by (fact Sup_image_eq)
   1.395  
   1.396  lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
   1.397 -  by (auto simp add: SUP_def image_def)
   1.398 +  using Union_iff [of _ "B ` A"] by simp
   1.399  
   1.400  lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
   1.401    -- {* The order of the premises presupposes that @{term A} is rigid;
   1.402 @@ -1214,13 +1244,13 @@
   1.403  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.404    by (rule sym) (rule SUP_sup_distrib)
   1.405  
   1.406 -lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"
   1.407 -  by (simp only: INT_Int_distrib INF_def)
   1.408 +lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)" -- {* FIXME drop *}
   1.409 +  by (simp add: INT_Int_distrib)
   1.410  
   1.411 -lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"
   1.412 +lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" -- {* FIXME drop *}
   1.413    -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
   1.414    -- {* Union of a family of unions *}
   1.415 -  by (simp only: UN_Un_distrib SUP_def)
   1.416 +  by (simp add: UN_Un_distrib)
   1.417  
   1.418  lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
   1.419    by (fact sup_INF)