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 (clarsimp simp add: conjugation_pair_def)
  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"
  by (metis conj_involution conj_residuated maddux1)
  
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)"
  by (metis conj_involution conj_residuated maddux2)
  
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 = ⊥}"
    by (simp add: inf_bot_iff_le)
  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)"
  by (simp add: conjugation_pair_def conjugation_multl)
  
lemma conjugation_pair_multr [simp]: "conjugation_pair (λx. y⋅x) (λx. y ⊳ x)"
  by (simp add: conjugation_pair_def conjugation_multr)
  
lemma conjugation_pair_conj [simp]: "conjugation_pair (λx. y ⊲ x) (λx. x ⊳ y)"
  by (simp add: conjugation_pair_def conjugation_conj)
  
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