remove lattice syntax from countable complete lattice
authorhoelzl
Fri Feb 19 12:25:57 2016 +0100 (2016-02-19)
changeset 62374cb27a55d868a
parent 62373 ea7a442e9a56
child 62375 670063003ad3
remove lattice syntax from countable complete lattice
src/HOL/Library/Countable_Complete_Lattices.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Order_Continuity.thy
     1.1 --- a/src/HOL/Library/Countable_Complete_Lattices.thy	Thu Feb 18 13:54:44 2016 +0100
     1.2 +++ b/src/HOL/Library/Countable_Complete_Lattices.thy	Fri Feb 19 12:25:57 2016 +0100
     1.3 @@ -5,169 +5,169 @@
     1.4  section \<open>Countable Complete Lattices\<close>
     1.5  
     1.6  theory Countable_Complete_Lattices
     1.7 -  imports Main Lattice_Syntax Countable_Set
     1.8 +  imports Main Countable_Set
     1.9  begin
    1.10  
    1.11  lemma UNIV_nat_eq: "UNIV = insert 0 (range Suc)"
    1.12    by (metis UNIV_eq_I nat.nchotomy insertCI rangeI)
    1.13  
    1.14  class countable_complete_lattice = lattice + Inf + Sup + bot + top +
    1.15 -  assumes ccInf_lower: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
    1.16 -  assumes ccInf_greatest: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
    1.17 -  assumes ccSup_upper: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
    1.18 -  assumes ccSup_least: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
    1.19 -  assumes ccInf_empty [simp]: "\<Sqinter>{} = \<top>"
    1.20 -  assumes ccSup_empty [simp]: "\<Squnion>{} = \<bottom>"
    1.21 +  assumes ccInf_lower: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> Inf A \<le> x"
    1.22 +  assumes ccInf_greatest: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf A"
    1.23 +  assumes ccSup_upper: "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> Sup A"
    1.24 +  assumes ccSup_least: "countable A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z"
    1.25 +  assumes ccInf_empty [simp]: "Inf {} = top"
    1.26 +  assumes ccSup_empty [simp]: "Sup {} = bot"
    1.27  begin
    1.28  
    1.29  subclass bounded_lattice
    1.30  proof
    1.31    fix a
    1.32 -  show "\<bottom> \<le> a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric])
    1.33 -  show "a \<le> \<top>" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric])
    1.34 +  show "bot \<le> a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric])
    1.35 +  show "a \<le> top" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric])
    1.36  qed
    1.37  
    1.38 -lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> f i"
    1.39 +lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (INF i :A. f i) \<le> f i"
    1.40    using ccInf_lower [of "f ` A"] by simp
    1.41  
    1.42 -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.43 +lemma ccINF_greatest: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (INF i :A. f i)"
    1.44    using ccInf_greatest [of "f ` A"] by auto
    1.45  
    1.46 -lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (\<Squnion>i\<in>A. f i)"
    1.47 +lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (SUP i :A. f i)"
    1.48    using ccSup_upper [of "f ` A"] by simp
    1.49  
    1.50 -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.51 +lemma ccSUP_least: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (SUP i :A. f i) \<le> u"
    1.52    using ccSup_least [of "f ` A"] by auto
    1.53  
    1.54 -lemma ccInf_lower2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> \<Sqinter>A \<le> v"
    1.55 +lemma ccInf_lower2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> Inf A \<le> v"
    1.56    using ccInf_lower [of A u] by auto
    1.57  
    1.58 -lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> u"
    1.59 +lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (INF i :A. f i) \<le> u"
    1.60    using ccINF_lower [of A i f] by auto
    1.61  
    1.62 -lemma ccSup_upper2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> \<Squnion>A"
    1.63 +lemma ccSup_upper2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> Sup A"
    1.64    using ccSup_upper [of A u] by auto
    1.65  
    1.66 -lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (\<Squnion>i\<in>A. f i)"
    1.67 +lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (SUP i :A. f i)"
    1.68    using ccSUP_upper [of A i f] by auto
    1.69  
    1.70 -lemma le_ccInf_iff: "countable A \<Longrightarrow> b \<le> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)"
    1.71 +lemma le_ccInf_iff: "countable A \<Longrightarrow> b \<le> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)"
    1.72    by (auto intro: ccInf_greatest dest: ccInf_lower)
    1.73  
    1.74 -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.75 +lemma le_ccINF_iff: "countable A \<Longrightarrow> u \<le> (INF i :A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
    1.76    using le_ccInf_iff [of "f ` A"] by simp
    1.77  
    1.78 -lemma ccSup_le_iff: "countable A \<Longrightarrow> \<Squnion>A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)"
    1.79 +lemma ccSup_le_iff: "countable A \<Longrightarrow> Sup A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)"
    1.80    by (auto intro: ccSup_least dest: ccSup_upper)
    1.81  
    1.82 -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.83 +lemma ccSUP_le_iff: "countable A \<Longrightarrow> (SUP i :A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
    1.84    using ccSup_le_iff [of "f ` A"] by simp
    1.85  
    1.86 -lemma ccInf_insert [simp]: "countable A \<Longrightarrow> \<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    1.87 +lemma ccInf_insert [simp]: "countable A \<Longrightarrow> Inf (insert a A) = inf a (Inf A)"
    1.88    by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower)
    1.89  
    1.90 -lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFIMUM A f"
    1.91 +lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x:insert a A. f x) = inf (f a) (INFIMUM A f)"
    1.92    unfolding image_insert by simp
    1.93  
    1.94 -lemma ccSup_insert [simp]: "countable A \<Longrightarrow> \<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.95 +lemma ccSup_insert [simp]: "countable A \<Longrightarrow> Sup (insert a A) = sup a (Sup A)"
    1.96    by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper)
    1.97  
    1.98 -lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPREMUM A f"
    1.99 +lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x:insert a A. f x) = sup (f a) (SUPREMUM A f)"
   1.100    unfolding image_insert by simp
   1.101  
   1.102 -lemma ccINF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   1.103 +lemma ccINF_empty [simp]: "(INF x:{}. f x) = top"
   1.104    unfolding image_empty by simp
   1.105  
   1.106 -lemma ccSUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
   1.107 +lemma ccSUP_empty [simp]: "(SUP x:{}. f x) = bot"
   1.108    unfolding image_empty by simp
   1.109  
   1.110 -lemma ccInf_superset_mono: "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<le> \<Sqinter>B"
   1.111 +lemma ccInf_superset_mono: "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> Inf A \<le> Inf B"
   1.112    by (auto intro: ccInf_greatest ccInf_lower countable_subset)
   1.113  
   1.114 -lemma ccSup_subset_mono: "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<Squnion>A \<le> \<Squnion>B"
   1.115 +lemma ccSup_subset_mono: "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Sup A \<le> Sup B"
   1.116    by (auto intro: ccSup_least ccSup_upper countable_subset)
   1.117  
   1.118  lemma ccInf_mono:
   1.119    assumes [intro]: "countable B" "countable A"
   1.120    assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
   1.121 -  shows "\<Sqinter>A \<le> \<Sqinter>B"
   1.122 +  shows "Inf A \<le> Inf B"
   1.123  proof (rule ccInf_greatest)
   1.124    fix b assume "b \<in> B"
   1.125    with assms obtain a where "a \<in> A" and "a \<le> b" by blast
   1.126 -  from \<open>a \<in> A\<close> have "\<Sqinter>A \<le> a" by (rule ccInf_lower[rotated]) auto
   1.127 -  with \<open>a \<le> b\<close> show "\<Sqinter>A \<le> b" by auto
   1.128 +  from \<open>a \<in> A\<close> have "Inf A \<le> a" by (rule ccInf_lower[rotated]) auto
   1.129 +  with \<open>a \<le> b\<close> show "Inf A \<le> b" by auto
   1.130  qed auto
   1.131  
   1.132  lemma ccINF_mono:
   1.133 -  "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.134 +  "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
   1.135    using ccInf_mono [of "g ` B" "f ` A"] by auto
   1.136  
   1.137  lemma ccSup_mono:
   1.138    assumes [intro]: "countable B" "countable A"
   1.139    assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
   1.140 -  shows "\<Squnion>A \<le> \<Squnion>B"
   1.141 +  shows "Sup A \<le> Sup B"
   1.142  proof (rule ccSup_least)
   1.143    fix a assume "a \<in> A"
   1.144    with assms obtain b where "b \<in> B" and "a \<le> b" by blast
   1.145 -  from \<open>b \<in> B\<close> have "b \<le> \<Squnion>B" by (rule ccSup_upper[rotated]) auto
   1.146 -  with \<open>a \<le> b\<close> show "a \<le> \<Squnion>B" by auto
   1.147 +  from \<open>b \<in> B\<close> have "b \<le> Sup B" by (rule ccSup_upper[rotated]) auto
   1.148 +  with \<open>a \<le> b\<close> show "a \<le> Sup B" by auto
   1.149  qed auto
   1.150  
   1.151  lemma ccSUP_mono:
   1.152 -  "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.153 +  "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
   1.154    using ccSup_mono [of "g ` B" "f ` A"] by auto
   1.155  
   1.156  lemma ccINF_superset_mono:
   1.157 -  "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.158 +  "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (INF x:A. f x) \<le> (INF x:B. g x)"
   1.159    by (blast intro: ccINF_mono countable_subset dest: subsetD)
   1.160  
   1.161  lemma ccSUP_subset_mono:
   1.162 -  "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.163 +  "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (SUP x:A. f x) \<le> (SUP x:B. g x)"
   1.164    by (blast intro: ccSUP_mono countable_subset dest: subsetD)
   1.165  
   1.166  
   1.167 -lemma less_eq_ccInf_inter: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)"
   1.168 +lemma less_eq_ccInf_inter: "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (Inf A) (Inf B) \<le> Inf (A \<inter> B)"
   1.169    by (auto intro: ccInf_greatest ccInf_lower)
   1.170  
   1.171 -lemma ccSup_inter_less_eq: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Squnion>(A \<inter> B) \<le> \<Squnion>A \<sqinter> \<Squnion>B "
   1.172 +lemma ccSup_inter_less_eq: "countable A \<Longrightarrow> countable B \<Longrightarrow> Sup (A \<inter> B) \<le> inf (Sup A) (Sup B)"
   1.173    by (auto intro: ccSup_least ccSup_upper)
   1.174  
   1.175 -lemma ccInf_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   1.176 +lemma ccInf_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)"
   1.177    by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2)
   1.178  
   1.179  lemma ccINF_union:
   1.180 -  "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.181 +  "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i:A \<union> B. M i) = inf (INF i:A. M i) (INF i:B. M i)"
   1.182    by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower)
   1.183  
   1.184 -lemma ccSup_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> \<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
   1.185 +lemma ccSup_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
   1.186    by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2)
   1.187  
   1.188  lemma ccSUP_union:
   1.189 -  "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.190 +  "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i:A \<union> B. M i) = sup (SUP i:A. M i) (SUP i:B. M i)"
   1.191    by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper)
   1.192  
   1.193 -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.194 +lemma ccINF_inf_distrib: "countable A \<Longrightarrow> inf (INF a:A. f a) (INF a:A. g a) = (INF a:A. inf (f a) (g a))"
   1.195    by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono)
   1.196  
   1.197 -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.198 +lemma ccSUP_sup_distrib: "countable A \<Longrightarrow> sup (SUP a:A. f a) (SUP a:A. g a) = (SUP a:A. sup (f a) (g a))"
   1.199    by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono)
   1.200  
   1.201 -lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
   1.202 +lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF i :A. f) = f"
   1.203    unfolding image_constant_conv by auto
   1.204  
   1.205 -lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
   1.206 +lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP i :A. f) = f"
   1.207    unfolding image_constant_conv by auto
   1.208  
   1.209 -lemma ccINF_top [simp]: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   1.210 +lemma ccINF_top [simp]: "(INF x:A. top) = top"
   1.211    by (cases "A = {}") simp_all
   1.212  
   1.213 -lemma ccSUP_bot [simp]: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
   1.214 +lemma ccSUP_bot [simp]: "(SUP x:A. bot) = bot"
   1.215    by (cases "A = {}") simp_all
   1.216  
   1.217 -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.218 +lemma ccINF_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"
   1.219    by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym)
   1.220  
   1.221 -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.222 +lemma ccSUP_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
   1.223    by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym)
   1.224  
   1.225  end
   1.226 @@ -176,62 +176,64 @@
   1.227    fixes a :: "'a::{countable_complete_lattice, linorder}"
   1.228  begin
   1.229  
   1.230 -lemma less_ccSup_iff: "countable S \<Longrightarrow> a < \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
   1.231 +lemma less_ccSup_iff: "countable S \<Longrightarrow> a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
   1.232    unfolding not_le [symmetric] by (subst ccSup_le_iff) auto
   1.233  
   1.234 -lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
   1.235 +lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
   1.236    using less_ccSup_iff [of "f ` A"] by simp
   1.237  
   1.238 -lemma ccInf_less_iff: "countable S \<Longrightarrow> \<Sqinter>S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
   1.239 +lemma ccInf_less_iff: "countable S \<Longrightarrow> Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
   1.240    unfolding not_le [symmetric] by (subst le_ccInf_iff) auto
   1.241  
   1.242 -lemma ccINF_less_iff: "countable A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
   1.243 +lemma ccINF_less_iff: "countable A \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
   1.244    using ccInf_less_iff [of "f ` A"] by simp
   1.245  
   1.246  end
   1.247  
   1.248  class countable_complete_distrib_lattice = countable_complete_lattice +
   1.249 -  assumes sup_ccInf: "countable B \<Longrightarrow> a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   1.250 -  assumes inf_ccSup: "countable B \<Longrightarrow> a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   1.251 +  assumes sup_ccInf: "countable B \<Longrightarrow> sup a (Inf B) = (INF b:B. sup a b)"
   1.252 +  assumes inf_ccSup: "countable B \<Longrightarrow> inf a (Sup B) = (SUP b:B. inf a b)"
   1.253  begin
   1.254  
   1.255  lemma sup_ccINF:
   1.256 -  "countable B \<Longrightarrow> a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   1.257 +  "countable B \<Longrightarrow> sup a (INF b:B. f b) = (INF b:B. sup a (f b))"
   1.258    by (simp only: sup_ccInf image_image countable_image)
   1.259  
   1.260  lemma inf_ccSUP:
   1.261 -  "countable B \<Longrightarrow> a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   1.262 +  "countable B \<Longrightarrow> inf a (SUP b:B. f b) = (SUP b:B. inf a (f b))"
   1.263    by (simp only: inf_ccSup image_image countable_image)
   1.264  
   1.265 -subclass distrib_lattice proof
   1.266 +subclass distrib_lattice
   1.267 +proof
   1.268    fix a b c
   1.269 -  from sup_ccInf[of "{b, c}" a] have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)"
   1.270 +  from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d:{b, c}. sup a d)"
   1.271      by simp
   1.272 -  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp
   1.273 +  then show "sup a (inf b c) = inf (sup a b) (sup a c)"
   1.274 +    by simp
   1.275  qed
   1.276  
   1.277  lemma ccInf_sup:
   1.278 -  "countable B \<Longrightarrow> \<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
   1.279 +  "countable B \<Longrightarrow> sup (Inf B) a = (INF b:B. sup b a)"
   1.280    by (simp add: sup_ccInf sup_commute)
   1.281  
   1.282  lemma ccSup_inf:
   1.283 -  "countable B \<Longrightarrow> \<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
   1.284 +  "countable B \<Longrightarrow> inf (Sup B) a = (SUP b:B. inf b a)"
   1.285    by (simp add: inf_ccSup inf_commute)
   1.286  
   1.287  lemma ccINF_sup:
   1.288 -  "countable B \<Longrightarrow> (\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
   1.289 +  "countable B \<Longrightarrow> sup (INF b:B. f b) a = (INF b:B. sup (f b) a)"
   1.290    by (simp add: sup_ccINF sup_commute)
   1.291  
   1.292  lemma ccSUP_inf:
   1.293 -  "countable B \<Longrightarrow> (\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
   1.294 +  "countable B \<Longrightarrow> inf (SUP b:B. f b) a = (SUP b:B. inf (f b) a)"
   1.295    by (simp add: inf_ccSUP inf_commute)
   1.296  
   1.297  lemma ccINF_sup_distrib2:
   1.298 -  "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.299 +  "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (INF a:A. f a) (INF b:B. g b) = (INF a:A. INF b:B. sup (f a) (g b))"
   1.300    by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup)
   1.301  
   1.302  lemma ccSUP_inf_distrib2:
   1.303 -  "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.304 +  "countable A \<Longrightarrow> countable B \<Longrightarrow> inf (SUP a:A. f a) (SUP b:B. g b) = (SUP a:A. SUP b:B. inf (f a) (g b))"
   1.305    by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf)
   1.306  
   1.307  context
   1.308 @@ -240,12 +242,12 @@
   1.309  begin
   1.310  
   1.311  lemma mono_ccInf:
   1.312 -  "countable A \<Longrightarrow> f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)"
   1.313 +  "countable A \<Longrightarrow> f (Inf A) \<le> (INF x:A. f x)"
   1.314    using \<open>mono f\<close>
   1.315    by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD)
   1.316  
   1.317  lemma mono_ccSup:
   1.318 -  "countable A \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
   1.319 +  "countable A \<Longrightarrow> (SUP x:A. f x) \<le> f (Sup A)"
   1.320    using \<open>mono f\<close> by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD)
   1.321  
   1.322  lemma mono_ccINF:
     2.1 --- a/src/HOL/Library/Extended_Nat.thy	Thu Feb 18 13:54:44 2016 +0100
     2.2 +++ b/src/HOL/Library/Extended_Nat.thy	Fri Feb 19 12:25:57 2016 +0100
     2.3 @@ -12,7 +12,6 @@
     2.4  class infinity =
     2.5    fixes infinity :: "'a"  ("\<infinity>")
     2.6  
     2.7 -
     2.8  subsection \<open>Type definition\<close>
     2.9  
    2.10  text \<open>
    2.11 @@ -26,7 +25,7 @@
    2.12  
    2.13  definition enat :: "nat \<Rightarrow> enat" where
    2.14    "enat n = Abs_enat (Some n)"
    2.15 - 
    2.16 +
    2.17  instantiation enat :: infinity
    2.18  begin
    2.19  
    2.20 @@ -40,7 +39,7 @@
    2.21    show "\<exists>to_nat::enat \<Rightarrow> nat. inj to_nat"
    2.22      by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject)
    2.23  qed
    2.24 - 
    2.25 +
    2.26  old_rep_datatype enat "\<infinity> :: enat"
    2.27  proof -
    2.28    fix P i assume "\<And>j. P (enat j)" "P \<infinity>"
    2.29 @@ -169,7 +168,7 @@
    2.30  lemma eSuc_plus_1:
    2.31    "eSuc n = n + 1"
    2.32    by (cases n) (simp_all add: eSuc_enat one_enat_def)
    2.33 -  
    2.34 +
    2.35  lemma plus_1_eSuc:
    2.36    "1 + q = eSuc q"
    2.37    "q + 1 = eSuc q"
    2.38 @@ -399,7 +398,7 @@
    2.39  
    2.40  lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m"
    2.41    by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
    2.42 - 
    2.43 +
    2.44  lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m"
    2.45    by (simp add: eSuc_def less_enat_def split: enat.splits)
    2.46  
    2.47 @@ -479,7 +478,7 @@
    2.48  lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
    2.49    by (simp add: eSuc_def split: enat.split)
    2.50  
    2.51 -lemma eSuc_Max: 
    2.52 +lemma eSuc_Max:
    2.53    assumes "finite A" "A \<noteq> {}"
    2.54    shows "eSuc (Max A) = Max (eSuc ` A)"
    2.55  using assms proof induction
     3.1 --- a/src/HOL/Library/Order_Continuity.thy	Thu Feb 18 13:54:44 2016 +0100
     3.2 +++ b/src/HOL/Library/Order_Continuity.thy	Fri Feb 19 12:25:57 2016 +0100
     3.3 @@ -393,12 +393,12 @@
     3.4  subsubsection \<open>Least fixed points in countable complete lattices\<close>
     3.5  
     3.6  definition (in countable_complete_lattice) cclfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
     3.7 -  where "cclfp f = (\<Squnion>i. (f ^^ i) \<bottom>)"
     3.8 +  where "cclfp f = (SUP i. (f ^^ i) bot)"
     3.9  
    3.10  lemma cclfp_unfold:
    3.11    assumes "sup_continuous F" shows "cclfp F = F (cclfp F)"
    3.12  proof -
    3.13 -  have "cclfp F = (\<Squnion>i. F ((F ^^ i) \<bottom>))"
    3.14 +  have "cclfp F = (SUP i. F ((F ^^ i) bot))"
    3.15      unfolding cclfp_def by (subst UNIV_nat_eq) auto
    3.16    also have "\<dots> = F (cclfp F)"
    3.17      unfolding cclfp_def
    3.18 @@ -409,7 +409,7 @@
    3.19  lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A \<le> A" shows "cclfp f \<le> A"
    3.20    unfolding cclfp_def
    3.21  proof (intro ccSUP_least)
    3.22 -  fix i show "(f ^^ i) \<bottom> \<le> A"
    3.23 +  fix i show "(f ^^ i) bot \<le> A"
    3.24    proof (induction i)
    3.25      case (Suc i) from monoD[OF f this] A show ?case
    3.26        by auto
    3.27 @@ -418,12 +418,12 @@
    3.28  
    3.29  lemma cclfp_transfer:
    3.30    assumes "sup_continuous \<alpha>" "mono f"
    3.31 -  assumes "\<alpha> \<bottom> = \<bottom>" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
    3.32 +  assumes "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
    3.33    shows "\<alpha> (cclfp f) = cclfp g"
    3.34  proof -
    3.35 -  have "\<alpha> (cclfp f) = (\<Squnion>i. \<alpha> ((f ^^ i) \<bottom>))"
    3.36 +  have "\<alpha> (cclfp f) = (SUP i. \<alpha> ((f ^^ i) bot))"
    3.37      unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono)
    3.38 -  moreover have "\<alpha> ((f ^^ i) \<bottom>) = (g ^^ i) \<bottom>" for i
    3.39 +  moreover have "\<alpha> ((f ^^ i) bot) = (g ^^ i) bot" for i
    3.40      by (induction i) (simp_all add: assms)
    3.41    ultimately show ?thesis
    3.42      by (simp add: cclfp_def)