src/HOL/Library/Countable_Complete_Lattices.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 69313 b021008c5397 permissions -rw-r--r--
improved code equations taken over from AFP
```     1 (*  Title:      HOL/Library/Countable_Complete_Lattices.thy
```
```     2     Author:     Johannes Hölzl
```
```     3 *)
```
```     4
```
```     5 section \<open>Countable Complete Lattices\<close>
```
```     6
```
```     7 theory Countable_Complete_Lattices
```
```     8   imports Main Countable_Set
```
```     9 begin
```
```    10
```
```    11 lemma UNIV_nat_eq: "UNIV = insert 0 (range Suc)"
```
```    12   by (metis UNIV_eq_I nat.nchotomy insertCI rangeI)
```
```    13
```
```    14 class countable_complete_lattice = lattice + Inf + Sup + bot + top +
```
```    15   assumes ccInf_lower: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> Inf A \<le> x"
```
```    16   assumes ccInf_greatest: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf A"
```
```    17   assumes ccSup_upper: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> Sup A"
```
```    18   assumes ccSup_least: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z"
```
```    19   assumes ccInf_empty [simp]: "Inf {} = top"
```
```    20   assumes ccSup_empty [simp]: "Sup {} = bot"
```
```    21 begin
```
```    22
```
```    23 subclass bounded_lattice
```
```    24 proof
```
```    25   fix a
```
```    26   show "bot \<le> a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric])
```
```    27   show "a \<le> top" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric])
```
```    28 qed
```
```    29
```
```    30 lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (INF i \<in> A. f i) \<le> f i"
```
```    31   using ccInf_lower [of "f ` A"] by simp
```
```    32
```
```    33 lemma ccINF_greatest: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (INF i \<in> A. f i)"
```
```    34   using ccInf_greatest [of "f ` A"] by auto
```
```    35
```
```    36 lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (SUP i \<in> A. f i)"
```
```    37   using ccSup_upper [of "f ` A"] by simp
```
```    38
```
```    39 lemma ccSUP_least: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (SUP i \<in> A. f i) \<le> u"
```
```    40   using ccSup_least [of "f ` A"] by auto
```
```    41
```
```    42 lemma ccInf_lower2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> Inf A \<le> v"
```
```    43   using ccInf_lower [of A u] by auto
```
```    44
```
```    45 lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (INF i \<in> A. f i) \<le> u"
```
```    46   using ccINF_lower [of A i f] by auto
```
```    47
```
```    48 lemma ccSup_upper2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> Sup A"
```
```    49   using ccSup_upper [of A u] by auto
```
```    50
```
```    51 lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (SUP i \<in> A. f i)"
```
```    52   using ccSUP_upper [of A i f] by auto
```
```    53
```
```    54 lemma le_ccInf_iff: "countable A \<Longrightarrow> b \<le> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)"
```
```    55   by (auto intro: ccInf_greatest dest: ccInf_lower)
```
```    56
```
```    57 lemma le_ccINF_iff: "countable A \<Longrightarrow> u \<le> (INF i \<in> A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
```
```    58   using le_ccInf_iff [of "f ` A"] by simp
```
```    59
```
```    60 lemma ccSup_le_iff: "countable A \<Longrightarrow> Sup A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)"
```
```    61   by (auto intro: ccSup_least dest: ccSup_upper)
```
```    62
```
```    63 lemma ccSUP_le_iff: "countable A \<Longrightarrow> (SUP i \<in> A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
```
```    64   using ccSup_le_iff [of "f ` A"] by simp
```
```    65
```
```    66 lemma ccInf_insert [simp]: "countable A \<Longrightarrow> Inf (insert a A) = inf a (Inf A)"
```
```    67   by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower)
```
```    68
```
```    69 lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x\<in>insert a A. f x) = inf (f a) (Inf (f ` A))"
```
```    70   unfolding image_insert by simp
```
```    71
```
```    72 lemma ccSup_insert [simp]: "countable A \<Longrightarrow> Sup (insert a A) = sup a (Sup A)"
```
```    73   by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper)
```
```    74
```
```    75 lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x\<in>insert a A. f x) = sup (f a) (Sup (f ` A))"
```
```    76   unfolding image_insert by simp
```
```    77
```
```    78 lemma ccINF_empty [simp]: "(INF x\<in>{}. f x) = top"
```
```    79   unfolding image_empty by simp
```
```    80
```
```    81 lemma ccSUP_empty [simp]: "(SUP x\<in>{}. f x) = bot"
```
```    82   unfolding image_empty by simp
```
```    83
```
```    84 lemma ccInf_superset_mono: "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> Inf A \<le> Inf B"
```
```    85   by (auto intro: ccInf_greatest ccInf_lower countable_subset)
```
```    86
```
```    87 lemma ccSup_subset_mono: "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Sup A \<le> Sup B"
```
```    88   by (auto intro: ccSup_least ccSup_upper countable_subset)
```
```    89
```
```    90 lemma ccInf_mono:
```
```    91   assumes [intro]: "countable B" "countable A"
```
```    92   assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
```
```    93   shows "Inf A \<le> Inf B"
```
```    94 proof (rule ccInf_greatest)
```
```    95   fix b assume "b \<in> B"
```
```    96   with assms obtain a where "a \<in> A" and "a \<le> b" by blast
```
```    97   from \<open>a \<in> A\<close> have "Inf A \<le> a" by (rule ccInf_lower[rotated]) auto
```
```    98   with \<open>a \<le> b\<close> show "Inf A \<le> b" by auto
```
```    99 qed auto
```
```   100
```
```   101 lemma ccINF_mono:
```
```   102   "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n\<in>A. f n) \<le> (INF n\<in>B. g n)"
```
```   103   using ccInf_mono [of "g ` B" "f ` A"] by auto
```
```   104
```
```   105 lemma ccSup_mono:
```
```   106   assumes [intro]: "countable B" "countable A"
```
```   107   assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
```
```   108   shows "Sup A \<le> Sup B"
```
```   109 proof (rule ccSup_least)
```
```   110   fix a assume "a \<in> A"
```
```   111   with assms obtain b where "b \<in> B" and "a \<le> b" by blast
```
```   112   from \<open>b \<in> B\<close> have "b \<le> Sup B" by (rule ccSup_upper[rotated]) auto
```
```   113   with \<open>a \<le> b\<close> show "a \<le> Sup B" by auto
```
```   114 qed auto
```
```   115
```
```   116 lemma ccSUP_mono:
```
```   117   "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n\<in>A. f n) \<le> (SUP n\<in>B. g n)"
```
```   118   using ccSup_mono [of "g ` B" "f ` A"] by auto
```
```   119
```
```   120 lemma ccINF_superset_mono:
```
```   121   "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (INF x\<in>A. f x) \<le> (INF x\<in>B. g x)"
```
```   122   by (blast intro: ccINF_mono countable_subset dest: subsetD)
```
```   123
```
```   124 lemma ccSUP_subset_mono:
```
```   125   "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (SUP x\<in>A. f x) \<le> (SUP x\<in>B. g x)"
```
```   126   by (blast intro: ccSUP_mono countable_subset dest: subsetD)
```
```   127
```
```   128
```
```   129 lemma less_eq_ccInf_inter: "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (Inf A) (Inf B) \<le> Inf (A \<inter> B)"
```
```   130   by (auto intro: ccInf_greatest ccInf_lower)
```
```   131
```
```   132 lemma ccSup_inter_less_eq: "countable A \<Longrightarrow> countable B \<Longrightarrow> Sup (A \<inter> B) \<le> inf (Sup A) (Sup B)"
```
```   133   by (auto intro: ccSup_least ccSup_upper)
```
```   134
```
```   135 lemma ccInf_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)"
```
```   136   by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2)
```
```   137
```
```   138 lemma ccINF_union:
```
```   139   "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i\<in>A \<union> B. M i) = inf (INF i\<in>A. M i) (INF i\<in>B. M i)"
```
```   140   by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower)
```
```   141
```
```   142 lemma ccSup_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
```
```   143   by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2)
```
```   144
```
```   145 lemma ccSUP_union:
```
```   146   "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i\<in>A \<union> B. M i) = sup (SUP i\<in>A. M i) (SUP i\<in>B. M i)"
```
```   147   by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper)
```
```   148
```
```   149 lemma ccINF_inf_distrib: "countable A \<Longrightarrow> inf (INF a\<in>A. f a) (INF a\<in>A. g a) = (INF a\<in>A. inf (f a) (g a))"
```
```   150   by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono)
```
```   151
```
```   152 lemma ccSUP_sup_distrib: "countable A \<Longrightarrow> sup (SUP a\<in>A. f a) (SUP a\<in>A. g a) = (SUP a\<in>A. sup (f a) (g a))"
```
```   153   by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono)
```
```   154
```
```   155 lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF i \<in> A. f) = f"
```
```   156   unfolding image_constant_conv by auto
```
```   157
```
```   158 lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP i \<in> A. f) = f"
```
```   159   unfolding image_constant_conv by auto
```
```   160
```
```   161 lemma ccINF_top [simp]: "(INF x\<in>A. top) = top"
```
```   162   by (cases "A = {}") simp_all
```
```   163
```
```   164 lemma ccSUP_bot [simp]: "(SUP x\<in>A. bot) = bot"
```
```   165   by (cases "A = {}") simp_all
```
```   166
```
```   167 lemma ccINF_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i\<in>A. INF j\<in>B. f i j) = (INF j\<in>B. INF i\<in>A. f i j)"
```
```   168   by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym)
```
```   169
```
```   170 lemma ccSUP_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i\<in>A. SUP j\<in>B. f i j) = (SUP j\<in>B. SUP i\<in>A. f i j)"
```
```   171   by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym)
```
```   172
```
```   173 end
```
```   174
```
```   175 context
```
```   176   fixes a :: "'a::{countable_complete_lattice, linorder}"
```
```   177 begin
```
```   178
```
```   179 lemma less_ccSup_iff: "countable S \<Longrightarrow> a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
```
```   180   unfolding not_le [symmetric] by (subst ccSup_le_iff) auto
```
```   181
```
```   182 lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (SUP i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
```
```   183   using less_ccSup_iff [of "f ` A"] by simp
```
```   184
```
```   185 lemma ccInf_less_iff: "countable S \<Longrightarrow> Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
```
```   186   unfolding not_le [symmetric] by (subst le_ccInf_iff) auto
```
```   187
```
```   188 lemma ccINF_less_iff: "countable A \<Longrightarrow> (INF i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
```
```   189   using ccInf_less_iff [of "f ` A"] by simp
```
```   190
```
```   191 end
```
```   192
```
```   193 class countable_complete_distrib_lattice = countable_complete_lattice +
```
```   194   assumes sup_ccInf: "countable B \<Longrightarrow> sup a (Inf B) = (INF b\<in>B. sup a b)"
```
```   195   assumes inf_ccSup: "countable B \<Longrightarrow> inf a (Sup B) = (SUP b\<in>B. inf a b)"
```
```   196 begin
```
```   197
```
```   198 lemma sup_ccINF:
```
```   199   "countable B \<Longrightarrow> sup a (INF b\<in>B. f b) = (INF b\<in>B. sup a (f b))"
```
```   200   by (simp only: sup_ccInf image_image countable_image)
```
```   201
```
```   202 lemma inf_ccSUP:
```
```   203   "countable B \<Longrightarrow> inf a (SUP b\<in>B. f b) = (SUP b\<in>B. inf a (f b))"
```
```   204   by (simp only: inf_ccSup image_image countable_image)
```
```   205
```
```   206 subclass distrib_lattice
```
```   207 proof
```
```   208   fix a b c
```
```   209   from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d\<in>{b, c}. sup a d)"
```
```   210     by simp
```
```   211   then show "sup a (inf b c) = inf (sup a b) (sup a c)"
```
```   212     by simp
```
```   213 qed
```
```   214
```
```   215 lemma ccInf_sup:
```
```   216   "countable B \<Longrightarrow> sup (Inf B) a = (INF b\<in>B. sup b a)"
```
```   217   by (simp add: sup_ccInf sup_commute)
```
```   218
```
```   219 lemma ccSup_inf:
```
```   220   "countable B \<Longrightarrow> inf (Sup B) a = (SUP b\<in>B. inf b a)"
```
```   221   by (simp add: inf_ccSup inf_commute)
```
```   222
```
```   223 lemma ccINF_sup:
```
```   224   "countable B \<Longrightarrow> sup (INF b\<in>B. f b) a = (INF b\<in>B. sup (f b) a)"
```
```   225   by (simp add: sup_ccINF sup_commute)
```
```   226
```
```   227 lemma ccSUP_inf:
```
```   228   "countable B \<Longrightarrow> inf (SUP b\<in>B. f b) a = (SUP b\<in>B. inf (f b) a)"
```
```   229   by (simp add: inf_ccSUP inf_commute)
```
```   230
```
```   231 lemma ccINF_sup_distrib2:
```
```   232   "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (INF a\<in>A. f a) (INF b\<in>B. g b) = (INF a\<in>A. INF b\<in>B. sup (f a) (g b))"
```
```   233   by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup)
```
```   234
```
```   235 lemma ccSUP_inf_distrib2:
```
```   236   "countable A \<Longrightarrow> countable B \<Longrightarrow> inf (SUP a\<in>A. f a) (SUP b\<in>B. g b) = (SUP a\<in>A. SUP b\<in>B. inf (f a) (g b))"
```
```   237   by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf)
```
```   238
```
```   239 context
```
```   240   fixes f :: "'a \<Rightarrow> 'b::countable_complete_lattice"
```
```   241   assumes "mono f"
```
```   242 begin
```
```   243
```
```   244 lemma mono_ccInf:
```
```   245   "countable A \<Longrightarrow> f (Inf A) \<le> (INF x\<in>A. f x)"
```
```   246   using \<open>mono f\<close>
```
```   247   by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD)
```
```   248
```
```   249 lemma mono_ccSup:
```
```   250   "countable A \<Longrightarrow> (SUP x\<in>A. f x) \<le> f (Sup A)"
```
```   251   using \<open>mono f\<close> by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD)
```
```   252
```
```   253 lemma mono_ccINF:
```
```   254   "countable I \<Longrightarrow> f (INF i \<in> I. A i) \<le> (INF x \<in> I. f (A x))"
```
```   255   by (intro countable_complete_lattice_class.ccINF_greatest monoD[OF \<open>mono f\<close>] ccINF_lower)
```
```   256
```
```   257 lemma mono_ccSUP:
```
```   258   "countable I \<Longrightarrow> (SUP x \<in> I. f (A x)) \<le> f (SUP i \<in> I. A i)"
```
```   259   by (intro countable_complete_lattice_class.ccSUP_least monoD[OF \<open>mono f\<close>] ccSUP_upper)
```
```   260
```
```   261 end
```
```   262
```
```   263 end
```
```   264
```
```   265 subsubsection \<open>Instances of countable complete lattices\<close>
```
```   266
```
```   267 instance "fun" :: (type, countable_complete_lattice) countable_complete_lattice
```
```   268   by standard
```
```   269      (auto simp: le_fun_def intro!: ccSUP_upper ccSUP_least ccINF_lower ccINF_greatest)
```
```   270
```
```   271 subclass (in complete_lattice) countable_complete_lattice
```
```   272   by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
```
```   273
```
```   274 subclass (in complete_distrib_lattice) countable_complete_distrib_lattice
```
```   275   by standard (auto intro: sup_Inf inf_Sup)
```
```   276
```
```   277 end
```