merged
authorhaftmann
Sun Jul 17 20:23:39 2011 +0200 (2011-07-17)
changeset 4386958be172c6ca4
parent 43864 58a7b3fdc193
parent 43868 9684251c7ec1
child 43870 92129f505125
merged
     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 -
   2.101 -lemma INF_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> INFI A f = INFI A g"
   2.102 -  by (simp add: INFI_def cong: image_cong)
   2.103 +lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   2.104 +  by (simp add: INFI_def)
   2.105  
   2.106 -lemma le_SUPI: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
   2.107 -  by (auto simp add: SUPR_def intro: Sup_upper)
   2.108 +lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
   2.109 +  by (simp add: INFI_def Inf_insert)
   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 (fact INF_bool_eq)
   2.407  
   2.408 -lemma INT_bool_eq: "(\<Inter>b. A b) = (A True \<inter> A False)"
   2.409 -  by (auto intro: bool_induct)
   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 {} = {{}}"