# Theory SpecialPseudoHoops

Up to index of Isabelle/HOL/LatticeProperties/PseudoHoops

theory SpecialPseudoHoops
imports PseudoHoopFilters PseudoWaisbergAlgebra
`header{* Some Classes of Pseudo-Hoops *}theory SpecialPseudoHoopsimports PseudoHoopFilters PseudoWaisbergAlgebrabeginclass 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"beginlemma 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_alllemma 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_allendclass cancel_pseudo_hoop_algebra_2 = pseudo_hoop_algebra +   assumes cancel_left: "b l-> (a * b) = a"  and cancel_right: "b r-> (b * a) = a"beginsubclass 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  endcontext cancel_pseudo_hoop_algebrabeginlemma 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])endclass 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_algebrabeginlemma 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)endsublocale 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 + oneclass bounded_wajsberg_pseudo_hoop_algebra = zero_one + wajsberg_pseudo_hoop_algebra +  assumes zero_smallest [simp]: "0 ≤ a"begin endsublocale 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 blastcontext bounded_wajsberg_pseudo_hoop_algebrabegindefinition  "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])endsublocale 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_allcontext pseudo_wajsberg_algebrabegin  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)endclass 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"beginlemma 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 simplemma 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 simplemma 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 simplemma 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 simplemma 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 simplemma 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 simplemma lemma_4_5_a: "a ≤ c ==> b ≤ c ==> a \<squnion>1 b ≤ c"  apply (subst left_lesseq)  apply (subst lemma_4_5_v)  by simplemma lemma_4_5_b: "a ≤ c ==> b ≤ c ==> a \<squnion>2 b ≤ c"  apply (subst right_lesseq)  apply (subst lemma_4_5_vi)  by simplemma 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)endsublocale 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 endsublocale 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_alllemma (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_alllemma (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_alllemma (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_alllemma (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_allcontext basic_pseudo_hoop_algebra begin endsublocale 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_algebrabeginlemma 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_alllemma 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_alllemma 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)endcontext wajsberg_pseudo_hoop_algebrabeginsubclass 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)endclass bounded_basic_pseudo_hoop_algebra = zero_one + basic_pseudo_hoop_algebra +  assumes zero_smallest [simp]: "0 ≤ a"begin endclass 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"beginendcontext pseudo_bl_algebra begin endsublocale 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_algebrabegin  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_allendcontext pseudo_bl_algebrabeginsubclass 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)endclass 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_algebrabeginsubclass 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])endclass 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}}"beginsubclass proper  apply unfold_locales  apply (cut_tac strong_simple)  apply (simp add: properfilters_def)  apply (case_tac "{1} = UNIV")  apply blast  by blastlemma 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 simplemma 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 blastlemma 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)endlemma (in pseudo_hoop_algebra) [simp]: "{1} ∈ filters"  apply (simp add: filters_def)  apply safe  apply (rule antisym)  by simp_allclass 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 blastendsublocale 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_algebrabeginlemma 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 simplemma 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 simpendclass 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"beginsubclass 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 blastlemma [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 simpendcontext basic_pseudo_hoop_algebra_A beginlemma [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 simpsubclass wajsberg_pseudo_hoop_algebra  apply unfold_locales  apply (rule antisym)  apply simp_all  apply (rule antisym)  by simp_allendclass strong_simple_basic_pseudo_hoop_algebra = strong_simple_pseudo_hoop_algebra + basic_pseudo_hoop_algebrabeginsubclass 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_localesendend`