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