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