# HG changeset patch # User hoelzl # Date 1455800084 -3600 # Node ID ea7a442e9a5659e810ba779331df1eb9b09a3d19 # Parent 4fe872ff91bfa0d4b5026adb751703c8c3e128e5 add countable complete lattices diff -r 4fe872ff91bf -r ea7a442e9a56 src/HOL/Library/Countable_Complete_Lattices.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Countable_Complete_Lattices.thy Thu Feb 18 13:54:44 2016 +0100 @@ -0,0 +1,275 @@ +(* Title: HOL/Library/Countable_Complete_Lattices.thy + Author: Johannes Hölzl +*) + +section \Countable Complete Lattices\ + +theory Countable_Complete_Lattices + imports Main Lattice_Syntax 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]: "\{} = \" +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]) +qed + +lemma ccINF_lower: "countable A \ i \ A \ (\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)" + using ccInf_greatest [of "f ` A"] by auto + +lemma ccSUP_upper: "countable A \ i \ A \ f i \ (\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" + using ccSup_least [of "f ` A"] by auto + +lemma ccInf_lower2: "countable A \ u \ A \ u \ v \ \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" + using ccINF_lower [of A i f] by auto + +lemma ccSup_upper2: "countable A \ u \ A \ v \ u \ v \ \A" + using ccSup_upper [of A u] by auto + +lemma ccSUP_upper2: "countable A \ i \ A \ u \ f i \ u \ (\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)" + by (auto intro: ccInf_greatest dest: ccInf_lower) + +lemma le_ccINF_iff: "countable A \ u \ (\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)" + by (auto intro: ccSup_least dest: ccSup_upper) + +lemma ccSUP_le_iff: "countable A \ (\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" + 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" + unfolding image_insert by simp + +lemma ccSup_insert [simp]: "countable A \ \insert a A = a \ \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" + unfolding image_insert by simp + +lemma ccINF_empty [simp]: "(\x\{}. f x) = \" + unfolding image_empty by simp + +lemma ccSUP_empty [simp]: "(\x\{}. f x) = \" + unfolding image_empty by simp + +lemma ccInf_superset_mono: "countable A \ B \ A \ \A \ \B" + by (auto intro: ccInf_greatest ccInf_lower countable_subset) + +lemma ccSup_subset_mono: "countable B \ A \ B \ \A \ \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" +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 +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)" + 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" +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 +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)" + 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)" + 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)" + by (blast intro: ccSUP_mono countable_subset dest: subsetD) + + +lemma less_eq_ccInf_inter: "countable A \ countable B \ \A \ \B \ \(A \ B)" + by (auto intro: ccInf_greatest ccInf_lower) + +lemma ccSup_inter_less_eq: "countable A \ countable B \ \(A \ B) \ \A \ \B " + by (auto intro: ccSup_least ccSup_upper) + +lemma ccInf_union_distrib: "countable A \ countable B \ \(A \ B) = \A \ \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)" + 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" + 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)" + 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)" + 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)" + 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" + unfolding image_constant_conv by auto + +lemma ccSUP_const [simp]: "A \ {} \ (\i\A. f) = f" + unfolding image_constant_conv by auto + +lemma ccINF_top [simp]: "(\x\A. \) = \" + by (cases "A = {}") simp_all + +lemma ccSUP_bot [simp]: "(\x\A. \) = \" + 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)" + 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)" + by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym) + +end + +context + fixes a :: "'a::{countable_complete_lattice, linorder}" +begin + +lemma less_ccSup_iff: "countable S \ a < \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)" + using less_ccSup_iff [of "f ` A"] by simp + +lemma ccInf_less_iff: "countable S \ \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)" + 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)" +begin + +lemma sup_ccINF: + "countable B \ a \ (\b\B. f b) = (\b\B. 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)" + by (simp only: inf_ccSup image_image countable_image) + +subclass distrib_lattice proof + fix a b c + from sup_ccInf[of "{b, c}" a] have "a \ \{b, c} = (\d\{b, c}. a \ d)" + by simp + then show "a \ b \ c = (a \ b) \ (a \ c)" by simp +qed + +lemma ccInf_sup: + "countable B \ \B \ a = (\b\B. b \ a)" + by (simp add: sup_ccInf sup_commute) + +lemma ccSup_inf: + "countable B \ \B \ a = (\b\B. b \ a)" + by (simp add: inf_ccSup inf_commute) + +lemma ccINF_sup: + "countable B \ (\b\B. f b) \ a = (\b\B. 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)" + 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)" + 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)" + by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf) + +context + fixes f :: "'a \ 'b::countable_complete_lattice" + assumes "mono f" +begin + +lemma mono_ccInf: + "countable A \ f (\A) \ (\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)" + using \mono f\ by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD) + +lemma mono_ccINF: + "countable I \ f (INF i : I. A i) \ (INF x : I. f (A x))" + by (intro countable_complete_lattice_class.ccINF_greatest monoD[OF \mono f\] ccINF_lower) + +lemma mono_ccSUP: + "countable I \ (SUP x : I. f (A x)) \ f (SUP i : I. A i)" + by (intro countable_complete_lattice_class.ccSUP_least monoD[OF \mono f\] ccSUP_upper) + +end + +end + +subsubsection \Instances of countable complete lattices\ + +instance "fun" :: (type, countable_complete_lattice) countable_complete_lattice + by standard + (auto simp: le_fun_def intro!: ccSUP_upper ccSUP_least ccINF_lower ccINF_greatest) + +subclass (in complete_lattice) countable_complete_lattice + by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) + +subclass (in complete_distrib_lattice) countable_complete_distrib_lattice + by standard (auto intro: sup_Inf inf_Sup) + +end \ No newline at end of file diff -r 4fe872ff91bf -r ea7a442e9a56 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Tue Feb 09 07:04:48 2016 +0100 +++ b/src/HOL/Library/Library.thy Thu Feb 18 13:54:44 2016 +0100 @@ -12,6 +12,7 @@ ContNotDenum Convex Countable + Countable_Complete_Lattices Countable_Set_Type Debug Diagonal_Subsequence diff -r 4fe872ff91bf -r ea7a442e9a56 src/HOL/Library/Order_Continuity.thy --- a/src/HOL/Library/Order_Continuity.thy Tue Feb 09 07:04:48 2016 +0100 +++ b/src/HOL/Library/Order_Continuity.thy Thu Feb 18 13:54:44 2016 +0100 @@ -1,30 +1,31 @@ (* Title: HOL/Library/Order_Continuity.thy - Author: David von Oheimb, TU Muenchen + Author: David von Oheimb, TU München + Author: Johannes Hölzl, TU München *) -section \Continuity and iterations (of set transformers)\ +section \Continuity and iterations\ theory Order_Continuity -imports Complex_Main +imports Complex_Main Countable_Complete_Lattices begin (* TODO: Generalize theory to chain-complete partial orders *) lemma SUP_nat_binary: - "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)" - apply (auto intro!: antisym SUP_least) - apply (rule SUP_upper2[where i=0]) + "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::countable_complete_lattice)" + apply (auto intro!: antisym ccSUP_least) + apply (rule ccSUP_upper2[where i=0]) apply simp_all - apply (rule SUP_upper2[where i=1]) + apply (rule ccSUP_upper2[where i=1]) apply simp_all done lemma INF_nat_binary: - "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)" - apply (auto intro!: antisym INF_greatest) - apply (rule INF_lower2[where i=0]) + "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::countable_complete_lattice)" + apply (auto intro!: antisym ccINF_greatest) + apply (rule ccINF_lower2[where i=0]) apply simp_all - apply (rule INF_lower2[where i=1]) + apply (rule ccINF_lower2[where i=1]) apply simp_all done @@ -39,7 +40,8 @@ subsection \Continuity for complete lattices\ definition - sup_continuous :: "('a::complete_lattice \ 'b::complete_lattice) \ bool" where + sup_continuous :: "('a::countable_complete_lattice \ 'b::countable_complete_lattice) \ bool" +where "sup_continuous F \ (\M::nat \ 'a. mono M \ F (SUP i. M i) = (SUP i. F (M i)))" lemma sup_continuousD: "sup_continuous F \ mono M \ F (SUP i::nat. M i) = (SUP i. F (M i))" @@ -79,26 +81,26 @@ lemma sup_continuous_sup[order_continuous_intros]: "sup_continuous f \ sup_continuous g \ sup_continuous (\x. sup (f x) (g x))" - by (simp add: sup_continuous_def SUP_sup_distrib) + by (simp add: sup_continuous_def ccSUP_sup_distrib) lemma sup_continuous_inf[order_continuous_intros]: - fixes P Q :: "'a :: complete_lattice \ 'b :: complete_distrib_lattice" + fixes P Q :: "'a :: countable_complete_lattice \ 'b :: countable_complete_distrib_lattice" assumes P: "sup_continuous P" and Q: "sup_continuous Q" shows "sup_continuous (\x. inf (P x) (Q x))" unfolding sup_continuous_def proof (safe intro!: antisym) fix M :: "nat \ 'a" assume M: "incseq M" have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \ (SUP j i. inf (P (M i)) (Q (M j)))" - unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_SUP SUP_inf .. + by (simp add: sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_ccSUP ccSUP_inf) also have "\ \ (SUP i. inf (P (M i)) (Q (M i)))" - proof (intro SUP_least) + proof (intro ccSUP_least) fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j)) \ (SUP i. inf (P (M i)) (Q (M i)))" - by (intro SUP_upper2[of "sup i j"] inf_mono) (auto simp: mono_def) - qed + by (intro ccSUP_upper2[of _ "sup i j"] inf_mono) (auto simp: mono_def) + qed auto finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \ (SUP i. inf (P (M i)) (Q (M i)))" . - + show "(SUP i. inf (P (M i)) (Q (M i))) \ inf (P (SUP i. M i)) (Q (SUP i. M i))" - unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro SUP_least inf_mono SUP_upper) + unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro ccSUP_least inf_mono ccSUP_upper) auto qed lemma sup_continuous_and[order_continuous_intros]: @@ -203,7 +205,8 @@ by (rule lfp_transfer_bounded[where P=top]) (auto dest: sup_continuousD) definition - inf_continuous :: "('a::complete_lattice \ 'b::complete_lattice) \ bool" where + inf_continuous :: "('a::countable_complete_lattice \ 'b::countable_complete_lattice) \ bool" +where "inf_continuous F \ (\M::nat \ 'a. antimono M \ F (INF i. M i) = (INF i. F (M i)))" lemma inf_continuousD: "inf_continuous F \ antimono M \ F (INF i::nat. M i) = (INF i. F (M i))" @@ -231,25 +234,25 @@ lemma inf_continuous_inf[order_continuous_intros]: "inf_continuous f \ inf_continuous g \ inf_continuous (\x. inf (f x) (g x))" - by (simp add: inf_continuous_def INF_inf_distrib) + by (simp add: inf_continuous_def ccINF_inf_distrib) lemma inf_continuous_sup[order_continuous_intros]: - fixes P Q :: "'a :: complete_lattice \ 'b :: complete_distrib_lattice" + fixes P Q :: "'a :: countable_complete_lattice \ 'b :: countable_complete_distrib_lattice" assumes P: "inf_continuous P" and Q: "inf_continuous Q" shows "inf_continuous (\x. sup (P x) (Q x))" unfolding inf_continuous_def proof (safe intro!: antisym) fix M :: "nat \ 'a" assume M: "decseq M" show "sup (P (INF i. M i)) (Q (INF i. M i)) \ (INF i. sup (P (M i)) (Q (M i)))" - unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro INF_greatest sup_mono INF_lower) + unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro ccINF_greatest sup_mono ccINF_lower) auto have "(INF i. sup (P (M i)) (Q (M i))) \ (INF j i. sup (P (M i)) (Q (M j)))" - proof (intro INF_greatest) + proof (intro ccINF_greatest) fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j)) \ (INF i. sup (P (M i)) (Q (M i)))" - by (intro INF_lower2[of "sup i j"] sup_mono) (auto simp: mono_def antimono_def) - qed + by (intro ccINF_lower2[of _ "sup i j"] sup_mono) (auto simp: mono_def antimono_def) + qed auto also have "\ \ sup (P (INF i. M i)) (Q (INF i. M i))" - unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] INF_sup sup_INF .. + by (simp add: inf_continuousD[OF P M] inf_continuousD[OF Q M] ccINF_sup sup_ccINF) finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \ (INF i. sup (P (M i)) (Q (M i)))" . qed @@ -348,7 +351,7 @@ using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"] unfolding funpow_Suc_right by simp qed - + have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))" unfolding inf_continuous_gfp[OF f] proof (rule INF_eq) @@ -387,4 +390,43 @@ qed (auto intro: Inf_greatest) qed +subsubsection \Least fixed points in countable complete lattices\ + +definition (in countable_complete_lattice) cclfp :: "('a \ 'a) \ 'a" + where "cclfp f = (\i. (f ^^ i) \)" + +lemma cclfp_unfold: + assumes "sup_continuous F" shows "cclfp F = F (cclfp F)" +proof - + have "cclfp F = (\i. F ((F ^^ i) \))" + unfolding cclfp_def by (subst UNIV_nat_eq) auto + also have "\ = F (cclfp F)" + unfolding cclfp_def + by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono) + finally show ?thesis . +qed + +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" + proof (induction i) + case (Suc i) from monoD[OF f this] A show ?case + by auto + qed simp +qed simp + +lemma cclfp_transfer: + assumes "sup_continuous \" "mono f" + assumes "\ \ = \" "\x. \ (f x) = g (\ x)" + shows "\ (cclfp f) = cclfp g" +proof - + have "\ (cclfp f) = (\i. \ ((f ^^ i) \))" + unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono) + moreover have "\ ((f ^^ i) \) = (g ^^ i) \" for i + by (induction i) (simp_all add: assms) + ultimately show ?thesis + by (simp add: cclfp_def) +qed + end