summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Thu, 14 Mar 2019 09:46:09 +0100 | |

changeset 69909 | 5382f5691a11 |

parent 69908 | 1bd74a0944b3 |

child 69910 | 0c0f7b4a72bf |

proper theory for type of dual ordered lattice in distribution

src/HOL/Library/Dual_Ordered_Lattice.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Library.thy | file | annotate | diff | comparison | revisions |

--- /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 \<open>Type of dual ordered lattices\<close> + +theory Dual_Ordered_Lattice +imports Main +begin + +text \<open> + The \<^emph>\<open>dual\<close> of an ordered structure is an isomorphic copy of the + underlying type, with the \<open>\<le>\<close> 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. +\<close> + +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 \<longleftrightarrow> undual x = undual y" + by transfer simp + +lemma eq_dual_iff [iff]: + "dual x = dual y \<longleftrightarrow> 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 \<circ> dual = id" + by (simp add: fun_eq_iff) + +lemma dual_comp_undual [simp]: + "dual \<circ> 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 \<open>Pointwise ordering\<close> + +instantiation dual :: (ord) ord +begin + +lift_definition less_eq_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool" + is "(\<ge>)" . + +lift_definition less_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool" + is "(>)" . + +instance .. + +end + +lemma dual_less_eqI: + "x \<le> y" if "undual y \<le> undual x" + using that by transfer assumption + +lemma dual_less_eq_iff: + "x \<le> y \<longleftrightarrow> undual y \<le> undual x" + by transfer simp + +lemma less_eq_dual_iff [iff]: + "dual x \<le> dual y \<longleftrightarrow> y \<le> 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 \<longleftrightarrow> undual y < undual x" + by transfer simp + +lemma less_dual_iff [iff]: + "dual x < dual y \<longleftrightarrow> 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 \<open>Binary infimum and supremum\<close> + +instantiation dual :: (sup) inf +begin + +lift_definition inf_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> '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 \<Rightarrow> 'a dual \<Rightarrow> '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 \<open>Top and bottom elements\<close> + +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 \<open>Complement\<close> + +instantiation dual :: (uminus) uminus +begin + +lift_definition uminus_dual :: "'a dual \<Rightarrow> '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 \<Rightarrow> 'a dual \<Rightarrow> 'a dual" + is "\<lambda>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 \<open>Complete lattice operations\<close> + +text \<open> + The class of complete lattices is closed under formation of dual + structures. +\<close> + +instantiation dual :: (Sup) Inf +begin + +lift_definition Inf_dual :: "'a dual set \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> 'a" + and g :: "'a dual \<Rightarrow> 'a dual" + assumes "mono f" + defines "g \<equiv> dual \<circ> f \<circ> undual" +begin + +private lemma mono_dual: + "mono g" +proof + fix x y :: "'a dual" + assume "x \<le> y" + then have "undual y \<le> undual x" + by (simp add: dual_less_eq_iff) + with \<open>mono f\<close> have "f (undual y) \<le> f (undual x)" + by (rule monoD) + then have "(dual \<circ> f \<circ> undual) x \<le> (dual \<circ> f \<circ> undual) y" + by simp + then show "g x \<le> 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))) \<le> dual (f (undual (gfp g)))" + by (simp add: g_def) + with mono_dual have "f (undual (gfp g)) \<le> undual (gfp g)" + by (simp add: gfp_unfold [where f = g, symmetric] dual_less_eq_iff) + then show "?lhs \<le> ?rhs" + by (rule lfp_lowerbound) + from \<open>mono f\<close> have "dual (lfp f) \<le> dual (undual (gfp g))" + by (simp add: lfp_fixpoint gfp_upperbound g_def) + then show "?rhs \<le> ?lhs" + by (simp only: less_eq_dual_iff) +qed + +lemma gfp_dual_lfp: + "gfp f = undual (lfp g)" +proof - + have "mono (\<lambda>x. undual (undual x))" + by (rule monoI) (simp add: dual_less_eq_iff) + moreover have "mono (\<lambda>a. dual (dual (f a)))" + using \<open>mono f\<close> by (auto intro: monoI dest: monoD) + moreover have "gfp f = gfp (\<lambda>x. undual (undual (dual (dual (f x)))))" + by simp + ultimately have "undual (undual (gfp (\<lambda>x. dual + (dual (f (undual (undual x))))))) = + gfp (\<lambda>x. undual (undual (dual (dual (f x)))))" + by (subst gfp_rolling [where g = "\<lambda>x. undual (undual x)"]) simp_all + then have "gfp f = + undual + (undual + (gfp (\<lambda>x. dual (dual (f (undual (undual x)))))))" + by simp + also have "\<dots> = undual (undual (gfp (dual \<circ> g \<circ> undual)))" + by (simp add: comp_def g_def) + also have "\<dots> = undual (lfp g)" + using mono_dual by (simp only: Dual_Ordered_Lattice.lfp_dual_gfp) + finally show ?thesis . +qed + +end + + +text \<open>Finally\<close> + +lifting_update dual.lifting +lifting_forget dual.lifting + +end