Theory Order_Theory
section ‹Partial orders, lattices and complete lattices›
theory Order_Theory
imports Set_Theory
begin
text ‹This theory uses no arithmetic; suppress HOL's ‹+›/‹-› notation (as ‹Ring_Theory› does) so that
it composes without ambiguity when imported alongside the ring/group developments, which rebind
those tokens to their locale operations.›
no_notation plus (infixl ‹+› 65)
no_notation minus (infixl ‹-› 65)
unbundle no uminus_syntax
text ‹Carrier-set order theory in the locale idiom of ‹Group_Theory›: a
@{term Partial_Order} fixes a carrier ‹L› and an order relation ‹⊑› (a binary predicate, with the
reflexive / antisymmetric / transitive axioms restricted to ‹L›). On top of this we build binary
lattices (least upper and greatest lower bounds of pairs) and complete lattices (of arbitrary
subsets). Unlike HOL-Algebra's record-based ‹weak_partial_order› over an equivalence, we fix the
relation directly, which keeps the statements close to the type-class order they specialise.›
subsection ‹Partial orders›
locale Partial_Order =
fixes L :: "'a set" and le :: "'a ⇒ 'a ⇒ bool" (infix ‹⊑› 50)
assumes reflexive [intro, simp]: "a ∈ L ⟹ a ⊑ a"
and antisymmetric: "⟦ a ∈ L; b ∈ L; a ⊑ b; b ⊑ a ⟧ ⟹ a = b"
and transitive [trans]: "⟦ a ∈ L; b ∈ L; c ∈ L; a ⊑ b; b ⊑ c ⟧ ⟹ a ⊑ c"
begin
subsubsection ‹Bounds›
text ‹‹x› is an upper bound of ‹A› (a subset of the carrier) if it dominates every element of ‹A›.›
definition upper_bound :: "'a ⇒ 'a set ⇒ bool"
where "upper_bound x A ⟷ x ∈ L ∧ (∀a∈A. a ⊑ x)"
definition lower_bound :: "'a ⇒ 'a set ⇒ bool"
where "lower_bound x A ⟷ x ∈ L ∧ (∀a∈A. x ⊑ a)"
lemma upper_boundI:
"⟦ x ∈ L; ⋀a. a ∈ A ⟹ a ⊑ x ⟧ ⟹ upper_bound x A"
unfolding upper_bound_def by blast
lemma upper_boundD: "⟦ upper_bound x A; a ∈ A ⟧ ⟹ a ⊑ x"
unfolding upper_bound_def by blast
lemma upper_bound_closed: "upper_bound x A ⟹ x ∈ L"
unfolding upper_bound_def by blast
lemma lower_boundI:
"⟦ x ∈ L; ⋀a. a ∈ A ⟹ x ⊑ a ⟧ ⟹ lower_bound x A"
unfolding lower_bound_def by blast
lemma lower_boundD: "⟦ lower_bound x A; a ∈ A ⟧ ⟹ x ⊑ a"
unfolding lower_bound_def by blast
lemma lower_bound_closed: "lower_bound x A ⟹ x ∈ L"
unfolding lower_bound_def by blast
subsubsection ‹Suprema and infima›
text ‹‹s› is a least upper bound (supremum) of ‹A›: an upper bound below every upper bound.›
definition is_sup :: "'a ⇒ 'a set ⇒ bool"
where "is_sup s A ⟷ upper_bound s A ∧ (∀x. upper_bound x A ⟶ s ⊑ x)"
definition is_inf :: "'a ⇒ 'a set ⇒ bool"
where "is_inf i A ⟷ lower_bound i A ∧ (∀x. lower_bound x A ⟶ x ⊑ i)"
lemma is_supI:
"⟦ upper_bound s A; ⋀x. upper_bound x A ⟹ s ⊑ x ⟧ ⟹ is_sup s A"
unfolding is_sup_def by blast
lemma is_sup_upper: "is_sup s A ⟹ upper_bound s A"
unfolding is_sup_def by blast
lemma is_sup_least: "⟦ is_sup s A; upper_bound x A ⟧ ⟹ s ⊑ x"
unfolding is_sup_def by blast
lemma is_infI:
"⟦ lower_bound i A; ⋀x. lower_bound x A ⟹ x ⊑ i ⟧ ⟹ is_inf i A"
unfolding is_inf_def by blast
lemma is_inf_lower: "is_inf i A ⟹ lower_bound i A"
unfolding is_inf_def by blast
lemma is_inf_greatest: "⟦ is_inf i A; lower_bound x A ⟧ ⟹ x ⊑ i"
unfolding is_inf_def by blast
text ‹Suprema and infima are unique when they exist (antisymmetry).›
lemma is_sup_unique:
assumes "is_sup s A" and "is_sup s' A"
shows "s = s'"
proof (rule antisymmetric)
show "s ∈ L" using assms(1) is_sup_upper upper_bound_closed by blast
show "s' ∈ L" using assms(2) is_sup_upper upper_bound_closed by blast
show "s ⊑ s'" using assms by (blast dest: is_sup_least is_sup_upper)
show "s' ⊑ s" using assms by (blast dest: is_sup_least is_sup_upper)
qed
lemma is_inf_unique:
assumes "is_inf i A" and "is_inf i' A"
shows "i = i'"
proof (rule antisymmetric)
show "i ∈ L" using assms(1) is_inf_lower lower_bound_closed by blast
show "i' ∈ L" using assms(2) is_inf_lower lower_bound_closed by blast
show "i ⊑ i'" using assms by (blast dest: is_inf_greatest is_inf_lower)
show "i' ⊑ i" using assms by (blast dest: is_inf_greatest is_inf_lower)
qed
end
subsection ‹Lattices›
text ‹A lattice is a partial order in which every pair of elements has a supremum (join) and an
infimum (meet).›
locale Lattice = Partial_Order +
assumes ex_sup: "⟦ a ∈ L; b ∈ L ⟧ ⟹ ∃s. is_sup s {a, b}"
and ex_inf: "⟦ a ∈ L; b ∈ L ⟧ ⟹ ∃i. is_inf i {a, b}"
begin
definition join :: "'a ⇒ 'a ⇒ 'a" (infixl ‹⊔› 65)
where "a ⊔ b = (THE s. is_sup s {a, b})"
definition meet :: "'a ⇒ 'a ⇒ 'a" (infixl ‹⊓› 70)
where "a ⊓ b = (THE i. is_inf i {a, b})"
lemma is_sup_join:
assumes "a ∈ L" "b ∈ L" shows "is_sup (a ⊔ b) {a, b}"
unfolding join_def by (rule theI') (use ex_sup[OF assms] is_sup_unique in blast)
lemma is_inf_meet:
assumes "a ∈ L" "b ∈ L" shows "is_inf (a ⊓ b) {a, b}"
unfolding meet_def by (rule theI') (use ex_inf[OF assms] is_inf_unique in blast)
lemma join_closed [intro, simp]: "⟦ a ∈ L; b ∈ L ⟧ ⟹ a ⊔ b ∈ L"
using upper_bound_closed[OF is_sup_upper[OF is_sup_join]] .
lemma meet_closed [intro, simp]: "⟦ a ∈ L; b ∈ L ⟧ ⟹ a ⊓ b ∈ L"
using lower_bound_closed[OF is_inf_lower[OF is_inf_meet]] .
text ‹The join dominates its arguments and is least among common upper bounds.›
lemma join_upper1: "⟦ a ∈ L; b ∈ L ⟧ ⟹ a ⊑ a ⊔ b"
using is_sup_join is_sup_upper by (blast dest: upper_boundD)
lemma join_upper2: "⟦ a ∈ L; b ∈ L ⟧ ⟹ b ⊑ a ⊔ b"
using is_sup_join is_sup_upper by (blast dest: upper_boundD)
lemma join_least: "⟦ a ∈ L; b ∈ L; a ⊑ c; b ⊑ c; c ∈ L ⟧ ⟹ a ⊔ b ⊑ c"
using is_sup_join by (blast intro: is_sup_least upper_boundI)
lemma meet_lower1: "⟦ a ∈ L; b ∈ L ⟧ ⟹ a ⊓ b ⊑ a"
using is_inf_meet is_inf_lower by (blast dest: lower_boundD)
lemma meet_lower2: "⟦ a ∈ L; b ∈ L ⟧ ⟹ a ⊓ b ⊑ b"
using is_inf_meet is_inf_lower by (blast dest: lower_boundD)
lemma meet_greatest: "⟦ a ∈ L; b ∈ L; c ⊑ a; c ⊑ b; c ∈ L ⟧ ⟹ c ⊑ a ⊓ b"
using is_inf_meet by (blast intro: is_inf_greatest lower_boundI)
subsubsection ‹Lattice laws›
lemma join_commutative:
assumes "a ∈ L" "b ∈ L" shows "a ⊔ b = b ⊔ a"
proof (rule is_sup_unique[OF is_sup_join[OF assms]])
show "is_sup (b ⊔ a) {a, b}" using is_sup_join[OF assms(2,1)] by (simp add: insert_commute)
qed
lemma meet_commutative:
assumes "a ∈ L" "b ∈ L" shows "a ⊓ b = b ⊓ a"
proof (rule is_inf_unique[OF is_inf_meet[OF assms]])
show "is_inf (b ⊓ a) {a, b}" using is_inf_meet[OF assms(2,1)] by (simp add: insert_commute)
qed
lemma join_idempotent [simp]: "a ∈ L ⟹ a ⊔ a = a"
by (rule antisymmetric) (auto simp: join_upper1 join_least)
lemma meet_idempotent [simp]: "a ∈ L ⟹ a ⊓ a = a"
by (rule antisymmetric) (auto simp: meet_lower1 meet_greatest)
text ‹Absorption laws.›
lemma join_absorb: "⟦ a ∈ L; b ∈ L ⟧ ⟹ a ⊔ (a ⊓ b) = a"
by (rule antisymmetric) (auto simp: join_upper1 join_least meet_lower1)
lemma meet_absorb: "⟦ a ∈ L; b ∈ L ⟧ ⟹ a ⊓ (a ⊔ b) = a"
by (rule antisymmetric) (auto simp: meet_lower1 meet_greatest join_upper1)
text ‹The order is recovered from the join (equivalently the meet).›
lemma le_iff_join:
assumes a: "a ∈ L" and b: "b ∈ L" shows "(a ⊑ b) = (a ⊔ b = b)"
proof
assume ab: "a ⊑ b"
show "a ⊔ b = b"
proof (rule antisymmetric)
show "a ⊔ b ∈ L" using a b by simp
show "b ∈ L" by (rule b)
show "a ⊔ b ⊑ b" using join_least[OF a b ab] b by simp
show "b ⊑ a ⊔ b" by (rule join_upper2[OF a b])
qed
next
assume "a ⊔ b = b"
then show "a ⊑ b" using join_upper1[OF a b] by simp
qed
end
subsection ‹Complete lattices›
text ‹A complete lattice: every subset of the carrier has a supremum and an infimum.›
locale Complete_Lattice = Partial_Order +
assumes ex_Sup: "A ⊆ L ⟹ ∃s. is_sup s A"
and ex_Inf: "A ⊆ L ⟹ ∃i. is_inf i A"
begin
definition Sup :: "'a set ⇒ 'a" (‹⨆›)
where "⨆ A = (THE s. is_sup s A)"
definition Inf :: "'a set ⇒ 'a" (‹⨅›)
where "⨅ A = (THE i. is_inf i A)"
lemma is_sup_Sup: "A ⊆ L ⟹ is_sup (⨆ A) A"
unfolding Sup_def by (rule theI') (use ex_Sup is_sup_unique in blast)
lemma is_inf_Inf: "A ⊆ L ⟹ is_inf (⨅ A) A"
unfolding Inf_def by (rule theI') (use ex_Inf is_inf_unique in blast)
lemma Sup_closed [intro, simp]: "A ⊆ L ⟹ ⨆ A ∈ L"
using is_sup_Sup is_sup_upper upper_bound_closed by blast
lemma Inf_closed [intro, simp]: "A ⊆ L ⟹ ⨅ A ∈ L"
using is_inf_Inf is_inf_lower lower_bound_closed by blast
lemma Sup_upper: "⟦ A ⊆ L; a ∈ A ⟧ ⟹ a ⊑ ⨆ A"
using is_sup_Sup is_sup_upper by (blast dest: upper_boundD)
lemma Sup_least: "⟦ A ⊆ L; upper_bound x A ⟧ ⟹ ⨆ A ⊑ x"
using is_sup_Sup by (blast dest: is_sup_least)
lemma Inf_lower: "⟦ A ⊆ L; a ∈ A ⟧ ⟹ ⨅ A ⊑ a"
using is_inf_Inf is_inf_lower by (blast dest: lower_boundD)
lemma Inf_greatest: "⟦ A ⊆ L; lower_bound x A ⟧ ⟹ x ⊑ ⨅ A"
using is_inf_Inf by (blast dest: is_inf_greatest)
text ‹Top and bottom: the sup and inf of the whole carrier.›
definition top :: 'a (‹⊤›) where "⊤ = ⨆ L"
definition bottom :: 'a (‹⊥›) where "⊥ = ⨅ L"
lemma top_closed [intro, simp]: "⊤ ∈ L" unfolding top_def by simp
lemma bottom_closed [intro, simp]: "⊥ ∈ L" unfolding bottom_def by simp
lemma top_greatest: "a ∈ L ⟹ a ⊑ ⊤"
unfolding top_def using Sup_upper by blast
lemma bottom_least: "a ∈ L ⟹ ⊥ ⊑ a"
unfolding bottom_def using Inf_lower by blast
text ‹A complete lattice is a lattice (binary sup/inf are the two-element cases).›
sublocale Lattice
proof
fix a b assume "a ∈ L" "b ∈ L"
then have "{a, b} ⊆ L" by simp
then show "∃s. is_sup s {a, b}" and "∃i. is_inf i {a, b}"
using ex_Sup ex_Inf by blast+
qed
end
subsection ‹Isotone maps›
text ‹An isotone (order-preserving, monotone) map between two partial orders.›
definition isotone :: "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'b set ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool"
where "isotone LX leX LY leY f ⟷
f ∈ LX → LY ∧ (∀x∈LX. ∀y∈LX. leX x y ⟶ leY (f x) (f y))"
lemma isotoneI:
"⟦ f ∈ LX → LY; ⋀x y. ⟦ x ∈ LX; y ∈ LX; leX x y ⟧ ⟹ leY (f x) (f y) ⟧
⟹ isotone LX leX LY leY f"
unfolding isotone_def by blast
lemma isotone_closed: "⟦ isotone LX leX LY leY f; x ∈ LX ⟧ ⟹ f x ∈ LY"
unfolding isotone_def by blast
lemma isotone_le: "⟦ isotone LX leX LY leY f; x ∈ LX; y ∈ LX; leX x y ⟧ ⟹ leY (f x) (f y)"
unfolding isotone_def by blast
subsection ‹Galois connections›
text ‹A (monotone) Galois connection between two partial orders ‹X› and ‹Y›: a lower adjoint
‹f : X → Y› and an upper adjoint ‹g : Y → X› linked by the defining adjunction
‹f x ⊑⇘Y⇙ y ⟷ x ⊑⇘X⇙ g y›. This is the abstract backbone of correspondences such as the Galois
correspondence between subgroups and intermediate fields.›
locale Galois_Connection =
X: Partial_Order LX leX + Y: Partial_Order LY leY
for LX and leX (infix ‹⊑⇩X› 50) and LY and leY (infix ‹⊑⇩Y› 50) +
fixes f :: "'a ⇒ 'b" and g :: "'b ⇒ 'a"
assumes f_closed: "f ∈ LX → LY"
and g_closed: "g ∈ LY → LX"
and galois: "⟦ x ∈ LX; y ∈ LY ⟧ ⟹ f x ⊑⇩Y y ⟷ x ⊑⇩X g y"
begin
lemma f_in: "x ∈ LX ⟹ f x ∈ LY" using f_closed by auto
lemma g_in: "y ∈ LY ⟹ g y ∈ LX" using g_closed by auto
text ‹Unit and counit of the adjunction: ‹x ⊑ g (f x)› and ‹f (g y) ⊑ y›.›
lemma unit: "x ∈ LX ⟹ x ⊑⇩X g (f x)"
using galois[of x "f x"] f_in by simp
lemma counit: "y ∈ LY ⟹ f (g y) ⊑⇩Y y"
using galois[of "g y" y] g_in by simp
text ‹Both adjoints are isotone.›
lemma lower_isotone: "isotone LX leX LY leY f"
proof (rule isotoneI[OF f_closed])
fix x x' assume x: "x ∈ LX" and x': "x' ∈ LX" and le: "x ⊑⇩X x'"
have "x ⊑⇩X g (f x')"
using le unit[OF x'] x x' g_in f_in by (blast intro: X.transitive)
then show "f x ⊑⇩Y f x'" using galois[OF x f_in[OF x']] by simp
qed
lemma upper_isotone: "isotone LY leY LX leX g"
proof (rule isotoneI[OF g_closed])
fix y y' assume y: "y ∈ LY" and y': "y' ∈ LY" and le: "y ⊑⇩Y y'"
have "f (g y) ⊑⇩Y y'"
using le counit[OF y] y y' f_in g_in by (blast intro: Y.transitive)
then show "g y ⊑⇩X g y'" using galois[OF g_in[OF y] y'] by simp
qed
text ‹The composite ‹g ∘ f› is a closure operator on ‹X›: expansive (@{thm unit}), isotone, and
idempotent. Dually ‹f ∘ g› is a kernel (interior) operator on ‹Y›. The two ∗‹semi-inverse›
identities below --- ‹f (g (f x)) = f x› and ‹g (f (g y)) = g y› --- underlie idempotence.›
lemma lower_semi_inverse: "x ∈ LX ⟹ f (g (f x)) = f x"
proof (rule Y.antisymmetric)
assume x: "x ∈ LX"
show "f (g (f x)) ∈ LY" using x f_in g_in by blast
show "f x ∈ LY" using x f_in by blast
show "f (g (f x)) ⊑⇩Y f x" using counit[OF f_in[OF x]] .
have gfx: "g (f x) ∈ LX" using x f_in g_in by blast
show "f x ⊑⇩Y f (g (f x))"
by (rule isotone_le[OF lower_isotone x gfx unit[OF x]])
qed
lemma upper_semi_inverse: "y ∈ LY ⟹ g (f (g y)) = g y"
proof (rule X.antisymmetric)
assume y: "y ∈ LY"
show "g (f (g y)) ∈ LX" using y g_in f_in by blast
show "g y ∈ LX" using y g_in by blast
show "g y ⊑⇩X g (f (g y))" using unit[OF g_in[OF y]] .
have fgy: "f (g y) ∈ LY" using y g_in f_in by blast
show "g (f (g y)) ⊑⇩X g y"
by (rule isotone_le[OF upper_isotone fgy y counit[OF y]])
qed
text ‹Idempotence of the closure operator ‹g ∘ f› on ‹X›.›
lemma closure_idempotent: "x ∈ LX ⟹ g (f (g (f x))) = g (f x)"
using upper_semi_inverse[OF f_in] by simp
text ‹Idempotence of the kernel operator ‹f ∘ g› on ‹Y›.›
lemma kernel_idempotent: "y ∈ LY ⟹ f (g (f (g y))) = f (g y)"
using lower_semi_inverse[OF g_in] by simp
end
end