# Theory PseudoWaisbergAlgebra

Up to index of Isabelle/HOL/LatticeProperties/PseudoHoops

theory PseudoWaisbergAlgebra
imports Operations
`header{* Pseudo Waisberg Algebra *}theory PseudoWaisbergAlgebraimports Operationsbeginclass 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"beginlemma P1_a [simp]: "x l-> x = 1"  apply (cut_tac a = 1 and b = 1 and c = x in W3b)  by simplemma P1_b [simp]: "x r-> x = 1"  apply (cut_tac a = 1 and b = 1 and c = x in W3a)  by simplemma 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_alllemma 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_alllemma 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_alllemma P3_a: "(x l-> 1) r-> 1 = 1"  apply (unfold W2a)  by simplemma P3_b: "(x r-> 1) l-> 1 = 1"  apply (unfold W2c)  by simplemma 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 simplemma 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 simplemma 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 simplemma 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 simplemma P6_a: "x l-> (y r-> x) = 1"  apply (cut_tac a = y and b = 1 and c = x in W3b)  by simplemma P6_b: "x r-> (y l-> x) = 1"  apply (cut_tac a = y and b = 1 and c = x in W3a)  by simplemma 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)    qedlemma 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"endsublocale 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_allsublocale 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_allsublocale 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 simpsublocale 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 simpcontext impl_lr_algebrabeginlemma 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 simplemma 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)endclass one_ord = one + ordclass 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)"beginlemma 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 simplemma 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 simplemma 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 simpsubclass order  apply (subgoal_tac "op ≤ = lesseq_a ∧ op < = 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)endclass one_zero_uminus = one + zero + left_uminus + right_uminusclass 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"beginlemma 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 simplemma 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 antisym)      apply (simp add: order_r B)       by (simp add: order_l A)    qedlemma C3_b: "x r-> 0 = -r x"  apply (rule 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 simplemma C5_a: "-r x l-> -r y = y r-> x"  apply (rule 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 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 simplemma 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)endclass pseudo_wajsberg_algebra = impl_neg_lr_algebra +  assumes   W6: "-r (a l-> -l b) = -l (b r-> -r a)"begindefinition  "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))"endsublocale pseudo_wajsberg_algebra < slattice_inf_a!:semilattice_inf inf_a "op ≤" "op <"  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 "op ≤" "op <"  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    qedcontext pseudo_wajsberg_algebrabeginlemma inf_a_b: "inf_a = inf_b"  apply (simp add: fun_eq_iff)  apply clarify  apply (rule antisym)  by simp_allendend`