Up to index of Isabelle/HOL/LatticeProperties/PseudoHoops
theory PseudoWaisbergAlgebraheader{* 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 "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)
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 antisym)
apply (simp add: order_r B)
by (simp add: order_l A)
qed
lemma 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 simp
lemma 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 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 "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
qed
context pseudo_wajsberg_algebra
begin
lemma inf_a_b: "inf_a = inf_b"
apply (simp add: fun_eq_iff)
apply clarify
apply (rule antisym)
by simp_all
end
end