Theory PseudoWaisbergAlgebra

section‹Pseudo Waisberg Algebra›

theory PseudoWaisbergAlgebra
imports Operations
begin

class impl_lr_algebra = one + left_imp + right_imp + 
  assumes W1a [simp]: "1 l→ a = a"
  and W1b [simp]: "1 r→ a = a"

  and W2a: "(a l→ b) r→ b = (b l→ a) r→ a"
  and W2b: "(b l→ a) r→ a = (b r→ a) l→ a"
  and W2c: "(b r→ a) l→ a = (a r→ b) l→ b"

  and W3a: "(a l→ b) l→ ((b l→ c) r→ (a l→ c)) = 1"
  and W3b: "(a r→ b) r→ ((b r→ c) l→ (a r→ c)) = 1"

begin

lemma P1_a [simp]: "x l→ x = 1"
  apply (cut_tac a = 1 and b = 1 and c = x in W3b)
  by simp

lemma P1_b [simp]: "x r→ x = 1"
  apply (cut_tac a = 1 and b = 1 and c = x in W3a)
  by simp

lemma P2_a: "x l→ y = 1 ⟹ y l→ x = 1 ⟹ x = y"
  apply (subgoal_tac "(y l→ x) r→ x = y")
  apply simp
  apply (subgoal_tac "(x l→ y) r→ y = y")
  apply (unfold W2a)
  by simp_all

lemma P2_b: "x r→ y = 1 ⟹ y r→ x = 1 ⟹ x = y"
  apply (subgoal_tac "(y r→ x) l→ x = y")
  apply simp
  apply (subgoal_tac "(x r→ y) l→ y = y")
  apply (unfold W2c)
  by simp_all

lemma P2_c: "x l→ y = 1 ⟹ y r→ x = 1 ⟹ x = y"
  apply (subgoal_tac "(y r→ x) l→ x = y")
  apply simp
  apply (subgoal_tac "(x l→ y) r→ y = y")
  apply (unfold W2b) [1]
  apply (unfold W2c) [1]
  by simp_all

lemma P3_a: "(x l→ 1) r→ 1 = 1"
  apply (unfold W2a)
  by simp

lemma P3_b: "(x r→ 1) l→ 1 = 1"
  apply (unfold W2c)
  by simp

lemma P4_a [simp]: "x l→ 1 = 1"
  apply (subgoal_tac "x l→ ((x l→ 1) r→ 1) = 1")
  apply (simp add: P3_a)
  apply (cut_tac a = 1 and b = x and c = 1 in W3a)
  by simp

lemma P4_b [simp]: "x r→ 1 = 1"
  apply (subgoal_tac "x r→ ((x r→ 1) l→ 1) = 1")
  apply (simp add: P3_b)
  apply (cut_tac a = 1 and b = x and c = 1 in W3b)
  by simp

lemma P5_a: "x l→ y = 1 ⟹ y l→ z = 1 ⟹ x l→ z = 1"
  apply (cut_tac a = x and b = y and c = z in W3a)
  by simp

lemma P5_b: "x r→ y = 1 ⟹ y r→ z = 1 ⟹ x r→ z = 1"
  apply (cut_tac a = x and b = y and c = z in W3b)
  by simp

lemma P6_a: "x l→ (y r→ x) = 1"
  apply (cut_tac a = y and b = 1 and c = x in W3b)
  by simp

lemma P6_b: "x r→ (y l→ x) = 1"
  apply (cut_tac a = y and b = 1 and c = x in W3a)
  by simp

lemma P7: "(x l→ (y r→ z) = 1) = (y r→ (x l→ z) = 1)"
  proof
    fix x y z assume A: "x l→ y r→ z = 1" show "y r→ x l→ z = 1"
      apply (rule_tac y = "(z r→ y) l→ y" in P5_b)
      apply (simp add: P6_b)
      apply (unfold W2c)
      apply (subgoal_tac "(x l→ (y r→ z)) l→ (((y r→ z) l→ z) r→ x l→ z) = 1")
      apply (unfold A) [1]
      apply simp
      by (simp add: W3a)
    next
    fix x y z assume A: "y r→ x l→ z = 1" show "x l→ y r→ z = 1"
      apply (rule_tac y = "(z l→ x) r→ x" in P5_a)
      apply (simp add: P6_a)
      apply (unfold W2a)
      apply (subgoal_tac "(y r→ x l→ z) r→ (((x l→ z) r→ z) l→ y r→ z) = 1")
      apply (unfold A) [1]
      apply simp
      by (simp add: W3b)
    qed

lemma P8_a: "(x l→ y) r→ ((z l→ x) l→ (z l→ y)) = 1"
  by (simp add: W3a P7 [THEN sym])


lemma P8_b: "(x r→ y) l→ ((z r→ x) r→ (z r→ y)) = 1"
  by (simp add: W3b P7)

lemma P9: "x l→ (y r→ z) = y r→ (x l→ z)"
  apply (rule P2_c)
  apply (subst P7)
  apply (rule_tac y = "(z r→ y) l→ y" in P5_b)
  apply (simp add: P6_b)
  apply (subst W2c)
  apply (rule P8_a)
  apply (subst P7 [THEN sym])
  apply (rule_tac y = "(z l→ x) r→ x" in P5_a)
  apply (simp add: P6_a)
  apply (subst W2a)
  by (simp add: P8_b)

definition
  "lesseq_a a b = (a l→ b = 1)"

definition
  "less_a a b = (lesseq_a a b ∧ ¬ lesseq_a b a)"

definition
  "lesseq_b a b = (a r→ b = 1)"

definition
  "less_b a b = (lesseq_b a b ∧ ¬ lesseq_b b a)"

definition
  "sup_a a b = (a l→ b) r→ b"

end

sublocale impl_lr_algebra < order_a:order lesseq_a less_a
  apply unfold_locales
  apply (simp add: less_a_def)
  apply (simp_all add: lesseq_a_def)
  apply (rule P5_a)
  apply simp_all
  apply (rule P2_a)
  by simp_all

sublocale impl_lr_algebra < order_b:order lesseq_b less_b
  apply unfold_locales
  apply (simp add: less_b_def)
  apply (simp_all add: lesseq_b_def)
  apply (rule P5_b)
  apply simp_all
  apply (rule P2_b)
  by simp_all

sublocale impl_lr_algebra < slattice_a:semilattice_sup sup_a lesseq_a less_a
  apply unfold_locales
  apply (simp_all add: lesseq_a_def sup_a_def)
  apply (simp add: P9)
  apply (simp add: P9)
  apply (subst W2a)
  apply (subgoal_tac "((z l→ y) r→ y) l→ ((y l→ x) r→ x) = 1")
  apply simp
  apply (subgoal_tac "((z l→ y) r→ y) l→ ((x l→ y) r→ y) = 1")
  apply (simp add: W2a)
  apply (subgoal_tac "((z l→ y) r→ y) l→ (x l→ y) r→ y = ((x l→ y) r→ (z l→ y)) r→ (((z l→ y) r→ y) l→ (x l→ y) r→ y)")
  apply (simp add: W3b)
  apply (subgoal_tac "(x l→ y) r→ z l→ y = 1")
  apply simp
  apply (cut_tac a = z and b = x and c = y in W3a)
  by simp

sublocale impl_lr_algebra < slattice_b:semilattice_sup sup_a lesseq_b less_b
  apply unfold_locales
  apply (simp_all add: lesseq_b_def sup_a_def)
  apply (simp_all add: W2b)
  apply (simp add: P9 [THEN sym])
  apply (simp add: P9 [THEN sym])
  apply (subst W2c)
  apply (subgoal_tac "((z r→ y) l→ y) r→ ((y r→ x) l→ x) = 1")
  apply simp
  apply (subgoal_tac "((z r→ y) l→ y) r→ ((x r→ y) l→ y) = 1")
  apply (simp add: W2c)
  apply (subgoal_tac "((z r→ y) l→ y) r→ (x r→ y) l→ y = ((x r→ y) l→ (z r→ y)) l→ (((z r→ y) l→ y) r→ (x r→ y) l→ y)")
  apply (simp add: W3a)
  apply (subgoal_tac "(x r→ y) l→ z r→ y = 1")
  apply simp
  apply (cut_tac a = z and b = x and c = y in W3b)
  by simp


context impl_lr_algebra
begin
lemma lesseq_a_b: "lesseq_b = lesseq_a"
  apply (simp add: fun_eq_iff)
  apply clarify
  apply (cut_tac x = x and y = xa in slattice_a.le_iff_sup)
  apply (cut_tac x = x and y = xa in slattice_b.le_iff_sup)
  by simp

lemma P10: "(a l→ b = 1) = (a r→ b = 1)"
  apply (cut_tac lesseq_a_b)
  by (simp add: fun_eq_iff lesseq_a_def lesseq_b_def)
end

class one_ord = one + ord

class impl_lr_ord_algebra = impl_lr_algebra + one_ord +
  assumes
     order: "a ≤ b = (a l→ b = 1)"
  and
     strict: "a < b = (a ≤ b ∧ ¬ b ≤ a)"
begin
lemma order_l: "(a ≤ b) = (a l→ b = 1)"
  by (simp add: order)

lemma order_r: "(a ≤ b) = (a r→ b = 1)"
  by (simp add: order P10)

lemma P11_a: "a ≤ b l→ a"
  by (simp add: order_r P6_b)

lemma P11_b: "a ≤ b r→ a"
  by (simp add: order_l P6_a)

lemma P12: "(a ≤ b l→ c) = (b ≤ a r→ c)" 
  apply (subst order_r)
  apply (subst order_l)
  by (simp add: P7)

lemma P13_a: "a ≤ b ⟹ b l→ c ≤ a l→ c"
  apply (subst order_r)
  apply (simp add: order_l)
  apply (cut_tac a = a and b = b and c = c in W3a)
  by simp

lemma P13_b: "a ≤ b ⟹ b r→ c ≤ a r→ c"
  apply (subst order_l)
  apply (simp add: order_r)
  apply (cut_tac a = a and b = b and c = c in W3b)
  by simp

lemma P14_a: "a ≤ b ⟹ c l→ a ≤ c l→ b"
  apply (simp add: order_l)
  apply (cut_tac x = a and y = b and z = c in P8_a)
  by simp
  
lemma P14_b: "a ≤ b ⟹ c r→ a ≤ c r→ b"
  apply (simp add: order_r)
  apply (cut_tac x = a and y = b and z = c in P8_b)
  by simp

subclass order
  apply (subgoal_tac "(≤) = lesseq_a ∧ (<) = less_a")
  apply simp
  apply unfold_locales
  apply safe
  by (simp_all add: fun_eq_iff lesseq_a_def less_a_def order_l strict)

end

class one_zero_uminus = one + zero + left_uminus + right_uminus

class impl_neg_lr_algebra = impl_lr_ord_algebra + one_zero_uminus +
  assumes
      W4: "-l 1 = -r 1"
  and W5a: "(-l a r→ -l b) l→ (b l→ a) = 1"
  and W5b: "(-r a l→ -r b) l→ (b r→ a) = 1"
  and zero_def: "0 = -l 1"
begin

lemma zero_r_def: "0 = -r 1"
  by (simp add: zero_def W4)

lemma C1_a [simp]: "(-l x r→ 0) l→ x = 1"
  apply (unfold zero_def)
  apply (cut_tac a = x and b = 1 in W5a)
  by simp

lemma C1_b [simp]: "(-r x l→ 0) r→ x = 1"
  apply (unfold zero_r_def)
  apply (cut_tac a = x and b = 1 in W5b)
  by (simp add: P10)

lemma C2_b [simp]: "0 r→ x = 1"
  apply (cut_tac x= "-r x l→ 0" and y = x and z = 0 in P8_b) 
  by (simp add: P6_b)
  
lemma C2_a [simp]: "0 l→ x = 1"
  by (simp add: P10)

lemma C3_a: "x l→ 0 = -l x"
  proof -
    have A: "-l x l→ (x l→ 0) = 1"
      apply (cut_tac x = "-l x" and y = "-l (-r 1)" in P6_a)
      apply (cut_tac a = "-r 1" and b = "x" in W5a)
      apply (unfold zero_r_def)
      apply (rule_tac y = " -l (-r (1::'a)) r→ -l x" in P5_a)
      by simp_all
    have B: "(x l→ 0) r→ -l x = 1"
      apply (cut_tac a = "-l x r→ 0" and b = x and c = 0 in W3a)
      apply simp
      apply (cut_tac b = "-l x" and a = 0 in W2c)
      by simp
    show "x l→ 0 = -l x"
      apply (rule order.antisym)
      apply (simp add: order_r B) 
      by (simp add: order_l A)
    qed

lemma C3_b: "x r→ 0 = -r x"
  apply (rule order.antisym)
  apply (simp add: order_l)
  apply (cut_tac x = x in C1_b)
  apply (cut_tac a = "-r x l→ 0" and b = x and c = 0 in W3b)
  apply simp
  apply (cut_tac b = "-r x" and a = 0 in W2a)
  apply simp
  apply (cut_tac x = "-r x" and y = "-r (-l 1)" in P6_b)
  apply (cut_tac a = "-l 1" and b = "x" in W5b)
  apply (unfold zero_def order_r)
  apply (rule_tac y = " -r (-l (1::'a)) l→ -r x" in P5_b)
  by (simp_all add: P10)

lemma C4_a [simp]: "-r (-l x) = x" 
  apply (unfold C3_b [THEN sym] C3_a [THEN sym])
  apply (subst W2a)
  by simp
 
lemma C4_b [simp]: "-l (-r x) = x" 
  apply (unfold C3_b [THEN sym] C3_a [THEN sym])
  apply (subst W2c)
  by simp

lemma C5_a: "-r x l→ -r y = y r→ x"
  apply (rule order.antisym)
  apply (simp add: order_l W5b)
  apply (cut_tac a = "-r y" and b = "-r x" in W5a)
  by (simp add: order_l)
  
  
lemma C5_b: "-l x r→ -l y = y l→ x"
  apply (rule order.antisym)
  apply (simp add: order_l W5a)
  apply (cut_tac a = "-l y" and b = "-l x" in W5b)
  by (simp add: order_l)

lemma C6: "-r x l→ y = -l y r→ x"
  apply (cut_tac x = x and y = "-l y" in C5_a)
  by simp

lemma C7_a: "(x ≤ y) = (-l y ≤ -l x)"
  apply (subst order_l)
  apply (subst order_r)
  by (simp add: C5_b)
 
lemma C7_b: "(x ≤ y) = (-r y ≤ -r x)"
  apply (subst order_r)
  apply (subst order_l)
  by (simp add: C5_a)

end

class pseudo_wajsberg_algebra = impl_neg_lr_algebra +
  assumes 
  W6: "-r (a l→ -l b) = -l (b r→ -r a)"
begin
definition
  "mult a b = -r (a l→ -l b)"

definition
  "inf_a a b = -l (a r→ -r (a l→ b))"

definition
  "inf_b a b = -r (b l→ -l (b r→ a))"

end

sublocale pseudo_wajsberg_algebra < slattice_inf_a:semilattice_inf inf_a "(≤)" "(<)"
  apply unfold_locales
  apply (simp_all add: inf_a_def)
  apply (subst C7_b) 
  apply (simp add: order_l P9 C5_a P10 [THEN sym] P6_a)
  apply (subst C7_b) 
  apply (simp add: order_l P9 C5_a P10 [THEN sym] P6_a)
  apply (subst W6 [THEN sym])
  apply (subst C7_a)
  apply simp
  proof -
    fix x y z
    assume A: "x ≤ y"
    assume B: "x ≤ z"
    have C: "x l→ y = 1" by (simp add: order_l [THEN sym] A)
    have E: "((y l→ z) l→ -l y) l→ -l x = ((y l→ z) l→ -l y) l→ ((x l→ y) l→ -l x)"
      by (simp add: C)
    have F: "((y l→ z) l→ -l y) l→ ((x l→ y) l→ -l x) =  ((y l→ z) l→ -l y) l→ ((-l y r→ -l x) l→ -l x)"
      by (simp add: C5_b)
    have G: "((y l→ z) l→ -l y) l→ ((-l y r→ -l x) l→ -l x) = ((y l→ z) l→ -l y) l→ ((-l x r→ -l y) l→ -l y)"
      by (simp add: W2c)
    have H: "((y l→ z) l→ -l y) l→ ((-l x r→ -l y) l→ -l y) = ((y l→ z) l→ -l y) l→ ((y l→ x) l→ -l y)"
      by (simp add: C5_b)
    have I: "((y l→ z) l→ -l y) l→ ((y l→ x) l→ -l y) = 1"
      apply (simp add: order_l [THEN sym] P14_a)
      apply (rule P13_a)
      apply (rule P14_a)
      by (simp add: B)
    show "(y l→ z) l→ -l y ≤ -l x"
      by (simp add: order_l E F G H I)
    next
    qed
      

sublocale pseudo_wajsberg_algebra < slattice_inf_b:semilattice_inf inf_b "(≤)" "(<)"
  apply unfold_locales
  apply (simp_all add: inf_b_def)
  apply (subst C7_a)
  apply (simp add: order_r P9 [THEN sym] C5_b P10 P6_b)
  apply (subst C7_a) 
  apply (simp add: order_r P9 [THEN sym] C5_b P10 P6_b)
  apply (subst W6)
  apply (subst C7_b)
  apply simp
  proof -
    fix x y z
    assume A: "x ≤ y"
    assume B: "x ≤ z"
    have C: "x r→ z = 1" by (simp add: order_r [THEN sym] B)
    have E: "((z r→ y) r→ -r z) r→ -r x = ((z r→ y) r→ -r z) r→ ((x r→ z) r→ -r x)"
      by (simp add: C)
    have F: "((z r→ y) r→ -r z) r→ ((x r→ z) r→ -r x) =  ((z r→ y) r→ -r z) r→ ((-r z l→ -r x) r→ -r x)"
      by (simp add: C5_a)
    have G: "((z r→ y) r→ -r z) r→ ((-r z l→ -r x) r→ -r x) = ((z r→ y) r→ -r z) r→ ((-r x l→ -r z) r→ -r z)"
      by (simp add: W2a)
    have H: "((z r→ y) r→ -r z) r→ ((-r x l→ -r z) r→ -r z) = ((z r→ y) r→ -r z) r→ ((z r→ x) r→ -r z)"
      by (simp add: C5_a)
    have I: "((z r→ y) r→ -r z) r→ ((z r→ x) r→ -r z) = 1"
      apply (simp add: order_r [THEN sym])
      apply (rule P13_b)
      apply (rule P14_b)
      by (simp add: A)
    show "(z r→ y) r→ -r z ≤ -r x"
      by (simp add: order_r E F G H I)
    next
    qed

context pseudo_wajsberg_algebra
begin
lemma inf_a_b: "inf_a = inf_b"
  apply (simp add: fun_eq_iff)
  apply clarify
  apply (rule order.antisym)
  by simp_all



end
end