--- /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
--- 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