# Theory Involutive_Residuated

```(* Title:      Involutive Residuated Structures
Author:     Victor Gomes
Maintainer: Victor Gomes <vborgesferreiragomes1 at sheffield.ac.uk>
*)

section ‹Involutive Residuated Structures›

theory Involutive_Residuated
imports Residuated_Lattices
begin

class uminus' =
fixes uminus' :: "'a ⇒ 'a" ("-'' _" [81] 80)

text ‹
Involutive posets is a structure where the double negation property holds for the
negation operations, and a Galois connection for negations exists.
›
class involutive_order = order + uminus + uminus' +
assumes gn: "x ≤ -'y ⟷ y ≤ -x"
and dn1[simp]: "-'(-x) = x"
and dn2[simp]: "-(-'x) = x"
(* The involutive pair (-', -) is compatible with multiplication *)
class involutive_pogroupoid = order + times + involutive_order +
assumes ipg1: "x⋅y ≤ z ⟷ (-z)⋅x ≤ -y"
and ipg2: "x⋅y ≤ z ⟷ y⋅(-'z) ≤ -'x"
begin

lemma neg_antitone: "x ≤ y ⟹ -y ≤ -x"
by (metis local.dn1 local.gn)

lemma neg'_antitone: "x ≤ y ⟹ -'y ≤ -'x"
by (metis local.dn2 local.gn)

subclass pogroupoid
proof
fix x y z assume assm: "x ≤ y"
show "x ⋅ z ≤ y ⋅ z"
by (metis assm local.ipg2 local.order_refl local.order_trans neg'_antitone)
show "z ⋅ x ≤ z ⋅ y"
by (metis assm local.dual_order.trans local.ipg1 local.order_refl neg_antitone)
qed

abbreviation inv_resl :: "'a ⇒ 'a ⇒ 'a" where
"inv_resl y x ≡ -(x⋅(-'y))"

abbreviation inv_resr :: "'a ⇒ 'a ⇒ 'a" where
"inv_resr x y ≡ -'((-y)⋅x)"

sublocale residuated_pogroupoid _ _ _ inv_resl inv_resr
proof
fix x y z
show "(x ≤ - (y ⋅ -' z)) = (x ⋅ y ≤ z)"
by (metis local.gn local.ipg2)
show "(x ⋅ y ≤ z) = (y ≤ -' (- z ⋅ x))"
by (metis local.gn local.ipg1)
qed

end

class division_order = order + residual_l_op + residual_r_op +
assumes div_galois: "x ≤ z ← y ⟷ y ≤ x → z"

class involutive_division_order = division_order + involutive_order +
assumes contraposition: "y → -x = -'y ← x"

context involutive_pogroupoid begin

sublocale involutive_division_order _ _ inv_resl inv_resr
proof
fix x y z
show "(x ≤ - (y ⋅ -' z)) = (y ≤ -' (- z ⋅ x))"
by (metis local.gn local.ipg1 local.ipg2)
show "-' (- (- x) ⋅ y) = - (x ⋅ -' (-' y))"
by (metis local.dn1 local.dn2 order.eq_iff local.gn local.jipsen1l local.jipsen1r local.resl_galois local.resr_galois)
qed

lemma inv_resr_neg [simp]: "inv_resr (-x) (-y) = inv_resl x y"
by (metis local.contraposition local.dn1)

lemma inv_resl_neg' [simp]: "inv_resl (-'x) (-'y) = inv_resr x y"
by (metis local.contraposition local.dn2)

lemma neg'_mult_resl: "-'((-y)⋅(-x)) = inv_resl x (-'y)"
by (metis inv_resr_neg local.dn2)

lemma neg_mult_resr: "-((-'y)⋅(-'x)) = inv_resr (-x) y"
by (metis neg'_mult_resl)

lemma resr_de_morgan1: "-'(inv_resr (-y) (-x)) = -'(inv_resl y x)"
by (metis local.dn1 neg_mult_resr)

lemma resr_de_morgan2: "-(inv_resl (-'x) (-'y)) = -(inv_resr x y)"
by (metis inv_resl_neg')

end

text ‹
We prove that an involutive division poset is equivalent to an involutive po-groupoid
by a lemma to avoid cyclic definitions
›
lemma (in involutive_division_order) inv_pogroupoid:
"class.involutive_pogroupoid (λx y. -(y → -'x)) uminus uminus' (≤) (<)"
proof
fix x y z
have "(- (y → -' x) ≤ z) = (-z ≤ -y ← x)"
by (metis local.contraposition local.dn1 local.dn2 local.gn local.div_galois)
thus "(- (y → -' x) ≤ z) = (- (x → -' (- z)) ≤ - y)"
by (metis local.contraposition local.div_galois local.dn1 local.dn2 local.gn)
moreover have "(- (x → -' (- z)) ≤ - y) = (- (-' z → -' y) ≤ -' x)"
apply (auto, metis local.contraposition local.div_galois local.dn1 local.dn2 local.gn)
by (metis local.contraposition local.div_galois local.dn1 local.dn2 local.gn)
ultimately show "(- (y → -' x) ≤ z) = (- (-' z → -' y) ≤ -' x)"
by metis
qed

context involutive_pogroupoid begin

definition negation_constant :: "'a ⇒ bool" where
"negation_constant a ≡ ∀x. -'x = inv_resr x a ∧ -x = inv_resl a x"

definition division_unit :: "'a ⇒ bool" where
"division_unit a ≡ ∀x. x = inv_resr a x ∧ x = inv_resl x a"

lemma neg_iff_div_unit: "(∃a. negation_constant a) ⟷ (∃b. division_unit b)"
unfolding negation_constant_def division_unit_def
apply safe
apply (rule_tac x="-a" in exI, auto)
apply (metis local.dn1 local.dn2)
apply (metis local.dn2)
apply (rule_tac x="-b" in exI, auto)
apply (metis local.contraposition)
apply (metis local.dn2)
done

end

end
```