# 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