# Theory Residuated_Boolean_Algebras

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

section ‹Residuated Boolean Algebras›

theory Residuated_Boolean_Algebras
imports Residuated_Lattices
begin

unbundle lattice_syntax

subsection ‹Conjugation on Boolean Algebras›

text ‹
Similarly, as in the previous section, we define the conjugation for
arbitrary residuated functions on boolean algebras.
›

context boolean_algebra
begin

lemma inf_bot_iff_le: "x ⊓ y = ⊥ ⟷ x ≤ -y"
by (metis le_iff_inf inf_sup_distrib1 inf_top_right sup_bot.left_neutral sup_compl_top compl_inf_bot inf.assoc inf_bot_right)

lemma le_iff_inf_bot: "x ≤ y ⟷ x ⊓ -y = ⊥"
by (metis inf_bot_iff_le compl_le_compl_iff inf_commute)

lemma indirect_eq: "(⋀z. x ≤ z ⟷ y ≤ z) ⟹ x = y"
by (metis order.eq_iff)

text ‹
Let $B$ be a boolean algebra. The maps $f$ and $g$ on $B$ are
a pair of conjugates if and only if for all $x, y \in B$,
$f(x) \sqcap y = \bot \Leftrightarrow x \sqcap g(t) = \bot$.
›

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

lemma conjugation_pair_commute: "conjugation_pair f g ⟹ conjugation_pair g f"
by (auto simp: conjugation_pair_def inf_commute)

lemma conjugate_iff_residuated: "conjugation_pair f g = residuated_pair f (λx. -g(-x))"
apply (clarsimp simp: conjugation_pair_def residuated_pair_def inf_bot_iff_le)
by (metis double_compl)

lemma conjugate_residuated: "conjugation_pair f g ⟹ residuated_pair f (λx. -g(-x))"
by (metis conjugate_iff_residuated)

lemma residuated_iff_conjugate: "residuated_pair f g = conjugation_pair f (λx. -g(-x))"
apply (clarsimp simp: conjugation_pair_def residuated_pair_def inf_bot_iff_le)
by (metis double_compl)

text ‹
A map $f$ has a conjugate pair if and only if it is residuated.
›

lemma conj_residuatedI1: "∃g. conjugation_pair f g ⟹ residuated f"
by (metis conjugate_iff_residuated residuated_def)

lemma conj_residuatedI2: "∃g. conjugation_pair g f ⟹ residuated f"
by (metis conj_residuatedI1 conjugation_pair_commute)

lemma exist_conjugateI[intro]: "residuated f ⟹ ∃g. conjugation_pair f g"
by (metis residuated_def residuated_iff_conjugate)

lemma exist_conjugateI2[intro]: "residuated f ⟹ ∃g. conjugation_pair g f"
by (metis exist_conjugateI conjugation_pair_commute)

text ‹
The conjugate of a residuated function $f$ is unique.
›

lemma unique_conjugate[intro]: "residuated f ⟹ ∃!g. conjugation_pair f g"
proof -
{
fix g h x assume "conjugation_pair f g" and "conjugation_pair f h"
hence "g = h"
apply (unfold conjugation_pair_def)
apply (rule ext)
apply (rule order.antisym)
by (metis le_iff_inf_bot inf_commute inf_compl_bot)+
}
moreover assume "residuated f"
ultimately show ?thesis by force
qed

lemma unique_conjugate2[intro]: "residuated f ⟹ ∃!g. conjugation_pair g f"
by (metis unique_conjugate conjugation_pair_commute)

text ‹
Since the conjugate of a residuated map is unique, we define a
conjugate operation.
›

definition conjugate :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"conjugate f ≡ THE g. conjugation_pair g f"

lemma conjugate_iff_def: "residuated f ⟹ f(x) ⊓ y = ⊥ ⟷ x ⊓ conjugate f y = ⊥"
apply (clarsimp simp: conjugate_def dest!: unique_conjugate)
apply (subgoal_tac "(THE g. conjugation_pair g f) = g")
apply (rule the1_equality)
by (auto intro: conjugation_pair_commute)

lemma conjugateI1: "residuated f ⟹ f(x) ⊓ y = ⊥ ⟹ x ⊓ conjugate f y = ⊥"
by (metis conjugate_iff_def)

lemma conjugateI2: "residuated f ⟹ x ⊓ conjugate f y = ⊥ ⟹ f(x) ⊓ y = ⊥"
by (metis conjugate_iff_def)

text ‹
Few more lemmas about conjugation follow.
›

lemma residuated_conj1: "residuated f ⟹ conjugation_pair f (conjugate f)"
using conjugateI1 conjugateI2 conjugation_pair_def by auto

lemma residuated_conj2: "residuated f ⟹ conjugation_pair (conjugate f) f"
using conjugateI1 conjugateI2 conjugation_pair_def inf_commute by auto

lemma conj_residuated: "residuated f ⟹ residuated (conjugate f)"
by (force dest!: residuated_conj2 intro: conj_residuatedI1)

lemma conj_involution: "residuated f ⟹ conjugate (conjugate f) = f"
by (metis conj_residuated residuated_conj1 residuated_conj2 unique_conjugate)

lemma residual_conj_eq: "residuated f ⟹ residual (conjugate f) = (λx. -f(-x))"
apply (unfold residual_def)
apply (rule the1_equality)
apply (rule residual_unique)
apply (auto intro: conj_residuated conjugate_residuated residuated_conj2)
done

lemma residual_conj_eq_ext: "residuated f ⟹ residual (conjugate f) x = -f(-x)"
by (metis residual_conj_eq)

lemma conj_iso: "residuated f ⟹ x ≤ y ⟹ conjugate f x ≤ conjugate f y"
by (metis conj_residuated res_iso)

lemma conjugate_strict: "residuated f ⟹ conjugate f ⊥ = ⊥"
by (metis conj_residuated residuated_strict)

lemma conjugate_sup: "residuated f ⟹ conjugate f (x ⊔ y) = conjugate f x ⊔ conjugate f y"
by (metis conj_residuated residuated_sup)

lemma conjugate_subinf: "residuated f ⟹ conjugate f (x ⊓ y) ≤ conjugate f x ⊓ conjugate f y"
by (auto simp: conj_iso)

text ‹
Next we prove some lemmas from Maddux's article. Similar lemmas have been proved in AFP entry
for relation algebras. They should be consolidated in the future.
›

lemma maddux1: "residuated f ⟹ f(x ⊓ - conjugate f(y)) ≤ f(x) ⊓ -y"
proof -
assume assm: "residuated f"
hence "f(x ⊓ - conjugate f(y)) ≤ f x"
by (metis inf_le1 res_iso)
moreover have "f(x ⊓ - conjugate f (y)) ⊓ y = ⊥"
by (metis assm conjugateI2 inf_bot_iff_le inf_le2)
ultimately show ?thesis
by (metis inf_bot_iff_le le_inf_iff)
qed

lemma maddux1': "residuated f ⟹ conjugate f(x ⊓ -f(y)) ≤ conjugate f(x) ⊓ -y"

lemma maddux2: "residuated f ⟹ f(x) ⊓ y ≤ f(x ⊓ conjugate f y)"
proof -
assume resf: "residuated f"
obtain z where z_def: "z = f(x ⊓ conjugate f y)" by auto
hence "f(x ⊓ conjugate f y) ⊓ -z = ⊥"
by (metis inf_compl_bot)
hence "x ⊓ conjugate f y ⊓ conjugate f (-z) = ⊥"
by (metis conjugate_iff_def resf)
hence "x ⊓ conjugate f (y ⊓ -z) = ⊥"
apply (subgoal_tac "conjugate f (y ⊓ -z) ≤ conjugate f y ⊓ conjugate f (-z)")
apply (metis (no_types, opaque_lifting) dual_order.trans inf.commute inf_bot_iff_le inf_left_commute)
by (metis conj_iso inf_le2 inf_top.left_neutral le_inf_iff resf)
hence "f(x) ⊓ y ⊓ -z = ⊥"
by (metis conjugateI2 inf.assoc resf)
thus ?thesis
by (metis double_compl inf_bot_iff_le z_def)
qed

lemma maddux2': "residuated f ⟹ conjugate f(x) ⊓ y ≤ conjugate f(x ⊓ f y)"

lemma residuated_conjugate_ineq: "residuated f ⟹ conjugate f x ≤ y ⟷ x ≤ -f(-y)"
by (metis conj_residuated residual_galois residual_conj_eq)

lemma residuated_comp_closed: "residuated f ⟹ residuated g ⟹ residuated (f o g)"
by (auto simp add: residuated_def residuated_pair_def)

lemma conjugate_comp: "residuated f ⟹ residuated g ⟹ conjugate (f o g) = conjugate g o conjugate f"
proof (rule ext, rule indirect_eq)
fix x y
assume assms: "residuated f" "residuated g"
have "conjugate (f o g) x ≤ y ⟷ x ≤ -f(g(-y))"
apply (subst residuated_conjugate_ineq)
using assms by (auto intro!: residuated_comp_closed)
also have "... ⟷ conjugate g (conjugate f x) ≤ y"
using assms by (simp add: residuated_conjugate_ineq)
finally show "(conjugate (f ∘ g) x ≤ y) = ((conjugate g ∘ conjugate f) x ≤ y)"
by auto
qed

lemma conjugate_comp_ext: "residuated f ⟹ residuated g ⟹ conjugate (λx. f (g x)) x = conjugate g (conjugate f x)"
using conjugate_comp by (simp add: comp_def)

end (* boolean_algebra *)

context complete_boolean_algebra begin

text ‹
On a complete boolean algebra, it is possible to give an explicit
definition of conjugation.
›

lemma conjugate_eq: "residuated f ⟹ conjugate f y = ⨅{x. y ≤ -f(-x)}"
proof -
assume assm: "residuated f" obtain g where g_def: "g = conjugate f" by auto
have "g y = ⨅{x. x ≥ g y}"
by (auto intro!: order.antisym Inf_lower Inf_greatest)
also have "... = ⨅{x. -x ⊓ g y = ⊥}"
also have "... = ⨅{x. f(-x) ⊓ y = ⊥}"
by (metis conjugate_iff_def assm g_def)
finally show ?thesis
by (simp add: g_def le_iff_inf_bot inf_commute)
qed

end (* complete_boolean_algebra *)

subsection ‹Residuated Boolean Structures›

text ‹
In this section, we present various residuated structures based on
boolean algebras.
The left and right conjugation of the multiplicative operation is
defined, and a number of facts is derived.
›

class residuated_boolean_algebra = boolean_algebra + residuated_pogroupoid
begin

subclass residuated_lgroupoid ..

definition conjugate_l :: "'a ⇒ 'a ⇒ 'a" (infixl "⊲" 60) where
"x ⊲ y ≡ -(-x ← y)"

definition conjugate_r :: "'a ⇒ 'a ⇒ 'a" (infixl "⊳" 60) where
"x ⊳ y ≡ -(x → -y)"

lemma residual_conjugate_r: "x → y = -(x ⊳ -y)"
by (metis conjugate_r_def double_compl)

lemma residual_conjugate_l: "x ← y = -(-x ⊲ y)"
by (metis conjugate_l_def double_compl)

lemma conjugation_multl: "x⋅y ⊓ z = ⊥ ⟷ x ⊓ (z ⊲ y) = ⊥"
by (metis conjugate_l_def double_compl le_iff_inf_bot resl_galois)

lemma conjugation_multr: "x⋅y ⊓ z = ⊥ ⟷ y ⊓ (x ⊳ z) = ⊥"
by (metis conjugate_r_def inf_bot_iff_le le_iff_inf_bot resr_galois)

lemma conjugation_conj: "(x ⊲ y) ⊓ z = ⊥ ⟷ y ⊓ (z ⊳ x) = ⊥"
by (metis inf_commute conjugation_multr conjugation_multl)

lemma conjugation_pair_multl [simp]: "conjugation_pair (λx. x⋅y) (λx. x ⊲ y)"

lemma conjugation_pair_multr [simp]: "conjugation_pair (λx. y⋅x) (λx. y ⊳ x)"

lemma conjugation_pair_conj [simp]: "conjugation_pair (λx. y ⊲ x) (λx. x ⊳ y)"

lemma residuated_conjl1 [simp]: "residuated (λx. x ⊲ y)"
by (metis conj_residuatedI2 conjugation_pair_multl)

lemma residuated_conjl2 [simp]: "residuated (λx. y ⊲ x)"
by (metis conj_residuatedI1 conjugation_pair_conj)

lemma residuated_conjr1 [simp]: "residuated (λx. y ⊳ x)"
by (metis conj_residuatedI2 conjugation_pair_multr)

lemma residuated_conjr2 [simp]: "residuated (λx. x ⊳ y)"
by (metis conj_residuatedI2 conjugation_pair_conj)

lemma conjugate_multr [simp]: "conjugate (λx. y⋅x) = (λx. y ⊳ x)"
by (metis conjugation_pair_multr residuated_conj1 residuated_multr unique_conjugate)

lemma conjugate_conjr1 [simp]: "conjugate (λx. y ⊳ x) = (λx. y⋅x)"
by (metis conjugate_multr conj_involution residuated_multr)

lemma conjugate_multl [simp]: "conjugate (λx. x⋅y) = (λx. x ⊲ y)"
by (metis conjugation_pair_multl residuated_conj1 residuated_multl unique_conjugate)

lemma conjugate_conjl1 [simp]: "conjugate (λx. x ⊲ y) = (λx. x⋅y)"
proof -
have "conjugate (conjugate (λx. x⋅y)) = conjugate (λx. x ⊲ y)" by simp
thus ?thesis
by (metis conj_involution[OF residuated_multl])
qed

lemma conjugate_conjl2[simp]: "conjugate (λx. y ⊲ x) = (λx. x ⊳ y)"
by (metis conjugation_pair_conj unique_conjugate residuated_conj1 residuated_conjl2)

lemma conjugate_conjr2[simp]: "conjugate (λx. x ⊳ y) = (λx. y ⊲ x)"
proof -
have "conjugate (conjugate (λx. y ⊲ x)) = conjugate (λx. x ⊳ y)" by simp
thus ?thesis
by (metis conj_involution[OF residuated_conjl2])
qed

lemma conjl1_iso: "x ≤ y ⟹ x ⊲ z ≤ y ⊲ z"
by (metis conjugate_l_def compl_mono resl_iso)

lemma conjl2_iso: "x ≤ y ⟹ z ⊲ x ≤ z ⊲ y"
by (metis res_iso residuated_conjl2)

lemma conjr1_iso: "x ≤ y ⟹ z ⊳ x ≤ z ⊳ y"
by (metis res_iso residuated_conjr1)

lemma conjr2_iso: "x ≤ y ⟹ x ⊳ z ≤ y ⊳ z"
by (metis conjugate_r_def compl_mono resr_antitonel)

lemma conjl1_sup: "z ⊲ (x ⊔ y) = (z ⊲ x) ⊔ (z ⊲ y)"
by (metis conjugate_l_def compl_inf resl_distr)

lemma conjl2_sup: "(x ⊔ y) ⊲ z = (x ⊲ z) ⊔ (y ⊲ z)"
by (metis (poly_guards_query) residuated_sup residuated_conjl1)

lemma conjr1_sup: "z ⊳ (x ⊔ y) = (z ⊳ x) ⊔ (z ⊳ y)"
by (metis residuated_sup residuated_conjr1)

lemma conjr2_sup: "(x ⊔ y) ⊳ z = (x ⊳ z) ⊔ (y ⊳ z)"
by (metis conjugate_r_def compl_inf resr_distl)

lemma conjl1_strict: "⊥ ⊲ x = ⊥"
by (metis residuated_strict residuated_conjl1)

lemma conjl2_strict: "x ⊲ ⊥ = ⊥"
by (metis residuated_strict residuated_conjl2)

lemma conjr1_strict: "⊥ ⊳ x = ⊥"
by (metis residuated_strict residuated_conjr2)

lemma conjr2_strict: "x ⊳ ⊥ = ⊥"
by (metis residuated_strict residuated_conjr1)

lemma conjl1_iff: "x ⊲ y ≤ z ⟷ x ≤ -(-z⋅y)"
by (metis conjugate_l_def compl_le_swap1 compl_le_swap2 resl_galois)

lemma conjl2_iff: "x ⊲ y ≤ z ⟷ y ≤ -(-z ⊳ x)"
by (metis conjl1_iff conjugate_r_def compl_le_swap2 double_compl resr_galois)

lemma conjr1_iff: "x ⊳ y ≤ z ⟷ y ≤ -(x⋅-z)"
by (metis conjugate_r_def compl_le_swap1 double_compl resr_galois)

lemma conjr2_iff: "x ⊳ y ≤ z ⟷ x ≤ -(y ⊲ -z)"
by (metis conjugation_conj double_compl inf.commute le_iff_inf_bot)

text ‹
We apply Maddux's lemmas regarding conjugation of an arbitrary residuated function
for each of the 6 functions.
›

lemma maddux1a: "a⋅(x ⊓ -(a ⊳ y)) ≤ a⋅x"
by (insert maddux1 [of "λx. a⋅x"]) simp

lemma maddux1a': "a⋅(x ⊓ -(a ⊳ y)) ≤ -y"
by (insert maddux1 [of "λx. a⋅x"]) simp

lemma maddux1b: "(x ⊓ -(y ⊲ a))⋅a ≤ x⋅a"
by (insert maddux1 [of "λx. x⋅a"]) simp

lemma maddux1b': "(x ⊓ -(y ⊲ a))⋅a ≤ -y"
by (insert maddux1 [of "λx. x⋅a"]) simp

lemma maddux1c: " a ⊲ x ⊓ -(y ⊳ a) ≤ a ⊲ x"
by (insert maddux1 [of "λx. a ⊲ x"]) simp

lemma maddux1c': "a ⊲ x ⊓ -(y ⊳ a) ≤ -y"
by (insert maddux1 [of "λx. a ⊲ x"]) simp

lemma maddux1d: "a ⊳ x ⊓ -(a⋅y) ≤ a ⊳ x"
by (insert maddux1 [of "λx. a ⊳ x"]) simp

lemma maddux1d': "a ⊳ x ⊓ -(a⋅y) ≤ -y"
by (insert maddux1 [of "λx. a ⊳ x"]) simp

lemma maddux1e: "x ⊓ -(y⋅a) ⊲ a ≤ x ⊲ a"
by (insert maddux1 [of "λx. x ⊲ a"]) simp

lemma maddux1e': "x ⊓ -(y⋅a) ⊲ a ≤ -y"
by (insert maddux1 [of "λx. x ⊲ a"]) simp

lemma maddux1f: "x ⊓ -(a ⊲ y) ⊳ a ≤ x ⊳ a"
by (insert maddux1 [of "λx. x ⊳ a"]) simp

lemma maddux1f': "x ⊓ -(a ⊲ y) ⊳ a ≤ -y"
by (insert maddux1 [of "λx. x ⊳ a"]) simp

lemma maddux2a: "a⋅x ⊓ y ≤ a⋅(x ⊓ (a ⊳ y))"
by (insert maddux2 [of "λx. a⋅x"]) simp

lemma maddux2b: "x⋅a ⊓ y ≤ (x ⊓ (y ⊲ a))⋅a"
by (insert maddux2 [of "λx. x⋅a"]) simp

lemma maddux2c: "(a ⊲ x) ⊓ y ≤ a ⊲ (x ⊓ (y ⊳ a))"
by (insert maddux2 [of "λx. a ⊲ x"]) simp

lemma maddux2d: "(a ⊳ x) ⊓ y ≤ a ⊳ (x ⊓ (a⋅y))"
by (insert maddux2 [of "λx. a ⊳ x"]) simp

lemma maddux2e: "(x ⊲ a) ⊓ y ≤ (x ⊓ (y⋅a)) ⊲ a"
by (insert maddux2 [of "λx. x ⊲ a"]) simp

lemma maddux2f: "(x ⊳ a) ⊓ y ≤ (x ⊓ (a ⊲ y)) ⊳ a"
by (insert maddux2 [of "λx. x ⊳ a"]) simp

text ‹
The multiplicative operation $\cdot$ on a residuated boolean algebra is generally not
associative. We prove some equivalences related to associativity.
›

lemma res_assoc_iff1: "(∀x y z. x⋅(y⋅z) = (x⋅y)⋅z) ⟷ (∀x y z. x ⊳ (y ⊳ z) = y⋅x ⊳ z)"
proof safe
fix x y z assume "∀x y z. x⋅(y⋅z) = (x⋅y)⋅z"
thus "x ⊳ (y ⊳ z) = y ⋅ x ⊳ z"
using conjugate_comp_ext[of "λz. y⋅z" "λz. x⋅z"] by auto
next
fix x y z assume "∀x y z. x ⊳ (y ⊳ z) = y⋅x ⊳ z"
thus "x⋅(y⋅z) = (x⋅y)⋅z"
using conjugate_comp_ext[of "λz. y ⊳ z" "λz. x ⊳ z"] by auto
qed

lemma res_assoc_iff2: "(∀x y z. x⋅(y⋅z) = (x⋅y)⋅z) ⟷ (∀x y z. x ⊲ (y ⋅ z) = (x ⊲ z) ⊲ y)"
proof safe
fix x y z assume "∀x y z. x⋅(y⋅z) = (x⋅y)⋅z"
hence "∀x y z. (x⋅y)⋅z = x⋅(y⋅z)" by simp
thus "x ⊲ (y ⋅ z) = (x ⊲ z) ⊲ y"
using conjugate_comp_ext[of "λx. x⋅z" "λx. x⋅y"] by auto
next
fix x y z assume "∀x y z. x ⊲ (y ⋅ z) = (x ⊲ z) ⊲ y"
hence "∀x y z. (x ⊲ z) ⊲ y = x ⊲ (y ⋅ z)" by simp
thus "x⋅(y⋅z) = (x⋅y)⋅z"
using conjugate_comp_ext[of "λz. z ⊲ y" "λx. x ⊲ z"] by auto
qed

lemma res_assoc_iff3: "(∀x y z. x⋅(y⋅z) = (x⋅y)⋅z) ⟷ (∀x y z. (x ⊳ y) ⊲ z = x ⊳ (y ⊲ z))"
proof safe
fix x y z assume "∀x y z. x⋅(y⋅z) = (x⋅y)⋅z"
thus "(x ⊳ y) ⊲ z = x ⊳ (y ⊲ z)"
using conjugate_comp_ext[of "λu. x⋅u" "λu. u⋅z"] and
conjugate_comp_ext[of "λu. u⋅z" "λu. x⋅u", symmetric]
by auto
next
fix x y z assume "∀x y z. (x ⊳ y) ⊲ z = x ⊳ (y ⊲ z)"
thus "x⋅(y⋅z) = (x⋅y)⋅z"
using conjugate_comp_ext[of "λu. x ⊳ u" "λu. u ⊲ z"] and
conjugate_comp_ext[of "λu. u ⊲ z" "λu. x ⊳ u", symmetric]
by auto
qed

end (* residuated_boolean_algebra *)

class unital_residuated_boolean = residuated_boolean_algebra + one +
assumes mult_onel [simp]: "x⋅1 = x"
and mult_oner [simp]: "1⋅x = x"
begin

text ‹
The following equivalences are taken from J{\'o}sson and Tsinakis.
›

lemma jonsson1a: "(∃f. ∀x y. x ⊳ y = f(x)⋅y) ⟷ (∀x y. x ⊳ y = (x ⊳ 1)⋅y)"
apply standard
apply force
apply (rule_tac x="λx. x ⊳ 1" in exI)
apply force
done

lemma jonsson1b: "(∀x y. x ⊳ y = (x ⊳ 1)⋅y) ⟷ (∀x y. x⋅y = (x ⊳ 1) ⊳ y)"
proof safe
fix x y
assume "∀x y. x ⊳ y = (x ⊳ 1)⋅y"
hence "conjugate (λy. x ⊳ y) = conjugate (λy. (x ⊳ 1)⋅y)" by metis
thus "x⋅y = (x ⊳ 1) ⊳ y" by simp
next
fix x y
assume "∀x y. x ⋅ y = x ⊳ 1 ⊳ y"
thus "x ⊳ y = (x ⊳ 1) ⋅ y"
by (metis mult_onel)
qed

lemma jonsson1c: "(∀x y. x ⊳ y = (x ⊳ 1)⋅y) ⟷ (∀x y. y ⊲ x = 1 ⊲ (x ⊲ y))"
proof safe
fix x y
assume "∀x y. x ⊳ y = (x ⊳ 1)⋅y"
hence "(λx. x ⊳ y) = (λx. (x ⊳ 1)⋅y)" by metis
hence "(λx. x ⊳ y) = (λx. x⋅y) o (λx. x ⊳ 1)" by force
hence "conjugate (λx. y ⊲ x) = (λx. x⋅y) o conjugate (λx. 1 ⊲ x)" by simp
hence "conjugate (conjugate (λx. y ⊲ x)) = conjugate ((λx. x⋅y) o conjugate (λx. 1 ⊲ x))" by simp
hence "(λx. y ⊲ x) = conjugate ((λx. x⋅y) o conjugate (λx. 1 ⊲ x))" by simp
also have "... = conjugate (conjugate (λx. 1 ⊲ x)) o conjugate (λx. x⋅y)"
by (subst conjugate_comp[symmetric]) simp_all
finally show "y ⊲ x = 1 ⊲ (x ⊲ y)" by simp
next
fix x y
assume "∀x y. y ⊲ x = 1 ⊲ (x ⊲ y)"
hence "(λx. y ⊲ x) = (λx. 1 ⊲ (x ⊲ y))" by metis
hence "(λx. y ⊲ x) = (λx. 1 ⊲ x) o conjugate (λx. x⋅y)" by force
hence "conjugate (λx. y ⊲ x) = conjugate ((λx. 1 ⊲ x) o conjugate (λx. x⋅y))" by metis
also have "... = conjugate (conjugate (λx. x⋅y)) o conjugate (λx. 1 ⊲ x)"
by (subst conjugate_comp[symmetric]) simp_all
finally have "(λx. x ⊳ y) = (λx. x⋅y) o (λx. x ⊳ 1)" by simp
hence "(λx. x ⊳ y) = (λx. (x ⊳ 1) ⋅ y)" by (simp add: comp_def)
thus "x ⊳ y = (x ⊳ 1) ⋅ y" by metis
qed

lemma jonsson2a: "(∃g. ∀x y. x ⊲ y = x⋅g(y)) ⟷ (∀x y. x ⊲ y = x⋅(1 ⊲ y))"
apply standard
apply force
apply (rule_tac x="λx. 1 ⊲ x" in exI)
apply force
done

lemma jonsson2b: "(∀x y. x ⊲ y = x⋅(1 ⊲ y)) ⟷ (∀x y. x⋅y = x ⊲ (1 ⊲ y))"
proof safe
fix x y
assume "∀x y. x ⊲ y = x⋅(1 ⊲ y)"
hence "conjugate (λx. x ⊲ y) = conjugate (λx. x⋅(1 ⊲ y))" by metis
thus "x⋅y = x ⊲ (1 ⊲ y)" by simp metis
next
fix x y
assume "∀x y. x⋅y = x ⊲ (1 ⊲ y)"
hence "(λx. x⋅y) = (λx. x ⊲ (1 ⊲ y))" by metis
hence "conjugate (λx. x⋅y) = conjugate (λx. x ⊲ (1 ⊲ y))" by metis
thus "x ⊲ y = x ⋅ (1 ⊲ y)" by simp metis
qed

lemma jonsson2c: "(∀x y. x ⊲ y = x⋅(1 ⊲ y)) ⟷ (∀x y. y ⊳ x = (x ⊳ y) ⊳ 1)"
proof safe
fix x y
assume "∀x y. x ⊲ y = x⋅(1 ⊲ y)"
hence "(λy. x ⊲ y) = (λy. x⋅(1 ⊲ y))" by metis
hence "(λy. x ⊲ y) = (λy. x⋅y) o (λy. 1 ⊲ y)" by force
hence "conjugate (λy. y ⊳ x) = (λy. x⋅y) o conjugate (λy. y ⊳ 1)" by force
hence "conjugate (conjugate (λy. y ⊳ x)) = conjugate ((λy. x⋅y) o conjugate (λy. y ⊳ 1))" by metis
hence "(λy. y ⊳ x) = conjugate ((λy. x⋅y) o conjugate (λy. y ⊳ 1))" by simp
also have "... = conjugate (conjugate (λy. y ⊳ 1)) o conjugate (λy. x⋅y)"
by (subst conjugate_comp[symmetric]) simp_all
finally have "(λy. y ⊳ x) = (λy. x ⊳ y ⊳ 1)" by (simp add: comp_def)
thus "y ⊳ x = x ⊳ y ⊳ 1" by metis
next
fix x y
assume "∀x y. y ⊳ x = x ⊳ y ⊳ 1"
hence "(λy. y ⊳ x) = (λy. x ⊳ y ⊳ 1)" by force
hence "(λy. y ⊳ x) = (λy. y ⊳ 1) o conjugate (λy. x⋅y)" by force
hence "conjugate (λy. y ⊳ x) = conjugate ((λy. y ⊳ 1) o conjugate (λy. x⋅y))" by metis
also have "... = conjugate (conjugate (λy. x⋅y)) o conjugate (λy. y ⊳ 1)"
by (subst conjugate_comp[symmetric]) simp_all
finally have "(λy. x ⊲ y) = (λy. x⋅y) o (λy. 1 ⊲ y)"
by (metis conjugate_conjr1 conjugate_conjr2 conjugate_multr)
thus "x ⊲ y = x ⋅ (1 ⊲ y)" by (simp add: comp_def)
qed

lemma jonsson3a: "(∀x. (x ⊳ 1) ⊳ 1 = x) ⟷ (∀x. 1 ⊲ (1 ⊲ x) = x)"
proof safe
fix x assume "∀x. x ⊳ 1 ⊳ 1 = x"
thus "1 ⊲ (1 ⊲ x) = x"
by (metis compl_le_swap1 compl_le_swap2 conjr2_iff order.eq_iff)
next
fix x assume "∀x. 1 ⊲ (1 ⊲ x) = x"
thus "x ⊳ 1 ⊳ 1 = x"
by (metis conjugate_l_def conjugate_r_def double_compl jipsen2r)
qed

lemma jonsson3b: "(∀x. (x ⊳ 1) ⊳ 1 = x) ⟹ (x ⊓ y) ⊳ 1 = (x ⊳ 1) ⊓ (y ⊳ 1)"
proof (rule order.antisym, auto simp: conjr2_iso)
assume assm: "∀x. (x ⊳ 1) ⊳ 1 = x"
hence "(x ⊳ 1) ⊓ (y ⊳ 1) ⊳ 1 = x ⊓ (((x ⊳ 1) ⊓ (y ⊳ 1) ⊳ 1) ⊓ y)"
by (metis (no_types) conjr2_iso inf.cobounded2 inf.commute inf.orderE)
hence "(x ⊳ 1) ⊓ (y ⊳ 1) ⊳ 1 ≤ x ⊓ y"
using inf.orderI inf_left_commute by presburger
thus "(x ⊳ 1) ⊓ (y ⊳ 1) ≤ x ⊓ y ⊳ 1"
using assm by (metis (no_types) conjr2_iso)
qed

lemma jonsson3c: "∀x. (x ⊳ 1) ⊳ 1 = x ⟹ x ⊳ 1 = 1 ⊲ x"
proof (rule indirect_eq)
fix z
assume assms: "∀x. (x ⊳ 1) ⊳ 1 = x"
hence "(x ⊳ 1) ⊓ -z = ⊥ ⟷ ((x ⊳ 1) ⊓ -z) ⊳ 1 = ⊥"
by (metis compl_sup conjugation_conj double_compl inf_bot_right sup_bot.left_neutral)
also have "... ⟷ -z⋅x ⊓ 1 = ⊥"
by (metis assms jonsson3b conjugation_multr)
finally have "(x ⊳ 1) ⊓ -z = ⊥ ⟷ (1 ⊲ x) ⊓ -z = ⊥"
by (metis conjugation_multl inf.commute)
thus "(x ⊳ 1 ≤ z) ⟷ (1 ⊲ x ≤ z)"
by (metis le_iff_inf_bot)
qed

end (* unital_residuated_boolean *)

class residuated_boolean_semigroup = residuated_boolean_algebra + semigroup_mult
begin

subclass residuated_boolean_algebra ..

text ‹
The following lemmas hold trivially, since they are equivalent to associativity.
›

lemma res_assoc1: "x ⊳ (y ⊳ z) = y⋅x ⊳ z"
by (metis res_assoc_iff1 mult_assoc)

lemma res_assoc2: "x ⊲ (y ⋅ z) = (x ⊲ z) ⊲ y"
by (metis res_assoc_iff2 mult_assoc)

lemma res_assoc3: "(x ⊳ y) ⊲ z = x ⊳ (y ⊲ z)"
by (metis res_assoc_iff3 mult_assoc)

end (*residuated_boolean_semigroup *)

class residuated_boolean_monoid = residuated_boolean_algebra + monoid_mult
begin

subclass unital_residuated_boolean
by standard auto

subclass residuated_lmonoid ..

lemma jonsson4: "(∀x y. x ⊲ y = x⋅(1 ⊲ y)) ⟷ (∀x y. x ⊳ y = (x ⊳ 1)⋅y)"
proof safe
fix x y assume assms: "∀x y. x ⊲ y = x⋅(1 ⊲ y)"
have "x ⊳ y = (y ⊳ x) ⊳ 1"
by (metis assms jonsson2c)
also have "... = (y ⊳ ((x ⊳ 1) ⊳ 1)) ⊳ 1"
by (metis assms jonsson2b jonsson3a mult_oner)
also have "... = (((x ⊳ 1)⋅y) ⊳ 1) ⊳ 1"
by (metis conjugate_r_def double_compl resr3)
also have "... = (x ⊳ 1)⋅y"
by (metis assms jonsson2b jonsson3a mult_oner)
finally show "x ⊳ y = (x ⊳ 1)⋅y" .
next
fix x y assume assms: "∀x y. x ⊳ y = (x ⊳ 1)⋅y"
have "y ⊲ x = 1 ⊲ (x ⊲ y)"
by (metis assms jonsson1c)
also have "... = 1 ⊲ ((1 ⊲ (1 ⊲ x)) ⊲ y)"
by (metis assms conjugate_l_def double_compl jonsson1c mult_1_right resl3)
also have "... = 1 ⊲ (1 ⊲ (y⋅(1 ⊲ x)))"
by (metis conjugate_l_def double_compl resl3)
also have "... = y⋅(1 ⊲ x)"
by (metis assms jonsson1b jonsson1c jonsson3c mult_onel)
finally show "y ⊲ x = y⋅(1 ⊲ x)" .
qed

end (* residuated_boolean_monoid *)

end