Theory Residuated_Lattices

(* Title:      Residuated Lattices
   Author:     Victor Gomes <vborgesferreiragomes1 at sheffield.ac.uk>
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
*)

theory Residuated_Lattices
  imports Kleene_Algebra.Signatures
begin

notation
  times (infixl "⋅" 70)
  
unbundle lattice_syntax

section ‹Residuated Lattices›

subsection ‹Residuated Functions on a Partial Order›

text ‹
  We follow Galatos and \emph{al.} to define residuated funtions on
  partial orders. Material from articles by Maddux, and J{\'o}sson and Tsinakis are also considered.
  
  This development should in the future be expanded to functions or categories where the sources and targets have
  different type.

  Let $P$ be a partial order, or a poset.
  A map $f : P \to P$ is residuated if there exists a map
  $g: P \to P$ such that $f(x) \le y \Leftrightarrow x \le g(y)$
  for all $x, y \in P$.
  That is, they are adjoints of a Galois connection.
›

context order begin

definition residuated_pair :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ bool" where
  "residuated_pair f g ≡ ∀x y. f(x) ≤ y ⟷ x ≤ g(y)"

theorem residuated_pairI [intro]: 
  assumes "∀x y. x ≤ y ⟶ f x ≤ f y"
  and "∀x y. x ≤ y ⟶ g x ≤ g y"
  and "∀x. x ≤ (g o f) x"
  and "∀x. (f o g) x ≤ x"
  shows "residuated_pair f g"
  by (metis assms comp_apply local.order_trans residuated_pair_def antisym)
  
definition residuated :: "('a ⇒ 'a) ⇒ bool" where
  "residuated f ≡ ∃g. residuated_pair f g"
  
text ‹
  If a map $f$ is residuated, then its residual $g$ is unique. 
›

lemma residual_unique: "residuated f ⟹ ∃!g. residuated_pair f g"
  unfolding residuated_def residuated_pair_def
  by (metis ext eq_refl order.antisym)
  
text ‹
  Since the residual of a map $f$ is unique, it makes sense to 
  define a residual operator. 
›
  
definition residual :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
  "residual f ≡ THE g. residuated_pair f g"

lemma residual_galois: "residuated f ⟹ f(x) ≤ y ⟷ x ≤ residual f y"
  apply (clarsimp simp: residuated_def residuated_pair_def)
  apply (subgoal_tac "residual f = g")
  apply (simp_all add: residual_def)
  apply (rule the1_equality)
  apply (metis residuated_def residuated_pair_def residual_unique) 
  by (simp add: residuated_pair_def)

lemma residual_galoisI1: "residuated f ⟹ f(x) ≤ y ⟹ x ≤ residual f y"
  by (metis residual_galois)

lemma residual_galoisI2: "residuated f ⟹ x ≤ residual f y ⟹ f(x) ≤ y"
  by (metis residual_galois)
  
text ‹
  A closure operator on a poset is a map that is expansive, isotone and
  idempotent.
  The composition of the residual of a function $f$ with $f$ is a closure operator.
›

definition closure :: "('a ⇒ 'a) ⇒ bool" where
  "closure f ≡ (∀x. x ≤ f x) ∧ (∀x y. x ≤ y ⟶ f x ≤ f y) ∧ (∀x. f(f x) = f x)"
  
lemma res_c1: "residuated f ⟹ x ≤ residual f (f x)"
  by (metis local.order.refl residual_galois)

lemma res_c2: "residuated f ⟹ x ≤ y ⟹ residual f (f x) ≤ residual f (f y)"
  by (metis local.order.refl local.order_trans residual_galois)
  
lemma res_c3: "residuated f ⟹ residual f (f (residual f (f x))) = residual f (f x)"
  by (metis order.eq_iff local.order_trans res_c1 residual_galois)

lemma res_closure: "residuated f ⟹ closure (residual f o f)"
  by (auto simp: closure_def intro: res_c1 res_c2 res_c3)

text ‹
  Dually, an interior operator on a poset is a map that is contractive, isotone and
  idempotent.
  The composition of $f$ with its residual is an interior operator.
›

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

lemma res_i1: "residuated f ⟹ f (residual f x) ≤ x"
  by (metis local.order.refl residual_galois)
  
lemma res_i2: "residuated f ⟹ x ≤ y ⟹ f (residual f x) ≤ f (residual f y)"
  by (metis local.order.refl local.order_trans residual_galois)
  
lemma res_i3: "residuated f ⟹ f (residual f (f (residual f x))) = f (residual f x)"
  by (metis local.antisym_conv res_c1 res_c3 res_i1 residual_galois)
  
lemma res_interior: "residuated f ⟹ interior (f o residual f)"
  by (auto simp: interior_def intro: res_i1 res_i2 res_i3)

text ‹Next we show a few basic lemmas about residuated maps.›

lemma res_iso: "residuated f ⟹ x ≤ y ⟹ f x ≤ f y"
  by (metis local.order.trans res_c1 residual_galois)
  
lemma res_residual_iso: "residuated f ⟹ x ≤ y ⟹ residual f x ≤ residual f y"
  by (metis local.order.trans res_i1 residual_galois)

lemma res_comp1 [simp]: "residuated f ⟹ f o residual f o f = f"
proof -
  assume resf: "residuated f"
  { 
    fix x
    have "(f o residual f o f) x = f x"
      by (metis resf comp_apply order.eq_iff res_c1 res_i1 res_iso)
  }
  thus ?thesis
    by (metis ext)
qed

lemma res_comp2 [simp]: "residuated f ⟹ residual f o f o residual f = residual f"
proof -
  assume resf: "residuated f"
  { 
    fix x
    have "(residual f o f o residual f) x = residual f x"
      by (metis resf comp_apply order.eq_iff res_c1 res_i1 res_residual_iso)
  }
  thus ?thesis
    by (metis ext)
qed

end (* order *)

text ‹
  A residuated function $f$ preserves all existing joins.
  Dually, its residual preserves all existing meets.
  We restrict our attention to semilattices, where binary joins or meets exist, and to
  complete lattices, where arbitrary joins and meets exist.
›

lemma (in semilattice_sup) residuated_sup: "residuated f ⟹ f (x ⊔ y) = f x ⊔ f y"
proof (rule order.antisym)
  assume assm: "residuated f"
  thus "f (x ⊔ y) ≤ f x ⊔ f y"
    by (metis local.residual_galoisI1 local.residual_galoisI2 local.sup.bounded_iff local.sup_ge1 local.sup_ge2)
  show "f x ⊔ f y ≤ f (x ⊔ y)"
    by (metis assm local.res_iso local.sup.bounded_iff local.sup_ge1 local.sup_ge2)
qed

lemma (in semilattice_inf) residuated_inf: "residuated f ⟹ residual f (x ⊓ y) = residual f x ⊓ residual f y"
proof (rule order.antisym)
  assume assm: "residuated f"
  thus "residual f (x ⊓ y) ≤ residual f x ⊓ residual f y"
    by (metis local.inf.boundedI local.inf.cobounded1 local.inf.cobounded2 local.res_residual_iso)
  show "residual f x ⊓ residual f y ≤ residual f (x ⊓ y)"
    by (metis assm local.inf.bounded_iff local.inf.cobounded1 local.inf.cobounded2 local.residual_galoisI1 local.residual_galoisI2)
qed

context bounded_lattice begin

lemma residuated_strict: "residuated f ⟹ f ⊥ = ⊥"
  by (metis local.bot_least local.bot_unique local.res_i1 local.res_iso)
  
lemma res_top: "residuated f ⟹ residual f ⊤ = ⊤"
  by (metis local.residual_galoisI1 local.top_greatest local.top_unique)

end

context complete_lattice begin

text ‹
  On a complete lattice, a function $f$ is residuated if and only if
  it preserves arbitrary (possibly infinite) joins.
  Dually, a function $g$ is a residual of a residuated funtion $f$
  if and only if $g$ preserver arbitrary meets. 
›

lemma residual_eq1: "residuated f ⟹ residual f y = ⨆ {x. f x ≤ y}"
proof (rule order.antisym)
  assume assm: "residuated f"
  thus "residual f y ≤ ⨆{x. f x ≤ y}"
    by (auto simp: res_i1 intro!: Sup_upper)
  show "⨆{x. f x ≤ y} ≤ residual f y"
    by (auto simp: assm intro!: Sup_least residual_galoisI1)
qed

lemma residual_eq2: "residuated f ⟹ f x = ⨅ {y. x ≤ residual f y}"
proof (rule order.antisym)
  assume assm: "residuated f"
  thus "f x ≤ ⨅{y. x ≤ residual f y}"
    by (auto intro: Inf_greatest residual_galoisI2)
  show "⨅{y. x ≤ residual f y} ≤ f x"
    using assm by (auto simp: res_c1 intro!: Inf_lower)
qed

lemma residuated_Sup: "residuated f ⟹ f(⨆ X) = ⨆{f x | x. x ∈ X}"
proof (rule order.antisym)
  assume assm: "residuated f"
  obtain y where y_def: "y = ⨆{f x |x. x ∈ X}" 
    by auto
  hence "∀x ∈ X. f x ≤ y"
    by (auto simp: y_def intro: Sup_upper)
  hence "∀x ∈ X. x ≤ residual f y"
    by (auto simp: assm intro!: residual_galoisI1)
  hence "⨆X ≤ residual f y"
    by (auto intro: Sup_least)
  thus "f(⨆ X) ≤ ⨆{f x |x. x ∈ X}"
    by (metis y_def assm residual_galoisI2)
qed (clarsimp intro!: Sup_least res_iso Sup_upper)

lemma residuated_Inf: "residuated f ⟹ residual f(⨅ X) = ⨅{residual f x | x. x ∈ X}"
proof (rule order.antisym, clarsimp intro!: Inf_greatest res_residual_iso Inf_lower)
  assume assm: "residuated f"
  obtain y where y_def: "y = ⨅{residual f x |x. x ∈ X}" 
    by auto
  hence "∀x ∈ X. y ≤ residual f x"
    by (auto simp: y_def intro: Inf_lower)
  hence "∀x ∈ X. f y ≤ x"
    by (metis assm residual_galoisI2)
  hence "f y ≤ ⨅ X"
    by (auto intro: Inf_greatest)
  thus "⨅{residual f x |x. x ∈ X} ≤ residual f (⨅X)"
    by (auto simp: assm y_def intro!: residual_galoisI1)
qed

lemma Sup_sup: "∀X. f(⨆ X) = ⨆{f x | x. x ∈ X} ⟹ f (x ⊔ y) = f x ⊔ f y"
  apply (erule_tac x="{x, y}" in allE)
  by (force intro: Sup_eqI)

lemma Sup_residuatedI: "∀X. f(⨆ X) = ⨆{f x | x. x ∈ X} ⟹ residuated f"
proof (unfold residuated_def residuated_pair_def, standard+)
  fix x y
  assume "f x ≤ y"
  thus "x ≤ ⨆{x. f x ≤ y}"
    by (clarsimp intro!: Sup_upper)
next
  fix x y
  assume assm: "∀X. f (⨆X) = ⨆{f x |x. x ∈ X}"
  hence f_iso: "∀x y. x ≤ y ⟶ f x ≤ f y"
    using Sup_sup by (auto simp: le_iff_sup)
  assume "x ≤ ⨆{x. f x ≤ y}"
  hence "f x ≤ f(⨆{x. f x ≤ y})"
    by (metis f_iso)
  also have "... = ⨆{f x | x . f x ≤ y}"
    using assm by auto
  finally show "f x ≤ y"
    apply (rule order_trans)
    by (auto intro!: Sup_least)
qed

lemma Inf_inf: "∀X. f(⨅ X) = ⨅{f x | x. x ∈ X} ⟹ f (x ⊓ y) = f x ⊓ f y"
  apply (erule_tac x="{x, y}" in allE)
  by (force intro: Inf_eqI)

lemma Inf_residuatedI: "∀X. ⨅{g x | x. x ∈ X} = g (⨅ X) ⟹ ∃f. residuated_pair f g"
proof (unfold residuated_pair_def, standard+)
  fix x y
  assume "x ≤ g y"
  thus "⨅{y. x ≤ g y} ≤ y"
    by (clarsimp intro!: Inf_lower)
next
  fix x y
  assume assm: "∀X. ⨅{g x | x. x ∈ X} = g (⨅ X)"
  hence g_iso: "∀x y. x ≤ y ⟶ g x ≤ g y"
    using Inf_inf by (auto simp: le_iff_inf)
  assume "⨅{y. x ≤ g y} ≤ y"
  hence "g (⨅{y. x ≤ g y}) ≤ g y"
    by (metis g_iso)
  hence "(⨅{g y | y. x ≤ g y}) ≤ g y"
    using assm apply (erule_tac x="{y. x ≤ g y}" in allE)
    by (auto intro!: Inf_lower)
  thus "x ≤ g y"
    apply (rule local.dual_order.trans)
    by (auto intro: Inf_greatest)
qed

end (* complete lattices *)

subsection ‹Residuated Structures›

text ‹
  In this section, we define residuated algebraic structures, starting from the simplest of all,
  a \emph{residuated partial ordered groupoid}, to 
  \emph{residuated l-monoids}, which are residuated 
  lattices where the multiplicative operator forms a monoid.
›

class pogroupoid = order + times +
  assumes mult_isor: "x ≤ y ⟹ x ⋅ z ≤ y ⋅ z"
  and mult_isol: "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"

text ‹
  A residuated partial ordered groupoid is simply a partial order and a multiplicative groupoid with 
  two extra operators satisfying the residuation laws.
  It is straighforward to prove that multiplication is compatible with the order,
  that is, multiplication is isotone.
  
  Most of the lemmas below come in pairs; they are related by opposition duality.
  Formalising this duality is left for future work.
›

class residual_r_op =
  fixes residual_r :: "'a ⇒ 'a ⇒ 'a" (infixr "→" 60)

class residual_l_op =
  fixes residual_l :: "'a ⇒ 'a ⇒ 'a" (infixl "←" 60)
  
class residuated_pogroupoid = order + times + residual_l_op + residual_r_op +
  assumes resl_galois: "x ≤ z ← y ⟷ x ⋅ y ≤ z"
  and resr_galois: "x ⋅ y ≤ z ⟷ y ≤ x → z"
begin

lemma reslI [intro]: "x ⋅ y ≤ z ⟹ x ≤ z ← y"
  by (metis resl_galois)

lemma resrI [intro]: "x ⋅ y ≤ z ⟹ y ≤ x → z"
  by (metis resr_galois)

lemma residuated_pair_multl [simp]: "residuated_pair (λx. x ⋅ y) (λx. x ← y)"
  by (auto simp: residuated_pair_def resl_galois)
  
lemma residuated_pair_multr [simp]: "residuated_pair (λy. x ⋅ y) (λy. x → y)"
  by (auto simp: residuated_pair_def resr_galois)

text ‹
  Multiplication is then obviously residuated.
›
  
lemma residuated_multl [simp]: "residuated (λx. x ⋅ y)"
  by (metis residuated_def residuated_pair_multl)

lemma residuated_multr [simp]: "residuated (λy. x ⋅ y)"
  by (metis residuated_def residuated_pair_multr)
  
lemma resl_eq [simp]: "residual (λx. x ⋅ y) = (λx. x ← y)"
  unfolding residual_def apply (rule the1_equality)
  by (auto simp: intro!: residual_unique)
  
lemma resr_eq [simp]: "residual (λy. x ⋅ y) = (λy. x → y)"
  unfolding residual_def apply (rule the1_equality)
  by (auto simp: intro!: residual_unique)
  
text ‹
  Next we prove a few lemmas, all of which are instantiation of more general facts about residuated functions.
›
  
lemma res_lc1: "x ≤ x ⋅ y ← y"
  by auto
  
lemma res_lc2: "x ≤ y ⟹ x ⋅ z ← z ≤ y ⋅ z ← z"
  by (metis local.res_c2 resl_eq residuated_multl)

lemma res_lc3 [simp]: "(x ⋅ y ← y) ⋅ y ← y = x ⋅ y ← y"
  by (metis local.res_c3 resl_eq residuated_multl)
  
lemma res_rc1: "x ≤ y → y ⋅ x"
  by auto

lemma res_rc2: "x ≤ y ⟹ z → z ⋅ x ≤ z → z ⋅ y"
  by (metis local.res_c2 resr_eq residuated_multr)

lemma res_rc3 [simp]: "y → y ⋅ (y → y ⋅ x) = y → y ⋅ x"
  by (metis local.res_c3 resr_eq residuated_multr)
  
lemma res_li1: "(x ← y) ⋅ y ≤ x"
  by (metis local.res_i1 resl_eq residuated_multl)
  
lemma res_li2: "x ≤ y ⟹ (x ← z) ⋅ z ≤ (y ← z) ⋅ z"
  by (metis local.res_i2 resl_eq residuated_multl)
  
lemma res_li3 [simp]: "((x ← y) ⋅ y ← y) ⋅ y = (x ← y) ⋅ y"
  by (metis local.res_i3 resl_eq residuated_multl)
  
lemma res_ri1: "y ⋅ (y → x) ≤ x"
  by (metis local.res_i1 resr_eq residuated_multr)
  
lemma res_ri2: "x ≤ y ⟹ z ⋅ (z → x) ≤ z ⋅ (z → y)"
  by (metis local.res_i2 resr_eq residuated_multr)
  
lemma res_ri3 [simp]: "y ⋅ (y → y ⋅ (y → x)) = y ⋅ (y → x)"
  by (metis local.res_i3 resr_eq residuated_multr)
  
subclass pogroupoid
proof
  fix x y z
  show "x ≤ y ⟹ x ⋅ z ≤ y ⋅ z"
    by (metis local.res_iso residuated_multl)
  show "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
    by (metis local.res_iso residuated_multr)
qed

lemma resl_iso: "x ≤ y ⟹ x ← z ≤ y ← z"
  by (metis res_residual_iso resl_eq residuated_multl)
  
lemma resr_iso: "x ≤ y ⟹ z → x ≤ z → y"
  by (metis res_residual_iso resr_eq residuated_multr)

lemma resl_comp1 [simp]: "(x ⋅ y ← y) ⋅ y = x ⋅ y"
  by (metis order.antisym local.mult_isor res_lc1 res_li1)
  
lemma resl_comp2 [simp]: "(x ← y) ⋅ y ← y = x ← y"
  by (metis order.eq_iff res_lc1 res_li1 resl_iso)
  
lemma resr_comp1 [simp]: "y ⋅ (y → y ⋅ x) = y ⋅ x"
  by (metis order.antisym local.mult_isol res_rc1 res_ri1)
  
lemma resr_comp2 [simp]: "y → y ⋅ (y → x) = y → x"
  by (metis order.eq_iff res_rc1 res_ri1 resr_iso)
  
lemma resl_antitoner: "x ≤ y ⟶ z ← y ≤ z ← x"
  by (metis local.dual_order.trans local.mult_isol res_li1 reslI)

lemma resr_antitonel: "x ≤ y ⟶ y → z ≤ x → z"
  by (metis local.dual_order.trans local.resl_galois res_ri1 resrI)

text ‹The following lemmas are taken from Galatos and \emph{al.}›

lemma jipsen1l: "x ≤ y ← (x → y)"
  by (metis res_ri1 reslI)
  
lemma jipsen1r: "x ≤ (y ← x) → y"
  by (metis res_li1 resrI)
  
lemma jipsen2l: "(y ← (x → y)) → y = x → y"
  by (metis jipsen1l jipsen1r order.eq_iff local.resr_antitonel)
  
lemma jipsen2r: "y ← ((y ← x) → y) = y ← x"
  by (metis jipsen1l jipsen1r order.eq_iff local.resl_antitoner)
  
end (* residuated_pogroupoid *)

text ‹
  In a residuated partial ordered semigroup, the multiplicative operator is associative.
›
  
class residuated_posemigroup = semigroup_mult + residuated_pogroupoid 
begin

lemma resl_trans: "(x ← y)  ⋅  (y ← z) ≤ x ← z"
  by (metis local.res_li1 local.resl_antitoner local.resl_galois mult_assoc)
  
lemma resr_trans: "(x → y)  ⋅  (y → z) ≤ x → z"
  by (metis local.res_ri1 local.resr_antitonel local.resr_galois mult_assoc)
  
lemma resr1: "(x → y) ⋅ z ≤ (x → y ⋅ z)"
  by (metis local.mult_isor local.res_ri1 local.resrI mult_assoc)
  
lemma resr2: "x → y ≤ z ⋅ x → z ⋅ y"
  by (metis local.mult_isol local.res_ri1 local.resrI mult_assoc)
  
lemma resr3: "x ⋅ y → z = y → (x → z)"
  by (metis order.eq_iff local.resr_galois mult_assoc)
  
lemma resl1: "z ⋅ (x ← y) ≤ (z ⋅ x ← y)"
  by (metis local.mult_isol local.res_li1 local.reslI mult_assoc)

lemma resl2: "x ← y ≤ x ⋅ z ← y ⋅ z"
  by (metis local.mult_isor local.res_li1 local.reslI mult_assoc)

lemma resl3: "x ← y ⋅ z = (x ← z) ← y"
  by (metis order.eq_iff local.resl_galois mult_assoc)
  
lemma residual_assoc: "x → (y ← z) = (x → y) ← z"
proof (rule order.antisym)
  show "x → (y ← z) ≤ (x → y) ← z"
    by (metis local.res_ri1 local.resl_galois local.resr_galois mult_assoc)
  show "(x → y) ← z ≤ x → (y ← z)"
    by (metis local.res_li1 local.resl_galois local.resr_galois mult_assoc)
qed

end (* residuated_posemigroup *)

text ‹
  In a residuated partially ordered monoid, the multiplicative operator has a unit $1$; that is,
  its reduct forms a monoid.
›

class residuated_pomonoid = monoid_mult + residuated_pogroupoid 
begin

subclass residuated_posemigroup ..

lemma resl_unit: "x ← 1 = x"
  by (metis local.mult_1_right local.resl_comp1)

lemma resr_unit: "1 → x = x"
  by (metis local.mult_1_left local.resr_comp1)
  
lemma mult_one_resl: "x ⋅ (1 ← y) ≤ x ← y"  
  by (metis local.mult_1_right local.resl1)

lemma mult_one_resr: "(x → 1) ⋅ y ≤ x → y"
  by (metis local.mult_1_left local.resr1)

text ‹More lemmas from Galatos and \emph{al.} follow.›

lemma jipsen3l: "1 ≤ x ← x"
  by (metis local.jipsen1l resr_unit)

lemma jipsen3r: "1 ≤ x → x"
  by (metis local.jipsen1r resl_unit)
  
lemma jipsen4l [simp]: "(x ← x) ⋅ x = x"
  by (metis local.mult_1_left local.resl_comp1)
  
lemma jipsen4r [simp]: "x ⋅ (x → x) = x"
  by (metis local.mult_1_right local.resr_comp1)
  
lemma jipsen5l [simp]: "(x ← x) ⋅ (x ← x) = x ← x"
  by (metis jipsen4l local.resl3)
  
lemma jipsen5r [simp]: "(x → x) ⋅ (x → x) = x → x"
  by (metis jipsen4r local.resr3)
  
lemma jipsen6l: "y ← x ≤ (y ← z) ← (x ← z)"
  by (metis local.resl_galois local.resl_trans)
  
lemma jipsen6r: "x → y ≤ (z → x) → (z → y)"
  by (metis local.resr_galois local.resr_trans)
  
lemma jipsen7l: "y ← x ≤ (z ← y) → (z ← x)"
  by (metis local.resr_galois local.resl_trans)
  
lemma jipsen7r: "x → y ≤ (x → z) ← (y → z)"
  by (metis local.resl_galois local.resr_trans)

end (* residuated_pomonoid *)

text ‹
  Residuated partially ordered groupoids can be expanded residuated join semilattice ordered groupoids.
  They are used as a base for action algebras, which are expansions 
  of Kleene algebras by operations of residuation.
  Action algebras can be found in the AFP entry for Kleene algebras.
›

class residuated_sup_lgroupoid = semilattice_sup + residuated_pogroupoid
begin

lemma distl: "x ⋅ (y ⊔ z) = x ⋅ y ⊔ x ⋅ z"
  by (metis local.residuated_multr local.residuated_sup)
  
lemma distr: "(x ⊔ y) ⋅ z = x ⋅ z ⊔ y ⋅ z"
  by (metis local.residuated_multl local.residuated_sup)
  
lemma resl_subdist_var: "x ← z ≤ (x ⊔ y) ← z"
  by (metis local.resl_iso local.sup_ge1)
 
lemma resl_subdist: "(x ← z) ⊔ (y ← z) ≤ (x ⊔ y) ← z"
  by (metis local.le_sup_iff local.sup_commute resl_subdist_var)
  
lemma resr_subdist_var: "(x → y) ≤ x → (y ⊔ z)"
  by (metis local.resr_iso local.sup_ge1)
  
lemma resr_subdist: "(x → y) ⊔ (x → z) ≤ x → (y ⊔ z)"
  by (metis sup_commute sup_least resr_subdist_var)
  
lemma resl_superdist_var: "x ← (y ⊔ z) ≤ x ← y"
  by (metis local.le_sup_iff local.res_li1 local.reslI local.resr_galois)
  
lemma resr_superdist_var: "(x ⊔ y) → z ≤ x → z"
  by (metis local.le_sup_iff local.res_ri1 local.resl_galois local.resrI)

end (* residuated_sup_lgroupoid *)

text ‹
  Similarly, semigroup and monoid variants can be defined.
›

class residuated_sup_lsemigroup = semilattice_sup + residuated_posemigroup
subclass (in residuated_sup_lsemigroup) residuated_sup_lgroupoid ..

class residuated_sup_lmonoid = semilattice_sup + residuated_posemigroup
subclass (in residuated_sup_lmonoid) residuated_sup_lsemigroup ..

text ‹
  By lattice duality, we define residuated meet semillatice ordered groupoid.
›

class residuated_inf_lgroupoid = semilattice_inf + residuated_pogroupoid
begin

lemma resl_dist: "(x ⊓ y) ← z = (x ← z) ⊓ (y ← z)"
  by (metis local.resl_eq local.residuated_inf local.residuated_multl)

lemma resr_dist: "x → (y ⊓ z) = (x → y) ⊓ (x → z)"
  by (metis local.resr_eq local.residuated_inf local.residuated_multr)

lemma resl_inf_superdist: "x ← y ≤ x ← (y ⊓ z)"
  by (metis local.inf_le1 local.resl_antitoner)

lemma resr_inf_superdist_var: "x → y ≤ (x ⊓ z) → y"
  by (metis local.inf_le1 local.resr_antitonel)
  
end (* residuated_inf_lgroupoid *)

class residuated_inf_lsemigroup = semilattice_inf + residuated_posemigroup
subclass (in residuated_inf_lsemigroup) residuated_inf_lgroupoid ..

class residuated_inf_lmonoid = semilattice_inf + residuated_posemigroup
subclass (in residuated_inf_lmonoid) residuated_inf_lsemigroup ..

text ‹
  Finally, we obtain residuated lattice groupoids. 
›

class residuated_lgroupoid = lattice + residuated_pogroupoid
begin

subclass residuated_sup_lgroupoid ..

lemma resl_distr: "z ← (x ⊔ y) = (z ← x) ⊓ (z ← y)"
proof (rule order.antisym)
  show "z ← x ⊔ y ≤ (z ← x) ⊓ (z ← y)"
    by (metis local.inf.bounded_iff local.resl_superdist_var local.sup_commute)
  show "(z ← x) ⊓ (z ← y) ≤ z ← x ⊔ y"
    by (metis local.inf.cobounded1 local.inf.cobounded2 local.resl_galois local.resr_galois local.sup.bounded_iff)
qed

lemma resr_distl: "(x ⊔ y) → z = (x → z) ⊓ (y → z)"
proof (rule order.antisym)
  show "x ⊔ y → z ≤ (x → z) ⊓ (y → z)"
    by (metis local.inf.bounded_iff local.resr_antitonel local.resr_superdist_var local.sup_ge2)
  show "(x → z) ⊓ (y → z) ≤ x ⊔ y → z"
    by (metis local.inf.cobounded1 local.inf.cobounded2 local.resl_galois local.resr_galois local.sup_least)
qed 

end (* residuated_lgroupoid *)

class residuated_lsemigroup = lattice + residuated_sup_lsemigroup
subclass (in residuated_lsemigroup) residuated_lgroupoid ..

class residuated_lmonoid = lattice + residuated_sup_lmonoid
subclass (in residuated_lmonoid) residuated_lsemigroup ..

class residuated_blgroupoid = bounded_lattice + residuated_pogroupoid
begin

lemma multl_strict [simp]: "x ⋅ ⊥ = ⊥"
  by (metis local.residuated_multr local.residuated_strict)

lemma multr_strict [simp]: "⊥ ⋅ x = ⊥"
  by (metis local.residuated_multl local.residuated_strict)

lemma resl_top [simp]: "⊤ ← x = ⊤"
  by (metis local.res_top local.residuated_multl local.resl_eq)

lemma resl_impl [simp]: "x ← ⊥ = ⊤"
  by (metis local.resl_comp2 multl_strict resl_top)

lemma resr_top [simp]: "x → ⊤ = ⊤"
  by (metis local.resrI local.top_greatest local.top_unique)

lemma resr_impl [simp]: "⊥ → x = ⊤"
  by (metis local.resr_comp2 multr_strict resr_top)

end (* residuated_blgroupoid *)

class residuated_blsemigroup = bounded_lattice + residuated_sup_lsemigroup
subclass (in residuated_blsemigroup) residuated_blgroupoid ..

class residuated_blmonoid = bounded_lattice + residuated_sup_lmonoid
subclass (in residuated_blmonoid) residuated_blsemigroup ..

class residuated_clgroupoid = complete_lattice + residuated_pogroupoid
begin

lemma resl_eq_def: "y ← x = ⨆ {z. z ⋅ x ≤ y}"
  by (metis local.residual_eq1 local.residuated_multl local.resl_eq)

lemma resr_eq_def: "x → y = ⨆ {z. x ⋅ z ≤ y}"
  by (metis local.residual_eq1 local.residuated_multr local.resr_eq)

lemma multl_def: "x ⋅ y = ⨅ {z. x ≤ z ← y}"
proof -
  have "⨅{ya. x ≤ residual (λa. a ⋅ y) ya} = ⨅{z. x ≤ z ← y}"
    by simp
  thus ?thesis
    by (metis residuated_multl residual_eq2)
qed

lemma multr_def: "x ⋅ y = ⨅ {z. y ≤ x → z}"
proof -
  have "⨅{ya. y ≤ residual ((⋅) x) ya} = ⨅{z. y ≤ x → z}"
    by simp
  thus ?thesis
    by (metis residuated_multr residual_eq2)
qed

end (* residuated_clgroupoid *)

class residuated_clsemigroup = complete_lattice + residuated_sup_lsemigroup
subclass (in residuated_clsemigroup) residuated_clgroupoid ..

class residuated_clmonoid = complete_lattice + residuated_sup_lmonoid
subclass (in residuated_clmonoid) residuated_clsemigroup ..

end