Theory Involutive_Residuated

(* Title:      Involutive Residuated Structures
   Author:     Victor Gomes
   Maintainer: Victor Gomes <vborgesferreiragomes1 at>

section ‹Involutive Residuated Structures›

theory Involutive_Residuated
  imports Residuated_Lattices

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: "xy  z  (-z)x  -y"
  and ipg2: "xy  z  y(-'z)  -'x"

lemma neg_antitone: "x  y  -y  -x"
  by (metis local.dn1

lemma neg'_antitone: "x  y  -'y  -'x"
  by (metis local.dn2
subclass pogroupoid
  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)

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
  fix x y z
  show "(x  - (y  -' z)) = (x  y  z)"
    by (metis local.ipg2)
  show "(x  y  z) = (y  -' (- z  x))"
    by (metis local.ipg1)


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 
  fix x y z
  show "(x  - (y  -' z)) = (y  -' (- z  x))"
    by (metis local.ipg1 local.ipg2)
  show "-' (- (- x)  y) = - (x  -' (-' y))"
    by (metis local.dn1 local.dn2 order.eq_iff local.jipsen1l local.jipsen1r local.resl_galois local.resr_galois)

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')

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' (≤) (<)"
  fix x y z
  have "(- (y  -' x)  z) = (-z  -y  x)"
    by (metis local.contraposition local.dn1 local.dn2 local.div_galois)
  thus "(- (y  -' x)  z) = (- (x  -' (- z))  - y)"
    by (metis local.contraposition local.div_galois local.dn1 local.dn2
  moreover have "(- (x  -' (- z))  - y) = (- (-' z  -' y)  -' x)"
    apply (auto, metis local.contraposition local.div_galois local.dn1 local.dn2
    by (metis local.contraposition local.div_galois local.dn1 local.dn2
  ultimately show "(- (y  -' x)  z) = (- (-' z  -' y)  -' x)" 
    by metis

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)