# Theory Dual_Ordered_Lattice

```(*  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 ∗‹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

code_datatype 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, code]:
"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"

lemma dual_comp_undual [simp]:
"dual ∘ undual = id"

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)"
qed

instantiation dual :: (equal) equal
begin

lift_definition equal_dual :: "'a dual ⇒ 'a dual ⇒ bool"
is HOL.equal .

instance
by (standard; transfer) (simp add: equal)

end

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"
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"
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)))"
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)))"
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
```