# HG changeset patch # User haftmann # Date 1552553169 -3600 # Node ID 5382f5691a11f66a0cc755c766c983fb1a059ec1 # Parent 1bd74a0944b3d0f0c5f4bf80ee7e56e5894aeec7 proper theory for type of dual ordered lattice in distribution diff -r 1bd74a0944b3 -r 5382f5691a11 src/HOL/Library/Dual_Ordered_Lattice.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Dual_Ordered_Lattice.thy Thu Mar 14 09:46:09 2019 +0100 @@ -0,0 +1,391 @@ +(* Title: Dual_Ordered_Lattice.thy + Authors: Makarius; Peter Gammie; Brian Huffman; Florian Haftmann, TU Muenchen +*) + +section \Type of dual ordered lattices\ + +theory Dual_Ordered_Lattice +imports Main +begin + +text \ + The \<^emph>\dual\ of an ordered structure is an isomorphic copy of the + underlying type, with the \\\ relation defined as the inverse + of the original one. + + The class of lattices is closed under formation of dual structures. + This means that for any theorem of lattice theory, the dualized + statement holds as well; this important fact simplifies many proofs + of lattice theory. +\ + +typedef 'a dual = "UNIV :: 'a set" + morphisms undual dual .. + +setup_lifting type_definition_dual + +lemma dual_eqI: + "x = y" if "undual x = undual y" + using that by transfer assumption + +lemma dual_eq_iff: + "x = y \ undual x = undual y" + by transfer simp + +lemma eq_dual_iff [iff]: + "dual x = dual y \ x = y" + by transfer simp + +lemma undual_dual [simp]: + "undual (dual x) = x" + by transfer rule + +lemma dual_undual [simp]: + "dual (undual x) = x" + by transfer rule + +lemma undual_comp_dual [simp]: + "undual \ dual = id" + by (simp add: fun_eq_iff) + +lemma dual_comp_undual [simp]: + "dual \ undual = id" + by (simp add: fun_eq_iff) + +lemma inj_dual: + "inj dual" + by (rule injI) simp + +lemma inj_undual: + "inj undual" + by (rule injI) (rule dual_eqI) + +lemma surj_dual: + "surj dual" + by (rule surjI [of _ undual]) simp + +lemma surj_undual: + "surj undual" + by (rule surjI [of _ dual]) simp + +lemma bij_dual: + "bij dual" + using inj_dual surj_dual by (rule bijI) + +lemma bij_undual: + "bij undual" + using inj_undual surj_undual by (rule bijI) + +instance dual :: (finite) finite +proof + from finite have "finite (range dual :: 'a dual set)" + by (rule finite_imageI) + then show "finite (UNIV :: 'a dual set)" + by (simp add: surj_dual) +qed + + +subsection \Pointwise ordering\ + +instantiation dual :: (ord) ord +begin + +lift_definition less_eq_dual :: "'a dual \ 'a dual \ bool" + is "(\)" . + +lift_definition less_dual :: "'a dual \ 'a dual \ bool" + is "(>)" . + +instance .. + +end + +lemma dual_less_eqI: + "x \ y" if "undual y \ undual x" + using that by transfer assumption + +lemma dual_less_eq_iff: + "x \ y \ undual y \ undual x" + by transfer simp + +lemma less_eq_dual_iff [iff]: + "dual x \ dual y \ y \ x" + by transfer simp + +lemma dual_lessI: + "x < y" if "undual y < undual x" + using that by transfer assumption + +lemma dual_less_iff: + "x < y \ undual y < undual x" + by transfer simp + +lemma less_dual_iff [iff]: + "dual x < dual y \ y < x" + by transfer simp + +instance dual :: (preorder) preorder + by (standard; transfer) (auto simp add: less_le_not_le intro: order_trans) + +instance dual :: (order) order + by (standard; transfer) simp + + +subsection \Binary infimum and supremum\ + +instantiation dual :: (sup) inf +begin + +lift_definition inf_dual :: "'a dual \ 'a dual \ 'a dual" + is sup . + +instance .. + +end + +lemma undual_inf_eq [simp]: + "undual (inf x y) = sup (undual x) (undual y)" + by (fact inf_dual.rep_eq) + +lemma dual_sup_eq [simp]: + "dual (sup x y) = inf (dual x) (dual y)" + by transfer rule + +instantiation dual :: (inf) sup +begin + +lift_definition sup_dual :: "'a dual \ 'a dual \ 'a dual" + is inf . + +instance .. + +end + +lemma undual_sup_eq [simp]: + "undual (sup x y) = inf (undual x) (undual y)" + by (fact sup_dual.rep_eq) + +lemma dual_inf_eq [simp]: + "dual (inf x y) = sup (dual x) (dual y)" + by transfer simp + +instance dual :: (semilattice_sup) semilattice_inf + by (standard; transfer) simp_all + +instance dual :: (semilattice_inf) semilattice_sup + by (standard; transfer) simp_all + +instance dual :: (lattice) lattice .. + +instance dual :: (distrib_lattice) distrib_lattice + by (standard; transfer) (fact inf_sup_distrib1) + + +subsection \Top and bottom elements\ + +instantiation dual :: (top) bot +begin + +lift_definition bot_dual :: "'a dual" + is top . + +instance .. + +end + +lemma undual_bot_eq [simp]: + "undual bot = top" + by (fact bot_dual.rep_eq) + +lemma dual_top_eq [simp]: + "dual top = bot" + by transfer rule + +instantiation dual :: (bot) top +begin + +lift_definition top_dual :: "'a dual" + is bot . + +instance .. + +end + +lemma undual_top_eq [simp]: + "undual top = bot" + by (fact top_dual.rep_eq) + +lemma dual_bot_eq [simp]: + "dual bot = top" + by transfer rule + +instance dual :: (order_top) order_bot + by (standard; transfer) simp + +instance dual :: (order_bot) order_top + by (standard; transfer) simp + +instance dual :: (bounded_lattice_top) bounded_lattice_bot .. + +instance dual :: (bounded_lattice_bot) bounded_lattice_top .. + +instance dual :: (bounded_lattice) bounded_lattice .. + + +subsection \Complement\ + +instantiation dual :: (uminus) uminus +begin + +lift_definition uminus_dual :: "'a dual \ 'a dual" + is uminus . + +instance .. + +end + +lemma undual_uminus_eq [simp]: + "undual (- x) = - undual x" + by (fact uminus_dual.rep_eq) + +lemma dual_uminus_eq [simp]: + "dual (- x) = - dual x" + by transfer rule + +instantiation dual :: (boolean_algebra) boolean_algebra +begin + +lift_definition minus_dual :: "'a dual \ 'a dual \ 'a dual" + is "\x y. - (y - x)" . + +instance + by (standard; transfer) (simp_all add: diff_eq ac_simps) + +end + +lemma undual_minus_eq [simp]: + "undual (x - y) = - (undual y - undual x)" + by (fact minus_dual.rep_eq) + +lemma dual_minus_eq [simp]: + "dual (x - y) = - (dual y - dual x)" + by transfer simp + + +subsection \Complete lattice operations\ + +text \ + The class of complete lattices is closed under formation of dual + structures. +\ + +instantiation dual :: (Sup) Inf +begin + +lift_definition Inf_dual :: "'a dual set \ 'a dual" + is Sup . + +instance .. + +end + +lemma undual_Inf_eq [simp]: + "undual (Inf A) = Sup (undual ` A)" + by (fact Inf_dual.rep_eq) + +lemma dual_Sup_eq [simp]: + "dual (Sup A) = Inf (dual ` A)" + by transfer simp + +instantiation dual :: (Inf) Sup +begin + +lift_definition Sup_dual :: "'a dual set \ 'a dual" + is Inf . + +instance .. + +end + +lemma undual_Sup_eq [simp]: + "undual (Sup A) = Inf (undual ` A)" + by (fact Sup_dual.rep_eq) + +lemma dual_Inf_eq [simp]: + "dual (Inf A) = Sup (dual ` A)" + by transfer simp + +instance dual :: (complete_lattice) complete_lattice + by (standard; transfer) (auto intro: Inf_lower Sup_upper Inf_greatest Sup_least) + +context + fixes f :: "'a::complete_lattice \ 'a" + and g :: "'a dual \ 'a dual" + assumes "mono f" + defines "g \ dual \ f \ undual" +begin + +private lemma mono_dual: + "mono g" +proof + fix x y :: "'a dual" + assume "x \ y" + then have "undual y \ undual x" + by (simp add: dual_less_eq_iff) + with \mono f\ have "f (undual y) \ f (undual x)" + by (rule monoD) + then have "(dual \ f \ undual) x \ (dual \ f \ undual) y" + by simp + then show "g x \ g y" + by (simp add: g_def) +qed + +lemma lfp_dual_gfp: + "lfp f = undual (gfp g)" (is "?lhs = ?rhs") +proof (rule antisym) + have "dual (undual (g (gfp g))) \ dual (f (undual (gfp g)))" + by (simp add: g_def) + with mono_dual have "f (undual (gfp g)) \ undual (gfp g)" + by (simp add: gfp_unfold [where f = g, symmetric] dual_less_eq_iff) + then show "?lhs \ ?rhs" + by (rule lfp_lowerbound) + from \mono f\ have "dual (lfp f) \ dual (undual (gfp g))" + by (simp add: lfp_fixpoint gfp_upperbound g_def) + then show "?rhs \ ?lhs" + by (simp only: less_eq_dual_iff) +qed + +lemma gfp_dual_lfp: + "gfp f = undual (lfp g)" +proof - + have "mono (\x. undual (undual x))" + by (rule monoI) (simp add: dual_less_eq_iff) + moreover have "mono (\a. dual (dual (f a)))" + using \mono f\ by (auto intro: monoI dest: monoD) + moreover have "gfp f = gfp (\x. undual (undual (dual (dual (f x)))))" + by simp + ultimately have "undual (undual (gfp (\x. dual + (dual (f (undual (undual x))))))) = + gfp (\x. undual (undual (dual (dual (f x)))))" + by (subst gfp_rolling [where g = "\x. undual (undual x)"]) simp_all + then have "gfp f = + undual + (undual + (gfp (\x. dual (dual (f (undual (undual x)))))))" + by simp + also have "\ = undual (undual (gfp (dual \ g \ undual)))" + by (simp add: comp_def g_def) + also have "\ = undual (lfp g)" + using mono_dual by (simp only: Dual_Ordered_Lattice.lfp_dual_gfp) + finally show ?thesis . +qed + +end + + +text \Finally\ + +lifting_update dual.lifting +lifting_forget dual.lifting + +end diff -r 1bd74a0944b3 -r 5382f5691a11 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Thu Mar 14 09:46:04 2019 +0100 +++ b/src/HOL/Library/Library.thy Thu Mar 14 09:46:09 2019 +0100 @@ -23,6 +23,7 @@ Discrete Disjoint_Sets Dlist + Dual_Ordered_Lattice Equipollence Extended Extended_Nat