add countable complete lattices
authorhoelzl
Thu Feb 18 13:54:44 2016 +0100 (2016-02-18)
changeset 62373ea7a442e9a56
parent 62372 4fe872ff91bf
child 62374 cb27a55d868a
add countable complete lattices
src/HOL/Library/Countable_Complete_Lattices.thy
src/HOL/Library/Library.thy
src/HOL/Library/Order_Continuity.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Countable_Complete_Lattices.thy	Thu Feb 18 13:54:44 2016 +0100
     1.3 @@ -0,0 +1,275 @@
     1.4 +(*  Title:      HOL/Library/Countable_Complete_Lattices.thy
     1.5 +    Author:     Johannes Hölzl
     1.6 +*)
     1.7 +
     1.8 +section \<open>Countable Complete Lattices\<close>
     1.9 +
    1.10 +theory Countable_Complete_Lattices
    1.11 +  imports Main Lattice_Syntax Countable_Set
    1.12 +begin
    1.13 +
    1.14 +lemma UNIV_nat_eq: "UNIV = insert 0 (range Suc)"
    1.15 +  by (metis UNIV_eq_I nat.nchotomy insertCI rangeI)
    1.16 +
    1.17 +class countable_complete_lattice = lattice + Inf + Sup + bot + top +
    1.18 +  assumes ccInf_lower: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
    1.19 +  assumes ccInf_greatest: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
    1.20 +  assumes ccSup_upper: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
    1.21 +  assumes ccSup_least: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
    1.22 +  assumes ccInf_empty [simp]: "\<Sqinter>{} = \<top>"
    1.23 +  assumes ccSup_empty [simp]: "\<Squnion>{} = \<bottom>"
    1.24 +begin
    1.25 +
    1.26 +subclass bounded_lattice
    1.27 +proof
    1.28 +  fix a
    1.29 +  show "\<bottom> \<le> a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric])
    1.30 +  show "a \<le> \<top>" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric])
    1.31 +qed
    1.32 +
    1.33 +lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> f i"
    1.34 +  using ccInf_lower [of "f ` A"] by simp
    1.35 +
    1.36 +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)"
    1.37 +  using ccInf_greatest [of "f ` A"] by auto
    1.38 +
    1.39 +lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (\<Squnion>i\<in>A. f i)"
    1.40 +  using ccSup_upper [of "f ` A"] by simp
    1.41 +
    1.42 +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"
    1.43 +  using ccSup_least [of "f ` A"] by auto
    1.44 +
    1.45 +lemma ccInf_lower2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> \<Sqinter>A \<le> v"
    1.46 +  using ccInf_lower [of A u] by auto
    1.47 +
    1.48 +lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> u"
    1.49 +  using ccINF_lower [of A i f] by auto
    1.50 +
    1.51 +lemma ccSup_upper2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> \<Squnion>A"
    1.52 +  using ccSup_upper [of A u] by auto
    1.53 +
    1.54 +lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (\<Squnion>i\<in>A. f i)"
    1.55 +  using ccSUP_upper [of A i f] by auto
    1.56 +
    1.57 +lemma le_ccInf_iff: "countable A \<Longrightarrow> b \<le> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)"
    1.58 +  by (auto intro: ccInf_greatest dest: ccInf_lower)
    1.59 +
    1.60 +lemma le_ccINF_iff: "countable A \<Longrightarrow> u \<le> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
    1.61 +  using le_ccInf_iff [of "f ` A"] by simp
    1.62 +
    1.63 +lemma ccSup_le_iff: "countable A \<Longrightarrow> \<Squnion>A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)"
    1.64 +  by (auto intro: ccSup_least dest: ccSup_upper)
    1.65 +
    1.66 +lemma ccSUP_le_iff: "countable A \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
    1.67 +  using ccSup_le_iff [of "f ` A"] by simp
    1.68 +
    1.69 +lemma ccInf_insert [simp]: "countable A \<Longrightarrow> \<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    1.70 +  by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower)
    1.71 +
    1.72 +lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFIMUM A f"
    1.73 +  unfolding image_insert by simp
    1.74 +
    1.75 +lemma ccSup_insert [simp]: "countable A \<Longrightarrow> \<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.76 +  by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper)
    1.77 +
    1.78 +lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPREMUM A f"
    1.79 +  unfolding image_insert by simp
    1.80 +
    1.81 +lemma ccINF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
    1.82 +  unfolding image_empty by simp
    1.83 +
    1.84 +lemma ccSUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
    1.85 +  unfolding image_empty by simp
    1.86 +
    1.87 +lemma ccInf_superset_mono: "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<le> \<Sqinter>B"
    1.88 +  by (auto intro: ccInf_greatest ccInf_lower countable_subset)
    1.89 +
    1.90 +lemma ccSup_subset_mono: "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<Squnion>A \<le> \<Squnion>B"
    1.91 +  by (auto intro: ccSup_least ccSup_upper countable_subset)
    1.92 +
    1.93 +lemma ccInf_mono:
    1.94 +  assumes [intro]: "countable B" "countable A"
    1.95 +  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
    1.96 +  shows "\<Sqinter>A \<le> \<Sqinter>B"
    1.97 +proof (rule ccInf_greatest)
    1.98 +  fix b assume "b \<in> B"
    1.99 +  with assms obtain a where "a \<in> A" and "a \<le> b" by blast
   1.100 +  from \<open>a \<in> A\<close> have "\<Sqinter>A \<le> a" by (rule ccInf_lower[rotated]) auto
   1.101 +  with \<open>a \<le> b\<close> show "\<Sqinter>A \<le> b" by auto
   1.102 +qed auto
   1.103 +
   1.104 +lemma ccINF_mono:
   1.105 +  "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)"
   1.106 +  using ccInf_mono [of "g ` B" "f ` A"] by auto
   1.107 +
   1.108 +lemma ccSup_mono:
   1.109 +  assumes [intro]: "countable B" "countable A"
   1.110 +  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
   1.111 +  shows "\<Squnion>A \<le> \<Squnion>B"
   1.112 +proof (rule ccSup_least)
   1.113 +  fix a assume "a \<in> A"
   1.114 +  with assms obtain b where "b \<in> B" and "a \<le> b" by blast
   1.115 +  from \<open>b \<in> B\<close> have "b \<le> \<Squnion>B" by (rule ccSup_upper[rotated]) auto
   1.116 +  with \<open>a \<le> b\<close> show "a \<le> \<Squnion>B" by auto
   1.117 +qed auto
   1.118 +
   1.119 +lemma ccSUP_mono:
   1.120 +  "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)"
   1.121 +  using ccSup_mono [of "g ` B" "f ` A"] by auto
   1.122 +
   1.123 +lemma ccINF_superset_mono:
   1.124 +  "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)"
   1.125 +  by (blast intro: ccINF_mono countable_subset dest: subsetD)
   1.126 +
   1.127 +lemma ccSUP_subset_mono:
   1.128 +  "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)"
   1.129 +  by (blast intro: ccSUP_mono countable_subset dest: subsetD)
   1.130 +
   1.131 +
   1.132 +lemma less_eq_ccInf_inter: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)"
   1.133 +  by (auto intro: ccInf_greatest ccInf_lower)
   1.134 +
   1.135 +lemma ccSup_inter_less_eq: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Squnion>(A \<inter> B) \<le> \<Squnion>A \<sqinter> \<Squnion>B "
   1.136 +  by (auto intro: ccSup_least ccSup_upper)
   1.137 +
   1.138 +lemma ccInf_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   1.139 +  by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2)
   1.140 +
   1.141 +lemma ccINF_union:
   1.142 +  "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)"
   1.143 +  by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower)
   1.144 +
   1.145 +lemma ccSup_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
   1.146 +  by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2)
   1.147 +
   1.148 +lemma ccSUP_union:
   1.149 +  "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)"
   1.150 +  by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper)
   1.151 +
   1.152 +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)"
   1.153 +  by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono)
   1.154 +
   1.155 +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)"
   1.156 +  by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono)
   1.157 +
   1.158 +lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
   1.159 +  unfolding image_constant_conv by auto
   1.160 +
   1.161 +lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
   1.162 +  unfolding image_constant_conv by auto
   1.163 +
   1.164 +lemma ccINF_top [simp]: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   1.165 +  by (cases "A = {}") simp_all
   1.166 +
   1.167 +lemma ccSUP_bot [simp]: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
   1.168 +  by (cases "A = {}") simp_all
   1.169 +
   1.170 +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)"
   1.171 +  by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym)
   1.172 +
   1.173 +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)"
   1.174 +  by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym)
   1.175 +
   1.176 +end
   1.177 +
   1.178 +context
   1.179 +  fixes a :: "'a::{countable_complete_lattice, linorder}"
   1.180 +begin
   1.181 +
   1.182 +lemma less_ccSup_iff: "countable S \<Longrightarrow> a < \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
   1.183 +  unfolding not_le [symmetric] by (subst ccSup_le_iff) auto
   1.184 +
   1.185 +lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
   1.186 +  using less_ccSup_iff [of "f ` A"] by simp
   1.187 +
   1.188 +lemma ccInf_less_iff: "countable S \<Longrightarrow> \<Sqinter>S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
   1.189 +  unfolding not_le [symmetric] by (subst le_ccInf_iff) auto
   1.190 +
   1.191 +lemma ccINF_less_iff: "countable A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
   1.192 +  using ccInf_less_iff [of "f ` A"] by simp
   1.193 +
   1.194 +end
   1.195 +
   1.196 +class countable_complete_distrib_lattice = countable_complete_lattice +
   1.197 +  assumes sup_ccInf: "countable B \<Longrightarrow> a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   1.198 +  assumes inf_ccSup: "countable B \<Longrightarrow> a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   1.199 +begin
   1.200 +
   1.201 +lemma sup_ccINF:
   1.202 +  "countable B \<Longrightarrow> a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   1.203 +  by (simp only: sup_ccInf image_image countable_image)
   1.204 +
   1.205 +lemma inf_ccSUP:
   1.206 +  "countable B \<Longrightarrow> a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   1.207 +  by (simp only: inf_ccSup image_image countable_image)
   1.208 +
   1.209 +subclass distrib_lattice proof
   1.210 +  fix a b c
   1.211 +  from sup_ccInf[of "{b, c}" a] have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)"
   1.212 +    by simp
   1.213 +  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp
   1.214 +qed
   1.215 +
   1.216 +lemma ccInf_sup:
   1.217 +  "countable B \<Longrightarrow> \<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
   1.218 +  by (simp add: sup_ccInf sup_commute)
   1.219 +
   1.220 +lemma ccSup_inf:
   1.221 +  "countable B \<Longrightarrow> \<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
   1.222 +  by (simp add: inf_ccSup inf_commute)
   1.223 +
   1.224 +lemma ccINF_sup:
   1.225 +  "countable B \<Longrightarrow> (\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
   1.226 +  by (simp add: sup_ccINF sup_commute)
   1.227 +
   1.228 +lemma ccSUP_inf:
   1.229 +  "countable B \<Longrightarrow> (\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
   1.230 +  by (simp add: inf_ccSUP inf_commute)
   1.231 +
   1.232 +lemma ccINF_sup_distrib2:
   1.233 +  "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)"
   1.234 +  by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup)
   1.235 +
   1.236 +lemma ccSUP_inf_distrib2:
   1.237 +  "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)"
   1.238 +  by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf)
   1.239 +
   1.240 +context
   1.241 +  fixes f :: "'a \<Rightarrow> 'b::countable_complete_lattice"
   1.242 +  assumes "mono f"
   1.243 +begin
   1.244 +
   1.245 +lemma mono_ccInf:
   1.246 +  "countable A \<Longrightarrow> f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)"
   1.247 +  using \<open>mono f\<close>
   1.248 +  by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD)
   1.249 +
   1.250 +lemma mono_ccSup:
   1.251 +  "countable A \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
   1.252 +  using \<open>mono f\<close> by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD)
   1.253 +
   1.254 +lemma mono_ccINF:
   1.255 +  "countable I \<Longrightarrow> f (INF i : I. A i) \<le> (INF x : I. f (A x))"
   1.256 +  by (intro countable_complete_lattice_class.ccINF_greatest monoD[OF \<open>mono f\<close>] ccINF_lower)
   1.257 +
   1.258 +lemma mono_ccSUP:
   1.259 +  "countable I \<Longrightarrow> (SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
   1.260 +  by (intro countable_complete_lattice_class.ccSUP_least monoD[OF \<open>mono f\<close>] ccSUP_upper)
   1.261 +
   1.262 +end
   1.263 +
   1.264 +end
   1.265 +
   1.266 +subsubsection \<open>Instances of countable complete lattices\<close>
   1.267 +
   1.268 +instance "fun" :: (type, countable_complete_lattice) countable_complete_lattice
   1.269 +  by standard
   1.270 +     (auto simp: le_fun_def intro!: ccSUP_upper ccSUP_least ccINF_lower ccINF_greatest)
   1.271 +
   1.272 +subclass (in complete_lattice) countable_complete_lattice
   1.273 +  by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
   1.274 +
   1.275 +subclass (in complete_distrib_lattice) countable_complete_distrib_lattice
   1.276 +  by standard (auto intro: sup_Inf inf_Sup)
   1.277 +
   1.278 +end
   1.279 \ No newline at end of file
     2.1 --- a/src/HOL/Library/Library.thy	Tue Feb 09 07:04:48 2016 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Thu Feb 18 13:54:44 2016 +0100
     2.3 @@ -12,6 +12,7 @@
     2.4    ContNotDenum
     2.5    Convex
     2.6    Countable
     2.7 +  Countable_Complete_Lattices
     2.8    Countable_Set_Type
     2.9    Debug
    2.10    Diagonal_Subsequence
     3.1 --- a/src/HOL/Library/Order_Continuity.thy	Tue Feb 09 07:04:48 2016 +0100
     3.2 +++ b/src/HOL/Library/Order_Continuity.thy	Thu Feb 18 13:54:44 2016 +0100
     3.3 @@ -1,30 +1,31 @@
     3.4  (*  Title:      HOL/Library/Order_Continuity.thy
     3.5 -    Author:     David von Oheimb, TU Muenchen
     3.6 +    Author:     David von Oheimb, TU München
     3.7 +    Author:     Johannes Hölzl, TU München
     3.8  *)
     3.9  
    3.10 -section \<open>Continuity and iterations (of set transformers)\<close>
    3.11 +section \<open>Continuity and iterations\<close>
    3.12  
    3.13  theory Order_Continuity
    3.14 -imports Complex_Main
    3.15 +imports Complex_Main Countable_Complete_Lattices
    3.16  begin
    3.17  
    3.18  (* TODO: Generalize theory to chain-complete partial orders *)
    3.19  
    3.20  lemma SUP_nat_binary:
    3.21 -  "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)"
    3.22 -  apply (auto intro!: antisym SUP_least)
    3.23 -  apply (rule SUP_upper2[where i=0])
    3.24 +  "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::countable_complete_lattice)"
    3.25 +  apply (auto intro!: antisym ccSUP_least)
    3.26 +  apply (rule ccSUP_upper2[where i=0])
    3.27    apply simp_all
    3.28 -  apply (rule SUP_upper2[where i=1])
    3.29 +  apply (rule ccSUP_upper2[where i=1])
    3.30    apply simp_all
    3.31    done
    3.32  
    3.33  lemma INF_nat_binary:
    3.34 -  "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)"
    3.35 -  apply (auto intro!: antisym INF_greatest)
    3.36 -  apply (rule INF_lower2[where i=0])
    3.37 +  "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::countable_complete_lattice)"
    3.38 +  apply (auto intro!: antisym ccINF_greatest)
    3.39 +  apply (rule ccINF_lower2[where i=0])
    3.40    apply simp_all
    3.41 -  apply (rule INF_lower2[where i=1])
    3.42 +  apply (rule ccINF_lower2[where i=1])
    3.43    apply simp_all
    3.44    done
    3.45  
    3.46 @@ -39,7 +40,8 @@
    3.47  subsection \<open>Continuity for complete lattices\<close>
    3.48  
    3.49  definition
    3.50 -  sup_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
    3.51 +  sup_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool"
    3.52 +where
    3.53    "sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    3.54  
    3.55  lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    3.56 @@ -79,26 +81,26 @@
    3.57  
    3.58  lemma sup_continuous_sup[order_continuous_intros]:
    3.59    "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))"
    3.60 -  by (simp add: sup_continuous_def SUP_sup_distrib)
    3.61 +  by (simp add: sup_continuous_def ccSUP_sup_distrib)
    3.62  
    3.63  lemma sup_continuous_inf[order_continuous_intros]:
    3.64 -  fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
    3.65 +  fixes P Q :: "'a :: countable_complete_lattice \<Rightarrow> 'b :: countable_complete_distrib_lattice"
    3.66    assumes P: "sup_continuous P" and Q: "sup_continuous Q"
    3.67    shows "sup_continuous (\<lambda>x. inf (P x) (Q x))"
    3.68    unfolding sup_continuous_def
    3.69  proof (safe intro!: antisym)
    3.70    fix M :: "nat \<Rightarrow> 'a" assume M: "incseq M"
    3.71    have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))"
    3.72 -    unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_SUP SUP_inf ..
    3.73 +    by (simp add: sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_ccSUP ccSUP_inf)
    3.74    also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))"
    3.75 -  proof (intro SUP_least)
    3.76 +  proof (intro ccSUP_least)
    3.77      fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j)) \<le> (SUP i. inf (P (M i)) (Q (M i)))"
    3.78 -      by (intro SUP_upper2[of "sup i j"] inf_mono) (auto simp: mono_def)
    3.79 -  qed
    3.80 +      by (intro ccSUP_upper2[of _ "sup i j"] inf_mono) (auto simp: mono_def)
    3.81 +  qed auto
    3.82    finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" .
    3.83 -  
    3.84 +
    3.85    show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))"
    3.86 -    unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro SUP_least inf_mono SUP_upper)
    3.87 +    unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro ccSUP_least inf_mono ccSUP_upper) auto
    3.88  qed
    3.89  
    3.90  lemma sup_continuous_and[order_continuous_intros]:
    3.91 @@ -203,7 +205,8 @@
    3.92    by (rule lfp_transfer_bounded[where P=top]) (auto dest: sup_continuousD)
    3.93  
    3.94  definition
    3.95 -  inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
    3.96 +  inf_continuous :: "('a::countable_complete_lattice \<Rightarrow> 'b::countable_complete_lattice) \<Rightarrow> bool"
    3.97 +where
    3.98    "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    3.99  
   3.100  lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
   3.101 @@ -231,25 +234,25 @@
   3.102  
   3.103  lemma inf_continuous_inf[order_continuous_intros]:
   3.104    "inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
   3.105 -  by (simp add: inf_continuous_def INF_inf_distrib)
   3.106 +  by (simp add: inf_continuous_def ccINF_inf_distrib)
   3.107  
   3.108  lemma inf_continuous_sup[order_continuous_intros]:
   3.109 -  fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
   3.110 +  fixes P Q :: "'a :: countable_complete_lattice \<Rightarrow> 'b :: countable_complete_distrib_lattice"
   3.111    assumes P: "inf_continuous P" and Q: "inf_continuous Q"
   3.112    shows "inf_continuous (\<lambda>x. sup (P x) (Q x))"
   3.113    unfolding inf_continuous_def
   3.114  proof (safe intro!: antisym)
   3.115    fix M :: "nat \<Rightarrow> 'a" assume M: "decseq M"
   3.116    show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))"
   3.117 -    unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro INF_greatest sup_mono INF_lower)
   3.118 +    unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro ccINF_greatest sup_mono ccINF_lower) auto
   3.119  
   3.120    have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))"
   3.121 -  proof (intro INF_greatest)
   3.122 +  proof (intro ccINF_greatest)
   3.123      fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j)) \<ge> (INF i. sup (P (M i)) (Q (M i)))"
   3.124 -      by (intro INF_lower2[of "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
   3.125 -  qed
   3.126 +      by (intro ccINF_lower2[of _ "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
   3.127 +  qed auto
   3.128    also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))"
   3.129 -    unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] INF_sup sup_INF ..
   3.130 +    by (simp add: inf_continuousD[OF P M] inf_continuousD[OF Q M] ccINF_sup sup_ccINF)
   3.131    finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" .
   3.132  qed
   3.133  
   3.134 @@ -348,7 +351,7 @@
   3.135        using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"]
   3.136        unfolding funpow_Suc_right by simp
   3.137    qed
   3.138 -    
   3.139 +
   3.140    have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))"
   3.141      unfolding inf_continuous_gfp[OF f]
   3.142    proof (rule INF_eq)
   3.143 @@ -387,4 +390,43 @@
   3.144    qed (auto intro: Inf_greatest)
   3.145  qed
   3.146  
   3.147 +subsubsection \<open>Least fixed points in countable complete lattices\<close>
   3.148 +
   3.149 +definition (in countable_complete_lattice) cclfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
   3.150 +  where "cclfp f = (\<Squnion>i. (f ^^ i) \<bottom>)"
   3.151 +
   3.152 +lemma cclfp_unfold:
   3.153 +  assumes "sup_continuous F" shows "cclfp F = F (cclfp F)"
   3.154 +proof -
   3.155 +  have "cclfp F = (\<Squnion>i. F ((F ^^ i) \<bottom>))"
   3.156 +    unfolding cclfp_def by (subst UNIV_nat_eq) auto
   3.157 +  also have "\<dots> = F (cclfp F)"
   3.158 +    unfolding cclfp_def
   3.159 +    by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono)
   3.160 +  finally show ?thesis .
   3.161 +qed
   3.162 +
   3.163 +lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A \<le> A" shows "cclfp f \<le> A"
   3.164 +  unfolding cclfp_def
   3.165 +proof (intro ccSUP_least)
   3.166 +  fix i show "(f ^^ i) \<bottom> \<le> A"
   3.167 +  proof (induction i)
   3.168 +    case (Suc i) from monoD[OF f this] A show ?case
   3.169 +      by auto
   3.170 +  qed simp
   3.171 +qed simp
   3.172 +
   3.173 +lemma cclfp_transfer:
   3.174 +  assumes "sup_continuous \<alpha>" "mono f"
   3.175 +  assumes "\<alpha> \<bottom> = \<bottom>" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
   3.176 +  shows "\<alpha> (cclfp f) = cclfp g"
   3.177 +proof -
   3.178 +  have "\<alpha> (cclfp f) = (\<Squnion>i. \<alpha> ((f ^^ i) \<bottom>))"
   3.179 +    unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono)
   3.180 +  moreover have "\<alpha> ((f ^^ i) \<bottom>) = (g ^^ i) \<bottom>" for i
   3.181 +    by (induction i) (simp_all add: assms)
   3.182 +  ultimately show ?thesis
   3.183 +    by (simp add: cclfp_def)
   3.184 +qed
   3.185 +
   3.186  end