Up to index of Isabelle/HOL/LatticeProperties/PseudoHoops
theory SpecialPseudoHoopsheader{* 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 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 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 \<squnion>1 b = (a l-> b) r-> b"
by (simp add: sup1_def wajsberg1)
lemma lemma_4_3_i_b: "a \<squnion>1 b = (b l-> a) r-> a"
by (simp add: sup1_def wajsberg1)
lemma lemma_4_3_ii_a: "a \<squnion>2 b = (a r-> b) l-> b"
by (simp add: sup2_def wajsberg2)
lemma lemma_4_3_ii_b: "a \<squnion>2 b = (b r-> a) l-> a"
by (simp add: sup2_def wajsberg2)
end
sublocale wajsberg_pseudo_hoop_algebra < lattice1!:pseudo_hoop_lattice_b "op \<squnion>1" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op 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 "op \<squnion>2" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op 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: "op \<squnion>1 = op \<squnion>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
sublocale bounded_wajsberg_pseudo_hoop_algebra < wajsberg!: pseudo_wajsberg_algebra "1" "op l->" "op r->" "op ≤" "op <" "0" "negl" "negr"
apply unfold_locales
apply simp_all
apply (simp add: lemma_4_3_i_a [THEN sym])
apply (rule antisym)
apply simp_all
apply (simp add: lemma_4_3_i_a [THEN sym] lemma_4_3_ii_a [THEN sym])
apply (rule antisym)
apply simp_all
apply (simp add: lemma_4_3_i_a [THEN sym] lemma_4_3_ii_a [THEN sym])
apply (rule antisym)
apply simp_all
apply (subst left_lesseq [THEN sym])
apply (simp add: lemma_2_5_16)
apply (subst right_lesseq [THEN sym])
apply (simp add: lemma_2_5_17)
apply (simp add: left_lesseq)
apply (simp add: less_def)
apply (simp_all add: negl_def negr_def)
apply (subst left_lesseq [THEN sym])
apply (subgoal_tac "b l-> a = ((b l-> 0) r-> 0) l-> ((a l-> 0) r-> 0)")
apply (simp add: lemma_2_5_17)
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 (simp add: lemma_2_5_16)
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 antisym)
by simp_all
context pseudo_wajsberg_algebra
begin
lemma "class.bounded_wajsberg_pseudo_hoop_algebra mult inf_a (op l->) (op ≤) (op <) 1 (op r->) (0::'a)"
apply unfold_locales
apply (simp add: inf_a_def mult_def W6)
apply (simp add: strict)
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 antisym)
apply simp_all
apply (simp add: C6 P9 [THEN sym] C5_b)
apply (simp add: inf_b_def [THEN sym])
apply (rule antisym)
apply simp_all
apply (simp add: inf_b_def [THEN sym])
apply (rule antisym)
apply simp_all
apply (simp add: W6)
apply (simp add: C6 [THEN sym])
apply (simp add: P9 C5_a)
apply (simp add: inf_b_def [THEN sym])
apply (simp add: W6 inf_a_def [THEN sym])
apply (rule antisym)
apply simp_all
apply (simp add: W2a)
by (simp add: W2c)
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) \<squnion>1 (b l-> a) = 1"
apply (cut_tac a = a and b = b and c = "(a l-> b) \<squnion>1 (b l-> a)" in B1)
apply (subgoal_tac "(a l-> b) l-> (a l-> b) \<squnion>1 (b l-> a) = 1 ∧ ((b l-> a) l-> (a l-> b) \<squnion>1 (b l-> a)) = 1")
apply (erule conjE)
apply simp
apply (rule 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) \<squnion>2 (b r-> a) = 1"
apply (cut_tac a = a and b = b and c = "(a r-> b) \<squnion>2 (b r-> a)" in B2)
apply (subgoal_tac "(a r-> b) r-> (a r-> b) \<squnion>2 (b r-> a) = 1 ∧ ((b r-> a) r-> (a r-> b) \<squnion>2 (b r-> a)) = 1")
apply (erule conjE)
apply simp
apply (rule 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 \<squnion>1 b) l-> b"
apply (rule 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 (simp add: sup1_def)
apply (rule lemma_2_5_13_a)
by simp
lemma lemma_4_5_iv: "a r-> b = (a \<squnion>2 b) r-> b"
apply (rule 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 (simp add: sup2_def)
apply (rule lemma_2_5_13_b)
by simp
lemma lemma_4_5_v: "(a \<squnion>1 b) l-> c = (a l-> c) \<sqinter> (b l-> c)"
apply (rule 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 antisym)
apply simp
apply (rule_tac y = "(a l-> b) l-> ((a l-> c) \<sqinter> (b l-> c) r-> a \<squnion>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 \<sqinter> c" in order_trans)
apply (subst (2) inf_l_def)
apply (rule_tac y = "((a l-> c) \<sqinter> (b l-> c)) * ((a \<squnion>1 b) \<sqinter> b)" in order_trans)
apply (subst (3) inf_l_def)
apply (simp add: mult_assoc)
apply (subgoal_tac "(a \<squnion>1 b \<sqinter> b) = b")
apply simp
apply (rule antisym, simp)
apply simp
apply simp
apply (rule_tac y = "((b l-> a) l-> ((a l-> c) \<sqinter> (b l-> c) r-> a \<squnion>1 b l-> c)) l-> ((a l-> c) \<sqinter> (b l-> c) r-> a \<squnion>1 b l-> c)" in order_trans)
apply (rule B1)
apply (subgoal_tac "(b l-> a) l-> ((a l-> c) \<sqinter> (b l-> c) r-> a \<squnion>1 b l-> c) = 1")
apply simp
apply (rule 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 \<sqinter> c" in order_trans)
apply (subst (2) inf_l_def)
apply (rule_tac y = "((a l-> c) \<sqinter> (b l-> c)) * ((a \<squnion>1 b) \<sqinter> a)" in order_trans)
apply (subst (3) inf_l_def)
apply (subst sup1.sup_comute1)
apply (simp add: mult_assoc)
apply (subgoal_tac "(a \<squnion>1 b \<sqinter> a) = a")
apply simp
apply (rule antisym, simp)
apply simp
by simp
lemma lemma_4_5_vi: "(a \<squnion>2 b) r-> c = (a r-> c) \<sqinter> (b r-> c)"
apply (rule 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 antisym)
apply simp
apply (rule_tac y = "(a r-> b) r-> ((a r-> c) \<sqinter> (b r-> c) l-> a \<squnion>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 \<sqinter> c" in order_trans)
apply (subst (2) inf_r_def)
apply (rule_tac y = "((a \<squnion>2 b) \<sqinter> b) * ((a r-> c) \<sqinter> (b r-> c))" in order_trans)
apply (subst (2) inf_r_def)
apply (simp add: mult_assoc)
apply (subgoal_tac "(a \<squnion>2 b \<sqinter> b) = b")
apply simp
apply (rule antisym, simp)
apply simp
apply simp
apply (rule_tac y = "((b r-> a) r-> ((a r-> c) \<sqinter> (b r-> c) l-> a \<squnion>2 b r-> c)) r-> ((a r-> c) \<sqinter> (b r-> c) l-> a \<squnion>2 b r-> c)" in order_trans)
apply (rule B2)
apply (subgoal_tac "(b r-> a) r-> ((a r-> c) \<sqinter> (b r-> c) l-> a \<squnion>2 b r-> c) = 1")
apply simp
apply (rule 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 \<sqinter> c" in order_trans)
apply (subst (2) inf_r_def)
apply (rule_tac y = "((a \<squnion>2 b) \<sqinter> a) * ((a r-> c) \<sqinter> (b r-> c))" in order_trans)
apply (subst (2) inf_r_def)
apply (subst (2) sup2.sup_comute)
apply (simp add: mult_assoc)
apply (subgoal_tac "(a \<squnion>2 b \<sqinter> a) = a")
apply simp
apply (rule antisym, simp)
apply simp
by simp
lemma lemma_4_5_a: "a ≤ c ==> b ≤ c ==> a \<squnion>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 \<squnion>2 b ≤ c"
apply (subst right_lesseq)
apply (subst lemma_4_5_vi)
by simp
lemma lemma_4_5: "a \<squnion>1 b = a \<squnion>2 b"
apply (rule antisym)
by (simp_all add: lemma_4_5_a lemma_4_5_b)
end
sublocale basic_pseudo_hoop_algebra < basic_lattice!:lattice "op \<sqinter>" "op ≤" "op <" "op \<squnion>1"
apply unfold_locales
by (simp_all add: lemma_4_5_a)
context pseudo_hoop_lattice begin end
sublocale basic_pseudo_hoop_algebra < pseudo_hoop_lattice "op \<squnion>1" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"
apply unfold_locales
by (simp_all add: basic_lattice.sup_assoc)
class sup_assoc_pseudo_hoop_algebra = pseudo_hoop_algebra +
assumes sup1_assoc: "a \<squnion>1 (b \<squnion>1 c) = (a \<squnion>1 b) \<squnion>1 c"
and sup2_assoc: "a \<squnion>2 (b \<squnion>2 c) = (a \<squnion>2 b) \<squnion>2 c"
sublocale sup_assoc_pseudo_hoop_algebra < sup1_lattice: pseudo_hoop_lattice "op \<squnion>1" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"
apply unfold_locales
by (simp add: sup1_assoc)
sublocale sup_assoc_pseudo_hoop_algebra < sup2_lattice: pseudo_hoop_lattice "op \<squnion>2" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"
apply unfold_locales
by (simp add: sup2_assoc)
class sup_assoc_pseudo_hoop_algebra_1 = sup_assoc_pseudo_hoop_algebra +
assumes union_impl: "(a l-> b) \<squnion>1 (b l-> a) = 1"
and union_impr: "(a r-> b) \<squnion>1 (b r-> a) = 1"
lemma (in pseudo_hoop_algebra) [simp]: "infimum {a, b} = {a \<sqinter> b}"
apply (simp add: infimum_def lower_bound_def)
apply safe
apply (rule antisym)
by simp_all
lemma (in pseudo_hoop_lattice) sup_impl_inf:
"(a \<squnion> b) l-> c = (a l-> c) \<sqinter> (b l->c)"
apply (cut_tac A = "{a, b}" and a = "a \<squnion> b" and b = c in lemma_2_8_i)
by simp_all
lemma (in pseudo_hoop_lattice) sup_impr_inf:
"(a \<squnion> b) r-> c = (a r-> c) \<sqinter> (b r->c)"
apply (cut_tac A = "{a, b}" and a = "a \<squnion> b" and b = c in lemma_2_8_i1)
by simp_all
lemma (in pseudo_hoop_lattice) sup_times:
"a * (b \<squnion> c) = (a * b) \<squnion> (a * c)"
apply (cut_tac A = "{b, c}" and b = "b \<squnion> c" and a = a in lemma_2_9_i)
by simp_all
lemma (in pseudo_hoop_lattice) sup_times_right:
"(b \<squnion> c) * a = (b * a) \<squnion> (c * a)"
apply (cut_tac A = "{b, c}" and b = "b \<squnion> 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 "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"
apply unfold_locales
apply (subst left_residual [THEN sym])
apply (rule_tac y = "(a l-> b) \<squnion>1 (b l-> a) l-> c" in order_trans)
apply (subst sup1_lattice.sup_impl_inf)
apply (simp add: lemma_2_5_11)
apply (simp add: union_impl)
apply (subst right_residual [THEN sym])
apply (rule_tac y = "(b r-> a) \<squnion>1 (a r-> b) r-> c" in order_trans)
apply (subst sup1_lattice.sup_impr_inf)
apply (simp add: lemma_2_5_11)
by (simp add: union_impr)
context basic_pseudo_hoop_algebra
begin
lemma lemma_4_8_i: "a * (b \<sqinter> c) = (a * b) \<sqinter> (a * c)"
apply (rule antisym)
apply simp
apply (subgoal_tac "a * (b \<sqinter> c) = (a * (b * (b r-> c))) \<squnion>1 (a * (c * (c r-> b)))")
apply simp
apply (drule drop_assumption)
apply (rule_tac y = "(((a * b) \<sqinter> (a * c)) * (b r-> c)) \<squnion>1 (((a * b) \<sqinter> (a * c)) * (c r-> b))" in order_trans)
apply (subst sup_times [THEN sym])
apply (simp add: lemma_4_5 lemma_4_5_ii)
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 \<sqinter> c = c \<sqinter> b")
apply simp
apply (rule antisym)
by simp_all
lemma lemma_4_8_ii: "(b \<sqinter> c) * a = (b * a) \<sqinter> (c * a)"
apply (rule antisym)
apply simp
apply (subgoal_tac "(b \<sqinter> c) * a = (((b l-> c) * b) * a) \<squnion>1 (((c l-> b) * c) * a)")
apply simp
apply (drule drop_assumption)
apply (rule_tac y = "((b l-> c) * ((b * a) \<sqinter> (c * a))) \<squnion>1 ((c l-> b) * ((b * a) \<sqinter> (c * a)))" in order_trans)
apply (subst sup_times_right [THEN sym])
apply (simp add: lemma_4_5_i)
apply (simp add: mult_assoc)
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 \<sqinter> c = c \<sqinter> b")
apply simp
apply (rule antisym)
by simp_all
lemma lemma_4_8_iii: "(a l-> b) l-> (b l-> a) = b l-> a"
apply (rule antisym)
apply (cut_tac a = a and b = b in lemma_4_5_i)
apply (unfold sup1_def right_lesseq, simp)
by (simp add: lemma_2_5_9_a)
lemma lemma_4_8_iv: "(a r-> b) r-> (b r-> a) = b r-> a"
apply (rule antisym)
apply (cut_tac a = a and b = b in lemma_4_5_ii)
apply (unfold sup2_def left_lesseq, simp)
by (simp add: lemma_2_5_9_b)
end
context wajsberg_pseudo_hoop_algebra
begin
subclass sup_assoc_pseudo_hoop_algebra_1
apply unfold_locales
apply (simp add: lattice1.sup_assoc)
apply (simp add: lattice2.sup_assoc)
apply (simp add: lemma_4_3_i_a)
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 (simp add: lemma_2_10_32)
apply (subst sup1_eq_sup2)
apply (simp add: lemma_4_3_ii_a)
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)
by (simp add: lemma_2_10_33)
end
class bounded_basic_pseudo_hoop_algebra = zero_one + basic_pseudo_hoop_algebra +
assumes zero_smallest [simp]: "0 ≤ a"
begin
end
class inf_a =
fixes inf_a :: "'a => 'a => 'a" (infixl "\<sqinter>1" 65)
class pseudo_bl_algebra = zero + sup + inf + monoid_mult + ord + left_imp + right_imp +
assumes bounded_lattice: "class.bounded_lattice inf (op ≤) (op <) 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 \<sqinter> b = (a l-> b) * a"
and inf_r_bl_def: "a \<sqinter> b = a * (a r-> b)"
and impl_sup_bl: "(a l-> b) \<squnion> (b l-> a) = 1"
and impr_sup_bl: "(a r-> b) \<squnion> (b r-> a) = 1"
begin
end
context pseudo_bl_algebra begin end
sublocale bounded_basic_pseudo_hoop_algebra < basic!:pseudo_bl_algebra 1 "op *" "0" "op \<sqinter>" "op \<squnion>1" "op l->" "op r->" "op ≤" "op <"
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)
apply (simp add: lemma_4_5)
by (rule lemma_4_5_ii)
sublocale pseudo_bl_algebra < bounded_lattice!: bounded_lattice "inf" "op ≤" "op <" "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.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.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.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 (simp add: left_residual_bl)
apply (rule conjI)
apply (simp add: left_residual_bl)
apply (rule conjI)
apply (simp add: mult_assoc)
apply (simp add: left_residual_bl)
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.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 (simp add: right_residual_bl)
apply (rule conjI)
apply (simp add: right_residual_bl)
apply (rule conjI)
apply (simp add: mult_assoc)
apply (simp add: right_residual_bl)
apply (simp add: right_residual_bl [THEN sym])
apply (rule_tac y="b * (b r-> c)" in bounded_lattice.order_trans)
apply (simp add: mult_assoc)
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.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: bounded_lattice.less_le_not_le)
apply (simp add: mult_1_left)
apply (simp add: mult_1_right)
apply (simp add: impl_one_bl)
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: impr_one_bl)
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.antisym)
apply simp_all
apply (subgoal_tac "a ≤ a \<squnion> b")
apply simp
apply (drule drop_assumption)
apply simp
by (simp add: bounded_lattice.sup_assoc)
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) \<squnion> (b l-> a)) l-> c" in bounded_lattice.order_trans)
apply (simp add: sup_impl_inf)
apply (simp add: impl_sup_bl)
apply (simp add: right_residual [THEN sym])
apply (rule_tac y = "((a r-> b) \<squnion> (b r-> a)) r-> c" in bounded_lattice.order_trans)
apply (simp add: sup_impr_inf)
by (simp add: impr_sup_bl)
end
class product_pseudo_hoop_algebra = basic_pseudo_hoop_algebra +
assumes P1: "b l-> b * b ≤ (a \<sqinter> (a l-> b)) l-> b"
and P2: "b r-> b * b ≤ (a \<sqinter> (a r-> b)) r-> b"
and P3: "((a l-> b) l-> b) * (c * a l-> d * a) * (c * b l-> d * b) ≤ c l-> d"
and P4: "((a r-> b) r-> b) * (a * c r-> a * d) * (b * c r-> b * d) ≤ c r-> d"
class cancel_basic_pseudo_hoop_algebra = basic_pseudo_hoop_algebra + cancel_pseudo_hoop_algebra
begin
subclass product_pseudo_hoop_algebra
apply unfold_locales
apply (rule_tac y = "1 l-> b" in order_trans)
apply (cut_tac a = 1 and b = b and c = b in lemma_4_2_i)
apply simp
apply (simp add: lemma_2_5_9_a)
apply (rule_tac y = "1 r-> b" in order_trans)
apply (cut_tac a = 1 and b = b and c = b in lemma_4_2_ii)
apply simp
apply (simp add: lemma_2_5_9_b)
apply (simp add: lemma_4_2_i [THEN sym])
by (simp add: lemma_4_2_ii [THEN sym])
end
class simple_pseudo_hoop_algebra = pseudo_hoop_algebra +
assumes simple: "normalfilters ∩ properfilters = {{1}}"
class proper = one +
assumes proper: "∃ a . a ≠ 1"
class strong_simple_pseudo_hoop_algebra = pseudo_hoop_algebra +
assumes strong_simple: "properfilters = {{1}}"
begin
subclass proper
apply unfold_locales
apply (cut_tac strong_simple)
apply (simp add: properfilters_def)
apply (case_tac "{1} = UNIV")
apply blast
by blast
lemma lemma_4_12_i_ii: "a ≠ 1 ==> filterof({a}) = UNIV"
apply (cut_tac strong_simple)
apply (simp add: properfilters_def)
apply (subgoal_tac "filterof {a} ∉ {F ∈ filters. F ≠ UNIV}")
apply (drule drop_assumption)
apply (drule drop_assumption)
apply simp
apply simp
apply safe
apply (subgoal_tac "a ∈ filterof {a}")
apply simp
apply (subst filterof_def)
by simp
lemma lemma_4_12_i_iii: "a ≠ 1 ==> (∃ n . a ^ n ≤ b)"
apply (drule lemma_4_12_i_ii)
apply (simp add: prop_3_2_i)
by blast
lemma lemma_4_12_i_iv: "a ≠ 1 ==> (∃ n . a l-n-> b = 1)"
apply (subst lemma_2_4_7_a)
apply (subst left_lesseq [THEN sym])
by (simp add: lemma_4_12_i_iii)
lemma lemma_4_12_i_v: "a ≠ 1 ==> (∃ n . a r-n-> b = 1)"
apply (subst lemma_2_4_7_b)
apply (subst right_lesseq [THEN sym])
by (simp add: lemma_4_12_i_iii)
end
lemma (in pseudo_hoop_algebra) [simp]: "{1} ∈ filters"
apply (simp add: filters_def)
apply safe
apply (rule antisym)
by simp_all
class strong_simple_pseudo_hoop_algebra_a = pseudo_hoop_algebra + proper +
assumes strong_simple_a: "a ≠ 1 ==> filterof({a}) = UNIV"
begin
subclass strong_simple_pseudo_hoop_algebra
apply unfold_locales
apply (simp add: properfilters_def)
apply safe
apply simp_all
apply (case_tac "xb = 1")
apply simp
apply (cut_tac a = xb in strong_simple_a)
apply simp
apply (simp add: filterof_def)
apply blast
apply (cut_tac proper)
by blast
end
sublocale strong_simple_pseudo_hoop_algebra < strong_simple_pseudo_hoop_algebra_a
apply unfold_locales
by (simp add: lemma_4_12_i_ii)
lemma (in pseudo_hoop_algebra) power_impl: "b l-> a = a ==> b ^ n l-> a = a"
apply (induct_tac n)
apply simp
by (simp add: left_impl_ded)
lemma (in pseudo_hoop_algebra) power_impr: "b r-> a = a ==> b ^ n r-> a = a"
apply (induct_tac n)
apply simp
by (simp add: right_impl_ded)
context strong_simple_pseudo_hoop_algebra
begin
lemma lemma_4_13_i: "b l-> a = a ==> a = 1 ∨ b = 1"
apply safe
apply (drule_tac a = b and b = a in lemma_4_12_i_iii)
apply safe
apply (subst (asm) left_lesseq)
apply (drule_tac n = n in power_impl)
by simp
lemma lemma_4_13_ii: "b r-> a = a ==> a = 1 ∨ b = 1"
apply safe
apply (drule_tac a = b and b = a in lemma_4_12_i_iii)
apply safe
apply (subst (asm) right_lesseq)
apply (drule_tac n = n in power_impr)
by simp
end
class basic_pseudo_hoop_algebra_A = basic_pseudo_hoop_algebra +
assumes left_impl_one: "b l-> a = a ==> a = 1 ∨ b = 1"
and right_impl_one: "b r-> a = a ==> a = 1 ∨ b = 1"
begin
subclass linorder
apply unfold_locales
apply (cut_tac a = "x" and b = "y" in lemma_4_8_iii)
apply (drule left_impl_one)
apply (simp add: left_lesseq)
by blast
lemma [simp]: "(a l-> b) r-> b ≤ (b l-> a) r-> a"
apply (case_tac "a = b")
apply simp
apply (cut_tac x = a and y =b in linear)
apply safe
apply (subst (asm) left_lesseq)
apply (simp add: lemma_2_10_24)
apply (subst (asm) left_lesseq)
apply simp
apply (subst left_lesseq)
apply (cut_tac b = "((a l-> b) r-> b) l-> a" and a = "a l-> b" in left_impl_one)
apply (simp add: lemma_2_10_32)
apply (simp add: left_lesseq [THEN sym])
apply safe
apply (erule notE)
by simp
end
context basic_pseudo_hoop_algebra_A begin
lemma [simp]: "(a r-> b) l-> b ≤ (b r-> a) l-> a"
apply (case_tac "a = b")
apply simp
apply (cut_tac x = a and y =b in linear)
apply safe
apply (subst (asm) right_lesseq)
apply simp
apply (simp add: lemma_2_10_26)
apply (unfold right_lesseq)
apply (cut_tac b = "((a r-> b) l-> b) r-> a" and a = "a r-> b" in right_impl_one)
apply (simp add: lemma_2_10_33)
apply (simp add: right_lesseq [THEN sym])
apply safe
apply (erule notE)
by simp
subclass wajsberg_pseudo_hoop_algebra
apply unfold_locales
apply (rule antisym)
apply simp_all
apply (rule antisym)
by simp_all
end
class strong_simple_basic_pseudo_hoop_algebra = strong_simple_pseudo_hoop_algebra + basic_pseudo_hoop_algebra
begin
subclass basic_pseudo_hoop_algebra_A
apply unfold_locales
apply (simp add: lemma_4_13_i)
by (simp add: lemma_4_13_ii)
subclass wajsberg_pseudo_hoop_algebra
by unfold_locales
end
end