Theory Lattice_Basics

(* Title:      Lattice Basics
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Lattice Basics›

text ‹
This theory provides notations, basic definitions and facts of lattice-related structures used throughout the subsequent development.
›

theory Lattice_Basics

imports Main

begin

subsection ‹General Facts and Notations›

text ‹
The following results extend basic Isabelle/HOL facts.
›

lemma imp_as_conj:
  assumes "P x ⟹ Q x"
  shows "P x ∧ Q x ⟷ P x"
  using assms by auto

lemma if_distrib_2:
  "f (if c then x else y) (if c then z else w) = (if c then f x z else f y w)"
  by simp

lemma left_invertible_inj:
  "(∀x . g (f x) = x) ⟹ inj f"
  by (metis injI)

lemma invertible_bij:
  assumes "∀x . g (f x) = x"
      and "∀y . f (g y) = y"
    shows "bij f"
  by (metis assms bijI')

lemma finite_ne_subset_induct [consumes 3, case_names singleton insert]:
  assumes "finite F"
      and "F ≠ {}"
      and "F ⊆ S"
      and singleton: "⋀x . P {x}"
      and insert: "⋀x F . finite F ⟹ F ≠ {} ⟹ F ⊆ S ⟹ x ∈ S ⟹ x ∉ F ⟹ P F ⟹ P (insert x F)"
    shows "P F"
  using assms(1-3)
  apply (induct rule: finite_ne_induct)
  apply (simp add: singleton)
  by (simp add: insert)

lemma finite_set_of_finite_funs_pred:
  assumes "finite { x::'a . True }"
      and "finite { y::'b . P y }"
    shows "finite { f . (∀x::'a . P (f x)) }"
  using assms finite_set_of_finite_funs by force

text ‹
We use the following notations for the join, meet and complement operations.
Changing the precedence of the unary complement allows us to write terms like ‹--x› instead of ‹-(-x)›.
›

context sup
begin

notation sup (infixl "⊔" 65)

definition additive :: "('a ⇒ 'a) ⇒ bool"
  where "additive f ≡ ∀x y . f (x ⊔ y) = f x ⊔ f y"

end

context inf
begin

notation inf (infixl "⊓" 67)

end

context uminus
begin

no_notation uminus ("- _" [81] 80)

notation uminus ("- _" [80] 80)

end

subsection ‹Orders›

text ‹
We use the following definition of monotonicity for operations defined in classes.
The standard ‹mono› places a sort constraint on the target type.
We also give basic properties of Galois connections and lift orders to functions.
›

context ord
begin

definition isotone :: "('a ⇒ 'a) ⇒ bool"
  where "isotone f ≡ ∀x y . x ≤ y ⟶ f x ≤ f y"

definition galois :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ bool"
  where "galois l u ≡ ∀x y . l x ≤ y ⟷ x ≤ u y"

definition lifted_less_eq :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ bool" ("(_ ≤≤ _)" [51, 51] 50)
  where "f ≤≤ g ≡ ∀x . f x ≤ g x"

end

context order
begin

lemma order_lesseq_imp:
  "(∀z . x ≤ z ⟶ y ≤ z) ⟷ y ≤ x"
  using order_trans by blast

lemma galois_char:
  "galois l u ⟷ (∀x . x ≤ u (l x)) ∧ (∀x . l (u x) ≤ x) ∧ isotone l ∧ isotone u"
  apply (rule iffI)
  apply (metis (full_types) galois_def isotone_def order_refl order_trans)
  using galois_def isotone_def order_trans by blast

lemma galois_closure:
  "galois l u ⟹ l x = l (u (l x)) ∧ u x = u (l (u x))"
  by (simp add: galois_char isotone_def order.antisym)

lemma lifted_reflexive:
  "f = g ⟹ f ≤≤ g"
  by (simp add: lifted_less_eq_def)

lemma lifted_transitive:
  "f ≤≤ g ⟹ g ≤≤ h ⟹ f ≤≤ h"
  using lifted_less_eq_def order_trans by blast

lemma lifted_antisymmetric:
  "f ≤≤ g ⟹ g ≤≤ f ⟹ f = g"
  by (rule ext, rule order.antisym) (simp_all add: lifted_less_eq_def)

text ‹
If the image of a finite non-empty set under ‹f› is a totally ordered, there is an element that minimises the value of ‹f›.
›

lemma finite_set_minimal:
  assumes "finite s"
      and "s ≠ {}"
      and "∀x∈s . ∀y∈s . f x ≤ f y ∨ f y ≤ f x"
    shows "∃m∈s . ∀z∈s . f m ≤ f z"
  apply (rule finite_ne_subset_induct[where S=s])
  apply (rule assms(1))
  apply (rule assms(2))
  apply simp
  apply simp
  by (metis assms(3) insert_iff order_trans subsetD)

end

subsection ‹Semilattices›

text ‹
The following are basic facts in semilattices.
›

context semilattice_sup
begin

lemma sup_left_isotone:
  "x ≤ y ⟹ x ⊔ z ≤ y ⊔ z"
  using sup.mono by blast

lemma sup_right_isotone:
  "x ≤ y ⟹ z ⊔ x ≤ z ⊔ y"
  using sup.mono by blast

lemma sup_left_divisibility:
  "x ≤ y ⟷ (∃z . x ⊔ z = y)"
  using sup.absorb2 sup.cobounded1 by blast

lemma sup_right_divisibility:
  "x ≤ y ⟷ (∃z . z ⊔ x = y)"
  by (metis sup.cobounded2 sup.orderE)

lemma sup_same_context:
  "x ≤ y ⊔ z ⟹ y ≤ x ⊔ z ⟹ x ⊔ z = y ⊔ z"
  by (simp add: le_iff_sup sup_left_commute)

lemma sup_relative_same_increasing:
  "x ≤ y ⟹ x ⊔ z = x ⊔ w ⟹ y ⊔ z = y ⊔ w"
  using sup.assoc sup_right_divisibility by auto

end

text ‹
Every bounded semilattice is a commutative monoid.
Finite sums defined in commutative monoids are available via the following sublocale.
›

context bounded_semilattice_sup_bot
begin

sublocale sup_monoid: comm_monoid_add where plus = sup and zero = bot
  apply unfold_locales
  apply (simp add: sup_assoc)
  apply (simp add: sup_commute)
  by simp

end

context semilattice_inf
begin

lemma inf_same_context:
  "x ≤ y ⊓ z ⟹ y ≤ x ⊓ z ⟹ x ⊓ z = y ⊓ z"
  using order.antisym by auto

end

text ‹
The following class requires only the existence of upper bounds, which is a property common to bounded semilattices and (not necessarily bounded) lattices.
We use it in our development of filters.
›

class directed_semilattice_inf = semilattice_inf +
  assumes ub: "∃z . x ≤ z ∧ y ≤ z"

text ‹
We extend the ‹inf› sublocale, which dualises the order in semilattices, to bounded semilattices.
›

context bounded_semilattice_inf_top
begin

subclass directed_semilattice_inf
  apply unfold_locales
  using top_greatest by blast

sublocale inf: bounded_semilattice_sup_bot where sup = inf and less_eq = greater_eq and less = greater and bot = top
  by unfold_locales (simp_all add: less_le_not_le)

end

subsection ‹Lattices›

context lattice
begin

subclass directed_semilattice_inf
  apply unfold_locales
  using sup_ge1 sup_ge2 by blast

definition dual_additive :: "('a ⇒ 'a) ⇒ bool"
  where "dual_additive f ≡ ∀x y . f (x ⊔ y) = f x ⊓ f y"

end

text ‹
Not every bounded lattice has complements, but two elements might still be complements of each other as captured in the following definition.
In this situation we can apply, for example, the shunting property shown below.
We introduce most definitions using the ‹abbreviation› command.
›

context bounded_lattice
begin

abbreviation "complement x y ≡ x ⊔ y = top ∧ x ⊓ y = bot"

lemma complement_symmetric:
  "complement x y ⟹ complement y x"
  by (simp add: inf.commute sup.commute)

definition conjugate :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ bool"
  where "conjugate f g ≡ ∀x y . f x ⊓ y = bot ⟷ x ⊓ g y = bot"

end

class dense_lattice = bounded_lattice +
  assumes bot_meet_irreducible: "x ⊓ y = bot ⟶ x = bot ∨ y = bot"

context distrib_lattice
begin

lemma relative_equality:
  "x ⊔ z = y ⊔ z ⟹ x ⊓ z = y ⊓ z ⟹ x = y"
  by (metis inf.commute inf_sup_absorb inf_sup_distrib2)

end

text ‹
Distributive lattices with a greatest element are widely used in the construction theorem for Stone algebras.
›

class distrib_lattice_bot = bounded_lattice_bot + distrib_lattice

class distrib_lattice_top = bounded_lattice_top + distrib_lattice

class bounded_distrib_lattice = bounded_lattice + distrib_lattice
begin

subclass distrib_lattice_bot ..

subclass distrib_lattice_top ..

lemma complement_shunting:
  assumes "complement z w"
    shows "z ⊓ x ≤ y ⟷ x ≤ w ⊔ y"
proof
  assume 1: "z ⊓ x ≤ y"
  have "x = (z ⊔ w) ⊓ x"
    by (simp add: assms)
  also have "... ≤ y ⊔ (w ⊓ x)"
    using 1 sup.commute sup.left_commute inf_sup_distrib2 sup_right_divisibility by fastforce
  also have "... ≤ w ⊔ y"
    by (simp add: inf.coboundedI1)
  finally show "x ≤ w ⊔ y"
    .
next
  assume "x ≤ w ⊔ y"
  hence "z ⊓ x ≤ z ⊓ (w ⊔ y)"
    using inf.sup_right_isotone by auto
  also have "... = z ⊓ y"
    by (simp add: assms inf_sup_distrib1)
  also have "... ≤ y"
    by simp
  finally show "z ⊓ x ≤ y"
    .
qed

end

subsection ‹Linear Orders›

text ‹
We next consider lattices with a linear order structure.
In such lattices, join and meet are selective operations, which give the maximum and the minimum of two elements, respectively.
Moreover, the lattice is automatically distributive.
›

class bounded_linorder = linorder + order_bot + order_top

class linear_lattice = lattice + linorder
begin

lemma max_sup:
  "max x y = x ⊔ y"
  by (metis max.boundedI max.cobounded1 max.cobounded2 sup_unique)

lemma min_inf:
  "min x y = x ⊓ y"
  by (simp add: inf.absorb1 inf.absorb2 min_def)

lemma sup_inf_selective:
  "(x ⊔ y = x ∧ x ⊓ y = y) ∨ (x ⊔ y = y ∧ x ⊓ y = x)"
  by (meson inf.absorb1 inf.absorb2 le_cases sup.absorb1 sup.absorb2)

lemma sup_selective:
  "x ⊔ y = x ∨ x ⊔ y = y"
  using sup_inf_selective by blast

lemma inf_selective:
  "x ⊓ y = x ∨ x ⊓ y = y"
  using sup_inf_selective by blast

subclass distrib_lattice
  apply standard
  apply (rule order.antisym)
   apply (auto simp add: le_supI2)
  apply (metis inf_selective inf.coboundedI1 inf.coboundedI2 order.eq_iff)
  done

lemma sup_less_eq:
  "x ≤ y ⊔ z ⟷ x ≤ y ∨ x ≤ z"
  by (metis le_supI1 le_supI2 sup_selective)

lemma inf_less_eq:
  "x ⊓ y ≤ z ⟷ x ≤ z ∨ y ≤ z"
  by (metis inf.coboundedI1 inf.coboundedI2 inf_selective)

lemma sup_inf_sup:
  "x ⊔ y = (x ⊔ y) ⊔ (x ⊓ y)"
  by (metis sup_commute sup_inf_absorb sup_left_commute)

end

text ‹
The following class derives additional properties if the linear order of the lattice has a least and a greatest element.
›

class linear_bounded_lattice = bounded_lattice + linorder
begin

subclass linear_lattice ..

subclass bounded_linorder ..

subclass bounded_distrib_lattice ..

lemma sup_dense:
  "x ≠ top ⟹ y ≠ top ⟹ x ⊔ y ≠ top"
  by (metis sup_selective)

lemma inf_dense:
  "x ≠ bot ⟹ y ≠ bot ⟹ x ⊓ y ≠ bot"
  by (metis inf_selective)

lemma sup_not_bot:
  "x ≠ bot ⟹ x ⊔ y ≠ bot"
  by simp

lemma inf_not_top:
  "x ≠ top ⟹ x ⊓ y ≠ top"
  by simp

subclass dense_lattice
  apply unfold_locales
  using inf_dense by blast

end

text ‹
Every bounded linear order can be expanded to a bounded lattice.
Join and meet are maximum and minimum, respectively.
›

class linorder_lattice_expansion = bounded_linorder + sup + inf +
  assumes sup_def [simp]: "x ⊔ y = max x y"
  assumes inf_def [simp]: "x ⊓ y = min x y"
begin

subclass linear_bounded_lattice
  apply unfold_locales
  by auto

end

subsection ‹Non-trivial Algebras›

text ‹
Some results, such as the existence of certain filters, require that the algebras are not trivial.
This is not an assumption of the order and lattice classes that come with Isabelle/HOL; for example, ‹bot = top› may hold in bounded lattices.
›

class non_trivial =
  assumes consistent: "∃x y . x ≠ y"

class non_trivial_order = non_trivial + order

class non_trivial_order_bot = non_trivial_order + order_bot

class non_trivial_bounded_order = non_trivial_order_bot + order_top
begin

lemma bot_not_top:
  "bot ≠ top"
proof -
  from consistent obtain x y :: 'a where "x ≠ y"
    by auto
  thus ?thesis
    by (metis bot_less top.extremum_strict)
qed

end

subsection ‹Homomorphisms›

text ‹
This section gives definitions of lattice homomorphisms and isomorphisms and basic properties.
›

class sup_inf_top_bot_uminus = sup + inf + top + bot + uminus
class sup_inf_top_bot_uminus_ord = sup_inf_top_bot_uminus + ord

context boolean_algebra
begin

subclass sup_inf_top_bot_uminus_ord .

end

abbreviation sup_homomorphism :: "('a::sup ⇒ 'b::sup) ⇒ bool"
  where "sup_homomorphism f ≡ ∀x y . f (x ⊔ y) = f x ⊔ f y"

abbreviation inf_homomorphism :: "('a::inf ⇒ 'b::inf) ⇒ bool"
  where "inf_homomorphism f ≡ ∀x y . f (x ⊓ y) = f x ⊓ f y"

abbreviation bot_homomorphism :: "('a::bot ⇒ 'b::bot) ⇒ bool"
  where "bot_homomorphism f ≡ f bot = bot"

abbreviation top_homomorphism :: "('a::top ⇒ 'b::top) ⇒ bool"
  where "top_homomorphism f ≡ f top = top"

abbreviation minus_homomorphism :: "('a::minus ⇒ 'b::minus) ⇒ bool"
  where "minus_homomorphism f ≡ ∀x y . f (x - y) = f x - f y"

abbreviation uminus_homomorphism :: "('a::uminus ⇒ 'b::uminus) ⇒ bool"
  where "uminus_homomorphism f ≡ ∀x . f (-x) = -f x"

abbreviation sup_inf_homomorphism :: "('a::{sup,inf} ⇒ 'b::{sup,inf}) ⇒ bool"
  where "sup_inf_homomorphism f ≡ sup_homomorphism f ∧ inf_homomorphism f"

abbreviation sup_inf_top_homomorphism :: "('a::{sup,inf,top} ⇒ 'b::{sup,inf,top}) ⇒ bool"
  where "sup_inf_top_homomorphism f ≡ sup_inf_homomorphism f ∧ top_homomorphism f"

abbreviation sup_inf_top_bot_homomorphism :: "('a::{sup,inf,top,bot} ⇒ 'b::{sup,inf,top,bot}) ⇒ bool"
  where "sup_inf_top_bot_homomorphism f ≡ sup_inf_top_homomorphism f ∧ bot_homomorphism f"

abbreviation bounded_lattice_homomorphism :: "('a::bounded_lattice ⇒ 'b::bounded_lattice) ⇒ bool"
  where "bounded_lattice_homomorphism f ≡ sup_inf_top_bot_homomorphism f"

abbreviation sup_inf_top_bot_uminus_homomorphism :: "('a::sup_inf_top_bot_uminus ⇒ 'b::sup_inf_top_bot_uminus) ⇒ bool"
  where "sup_inf_top_bot_uminus_homomorphism f ≡ sup_inf_top_bot_homomorphism f ∧ uminus_homomorphism f"

abbreviation sup_inf_top_bot_uminus_ord_homomorphism :: "('a::sup_inf_top_bot_uminus_ord ⇒ 'b::sup_inf_top_bot_uminus_ord) ⇒ bool"
  where "sup_inf_top_bot_uminus_ord_homomorphism f ≡ sup_inf_top_bot_uminus_homomorphism f ∧ (∀x y . x ≤ y ⟶ f x ≤ f y)"

abbreviation sup_inf_top_isomorphism :: "('a::{sup,inf,top} ⇒ 'b::{sup,inf,top}) ⇒ bool"
  where "sup_inf_top_isomorphism f ≡ sup_inf_top_homomorphism f ∧ bij f"

abbreviation bounded_lattice_top_isomorphism :: "('a::bounded_lattice_top ⇒ 'b::bounded_lattice_top) ⇒ bool"
  where "bounded_lattice_top_isomorphism f ≡ sup_inf_top_isomorphism f"

abbreviation sup_inf_top_bot_uminus_isomorphism :: "('a::sup_inf_top_bot_uminus ⇒ 'b::sup_inf_top_bot_uminus) ⇒ bool"
  where "sup_inf_top_bot_uminus_isomorphism f ≡ sup_inf_top_bot_uminus_homomorphism f ∧ bij f"

abbreviation boolean_algebra_isomorphism :: "('a::boolean_algebra ⇒ 'b::boolean_algebra) ⇒ bool"
  where "boolean_algebra_isomorphism f ≡ sup_inf_top_bot_uminus_isomorphism f ∧ minus_homomorphism f"

lemma sup_homomorphism_mono:
  "sup_homomorphism (f::'a::semilattice_sup ⇒ 'b::semilattice_sup) ⟹ mono f"
  by (metis le_iff_sup monoI)

lemma sup_isomorphism_ord_isomorphism:
  assumes "sup_homomorphism (f::'a::semilattice_sup ⇒ 'b::semilattice_sup)"
      and "bij f"
    shows "x ≤ y ⟷ f x ≤ f y"
proof
  assume "x ≤ y"
  thus "f x ≤ f y"
    by (metis assms(1) le_iff_sup)
next
  assume "f x ≤ f y"
  hence "f (x ⊔ y) = f y"
    by (simp add: assms(1) le_iff_sup)
  hence "x ⊔ y = y"
    by (metis injD bij_is_inj assms(2))
  thus "x ≤ y"
    by (simp add: le_iff_sup)
qed

lemma minus_homomorphism_default:
  assumes "∀x y::'a::{inf,minus,uminus} . x - y = x ⊓ -y"
      and "∀x y::'b::{inf,minus,uminus} . x - y = x ⊓ -y"
      and "inf_homomorphism (f::'a ⇒ 'b)"
      and "uminus_homomorphism f"
    shows "minus_homomorphism f"
  by (simp add: assms)

end