# HG changeset patch # User hoelzl # Date 1455881157 -3600 # Node ID cb27a55d868a1e36f56cc8254ac5512e82fa2f15 # Parent ea7a442e9a5659e810ba779331df1eb9b09a3d19 remove lattice syntax from countable complete lattice diff -r ea7a442e9a56 -r cb27a55d868a src/HOL/Library/Countable_Complete_Lattices.thy --- a/src/HOL/Library/Countable_Complete_Lattices.thy Thu Feb 18 13:54:44 2016 +0100 +++ b/src/HOL/Library/Countable_Complete_Lattices.thy Fri Feb 19 12:25:57 2016 +0100 @@ -5,169 +5,169 @@ section \Countable Complete Lattices\ theory Countable_Complete_Lattices - imports Main Lattice_Syntax Countable_Set + imports Main Countable_Set begin lemma UNIV_nat_eq: "UNIV = insert 0 (range Suc)" by (metis UNIV_eq_I nat.nchotomy insertCI rangeI) class countable_complete_lattice = lattice + Inf + Sup + bot + top + - assumes ccInf_lower: "countable A \ x \ A \ \A \ x" - assumes ccInf_greatest: "countable A \ (\x. x \ A \ z \ x) \ z \ \A" - assumes ccSup_upper: "countable A \ x \ A \ x \ \A" - assumes ccSup_least: "countable A \ (\x. x \ A \ x \ z) \ \A \ z" - assumes ccInf_empty [simp]: "\{} = \" - assumes ccSup_empty [simp]: "\{} = \" + assumes ccInf_lower: "countable A \ x \ A \ Inf A \ x" + assumes ccInf_greatest: "countable A \ (\x. x \ A \ z \ x) \ z \ Inf A" + assumes ccSup_upper: "countable A \ x \ A \ x \ Sup A" + assumes ccSup_least: "countable A \ (\x. x \ A \ x \ z) \ Sup A \ z" + assumes ccInf_empty [simp]: "Inf {} = top" + assumes ccSup_empty [simp]: "Sup {} = bot" begin subclass bounded_lattice proof fix a - show "\ \ a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric]) - show "a \ \" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric]) + show "bot \ a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric]) + show "a \ top" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric]) qed -lemma ccINF_lower: "countable A \ i \ A \ (\i\A. f i) \ f i" +lemma ccINF_lower: "countable A \ i \ A \ (INF i :A. f i) \ f i" using ccInf_lower [of "f ` A"] by simp -lemma ccINF_greatest: "countable A \ (\i. i \ A \ u \ f i) \ u \ (\i\A. f i)" +lemma ccINF_greatest: "countable A \ (\i. i \ A \ u \ f i) \ u \ (INF i :A. f i)" using ccInf_greatest [of "f ` A"] by auto -lemma ccSUP_upper: "countable A \ i \ A \ f i \ (\i\A. f i)" +lemma ccSUP_upper: "countable A \ i \ A \ f i \ (SUP i :A. f i)" using ccSup_upper [of "f ` A"] by simp -lemma ccSUP_least: "countable A \ (\i. i \ A \ f i \ u) \ (\i\A. f i) \ u" +lemma ccSUP_least: "countable A \ (\i. i \ A \ f i \ u) \ (SUP i :A. f i) \ u" using ccSup_least [of "f ` A"] by auto -lemma ccInf_lower2: "countable A \ u \ A \ u \ v \ \A \ v" +lemma ccInf_lower2: "countable A \ u \ A \ u \ v \ Inf A \ v" using ccInf_lower [of A u] by auto -lemma ccINF_lower2: "countable A \ i \ A \ f i \ u \ (\i\A. f i) \ u" +lemma ccINF_lower2: "countable A \ i \ A \ f i \ u \ (INF i :A. f i) \ u" using ccINF_lower [of A i f] by auto -lemma ccSup_upper2: "countable A \ u \ A \ v \ u \ v \ \A" +lemma ccSup_upper2: "countable A \ u \ A \ v \ u \ v \ Sup A" using ccSup_upper [of A u] by auto -lemma ccSUP_upper2: "countable A \ i \ A \ u \ f i \ u \ (\i\A. f i)" +lemma ccSUP_upper2: "countable A \ i \ A \ u \ f i \ u \ (SUP i :A. f i)" using ccSUP_upper [of A i f] by auto -lemma le_ccInf_iff: "countable A \ b \ \A \ (\a\A. b \ a)" +lemma le_ccInf_iff: "countable A \ b \ Inf A \ (\a\A. b \ a)" by (auto intro: ccInf_greatest dest: ccInf_lower) -lemma le_ccINF_iff: "countable A \ u \ (\i\A. f i) \ (\i\A. u \ f i)" +lemma le_ccINF_iff: "countable A \ u \ (INF i :A. f i) \ (\i\A. u \ f i)" using le_ccInf_iff [of "f ` A"] by simp -lemma ccSup_le_iff: "countable A \ \A \ b \ (\a\A. a \ b)" +lemma ccSup_le_iff: "countable A \ Sup A \ b \ (\a\A. a \ b)" by (auto intro: ccSup_least dest: ccSup_upper) -lemma ccSUP_le_iff: "countable A \ (\i\A. f i) \ u \ (\i\A. f i \ u)" +lemma ccSUP_le_iff: "countable A \ (SUP i :A. f i) \ u \ (\i\A. f i \ u)" using ccSup_le_iff [of "f ` A"] by simp -lemma ccInf_insert [simp]: "countable A \ \insert a A = a \ \A" +lemma ccInf_insert [simp]: "countable A \ Inf (insert a A) = inf a (Inf A)" by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower) -lemma ccINF_insert [simp]: "countable A \ (\x\insert a A. f x) = f a \ INFIMUM A f" +lemma ccINF_insert [simp]: "countable A \ (INF x:insert a A. f x) = inf (f a) (INFIMUM A f)" unfolding image_insert by simp -lemma ccSup_insert [simp]: "countable A \ \insert a A = a \ \A" +lemma ccSup_insert [simp]: "countable A \ Sup (insert a A) = sup a (Sup A)" by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper) -lemma ccSUP_insert [simp]: "countable A \ (\x\insert a A. f x) = f a \ SUPREMUM A f" +lemma ccSUP_insert [simp]: "countable A \ (SUP x:insert a A. f x) = sup (f a) (SUPREMUM A f)" unfolding image_insert by simp -lemma ccINF_empty [simp]: "(\x\{}. f x) = \" +lemma ccINF_empty [simp]: "(INF x:{}. f x) = top" unfolding image_empty by simp -lemma ccSUP_empty [simp]: "(\x\{}. f x) = \" +lemma ccSUP_empty [simp]: "(SUP x:{}. f x) = bot" unfolding image_empty by simp -lemma ccInf_superset_mono: "countable A \ B \ A \ \A \ \B" +lemma ccInf_superset_mono: "countable A \ B \ A \ Inf A \ Inf B" by (auto intro: ccInf_greatest ccInf_lower countable_subset) -lemma ccSup_subset_mono: "countable B \ A \ B \ \A \ \B" +lemma ccSup_subset_mono: "countable B \ A \ B \ Sup A \ Sup B" by (auto intro: ccSup_least ccSup_upper countable_subset) lemma ccInf_mono: assumes [intro]: "countable B" "countable A" assumes "\b. b \ B \ \a\A. a \ b" - shows "\A \ \B" + shows "Inf A \ Inf B" proof (rule ccInf_greatest) fix b assume "b \ B" with assms obtain a where "a \ A" and "a \ b" by blast - from \a \ A\ have "\A \ a" by (rule ccInf_lower[rotated]) auto - with \a \ b\ show "\A \ b" by auto + from \a \ A\ have "Inf A \ a" by (rule ccInf_lower[rotated]) auto + with \a \ b\ show "Inf A \ b" by auto qed auto lemma ccINF_mono: - "countable A \ countable B \ (\m. m \ B \ \n\A. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)" + "countable A \ countable B \ (\m. m \ B \ \n\A. f n \ g m) \ (INF n:A. f n) \ (INF n:B. g n)" using ccInf_mono [of "g ` B" "f ` A"] by auto lemma ccSup_mono: assumes [intro]: "countable B" "countable A" assumes "\a. a \ A \ \b\B. a \ b" - shows "\A \ \B" + shows "Sup A \ Sup B" proof (rule ccSup_least) fix a assume "a \ A" with assms obtain b where "b \ B" and "a \ b" by blast - from \b \ B\ have "b \ \B" by (rule ccSup_upper[rotated]) auto - with \a \ b\ show "a \ \B" by auto + from \b \ B\ have "b \ Sup B" by (rule ccSup_upper[rotated]) auto + with \a \ b\ show "a \ Sup B" by auto qed auto lemma ccSUP_mono: - "countable A \ countable B \ (\n. n \ A \ \m\B. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)" + "countable A \ countable B \ (\n. n \ A \ \m\B. f n \ g m) \ (SUP n:A. f n) \ (SUP n:B. g n)" using ccSup_mono [of "g ` B" "f ` A"] by auto lemma ccINF_superset_mono: - "countable A \ B \ A \ (\x. x \ B \ f x \ g x) \ (\x\A. f x) \ (\x\B. g x)" + "countable A \ B \ A \ (\x. x \ B \ f x \ g x) \ (INF x:A. f x) \ (INF x:B. g x)" by (blast intro: ccINF_mono countable_subset dest: subsetD) lemma ccSUP_subset_mono: - "countable B \ A \ B \ (\x. x \ A \ f x \ g x) \ (\x\A. f x) \ (\x\B. g x)" + "countable B \ A \ B \ (\x. x \ A \ f x \ g x) \ (SUP x:A. f x) \ (SUP x:B. g x)" by (blast intro: ccSUP_mono countable_subset dest: subsetD) -lemma less_eq_ccInf_inter: "countable A \ countable B \ \A \ \B \ \(A \ B)" +lemma less_eq_ccInf_inter: "countable A \ countable B \ sup (Inf A) (Inf B) \ Inf (A \ B)" by (auto intro: ccInf_greatest ccInf_lower) -lemma ccSup_inter_less_eq: "countable A \ countable B \ \(A \ B) \ \A \ \B " +lemma ccSup_inter_less_eq: "countable A \ countable B \ Sup (A \ B) \ inf (Sup A) (Sup B)" by (auto intro: ccSup_least ccSup_upper) -lemma ccInf_union_distrib: "countable A \ countable B \ \(A \ B) = \A \ \B" +lemma ccInf_union_distrib: "countable A \ countable B \ Inf (A \ B) = inf (Inf A) (Inf B)" by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2) lemma ccINF_union: - "countable A \ countable B \ (\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)" + "countable A \ countable B \ (INF i:A \ B. M i) = inf (INF i:A. M i) (INF i:B. M i)" by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower) -lemma ccSup_union_distrib: "countable A \ countable B \ \(A \ B) = \A \ \B" +lemma ccSup_union_distrib: "countable A \ countable B \ Sup (A \ B) = sup (Sup A) (Sup B)" by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2) lemma ccSUP_union: - "countable A \ countable B \ (\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)" + "countable A \ countable B \ (SUP i:A \ B. M i) = sup (SUP i:A. M i) (SUP i:B. M i)" by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper) -lemma ccINF_inf_distrib: "countable A \ (\a\A. f a) \ (\a\A. g a) = (\a\A. f a \ g a)" +lemma ccINF_inf_distrib: "countable A \ inf (INF a:A. f a) (INF a:A. g a) = (INF a:A. inf (f a) (g a))" by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono) -lemma ccSUP_sup_distrib: "countable A \ (\a\A. f a) \ (\a\A. g a) = (\a\A. f a \ g a)" +lemma ccSUP_sup_distrib: "countable A \ sup (SUP a:A. f a) (SUP a:A. g a) = (SUP a:A. sup (f a) (g a))" by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono) -lemma ccINF_const [simp]: "A \ {} \ (\i\A. f) = f" +lemma ccINF_const [simp]: "A \ {} \ (INF i :A. f) = f" unfolding image_constant_conv by auto -lemma ccSUP_const [simp]: "A \ {} \ (\i\A. f) = f" +lemma ccSUP_const [simp]: "A \ {} \ (SUP i :A. f) = f" unfolding image_constant_conv by auto -lemma ccINF_top [simp]: "(\x\A. \) = \" +lemma ccINF_top [simp]: "(INF x:A. top) = top" by (cases "A = {}") simp_all -lemma ccSUP_bot [simp]: "(\x\A. \) = \" +lemma ccSUP_bot [simp]: "(SUP x:A. bot) = bot" by (cases "A = {}") simp_all -lemma ccINF_commute: "countable A \ countable B \ (\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)" +lemma ccINF_commute: "countable A \ countable B \ (INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)" by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym) -lemma ccSUP_commute: "countable A \ countable B \ (\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)" +lemma ccSUP_commute: "countable A \ countable B \ (SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)" by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym) end @@ -176,62 +176,64 @@ fixes a :: "'a::{countable_complete_lattice, linorder}" begin -lemma less_ccSup_iff: "countable S \ a < \S \ (\x\S. a < x)" +lemma less_ccSup_iff: "countable S \ a < Sup S \ (\x\S. a < x)" unfolding not_le [symmetric] by (subst ccSup_le_iff) auto -lemma less_ccSUP_iff: "countable A \ a < (\i\A. f i) \ (\x\A. a < f x)" +lemma less_ccSUP_iff: "countable A \ a < (SUP i:A. f i) \ (\x\A. a < f x)" using less_ccSup_iff [of "f ` A"] by simp -lemma ccInf_less_iff: "countable S \ \S < a \ (\x\S. x < a)" +lemma ccInf_less_iff: "countable S \ Inf S < a \ (\x\S. x < a)" unfolding not_le [symmetric] by (subst le_ccInf_iff) auto -lemma ccINF_less_iff: "countable A \ (\i\A. f i) < a \ (\x\A. f x < a)" +lemma ccINF_less_iff: "countable A \ (INF i:A. f i) < a \ (\x\A. f x < a)" using ccInf_less_iff [of "f ` A"] by simp end class countable_complete_distrib_lattice = countable_complete_lattice + - assumes sup_ccInf: "countable B \ a \ \B = (\b\B. a \ b)" - assumes inf_ccSup: "countable B \ a \ \B = (\b\B. a \ b)" + assumes sup_ccInf: "countable B \ sup a (Inf B) = (INF b:B. sup a b)" + assumes inf_ccSup: "countable B \ inf a (Sup B) = (SUP b:B. inf a b)" begin lemma sup_ccINF: - "countable B \ a \ (\b\B. f b) = (\b\B. a \ f b)" + "countable B \ sup a (INF b:B. f b) = (INF b:B. sup a (f b))" by (simp only: sup_ccInf image_image countable_image) lemma inf_ccSUP: - "countable B \ a \ (\b\B. f b) = (\b\B. a \ f b)" + "countable B \ inf a (SUP b:B. f b) = (SUP b:B. inf a (f b))" by (simp only: inf_ccSup image_image countable_image) -subclass distrib_lattice proof +subclass distrib_lattice +proof fix a b c - from sup_ccInf[of "{b, c}" a] have "a \ \{b, c} = (\d\{b, c}. a \ d)" + from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d:{b, c}. sup a d)" by simp - then show "a \ b \ c = (a \ b) \ (a \ c)" by simp + then show "sup a (inf b c) = inf (sup a b) (sup a c)" + by simp qed lemma ccInf_sup: - "countable B \ \B \ a = (\b\B. b \ a)" + "countable B \ sup (Inf B) a = (INF b:B. sup b a)" by (simp add: sup_ccInf sup_commute) lemma ccSup_inf: - "countable B \ \B \ a = (\b\B. b \ a)" + "countable B \ inf (Sup B) a = (SUP b:B. inf b a)" by (simp add: inf_ccSup inf_commute) lemma ccINF_sup: - "countable B \ (\b\B. f b) \ a = (\b\B. f b \ a)" + "countable B \ sup (INF b:B. f b) a = (INF b:B. sup (f b) a)" by (simp add: sup_ccINF sup_commute) lemma ccSUP_inf: - "countable B \ (\b\B. f b) \ a = (\b\B. f b \ a)" + "countable B \ inf (SUP b:B. f b) a = (SUP b:B. inf (f b) a)" by (simp add: inf_ccSUP inf_commute) lemma ccINF_sup_distrib2: - "countable A \ countable B \ (\a\A. f a) \ (\b\B. g b) = (\a\A. \b\B. f a \ g b)" + "countable A \ countable B \ sup (INF a:A. f a) (INF b:B. g b) = (INF a:A. INF b:B. sup (f a) (g b))" by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup) lemma ccSUP_inf_distrib2: - "countable A \ countable B \ (\a\A. f a) \ (\b\B. g b) = (\a\A. \b\B. f a \ g b)" + "countable A \ countable B \ inf (SUP a:A. f a) (SUP b:B. g b) = (SUP a:A. SUP b:B. inf (f a) (g b))" by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf) context @@ -240,12 +242,12 @@ begin lemma mono_ccInf: - "countable A \ f (\A) \ (\x\A. f x)" + "countable A \ f (Inf A) \ (INF x:A. f x)" using \mono f\ by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD) lemma mono_ccSup: - "countable A \ (\x\A. f x) \ f (\A)" + "countable A \ (SUP x:A. f x) \ f (Sup A)" using \mono f\ by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD) lemma mono_ccINF: diff -r ea7a442e9a56 -r cb27a55d868a src/HOL/Library/Extended_Nat.thy --- a/src/HOL/Library/Extended_Nat.thy Thu Feb 18 13:54:44 2016 +0100 +++ b/src/HOL/Library/Extended_Nat.thy Fri Feb 19 12:25:57 2016 +0100 @@ -12,7 +12,6 @@ class infinity = fixes infinity :: "'a" ("\") - subsection \Type definition\ text \ @@ -26,7 +25,7 @@ definition enat :: "nat \ enat" where "enat n = Abs_enat (Some n)" - + instantiation enat :: infinity begin @@ -40,7 +39,7 @@ show "\to_nat::enat \ nat. inj to_nat" by (rule exI[of _ "to_nat \ Rep_enat"]) (simp add: inj_on_def Rep_enat_inject) qed - + old_rep_datatype enat "\ :: enat" proof - fix P i assume "\j. P (enat j)" "P \" @@ -169,7 +168,7 @@ lemma eSuc_plus_1: "eSuc n = n + 1" by (cases n) (simp_all add: eSuc_enat one_enat_def) - + lemma plus_1_eSuc: "1 + q = eSuc q" "q + 1 = eSuc q" @@ -399,7 +398,7 @@ lemma eSuc_ile_mono [simp]: "eSuc n \ eSuc m \ n \ m" by (simp add: eSuc_def less_eq_enat_def split: enat.splits) - + lemma eSuc_mono [simp]: "eSuc n < eSuc m \ n < m" by (simp add: eSuc_def less_enat_def split: enat.splits) @@ -479,7 +478,7 @@ lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)" by (simp add: eSuc_def split: enat.split) -lemma eSuc_Max: +lemma eSuc_Max: assumes "finite A" "A \ {}" shows "eSuc (Max A) = Max (eSuc ` A)" using assms proof induction diff -r ea7a442e9a56 -r cb27a55d868a src/HOL/Library/Order_Continuity.thy --- a/src/HOL/Library/Order_Continuity.thy Thu Feb 18 13:54:44 2016 +0100 +++ b/src/HOL/Library/Order_Continuity.thy Fri Feb 19 12:25:57 2016 +0100 @@ -393,12 +393,12 @@ subsubsection \Least fixed points in countable complete lattices\ definition (in countable_complete_lattice) cclfp :: "('a \ 'a) \ 'a" - where "cclfp f = (\i. (f ^^ i) \)" + where "cclfp f = (SUP i. (f ^^ i) bot)" lemma cclfp_unfold: assumes "sup_continuous F" shows "cclfp F = F (cclfp F)" proof - - have "cclfp F = (\i. F ((F ^^ i) \))" + have "cclfp F = (SUP i. F ((F ^^ i) bot))" unfolding cclfp_def by (subst UNIV_nat_eq) auto also have "\ = F (cclfp F)" unfolding cclfp_def @@ -409,7 +409,7 @@ lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A \ A" shows "cclfp f \ A" unfolding cclfp_def proof (intro ccSUP_least) - fix i show "(f ^^ i) \ \ A" + fix i show "(f ^^ i) bot \ A" proof (induction i) case (Suc i) from monoD[OF f this] A show ?case by auto @@ -418,12 +418,12 @@ lemma cclfp_transfer: assumes "sup_continuous \" "mono f" - assumes "\ \ = \" "\x. \ (f x) = g (\ x)" + assumes "\ bot = bot" "\x. \ (f x) = g (\ x)" shows "\ (cclfp f) = cclfp g" proof - - have "\ (cclfp f) = (\i. \ ((f ^^ i) \))" + have "\ (cclfp f) = (SUP i. \ ((f ^^ i) bot))" unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono) - moreover have "\ ((f ^^ i) \) = (g ^^ i) \" for i + moreover have "\ ((f ^^ i) bot) = (g ^^ i) bot" for i by (induction i) (simp_all add: assms) ultimately show ?thesis by (simp add: cclfp_def)