further generalization from sets to complete lattices
authorhaftmann
Sun Jul 17 15:15:58 2011 +0200 (2011-07-17)
changeset 43865db18f4d0cc7d
parent 43855 01b13e9a1a7e
child 43866 8a50dc70cbff
further generalization from sets to complete lattices
NEWS
src/HOL/Complete_Lattice.thy
     1.1 --- a/NEWS	Sun Jul 17 08:45:06 2011 +0200
     1.2 +++ b/NEWS	Sun Jul 17 15:15:58 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 08:45:06 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 15:15:58 2011 +0200
     2.3 @@ -152,66 +152,74 @@
     2.4  context complete_lattice
     2.5  begin
     2.6  
     2.7 -lemma SUP_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> SUPR A f = SUPR A g"
     2.8 -  by (simp add: SUPR_def cong: image_cong)
     2.9 -
    2.10 -lemma INF_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> INFI A f = INFI A g"
    2.11 -  by (simp add: INFI_def cong: image_cong)
    2.12 +lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
    2.13 +  by (simp add: INFI_def)
    2.14  
    2.15 -lemma le_SUPI: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
    2.16 -  by (auto simp add: SUPR_def intro: Sup_upper)
    2.17 +lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
    2.18 +  by (simp add: INFI_def Inf_insert)
    2.19  
    2.20 -lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
    2.21 -  using le_SUPI[of i A M] by auto
    2.22 -
    2.23 -lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. M i) \<sqsubseteq> u"
    2.24 -  by (auto simp add: SUPR_def intro: Sup_least)
    2.25 -
    2.26 -lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> M i"
    2.27 +lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
    2.28    by (auto simp add: INFI_def intro: Inf_lower)
    2.29  
    2.30 -lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> u"
    2.31 -  using INF_leI[of i A M] by auto
    2.32 +lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
    2.33 +  using INF_leI [of i A f] by auto
    2.34  
    2.35 -lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. M i)"
    2.36 +lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
    2.37    by (auto simp add: INFI_def intro: Inf_greatest)
    2.38  
    2.39 -lemma SUP_le_iff: "(\<Squnion>i\<in>A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
    2.40 -  unfolding SUPR_def by (auto simp add: Sup_le_iff)
    2.41 +lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
    2.42 +  by (auto simp add: INFI_def le_Inf_iff)
    2.43  
    2.44 -lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
    2.45 -  unfolding INFI_def by (auto simp add: le_Inf_iff)
    2.46 -
    2.47 -lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. M) = M"
    2.48 +lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
    2.49    by (auto intro: antisym INF_leI le_INFI)
    2.50  
    2.51 -lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. M) = M"
    2.52 -  by (auto intro: antisym SUP_leI le_SUPI)
    2.53 +lemma INF_cong:
    2.54 +  "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.55 +  by (simp add: INFI_def image_def)
    2.56  
    2.57  lemma INF_mono:
    2.58    "(\<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.59    by (force intro!: Inf_mono simp: INFI_def)
    2.60  
    2.61 +lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
    2.62 +  by (intro INF_mono) auto
    2.63 +
    2.64 +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.65 +  by (iprover intro: INF_leI le_INFI order_trans antisym)
    2.66 +
    2.67 +lemma SUP_cong:
    2.68 +  "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.69 +  by (simp add: SUPR_def image_def)
    2.70 +
    2.71 +lemma le_SUPI: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    2.72 +  by (auto simp add: SUPR_def intro: Sup_upper)
    2.73 +
    2.74 +lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    2.75 +  using le_SUPI [of i A f] by auto
    2.76 +
    2.77 +lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
    2.78 +  by (auto simp add: SUPR_def intro: Sup_least)
    2.79 +
    2.80 +lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
    2.81 +  unfolding SUPR_def by (auto simp add: Sup_le_iff)
    2.82 +
    2.83 +lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
    2.84 +  by (auto intro: antisym SUP_leI le_SUPI)
    2.85 +
    2.86  lemma SUP_mono:
    2.87    "(\<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.88    by (force intro!: Sup_mono simp: SUPR_def)
    2.89  
    2.90 -lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
    2.91 -  by (intro INF_mono) auto
    2.92 -
    2.93  lemma SUP_subset:  "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
    2.94    by (intro SUP_mono) auto
    2.95  
    2.96 -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.97 -  by (iprover intro: INF_leI le_INFI order_trans antisym)
    2.98 -
    2.99  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.100    by (iprover intro: SUP_leI le_SUPI order_trans antisym)
   2.101  
   2.102 -lemma INFI_insert: "(\<Sqinter>x\<in>insert a A. B x) = B a \<sqinter> INFI A B"
   2.103 -  by (simp add: INFI_def Inf_insert)
   2.104 +lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
   2.105 +  by (simp add: SUPR_def)
   2.106  
   2.107 -lemma SUPR_insert: "(\<Squnion>x\<in>insert a A. B x) = B a \<squnion> SUPR A B"
   2.108 +lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   2.109    by (simp add: SUPR_def Sup_insert)
   2.110  
   2.111  end
   2.112 @@ -221,16 +229,16 @@
   2.113    shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   2.114    unfolding not_le [symmetric] le_Inf_iff by auto
   2.115  
   2.116 +lemma INF_less_iff:
   2.117 +  fixes a :: "'a::{complete_lattice,linorder}"
   2.118 +  shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   2.119 +  unfolding INFI_def Inf_less_iff by auto
   2.120 +
   2.121  lemma less_Sup_iff:
   2.122    fixes a :: "'a\<Colon>{complete_lattice,linorder}"
   2.123    shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   2.124    unfolding not_le [symmetric] Sup_le_iff by auto
   2.125  
   2.126 -lemma INF_less_iff:
   2.127 -  fixes a :: "'a::{complete_lattice,linorder}"
   2.128 -  shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   2.129 -  unfolding INFI_def Inf_less_iff by auto
   2.130 -
   2.131  lemma less_SUP_iff:
   2.132    fixes a :: "'a::{complete_lattice,linorder}"
   2.133    shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   2.134 @@ -474,13 +482,9 @@
   2.135    -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
   2.136    by (unfold INTER_def) blast
   2.137  
   2.138 -lemma (in complete_lattice) INFI_cong:
   2.139 -  "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.140 -  by (simp add: INFI_def image_def)
   2.141 -
   2.142  lemma INT_cong [cong]:
   2.143    "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.144 -  by (fact INFI_cong)
   2.145 +  by (fact INF_cong)
   2.146  
   2.147  lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
   2.148    by blast
   2.149 @@ -506,7 +510,7 @@
   2.150    shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
   2.151  proof -
   2.152    from assms obtain J where "I = insert k J" by blast
   2.153 -  then show ?thesis by (simp add: INFI_insert)
   2.154 +  then show ?thesis by (simp add: INF_insert)
   2.155  qed
   2.156  
   2.157  lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
   2.158 @@ -516,41 +520,74 @@
   2.159    by (fact le_INF_iff)
   2.160  
   2.161  lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
   2.162 -  by (fact INFI_insert)
   2.163 +  by (fact INF_insert)
   2.164 +
   2.165 +lemma (in complete_lattice) INF_union:
   2.166 +  "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
   2.167 +  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INFI INF_leI)
   2.168 +
   2.169 +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.170 +  by (fact INF_union)
   2.171 +
   2.172 +lemma INT_insert_distrib:
   2.173 +  "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   2.174 +  by blast
   2.175  
   2.176  -- {* continue generalization from here *}
   2.177  
   2.178 -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.179 -  by blast
   2.180 -
   2.181 -lemma INT_insert_distrib:
   2.182 -    "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   2.183 -  by blast
   2.184 +lemma (in complete_lattice) INF_constant:
   2.185 +  "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   2.186 +  by (simp add: INF_empty)
   2.187  
   2.188  lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
   2.189 -  by auto
   2.190 +  by (fact INF_constant)
   2.191 +
   2.192 +lemma (in complete_lattice) INF_eq:
   2.193 +  "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
   2.194 +  by (simp add: INFI_def image_def)
   2.195  
   2.196  lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
   2.197    -- {* Look: it has an \emph{existential} quantifier *}
   2.198 -  by blast
   2.199 +  by (fact INF_eq)
   2.200 +
   2.201 +lemma (in complete_lattice) INF_top_conv:
   2.202 + "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   2.203 + "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   2.204 +  by (auto simp add: INFI_def Inf_top_conv)
   2.205  
   2.206  lemma INTER_UNIV_conv [simp]:
   2.207   "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
   2.208   "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
   2.209 -  by blast+
   2.210 +  by (fact INF_top_conv)+
   2.211 +
   2.212 +lemma (in complete_lattice) INFI_UNIV_range:
   2.213 +  "(\<Sqinter>x\<in>UNIV. f x) = \<Sqinter>range f"
   2.214 +  by (simp add: INFI_def)
   2.215 +
   2.216 +lemma UNIV_bool [no_atp]: -- "FIXME move"
   2.217 +  "UNIV = {False, True}"
   2.218 +  by auto
   2.219  
   2.220 -lemma INT_bool_eq: "(\<Inter>b. A b) = (A True \<inter> A False)"
   2.221 -  by (auto intro: bool_induct)
   2.222 +lemma (in complete_lattice) INF_bool_eq:
   2.223 +  "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   2.224 +  by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
   2.225 +
   2.226 +lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
   2.227 +  by (fact INF_bool_eq)
   2.228 +
   2.229 +lemma (in complete_lattice) INF_anti_mono:
   2.230 +  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
   2.231 +  -- {* The last inclusion is POSITIVE! *}
   2.232 +  by (blast dest: subsetD)
   2.233 +
   2.234 +lemma INT_anti_mono:
   2.235 +  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
   2.236 +  -- {* The last inclusion is POSITIVE! *}
   2.237 +  by (blast dest: subsetD)
   2.238  
   2.239  lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
   2.240    by blast
   2.241  
   2.242 -lemma INT_anti_mono:
   2.243 -  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
   2.244 -    (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
   2.245 -  -- {* The last inclusion is POSITIVE! *}
   2.246 -  by (blast dest: subsetD)
   2.247 -
   2.248  lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)"
   2.249    by blast
   2.250