Theory SpecialPseudoHoops
section‹Some Classes of Pseudo-Hoops›
theory SpecialPseudoHoops
imports PseudoHoopFilters PseudoWaisbergAlgebra
begin
class cancel_pseudo_hoop_algebra = pseudo_hoop_algebra +
assumes mult_cancel_left: "a * b = a * c ⟹ b = c"
and mult_cancel_right: "b * a = c * a ⟹ b = c"
begin
lemma cancel_left_a: "b l→ (a * b) = a"
apply (rule_tac a = b in mult_cancel_right)
apply (subst inf_l_def [THEN sym])
apply (rule order.antisym)
by simp_all
lemma cancel_right_a: "b r→ (b * a) = a"
apply (rule_tac a = b in mult_cancel_left)
apply (subst inf_r_def [THEN sym])
apply (rule order.antisym)
by simp_all
end
class cancel_pseudo_hoop_algebra_2 = pseudo_hoop_algebra +
assumes cancel_left: "b l→ (a * b) = a"
and cancel_right: "b r→ (b * a) = a"
begin
subclass cancel_pseudo_hoop_algebra
apply unfold_locales
apply (subgoal_tac "b = a r→ (a * b) ∧ a r→ (a * b) = a r→ (a * c) ∧ a r→ (a * c) = c")
apply simp
apply (rule conjI)
apply (subst cancel_right)
apply simp
apply (rule conjI)
apply simp
apply (subst cancel_right)
apply simp
apply (subgoal_tac "b = a l→ (b * a) ∧ a l→ (b * a) = a l→ (c * a) ∧ a l→ (c * a) = c")
apply simp
apply (rule conjI)
apply (subst cancel_left)
apply simp
apply (rule conjI)
apply simp
apply (subst cancel_left)
by simp
end
context cancel_pseudo_hoop_algebra
begin
lemma lemma_4_2_i: "a l→ b = (a * c) l→ (b * c)"
apply (subgoal_tac "a l→ b = a l→ (c l→ (b * c)) ∧ a l→ (c l→ (b * c)) = (a * c) l→ (b * c)")
apply simp
apply (rule conjI)
apply (simp add: cancel_left_a)
by (simp add: left_impl_ded)
lemma lemma_4_2_ii: "a r→ b = (c * a) r→ (c * b)"
apply (subgoal_tac "a r→ b = a r→ (c r→ (c * b)) ∧ a r→ (c r→ (c * b)) = (c * a) r→ (c * b)")
apply simp
apply (rule conjI)
apply (simp add: cancel_right_a)
by (simp add: right_impl_ded)
lemma lemma_4_2_iii: "(a * c ≤ b * c) = (a ≤ b)"
by (simp add: left_lesseq lemma_4_2_i [THEN sym])
lemma lemma_4_2_iv: "(c * a ≤ c * b) = (a ≤ b)"
by (simp add: right_lesseq lemma_4_2_ii [THEN sym])
end
class wajsberg_pseudo_hoop_algebra = pseudo_hoop_algebra +
assumes wajsberg1: "(a l→ b) r→ b = (b l→ a) r→ a"
and wajsberg2: "(a r→ b) l→ b = (b r→ a) l→ a"
context wajsberg_pseudo_hoop_algebra
begin
lemma lemma_4_3_i_a: "a ⊔1 b = (a l→ b) r→ b"
by (simp add: sup1_def wajsberg1)
lemma lemma_4_3_i_b: "a ⊔1 b = (b l→ a) r→ a"
by (simp add: sup1_def wajsberg1)
lemma lemma_4_3_ii_a: "a ⊔2 b = (a r→ b) l→ b"
by (simp add: sup2_def wajsberg2)
lemma lemma_4_3_ii_b: "a ⊔2 b = (b r→ a) l→ a"
by (simp add: sup2_def wajsberg2)
end
sublocale wajsberg_pseudo_hoop_algebra < lattice1:pseudo_hoop_lattice_b "(⊔1)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales
apply (simp add: lemma_4_3_i_a)
by (simp add: lemma_2_5_13_b lemma_2_5_13_a)
class zero_one = zero + one
class bounded_wajsberg_pseudo_hoop_algebra = zero_one + wajsberg_pseudo_hoop_algebra +
assumes zero_smallest [simp]: "0 ≤ a"
begin
end
sublocale wajsberg_pseudo_hoop_algebra < lattice2:pseudo_hoop_lattice_b "(⊔2)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales
apply (simp add: lemma_4_3_ii_a)
by (simp add: lemma_2_5_13_b lemma_2_5_13_a)
lemma (in wajsberg_pseudo_hoop_algebra) sup1_eq_sup2: "(⊔1) = (⊔2)"
apply (simp add: fun_eq_iff)
apply safe
apply (cut_tac a = x and b = xa in lattice1.supremum_pair)
apply (cut_tac a = x and b = xa in lattice2.supremum_pair)
by blast
context bounded_wajsberg_pseudo_hoop_algebra
begin
definition
"negl a = a l→ 0"
definition
"negr a = a r→ 0"
lemma [simp]: "0 l→ a = 1"
by (simp add: order [THEN sym])
lemma [simp]: "0 r→ a = 1"
by (simp add: order_r [THEN sym])
end