src/HOL/Library/Dual_Ordered_Lattice.thy

consistent hosts ordering;

(*  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

code_datatype 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, 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 \<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

instantiation dual :: (equal) equal
begin

lift_definition equal_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool"
  is HOL.equal .

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

end


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