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