locale_experiment.thy

theory locale_experiment
imports Main
begin

section \<open>Algebraic formulation of a semilattice\<close>

locale semigroup =
  fixes ap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes assoc: "\<And>x y z. ap x (ap y z) = ap (ap x y) z"

locale commutative_semigroup = semigroup +
  assumes comm: "\<And>x y. ap x y = ap y x"

locale idempotent_semigroup = semigroup +
  assumes idem: "\<And>x. ap x x = x"

locale alg_semilattice
  = commutative_semigroup meet + idempotent_semigroup meet
  for meet

lemmas (in alg_semilattice)
  alg_semilattice_assms = assoc comm idem

section \<open>Order-theoretic formulation of a semilattice\<close>

locale partial_order =
  fixes ord :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes refl: "\<And>x. ord x x"
  assumes trans: "\<And>x y z. ord x y \<Longrightarrow> ord y z \<Longrightarrow> ord x z"
  assumes anti: "\<And>x y. ord x y \<Longrightarrow> ord y x \<Longrightarrow> x = y"

locale ord_semilattice = partial_order +
  fixes glb :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes lower_bound_l: "\<And>x y. ord (glb x y) x"
  assumes lower_bound_r: "\<And>x y. ord (glb x y) y"
  assumes greatest: "\<And>x y t. ord t x \<Longrightarrow> ord t y \<Longrightarrow> ord t (glb x y)"

lemmas (in ord_semilattice)
  ord_semilattice_assms = refl trans anti lower_bound_l lower_bound_r greatest

section \<open>Restriction of @{term ord_semilattice} to the natural ordering\<close>

abbreviation natural_order :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
  "natural_order f \<equiv> \<lambda>x y. x = f x y"

locale natural_ord_semilattice = ord_semilattice "natural_order meet" meet for meet

section \<open>Correspondences between @{term ord_semilattice} and @{term alg_semilattice}\<close>

text \<open>Every @{term ord_semilattice} is an @{term alg_semilattice}.\<close>
sublocale ord_semilattice < alg_of_ord?: alg_semilattice glb
  apply unfold_locales
  apply (meson anti greatest trans lower_bound_l lower_bound_r)
  apply (simp add: anti greatest lower_bound_l lower_bound_r)
  apply (simp add: anti greatest refl lower_bound_r)
  done

text \<open>Every @{term alg_semilattice} induces an @{term ord_semilattice} via the @{term natural_order}.\<close>
sublocale alg_semilattice < ord_of_alg?: natural_ord_semilattice meet
  apply unfold_locales
  apply (simp add: idem)
  apply (metis assoc)
  apply (simp add: comm)
  apply (simp add: assoc comm idem)
  apply (metis assoc idem)
  apply (simp add: assoc)
  done

section \<open>Examples\<close>

abbreviation min_order :: "'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" where
  "min_order \<equiv> min"

text \<open>We show that @{term min_order} gives an @{term alg_semilattice}.\<close>
global_interpretation min_order_alg: alg_semilattice min_order
  apply unfold_locales
  apply (rule min.assoc[symmetric])
  apply (rule min.commute)
  apply (rule min.idem)
  done

text \<open>It follows that it is also an @{term ord_semilattice}.\<close>
thm min_order_alg.ord_semilattice_assms

lemma natural_order_min_order_less_eq: "natural_order min_order = less_eq"
  unfolding min_def by auto

abbreviation max_order :: "'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" where
  "max_order \<equiv> max"

text \<open>We show that @{term max_order} gives a @{term natural_ord_semilattice}.\<close>
global_interpretation max_order_alg: natural_ord_semilattice max_order
  apply unfold_locales
  apply simp
  apply (metis max.assoc)
  apply (simp add: max.commute)
  apply (simp add: max.commute)
  apply simp
  apply linarith
  done

text \<open>It follows that it is also an @{term alg_semilattice}.\<close>
thm max_order_alg.alg_semilattice_assms

lemma natural_order_max_order_greater_eq: "natural_order max_order = greater_eq"
  unfolding max_def by fastforce

end