1.1 --- a/NEWS Sun Jul 17 14:21:19 2011 +0200
1.2 +++ b/NEWS Sun Jul 17 20:23:39 2011 +0200
1.3 @@ -63,6 +63,11 @@
1.4 * Classes bot and top require underlying partial order rather than preorder:
1.5 uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
1.6
1.7 +* Class 'complete_lattice': generalized a couple of lemmas from sets;
1.8 +generalized theorems INF_cong and SUP_cong. More consistent names: TBD.
1.9 +
1.10 +INCOMPATIBILITY.
1.11 +
1.12 * Archimedian_Field.thy:
1.13 floor now is defined as parameter of a separate type class floor_ceiling.
1.14
2.1 --- a/src/HOL/Complete_Lattice.thy Sun Jul 17 14:21:19 2011 +0200
2.2 +++ b/src/HOL/Complete_Lattice.thy Sun Jul 17 20:23:39 2011 +0200
2.3 @@ -33,7 +33,7 @@
2.4 begin
2.5
2.6 lemma dual_complete_lattice:
2.7 - "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
2.8 + "class.complete_lattice Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
2.9 by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
2.10 (unfold_locales, (fact bot_least top_greatest
2.11 Sup_upper Sup_least Inf_lower Inf_greatest)+)
2.12 @@ -109,10 +109,79 @@
2.13 qed
2.14
2.15 lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
2.16 - using Sup_upper[of u A] by auto
2.17 + using Sup_upper [of u A] by auto
2.18
2.19 lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
2.20 - using Inf_lower[of u A] by auto
2.21 + using Inf_lower [of u A] by auto
2.22 +
2.23 +lemma Inf_less_eq:
2.24 + assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
2.25 + and "A \<noteq> {}"
2.26 + shows "\<Sqinter>A \<sqsubseteq> u"
2.27 +proof -
2.28 + from `A \<noteq> {}` obtain v where "v \<in> A" by blast
2.29 + moreover with assms have "v \<sqsubseteq> u" by blast
2.30 + ultimately show ?thesis by (rule Inf_lower2)
2.31 +qed
2.32 +
2.33 +lemma less_eq_Sup:
2.34 + assumes "\<And>v. v \<in> A \<Longrightarrow> u \<sqsubseteq> v"
2.35 + and "A \<noteq> {}"
2.36 + shows "u \<sqsubseteq> \<Squnion>A"
2.37 +proof -
2.38 + from `A \<noteq> {}` obtain v where "v \<in> A" by blast
2.39 + moreover with assms have "u \<sqsubseteq> v" by blast
2.40 + ultimately show ?thesis by (rule Sup_upper2)
2.41 +qed
2.42 +
2.43 +lemma Inf_inter_less_eq: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
2.44 + by (auto intro: Inf_greatest Inf_lower)
2.45 +
2.46 +lemma Sup_inter_greater_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
2.47 + by (auto intro: Sup_least Sup_upper)
2.48 +
2.49 +lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
2.50 + by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
2.51 +
2.52 +lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
2.53 + by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
2.54 +
2.55 +lemma Inf_top_conv [no_atp]:
2.56 + "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
2.57 + "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
2.58 +proof -
2.59 + show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
2.60 + proof
2.61 + assume "\<forall>x\<in>A. x = \<top>"
2.62 + then have "A = {} \<or> A = {\<top>}" by auto
2.63 + then show "\<Sqinter>A = \<top>" by auto
2.64 + next
2.65 + assume "\<Sqinter>A = \<top>"
2.66 + show "\<forall>x\<in>A. x = \<top>"
2.67 + proof (rule ccontr)
2.68 + assume "\<not> (\<forall>x\<in>A. x = \<top>)"
2.69 + then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
2.70 + then obtain B where "A = insert x B" by blast
2.71 + with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
2.72 + qed
2.73 + qed
2.74 + then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
2.75 +qed
2.76 +
2.77 +lemma Sup_bot_conv [no_atp]:
2.78 + "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
2.79 + "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
2.80 +proof -
2.81 + interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
2.82 + by (fact dual_complete_lattice)
2.83 + from dual.Inf_top_conv show ?P and ?Q by simp_all
2.84 +qed
2.85 +
2.86 +lemma Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
2.87 + by (auto intro: Inf_greatest Inf_lower)
2.88 +
2.89 +lemma Sup_anti_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
2.90 + by (auto intro: Sup_least Sup_upper)
2.91
2.92 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
2.93 "INFI A f = \<Sqinter> (f ` A)"
2.94 @@ -152,66 +221,116 @@
2.95 context complete_lattice
2.96 begin
2.97
2.98 -lemma SUP_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> SUPR A f = SUPR A g"
2.99 - by (simp add: SUPR_def cong: image_cong)
2.100 +lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
2.101 + by (simp add: INFI_def)
2.102
2.103 -lemma INF_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> INFI A f = INFI A g"
2.104 - by (simp add: INFI_def cong: image_cong)
2.105 +lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
2.106 + by (simp add: INFI_def Inf_insert)
2.107
2.108 -lemma le_SUPI: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
2.109 - by (auto simp add: SUPR_def intro: Sup_upper)
2.110 -
2.111 -lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
2.112 - using le_SUPI[of i A M] by auto
2.113 -
2.114 -lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. M i) \<sqsubseteq> u"
2.115 - by (auto simp add: SUPR_def intro: Sup_least)
2.116 -
2.117 -lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> M i"
2.118 +lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
2.119 by (auto simp add: INFI_def intro: Inf_lower)
2.120
2.121 -lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> u"
2.122 - using INF_leI[of i A M] by auto
2.123 +lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
2.124 + using INF_leI [of i A f] by auto
2.125
2.126 -lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. M i)"
2.127 +lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
2.128 by (auto simp add: INFI_def intro: Inf_greatest)
2.129
2.130 -lemma SUP_le_iff: "(\<Squnion>i\<in>A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
2.131 - unfolding SUPR_def by (auto simp add: Sup_le_iff)
2.132 +lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
2.133 + by (auto simp add: INFI_def le_Inf_iff)
2.134
2.135 -lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
2.136 - unfolding INFI_def by (auto simp add: le_Inf_iff)
2.137 -
2.138 -lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. M) = M"
2.139 +lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
2.140 by (auto intro: antisym INF_leI le_INFI)
2.141
2.142 -lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. M) = M"
2.143 - by (auto intro: antisym SUP_leI le_SUPI)
2.144 +lemma INF_cong:
2.145 + "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.146 + by (simp add: INFI_def image_def)
2.147
2.148 lemma INF_mono:
2.149 "(\<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.150 by (force intro!: Inf_mono simp: INFI_def)
2.151
2.152 +lemma INF_subset: "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
2.153 + by (intro INF_mono) auto
2.154 +
2.155 +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.156 + by (iprover intro: INF_leI le_INFI order_trans antisym)
2.157 +
2.158 +lemma (in complete_lattice) INFI_empty:
2.159 + "(\<Sqinter>x\<in>{}. B x) = \<top>"
2.160 + by (simp add: INFI_def)
2.161 +
2.162 +lemma (in complete_lattice) INFI_absorb:
2.163 + assumes "k \<in> I"
2.164 + shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
2.165 +proof -
2.166 + from assms obtain J where "I = insert k J" by blast
2.167 + then show ?thesis by (simp add: INF_insert)
2.168 +qed
2.169 +
2.170 +lemma (in complete_lattice) INF_union:
2.171 + "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
2.172 + by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INFI INF_leI)
2.173 +
2.174 +lemma (in complete_lattice) INF_constant:
2.175 + "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
2.176 + by (simp add: INF_empty)
2.177 +
2.178 +lemma (in complete_lattice) INF_eq:
2.179 + "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
2.180 + by (simp add: INFI_def image_def)
2.181 +
2.182 +lemma (in complete_lattice) INF_top_conv:
2.183 + "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
2.184 + "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
2.185 + by (auto simp add: INFI_def Inf_top_conv)
2.186 +
2.187 +lemma (in complete_lattice) INFI_UNIV_range:
2.188 + "(\<Sqinter>x\<in>UNIV. f x) = \<Sqinter>range f"
2.189 + by (simp add: INFI_def)
2.190 +
2.191 +lemma (in complete_lattice) INF_bool_eq:
2.192 + "(\<Sqinter>b. A b) = A True \<sqinter> A False"
2.193 + by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
2.194 +
2.195 +lemma (in complete_lattice) INF_anti_mono:
2.196 + "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>B. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
2.197 + -- {* The last inclusion is POSITIVE! *}
2.198 + by (blast intro: INF_mono dest: subsetD)
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: SUPR_def image_def)
2.203 +
2.204 +lemma le_SUPI: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
2.205 + by (auto simp add: SUPR_def intro: Sup_upper)
2.206 +
2.207 +lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
2.208 + using le_SUPI [of i A f] by auto
2.209 +
2.210 +lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
2.211 + by (auto simp add: SUPR_def intro: Sup_least)
2.212 +
2.213 +lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
2.214 + unfolding SUPR_def by (auto simp add: Sup_le_iff)
2.215 +
2.216 +lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
2.217 + by (auto intro: antisym SUP_leI le_SUPI)
2.218 +
2.219 lemma SUP_mono:
2.220 "(\<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.221 by (force intro!: Sup_mono simp: SUPR_def)
2.222
2.223 -lemma INF_subset: "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
2.224 - by (intro INF_mono) auto
2.225 -
2.226 lemma SUP_subset: "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
2.227 by (intro SUP_mono) auto
2.228
2.229 -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.230 - by (iprover intro: INF_leI le_INFI order_trans antisym)
2.231 -
2.232 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.233 by (iprover intro: SUP_leI le_SUPI order_trans antisym)
2.234
2.235 -lemma INFI_insert: "(\<Sqinter>x\<in>insert a A. B x) = B a \<sqinter> INFI A B"
2.236 - by (simp add: INFI_def Inf_insert)
2.237 +lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
2.238 + by (simp add: SUPR_def)
2.239
2.240 -lemma SUPR_insert: "(\<Squnion>x\<in>insert a A. B x) = B a \<squnion> SUPR A B"
2.241 +lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
2.242 by (simp add: SUPR_def Sup_insert)
2.243
2.244 end
2.245 @@ -221,16 +340,16 @@
2.246 shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
2.247 unfolding not_le [symmetric] le_Inf_iff by auto
2.248
2.249 +lemma INF_less_iff:
2.250 + fixes a :: "'a::{complete_lattice,linorder}"
2.251 + shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
2.252 + unfolding INFI_def Inf_less_iff by auto
2.253 +
2.254 lemma less_Sup_iff:
2.255 fixes a :: "'a\<Colon>{complete_lattice,linorder}"
2.256 shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
2.257 unfolding not_le [symmetric] Sup_le_iff by auto
2.258
2.259 -lemma INF_less_iff:
2.260 - fixes a :: "'a::{complete_lattice,linorder}"
2.261 - shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
2.262 - unfolding INFI_def Inf_less_iff by auto
2.263 -
2.264 lemma less_SUP_iff:
2.265 fixes a :: "'a::{complete_lattice,linorder}"
2.266 shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
2.267 @@ -343,16 +462,6 @@
2.268 lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
2.269 by (fact Inf_lower)
2.270
2.271 -lemma (in complete_lattice) Inf_less_eq:
2.272 - assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
2.273 - and "A \<noteq> {}"
2.274 - shows "\<Sqinter>A \<sqsubseteq> u"
2.275 -proof -
2.276 - from `A \<noteq> {}` obtain v where "v \<in> A" by blast
2.277 - moreover with assms have "v \<sqsubseteq> u" by blast
2.278 - ultimately show ?thesis by (rule Inf_lower2)
2.279 -qed
2.280 -
2.281 lemma Inter_subset:
2.282 "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
2.283 by (fact Inf_less_eq)
2.284 @@ -372,48 +481,17 @@
2.285 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
2.286 by (fact Inf_insert)
2.287
2.288 -lemma (in complete_lattice) Inf_inter_less: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
2.289 - by (auto intro: Inf_greatest Inf_lower)
2.290 -
2.291 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
2.292 - by (fact Inf_inter_less)
2.293 -
2.294 -lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
2.295 - by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
2.296 + by (fact Inf_inter_less_eq)
2.297
2.298 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
2.299 by (fact Inf_union_distrib)
2.300
2.301 -lemma (in complete_lattice) Inf_top_conv [no_atp]:
2.302 - "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
2.303 - "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
2.304 -proof -
2.305 - show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
2.306 - proof
2.307 - assume "\<forall>x\<in>A. x = \<top>"
2.308 - then have "A = {} \<or> A = {\<top>}" by auto
2.309 - then show "\<Sqinter>A = \<top>" by auto
2.310 - next
2.311 - assume "\<Sqinter>A = \<top>"
2.312 - show "\<forall>x\<in>A. x = \<top>"
2.313 - proof (rule ccontr)
2.314 - assume "\<not> (\<forall>x\<in>A. x = \<top>)"
2.315 - then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
2.316 - then obtain B where "A = insert x B" by blast
2.317 - with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
2.318 - qed
2.319 - qed
2.320 - then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
2.321 -qed
2.322 -
2.323 -lemma Inter_UNIV_conv [simp,no_atp]:
2.324 +lemma Inter_UNIV_conv [simp, no_atp]:
2.325 "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
2.326 "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
2.327 by (fact Inf_top_conv)+
2.328
2.329 -lemma (in complete_lattice) Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
2.330 - by (auto intro: Inf_greatest Inf_lower)
2.331 -
2.332 lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
2.333 by (fact Inf_anti_mono)
2.334
2.335 @@ -474,13 +552,9 @@
2.336 -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
2.337 by (unfold INTER_def) blast
2.338
2.339 -lemma (in complete_lattice) INFI_cong:
2.340 - "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.341 - by (simp add: INFI_def image_def)
2.342 -
2.343 lemma INT_cong [cong]:
2.344 "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.345 - by (fact INFI_cong)
2.346 + by (fact INF_cong)
2.347
2.348 lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
2.349 by blast
2.350 @@ -494,21 +568,9 @@
2.351 lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
2.352 by (fact le_INFI)
2.353
2.354 -lemma (in complete_lattice) INFI_empty:
2.355 - "(\<Sqinter>x\<in>{}. B x) = \<top>"
2.356 - by (simp add: INFI_def)
2.357 -
2.358 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
2.359 by (fact INFI_empty)
2.360
2.361 -lemma (in complete_lattice) INFI_absorb:
2.362 - assumes "k \<in> I"
2.363 - shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
2.364 -proof -
2.365 - from assms obtain J where "I = insert k J" by blast
2.366 - then show ?thesis by (simp add: INFI_insert)
2.367 -qed
2.368 -
2.369 lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
2.370 by (fact INFI_absorb)
2.371
2.372 @@ -516,41 +578,38 @@
2.373 by (fact le_INF_iff)
2.374
2.375 lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
2.376 - by (fact INFI_insert)
2.377 -
2.378 --- {* continue generalization from here *}
2.379 + by (fact INF_insert)
2.380
2.381 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.382 - by blast
2.383 + by (fact INF_union)
2.384
2.385 lemma INT_insert_distrib:
2.386 - "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
2.387 + "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
2.388 by blast
2.389
2.390 lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
2.391 - by auto
2.392 + by (fact INF_constant)
2.393
2.394 lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
2.395 -- {* Look: it has an \emph{existential} quantifier *}
2.396 - by blast
2.397 + by (fact INF_eq)
2.398
2.399 lemma INTER_UNIV_conv [simp]:
2.400 "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
2.401 "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
2.402 - by blast+
2.403 + by (fact INF_top_conv)+
2.404
2.405 -lemma INT_bool_eq: "(\<Inter>b. A b) = (A True \<inter> A False)"
2.406 - by (auto intro: bool_induct)
2.407 +lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
2.408 + by (fact INF_bool_eq)
2.409 +
2.410 +lemma INT_anti_mono:
2.411 + "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>B. g x)"
2.412 + -- {* The last inclusion is POSITIVE! *}
2.413 + by (fact INF_anti_mono)
2.414
2.415 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
2.416 by blast
2.417
2.418 -lemma INT_anti_mono:
2.419 - "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
2.420 - (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
2.421 - -- {* The last inclusion is POSITIVE! *}
2.422 - by (blast dest: subsetD)
2.423 -
2.424 lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)"
2.425 by blast
2.426
3.1 --- a/src/HOL/Finite_Set.thy Sun Jul 17 14:21:19 2011 +0200
3.2 +++ b/src/HOL/Finite_Set.thy Sun Jul 17 20:23:39 2011 +0200
3.3 @@ -477,20 +477,14 @@
3.4 lemma finite [simp]: "finite (A \<Colon> 'a set)"
3.5 by (rule subset_UNIV finite_UNIV finite_subset)+
3.6
3.7 -lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
3.8 +lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True"
3.9 by simp
3.10
3.11 end
3.12
3.13 -lemma UNIV_unit [no_atp]:
3.14 - "UNIV = {()}" by auto
3.15 -
3.16 instance unit :: finite proof
3.17 qed (simp add: UNIV_unit)
3.18
3.19 -lemma UNIV_bool [no_atp]:
3.20 - "UNIV = {False, True}" by auto
3.21 -
3.22 instance bool :: finite proof
3.23 qed (simp add: UNIV_bool)
3.24
4.1 --- a/src/HOL/Product_Type.thy Sun Jul 17 14:21:19 2011 +0200
4.2 +++ b/src/HOL/Product_Type.thy Sun Jul 17 20:23:39 2011 +0200
4.3 @@ -84,9 +84,12 @@
4.4 f} rather than by @{term [source] "%u. f ()"}.
4.5 *}
4.6
4.7 -lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
4.8 +lemma unit_abs_eta_conv [simp, no_atp]: "(%u::unit. f ()) = f"
4.9 by (rule ext) simp
4.10
4.11 +lemma UNIV_unit [no_atp]:
4.12 + "UNIV = {()}" by auto
4.13 +
4.14 instantiation unit :: default
4.15 begin
4.16
5.1 --- a/src/HOL/Set.thy Sun Jul 17 14:21:19 2011 +0200
5.2 +++ b/src/HOL/Set.thy Sun Jul 17 20:23:39 2011 +0200
5.3 @@ -1487,6 +1487,9 @@
5.4 lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
5.5 by (auto intro: bool_contrapos)
5.6
5.7 +lemma UNIV_bool [no_atp]: "UNIV = {False, True}"
5.8 + by (auto intro: bool_induct)
5.9 +
5.10 text {* \medskip @{text Pow} *}
5.11
5.12 lemma Pow_empty [simp]: "Pow {} = {{}}"