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

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)

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"

lemma lemma_4_3_i_b: "a ⊔1 b = (b l→ a) r→ a"

lemma lemma_4_3_ii_a: "a ⊔2 b = (a r→ b) l→ b"

lemma lemma_4_3_ii_b: "a ⊔2 b = (b r→ a) l→ a"
end

sublocale wajsberg_pseudo_hoop_algebra < lattice1:pseudo_hoop_lattice_b "(⊔1)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales

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

lemma (in wajsberg_pseudo_hoop_algebra) sup1_eq_sup2: "(⊔1) = (⊔2)"
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

sublocale bounded_wajsberg_pseudo_hoop_algebra < wajsberg: pseudo_wajsberg_algebra "1"  "(l→)"  "(r→)"  "(≤)" "(<)" "0" "negl" "negr"
apply unfold_locales
apply simp_all
apply (simp add:  lemma_4_3_i_a [THEN sym])
apply (rule order.antisym)
apply simp_all
apply (simp add:  lemma_4_3_i_a [THEN sym] lemma_4_3_ii_a [THEN sym])
apply (rule order.antisym)
apply simp_all
apply (simp add:  lemma_4_3_i_a [THEN sym] lemma_4_3_ii_a [THEN sym])
apply (rule order.antisym)
apply simp_all
apply (subst left_lesseq [THEN sym])
apply (subst right_lesseq [THEN sym])
apply (subst left_lesseq [THEN sym])
apply (subgoal_tac "b l→ a = ((b l→ 0) r→ 0) l→ ((a l→ 0) r→ 0)")
apply (subst wajsberg1)
apply simp
apply (subst wajsberg1)
apply simp
apply (subst left_lesseq [THEN sym])
apply (subgoal_tac "b r→ a = ((b r→ 0) l→ 0) r→ ((a r→ 0) l→ 0)")
apply (subst wajsberg2)
apply simp
apply (subst wajsberg2)
apply simp
apply (simp add: left_impl_ded [THEN sym])
apply (simp add: right_impl_ded [THEN sym])
apply (simp add:  lemma_4_3_i_a [THEN sym] lemma_4_3_ii_a [THEN sym])
apply (rule order.antisym)
by simp_all

context pseudo_wajsberg_algebra
begin
lemma "class.bounded_wajsberg_pseudo_hoop_algebra mult inf_a (l→) (≤) (<) 1 (r→) (0::'a)"
apply unfold_locales
apply (simp add: inf_a_def mult_def W6)
apply (simp_all add: mult_def order_l strict)
apply (simp add: zero_def [THEN sym] C3_a)
apply (simp add: W6 inf_a_def [THEN sym])
apply (rule order.antisym)
apply simp_all
apply (simp add: C6 P9 [THEN sym] C5_b)
apply (simp add: inf_b_def [THEN sym])
apply (rule order.antisym)
apply simp_all
apply (simp add: inf_b_def [THEN sym])
apply (rule order.antisym)
apply simp_all
apply (simp add: C6 [THEN sym])
apply (simp add: inf_b_def [THEN sym])
apply (simp add: W6 inf_a_def [THEN sym])
apply (rule order.antisym)
apply simp_all

end

class basic_pseudo_hoop_algebra = pseudo_hoop_algebra +
assumes B1: "(a l→ b) l→ c ≤ ((b l→ a) l→ c) l→ c"
and B2: "(a r→ b) r→ c ≤ ((b r→ a) r→ c) r→ c"
begin
lemma lemma_4_5_i: "(a l→ b) ⊔1 (b l→ a) = 1"
apply (cut_tac a = a and b = b and c = "(a l→ b) ⊔1 (b l→ a)" in B1)
apply (subgoal_tac "(a l→ b) l→ (a l→ b) ⊔1 (b l→ a) = 1 ∧ ((b l→ a) l→ (a l→ b) ⊔1 (b l→ a)) = 1")
apply (erule conjE)
apply simp
apply (rule order.antisym)
apply simp
apply simp
apply safe
apply (subst left_lesseq [THEN sym])
apply simp
apply (subst left_lesseq [THEN sym])
by simp

lemma lemma_4_5_ii: "(a r→ b) ⊔2 (b r→ a) = 1"
apply (cut_tac a = a and b = b and c = "(a r→ b) ⊔2 (b r→ a)" in B2)
apply (subgoal_tac "(a r→ b) r→ (a r→ b) ⊔2 (b r→ a) = 1 ∧ ((b r→ a) r→ (a r→ b) ⊔2 (b r→ a)) = 1")
apply (erule conjE)
apply simp
apply (rule order.antisym)
apply simp
apply simp
apply safe
apply (subst right_lesseq [THEN sym])
apply simp
apply (subst right_lesseq [THEN sym])
by simp

lemma lemma_4_5_iii: "a l→ b = (a ⊔1 b) l→ b"
apply (rule order.antisym)
apply (rule_tac y = "((a l→ b) r→ b) l→ b" in order_trans)
apply (rule lemma_2_10_26)
apply (rule lemma_2_5_13_a)
apply (rule lemma_2_5_13_a)
by simp

lemma lemma_4_5_iv: "a r→ b = (a ⊔2 b) r→ b"
apply (rule order.antisym)
apply (rule_tac y = "((a r→ b) l→ b) r→ b" in order_trans)
apply (rule lemma_2_10_24)
apply (rule lemma_2_5_13_b)
apply (rule lemma_2_5_13_b)
by simp

lemma lemma_4_5_v: "(a ⊔1 b) l→ c = (a l→ c) ⊓ (b l→ c)"
apply (rule order.antisym)
apply simp
apply safe
apply (rule lemma_2_5_13_a)
apply simp
apply (rule lemma_2_5_13_a)
apply simp
apply (subst right_lesseq)
apply (rule order.antisym)
apply simp
apply (rule_tac y = "(a l→ b) l→ ((a l→ c) ⊓ (b l→ c) r→ a ⊔1 b l→ c)" in order_trans)
apply (subst left_residual [THEN sym])
apply simp
apply (subst lemma_4_5_iii)
apply (subst right_residual [THEN sym])
apply (subst left_residual [THEN sym])
apply (rule_tac y = "b ⊓ c" in order_trans)
apply (subst (2) inf_l_def)
apply (rule_tac y = "((a l→ c) ⊓ (b l→ c)) * ((a ⊔1 b) ⊓ b)" in order_trans)
apply (subst (3) inf_l_def)
apply (subgoal_tac "(a ⊔1 b ⊓ b) = b")
apply simp
apply (rule order.antisym, simp)
apply simp
apply simp
apply (rule_tac y = "((b l→ a) l→ ((a l→ c) ⊓ (b l→ c) r→ a ⊔1 b l→ c)) l→ ((a l→ c) ⊓ (b l→ c) r→ a ⊔1 b l→ c)" in order_trans)
apply (rule B1)
apply (subgoal_tac "(b l→ a) l→ ((a l→ c) ⊓ (b l→ c) r→ a ⊔1 b l→ c) = 1")
apply simp
apply (rule order.antisym)
apply simp
apply (subst left_residual [THEN sym])
apply simp
apply (subst lemma_4_5_iii)
apply (subst right_residual [THEN sym])
apply (subst left_residual [THEN sym])
apply (rule_tac y = "a ⊓ c" in order_trans)
apply (subst (2) inf_l_def)
apply (rule_tac y = "((a l→ c) ⊓ (b l→ c)) * ((a ⊔1 b) ⊓ a)" in order_trans)
apply (subst (3) inf_l_def)
apply (subst sup1.sup_comute1)
apply (subgoal_tac "(a ⊔1 b ⊓ a) = a")
apply simp
apply (rule order.antisym, simp)
apply simp
by simp

lemma lemma_4_5_vi: "(a ⊔2 b) r→ c = (a r→ c) ⊓ (b r→ c)"
apply (rule order.antisym)
apply simp
apply safe
apply (rule lemma_2_5_13_b)
apply simp
apply (rule lemma_2_5_13_b)
apply simp
apply (subst left_lesseq)
apply (rule order.antisym)
apply simp
apply (rule_tac y = "(a r→ b) r→ ((a r→ c) ⊓ (b r→ c) l→ a ⊔2 b r→ c)" in order_trans)
apply (subst right_residual [THEN sym])
apply simp
apply (subst lemma_4_5_iv)
apply (subst left_residual [THEN sym])
apply (subst right_residual [THEN sym])
apply (rule_tac y = "b ⊓ c" in order_trans)
apply (subst (2) inf_r_def)
apply (rule_tac y = "((a ⊔2 b) ⊓ b) * ((a r→ c) ⊓ (b r→ c))" in order_trans)
apply (subst (2) inf_r_def)
apply (subgoal_tac "(a ⊔2 b ⊓ b) = b")
apply simp
apply (rule order.antisym, simp)
apply simp
apply simp
apply (rule_tac y = "((b r→ a) r→ ((a r→ c) ⊓ (b r→ c) l→ a ⊔2 b r→ c)) r→ ((a r→ c) ⊓ (b r→ c) l→ a ⊔2 b r→ c)" in order_trans)
apply (rule B2)
apply (subgoal_tac "(b r→ a) r→ ((a r→ c) ⊓ (b r→ c) l→ a ⊔2 b r→ c) = 1")
apply simp
apply (rule order.antisym)
apply simp
apply (subst right_residual [THEN sym])
apply simp
apply (subst lemma_4_5_iv)
apply (subst left_residual [THEN sym])
apply (subst right_residual [THEN sym])
apply (rule_tac y = "a ⊓ c" in order_trans)
apply (subst (2) inf_r_def)
apply (rule_tac y = "((a ⊔2 b) ⊓ a) * ((a r→ c) ⊓ (b r→ c))" in order_trans)
apply (subst (2) inf_r_def)
apply (subst (2) sup2.sup_comute)
apply (subgoal_tac "(a ⊔2 b ⊓ a) = a")
apply simp
apply (rule order.antisym, simp)
apply simp
by simp

lemma lemma_4_5_a: "a ≤ c ⟹ b ≤ c ⟹ a ⊔1 b ≤ c"
apply (subst left_lesseq)
apply (subst lemma_4_5_v)
by simp

lemma lemma_4_5_b: "a ≤ c ⟹ b ≤ c ⟹ a ⊔2 b ≤ c"
apply (subst right_lesseq)
apply (subst lemma_4_5_vi)
by simp

lemma lemma_4_5: "a ⊔1 b = a ⊔2 b"
apply (rule order.antisym)
end

sublocale basic_pseudo_hoop_algebra <  basic_lattice:lattice "(⊓)" "(≤)" "(<)" "(⊔1)"
apply unfold_locales

context pseudo_hoop_lattice begin end

sublocale basic_pseudo_hoop_algebra <  pseudo_hoop_lattice "(⊔1)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales

class sup_assoc_pseudo_hoop_algebra = pseudo_hoop_algebra +
assumes sup1_assoc: "a ⊔1 (b ⊔1 c) = (a ⊔1 b) ⊔1 c"
and sup2_assoc: "a ⊔2 (b ⊔2 c) = (a ⊔2 b) ⊔2 c"

sublocale sup_assoc_pseudo_hoop_algebra <  sup1_lattice: pseudo_hoop_lattice "(⊔1)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales

sublocale sup_assoc_pseudo_hoop_algebra <  sup2_lattice: pseudo_hoop_lattice "(⊔2)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales

class sup_assoc_pseudo_hoop_algebra_1 = sup_assoc_pseudo_hoop_algebra +
assumes union_impl: "(a l→ b) ⊔1 (b l→ a) = 1"
and union_impr: "(a r→ b) ⊔1 (b r→ a) = 1"

lemma (in pseudo_hoop_algebra) [simp]: "infimum {a, b} = {a ⊓ b}"
apply safe
apply (rule order.antisym)
by simp_all

lemma (in pseudo_hoop_lattice) sup_impl_inf:
"(a ⊔ b) l→ c = (a l→ c) ⊓ (b l→c)"
apply (cut_tac A = "{a, b}" and a = "a ⊔ b" and b = c in lemma_2_8_i)
by simp_all

lemma (in pseudo_hoop_lattice) sup_impr_inf:
"(a ⊔ b) r→ c = (a r→ c) ⊓ (b r→c)"
apply (cut_tac A = "{a, b}" and a = "a ⊔ b" and b = c in lemma_2_8_i1)
by simp_all

lemma (in pseudo_hoop_lattice) sup_times:
"a * (b ⊔ c) = (a * b) ⊔ (a * c)"
apply (cut_tac A = "{b, c}" and b = "b ⊔ c" and a = a in lemma_2_9_i)
by simp_all

lemma (in pseudo_hoop_lattice) sup_times_right:
"(b ⊔ c) * a = (b * a) ⊔ (c * a)"
apply (cut_tac A = "{b, c}" and b = "b ⊔ c" and a = a in lemma_2_9_i1)
by simp_all

context basic_pseudo_hoop_algebra begin end

sublocale sup_assoc_pseudo_hoop_algebra_1 <  basic_1: basic_pseudo_hoop_algebra  "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales
apply (subst left_residual [THEN sym])
apply (rule_tac y = "(a l→ b) ⊔1 (b l→ a) l→ c" in order_trans)
apply (subst sup1_lattice.sup_impl_inf)
apply (subst right_residual [THEN sym])
apply (rule_tac y = "(b r→ a) ⊔1 (a r→ b) r→ c" in order_trans)
apply (subst sup1_lattice.sup_impr_inf)

context basic_pseudo_hoop_algebra
begin

lemma lemma_4_8_i: "a * (b ⊓ c) = (a * b) ⊓ (a * c)"
apply (rule order.antisym)
apply simp
apply (subgoal_tac "a * (b ⊓ c) = (a * (b * (b r→ c))) ⊔1 (a * (c * (c r→ b)))")
apply simp
apply (drule drop_assumption)
apply (rule_tac y = "(((a * b) ⊓ (a * c)) * (b r→ c)) ⊔1 (((a * b) ⊓ (a * c)) * (c r→ b))" in order_trans)
apply (subst sup_times [THEN sym])
apply (simp add: mult.assoc [THEN sym])
apply safe
apply (rule_tac y = "a * b * (b r→ c)" in order_trans)
apply simp
apply simp
apply (rule_tac y = "a * c * (c r→ b)" in order_trans)
apply simp
apply simp
apply (simp add: inf_r_def [THEN sym])
apply (subgoal_tac "b ⊓ c = c ⊓ b")
apply simp
apply (rule order.antisym)
by simp_all

lemma lemma_4_8_ii: "(b ⊓ c) * a = (b * a) ⊓ (c * a)"
apply (rule order.antisym)
apply simp
apply (subgoal_tac "(b ⊓ c) * a = (((b l→ c) * b) * a) ⊔1 (((c l→ b) * c) * a)")
apply simp
apply (drule drop_assumption)
apply (rule_tac y = "((b l→ c) * ((b * a) ⊓ (c * a))) ⊔1 ((c l→ b) * ((b * a) ⊓ (c * a)))" in order_trans)
apply (subst sup_times_right [THEN sym])
apply safe
apply (rule_tac y = "(b l→ c) * (b * a)" in order_trans)
apply simp_all
apply (rule_tac y = "(c l→ b) * (c * a)" in order_trans)
apply simp_all
apply (simp add: inf_l_def [THEN sym])
apply (subgoal_tac "b ⊓ c = c ⊓ b")
apply simp
apply (rule order.antisym)
by simp_all

lemma lemma_4_8_iii: "(a l→ b) l→ (b l→ a) = b l→ a"
apply (rule order.antisym)
apply (cut_tac a = a and b = b in lemma_4_5_i)
apply (unfold sup1_def right_lesseq, simp)

lemma lemma_4_8_iv: "(a r→ b) r→ (b r→ a) = b r→ a"
apply (rule order.antisym)
apply (cut_tac a = a and b = b in lemma_4_5_ii)
apply (unfold sup2_def left_lesseq, simp)

end

context wajsberg_pseudo_hoop_algebra
begin
subclass sup_assoc_pseudo_hoop_algebra_1
apply unfold_locales
apply (subgoal_tac "(a l→ b) l→ (b l→ a) = b l→ a")
apply simp
apply (subst lemma_2_10_30 [THEN sym])
apply (subst wajsberg1)
apply (subst sup1_eq_sup2)
apply (subgoal_tac "(a r→ b) r→ (b r→ a) = b r→ a")
apply simp
apply (subst lemma_2_10_31 [THEN sym])
apply (subst wajsberg2)
end

class bounded_basic_pseudo_hoop_algebra = zero_one + basic_pseudo_hoop_algebra +
assumes zero_smallest [simp]: "0 ≤ a"

class inf_a =
fixes inf_a :: "'a => 'a => 'a" (infixl "⊓1" 65)

class pseudo_bl_algebra = zero + sup + inf + monoid_mult + ord + left_imp + right_imp +
assumes  bounded_lattice: "class.bounded_lattice inf (≤) (<) sup 0 1"
and left_residual_bl: "(x * a ≤ b) = (x ≤ a l→ b)"
and right_residual_bl: "(a * x ≤ b) = (x ≤ a r→ b)"
and inf_l_bl_def: "a ⊓ b = (a l→ b) * a"
and inf_r_bl_def: "a ⊓ b = a * (a r→ b)"
and impl_sup_bl: "(a l→ b) ⊔ (b l→ a) = 1"
and impr_sup_bl: "(a r→ b) ⊔ (b r→ a) = 1"

sublocale bounded_basic_pseudo_hoop_algebra < basic: pseudo_bl_algebra 1 "(*)" "0"  "(⊓)" "(⊔1)" "(l→)" "(r→)" "(≤)" "(<)"
apply unfold_locales
apply (rule zero_smallest)
apply (rule left_residual)
apply (rule right_residual)
apply (rule inf_l_def)
apply (simp add: inf_r_def [THEN sym])
apply (rule lemma_4_5_i)
by (rule lemma_4_5_ii)

sublocale pseudo_bl_algebra < bounded_lattice: bounded_lattice "inf" "(≤)" "(<)" "sup" "0" "1"
by (rule bounded_lattice)

context pseudo_bl_algebra
begin
lemma impl_one_bl [simp]: "a l→ a = 1"
apply (rule bounded_lattice.order.antisym)
apply simp_all
apply (subst left_residual_bl [THEN sym])
by simp

lemma impr_one_bl [simp]: "a r→ a = 1"
apply (rule bounded_lattice.order.antisym)
apply simp_all
apply (subst right_residual_bl [THEN sym])
by simp

lemma impl_ded_bl: "((a * b) l→ c) = (a l→ (b l→ c))"
apply (rule bounded_lattice.order.antisym)
apply (case_tac "(a * b l→ c ≤ a l→ b l→ c) = ((a * b l→ c) * a ≤ b l→ c)
∧ ((a * b l→ c) * a ≤ b l→ c) = (((a * b l→ c) * a) * b ≤ c)
∧ (((a * b l→ c) * a) * b ≤ c) = ((a * b l→ c) * (a * b) ≤ c)
∧ ((a * b l→ c) * (a * b) ≤ c) = ((a * b l→ c) ≤ (a * b l→ c))")
apply simp
apply (erule notE)
apply (rule conjI)
apply (rule conjI)
apply (rule conjI)
apply (simp add: left_residual_bl [THEN sym])
apply (rule_tac y="(b l→ c) * b" in bounded_lattice.order_trans)
apply (simp add: mult.assoc [THEN sym])
apply (subst inf_l_bl_def [THEN sym])
apply (subst bounded_lattice.inf_commute)
apply (subst inf_l_bl_def)
apply (subst mult.assoc)
apply (subst left_residual_bl)
apply simp
apply (subst left_residual_bl)
by simp

lemma impr_ded_bl: "(b * a r→ c) = (a r→ (b r→ c))"
apply (rule bounded_lattice.order.antisym)
apply (case_tac "(b * a r→ c ≤ a r→ b r→ c) = (a * (b * a r→ c) ≤ b r→ c)
∧ (a * (b * a r→ c) ≤ b r→ c) = (b * (a * (b * a r→ c)) ≤ c)
∧ (b * ( a* (b * a r→ c)) ≤ c) = ((b * a) * (b * a r→ c) ≤ c)
∧ ((b * a) * (b * a r→ c) ≤ c) = ((b * a r→ c) ≤ (b * a r→ c))")
apply simp
apply (erule notE)
apply (rule conjI)
apply (rule conjI)
apply (rule conjI)
apply (simp add: right_residual_bl [THEN sym])
apply (rule_tac y="b * (b r→ c)" in bounded_lattice.order_trans)
apply (subst inf_r_bl_def [THEN sym])
apply (subst bounded_lattice.inf_commute)
apply (subst inf_r_bl_def)
apply (subst mult.assoc [THEN sym])
apply (subst right_residual_bl)
apply simp
apply (subst right_residual_bl)
by simp

lemma lesseq_impl_bl: "(a ≤ b) = (a l→ b = 1)"
apply (rule iffI)
apply (rule  bounded_lattice.order.antisym)
apply simp
apply (simp add: left_residual_bl [THEN sym])
apply (subgoal_tac "1 ≤ a l→ b")
apply (subst (asm) left_residual_bl [THEN sym])
by simp_all

end

context pseudo_bl_algebra
begin
subclass pseudo_hoop_lattice
apply unfold_locales
apply (rule inf_l_bl_def)
apply (simp add: inf_l_bl_def [THEN sym])
apply (rule bounded_lattice.inf_commute)
apply (rule impl_ded_bl)
apply (rule lesseq_impl_bl)
apply (rule inf_r_bl_def)
apply (simp add: inf_r_bl_def [THEN sym])
apply (rule bounded_lattice.inf_commute)
apply (rule impr_ded_bl)
apply (simp add: inf_r_bl_def [THEN sym] inf_l_bl_def [THEN sym])
apply (rule bounded_lattice.sup_commute)
apply simp
apply safe
apply (rule bounded_lattice.order.antisym)
apply simp_all
apply (subgoal_tac "a ≤  a ⊔ b")
apply simp
apply (drule drop_assumption)
apply simp

subclass bounded_basic_pseudo_hoop_algebra
apply unfold_locales
apply simp_all
apply (simp add: left_residual [THEN sym])
apply (rule_tac y = "((a l→ b) ⊔ (b l→ a)) l→ c" in bounded_lattice.order_trans)