# Theory Operations

section‹Operations›

theory Operations
imports Main
begin

class left_imp =
fixes imp_l :: "'a ⇒ 'a ⇒ 'a" (infixr "l→" 65)

class right_imp =
fixes imp_r :: "'a ⇒ 'a ⇒ 'a" (infixr "r→" 65)

class left_uminus =
fixes uminus_l :: "'a => 'a"  ("-l _" [81] 80)

class right_uminus =
fixes uminus_r :: "'a => 'a"  ("-r _" [81] 80)

end


# Theory LeftComplementedMonoid

section‹Left Complemented Monoid›

theory LeftComplementedMonoid
imports Operations LatticeProperties.Lattice_Prop
begin

class right_pordered_monoid_mult = order + monoid_mult +
assumes mult_right_mono: "a ≤ b ⟹ a * c ≤ b * c"

class one_greatest = one + ord +
assumes one_greatest [simp]: "a ≤ 1"

class integral_right_pordered_monoid_mult = right_pordered_monoid_mult + one_greatest

class left_residuated = ord + times + left_imp +
assumes left_residual: "(x * a ≤ b) = (x ≤ a l→ b)"

class left_residuated_pordered_monoid = integral_right_pordered_monoid_mult + left_residuated

class left_inf = inf + times + left_imp +
assumes inf_l_def: "(a ⊓ b)  = (a l→ b) * a"

class left_complemented_monoid = left_residuated_pordered_monoid + left_inf +
assumes right_divisibility: "(a ≤ b) = (∃ c . a = c * b)"
begin
lemma lcm_D: "a l→ a = 1"
apply (rule order.antisym, simp)
by (unfold left_residual [THEN sym], simp)

subclass semilattice_inf
apply unfold_locales
apply (metis inf_l_def right_divisibility)
apply (metis inf_l_def left_residual order_refl)
by (metis inf_l_def left_residual mult_right_mono right_divisibility)

lemma left_one_inf [simp]: "1 ⊓ a = a"
by (rule order.antisym, simp_all)

lemma left_one_impl [simp]: "1 l→ a = a"
(*by (metis inf_l_def left_one_inf mult.right_neutral)*)
proof -
have "1 l→ a = 1 ⊓ a" by (unfold inf_l_def, simp)
also have "1 ⊓ a = a" by simp
finally show ?thesis .
qed

lemma lcm_A: "(a l→ b) * a = (b l→ a) * b"
apply (unfold inf_l_def [THEN sym])

lemma lcm_B: "((a * b) l→ c) = (a l→ (b l→ c))"
apply (rule order.antisym)
apply (simp add: left_residual [THEN sym] mult.assoc)

apply (simp add: left_residual [THEN sym])
apply (rule_tac y="(b l→ c) * b" in order_trans)
apply (simp add: mult.assoc [THEN sym])
apply (rule mult_right_mono)

lemma lcm_C: "(a ≤ b) = ((a l→ b) = 1)"
(*by (metis eq_iff left_residual mult.left_neutral one_greatest)*)
proof -
have "(a ≤ b) = (1 * a ≤ b)" by simp
also have "… = (1 ≤ a l→ b)" by (unfold left_residual, simp)
also have "… = (a l→ b = 1)" apply safe by(rule order.antisym, simp_all)
finally show ?thesis .
qed

end

class less_def = ord +
assumes less_def: "(a < b) = ((a ≤ b) ∧ ¬ (b ≤ a))"

class one_times = one + times +
assumes one_left [simp]: "1 * a = a"
and one_right [simp]: "a * 1 = a"

class left_complemented_monoid_algebra = left_imp + one_times + left_inf + less_def +
assumes left_impl_one [simp]: "a l→ a = 1"
and left_impl_times: "(a l→ b) * a = (b l→ a) * b"
and left_impl_ded: "((a * b) l→ c) = (a l→ (b l→ c))"
and left_lesseq: "(a ≤ b) = ((a l→ b) = 1)"
begin
lemma A: "(1 l→ a) l→ 1 = 1"
proof -
have "(1 l→ a) l→ 1 = (1 l→ a) * 1 l→ 1" by simp
also have "... = (a l→ 1) * a l→ 1" by (subst left_impl_times, simp)
also have "... = 1" by (simp add: left_impl_ded)
finally show ?thesis .
qed

subclass order
proof
fix x y show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" by (unfold less_def, simp)
next
fix x show "x ≤ x" by (unfold left_lesseq, simp)
next
fix x y z assume a: "x ≤ y" assume b: "y ≤ z"
have "x l→ z = 1 * x l→ z" by simp
also have "... = (x l→ y) * x l→ z" by (cut_tac a, simp add: left_lesseq)
also have "... = (y l→ x) * y l→ z" by (simp add: left_impl_times)
also have "... = (y l→ x) l→ (y l→ z)" by (simp add: left_impl_ded)
also have "... = (y l→ x) l→ 1" by (cut_tac b, simp add: left_lesseq)
also have "... = (1 * y l→ x) l→ 1" by simp
also have "... = (1 l→ (y l→ x)) l→ 1" by (subst left_impl_ded, simp)
also have "... = 1" by (simp add: A)
finally show "x ≤ z"  by (simp add: left_lesseq)
next
fix x y z assume a: "x ≤ y" assume b: "y ≤ x"
have "x = (x l→ y) * x" by (cut_tac a, simp add: left_lesseq)
also have "... = (y l→ x) * y" by (simp add: left_impl_times)
also have "... = y" by (cut_tac b, simp add: left_lesseq)
finally show "x = y" .
qed

lemma B: "(1 l→ a) ≤ 1"
apply (unfold left_lesseq)
by (rule A)

lemma C: "a ≤ (1 l→ a)"
by (simp add: left_lesseq left_impl_ded [THEN sym])

lemma D: "a ≤ 1"
apply (rule_tac y = "1 l→ a" in order_trans)

lemma less_eq: "(a ≤ b) = (∃ c . a = (c * b))"
(*by (metis left_impl_ded left_impl_one left_impl_times left_lesseq one_left)*)
apply safe
apply (unfold left_lesseq)
apply (rule_tac x = "b l→ a" in exI)
apply (case_tac "c ≤ 1")

lemma F: "(a * b) * c l→ z = a * (b * c) l→ z"

lemma associativity: "(a * b) * c = a * (b * c)"
(*by (metis F left_impl_one left_impl_times one_left)*)
apply (rule order.antisym)
apply (unfold left_lesseq)
by (simp add: F [THEN sym])

lemma H: "a * b ≤ b"
by auto

lemma I: "a * b l→ b = 1"
apply (case_tac "a * b ≤ b")

lemma K: "a ≤ b ⟹ a * c ≤ b * c"
apply (unfold less_eq)
apply clarify
apply (rule_tac x = "ca" in exI)

lemma L: "(x * a ≤ b) = (x ≤ a l→ b)"

subclass left_complemented_monoid
apply unfold_locales
apply (simp_all add:  less_def D associativity K)
end

lemma (in left_complemented_monoid) left_complemented_monoid:
"class.left_complemented_monoid_algebra (*) inf (l→) (≤) (<) 1"
by (unfold_locales, simp_all add: less_le_not_le lcm_A lcm_B lcm_C lcm_D)

end


# Theory RightComplementedMonoid

section‹Right Complemented Monoid›

theory RightComplementedMonoid
imports LeftComplementedMonoid
begin

class left_pordered_monoid_mult = order + monoid_mult +
assumes mult_left_mono: "a ≤ b ⟹ c * a ≤ c * b"

class integral_left_pordered_monoid_mult = left_pordered_monoid_mult + one_greatest

class right_residuated = ord + times + right_imp +
assumes right_residual: "(a * x ≤ b) = (x ≤ a r→ b)"

class right_residuated_pordered_monoid = integral_left_pordered_monoid_mult + right_residuated

class right_inf = inf + times + right_imp +
assumes inf_r_def: "(a ⊓ b)  = a * (a r→ b)"

class right_complemented_monoid = right_residuated_pordered_monoid + right_inf +
assumes left_divisibility: "(a ≤ b) = (∃ c . a = b * c)"

sublocale right_complemented_monoid < dual: left_complemented_monoid "λ a b . b * a" "(⊓)" "(r→)" 1 "(≤)" "(<)"
apply unfold_locales
apply (simp_all add: inf_r_def mult.assoc mult_left_mono)

context right_complemented_monoid begin
lemma rcm_D: "a r→ a = 1"
by (rule dual.lcm_D)

subclass semilattice_inf
by unfold_locales

lemma right_semilattice_inf: "class.semilattice_inf inf (≤) (<)"
by unfold_locales

lemma right_one_inf [simp]: "1 ⊓ a = a"
by simp

lemma right_one_impl [simp]: "1 r→ a = a"
by simp

lemma rcm_A: "a * (a r→ b) = b * (b r→ a)"
by (rule dual.lcm_A)

lemma rcm_B: "((b * a) r→ c) = (a r→ (b r→ c))"
by (rule dual.lcm_B)

lemma rcm_C: "(a ≤ b) = ((a r→ b) = 1)"
by (rule dual.lcm_C)
end

class right_complemented_monoid_nole_algebra = right_imp + one_times + right_inf + less_def +
assumes right_impl_one [simp]: "a r→ a = 1"
and right_impl_times: "a * (a r→ b) = b * (b r→ a)"
and right_impl_ded: "((a * b) r→ c) = (b r→ (a r→ c))"

class right_complemented_monoid_algebra = right_complemented_monoid_nole_algebra +
assumes right_lesseq: "(a ≤ b) = ((a r→ b) = 1)"
begin
end

sublocale right_complemented_monoid_algebra < dual_algebra: left_complemented_monoid_algebra "λ a b . b * a" inf "(r→)" "(≤)" "(<)" 1
apply (unfold_locales, simp_all)
by (rule inf_r_def, rule right_impl_times, rule right_impl_ded, rule right_lesseq)

context right_complemented_monoid_algebra begin

subclass right_complemented_monoid
apply unfold_locales
apply simp_all
end

lemma (in right_complemented_monoid) right_complemented_monoid: "class.right_complemented_monoid_algebra (≤) (<) 1 (*) inf (r→)"
by (unfold_locales, simp_all add: less_le_not_le rcm_A rcm_B rcm_C rcm_D)

(*
sublocale right_complemented_monoid < rcm: right_complemented_monoid_algebra "(≤)" "(<)" 1 "( * )" inf "(r→)"
by (unfold_locales, simp_all add: less_le_not_le rcm_A rcm_B rcm_C rcm_D)
*)

end


# Theory PseudoHoops

section‹Pseudo-Hoops›

theory PseudoHoops
imports RightComplementedMonoid
begin

lemma drop_assumption:
"p ⟹ True"
by simp

class pseudo_hoop_algebra = left_complemented_monoid_algebra + right_complemented_monoid_nole_algebra +
assumes left_right_impl_times: "(a l→ b) * a = a * (a r→ b)"
begin
definition
"inf_rr a b  = a * (a r→ b)"

definition
"lesseq_r a b = (a r→ b = 1)"

definition
"less_r a b = (lesseq_r a b ∧ ¬ lesseq_r b a)"
end

(*
sublocale pseudo_hoop_algebra < right: right_complemented_monoid_algebra lesseq_r less_r 1 "( * )" inf_rr "(r→)";
apply unfold_locales;
apply simp_all;
apply (rule right_impl_times, rule right_impl_ded);
*)

context pseudo_hoop_algebra begin

lemma right_complemented_monoid_algebra: "class.right_complemented_monoid_algebra lesseq_r less_r 1 (*) inf_rr (r→)"
(* by unfold_locales;*)
apply unfold_locales
apply simp_all
apply (rule right_impl_times, rule right_impl_ded)

lemma inf_rr_inf [simp]: "inf_rr = (⊓)"
by (unfold fun_eq_iff, simp add: inf_rr_def inf_l_def left_right_impl_times)

lemma lesseq_lesseq_r: "lesseq_r a b = (a ≤ b)"
proof -
interpret A: right_complemented_monoid_algebra lesseq_r less_r 1 "(*)" inf_rr "(r→)"
by (rule right_complemented_monoid_algebra)
show "lesseq_r a b = (a ≤ b)"
apply (subst  le_iff_inf)
apply (subst A.dual_algebra.inf.absorb_iff1 [of a b])
apply (unfold inf_rr_inf [THEN sym])
by simp
qed
lemma [simp]: "lesseq_r = (≤)"
apply (unfold fun_eq_iff, simp add: lesseq_lesseq_r) done

lemma [simp]: "less_r = (<)"
by (unfold fun_eq_iff, simp add: less_r_def less_le_not_le)

subclass right_complemented_monoid_algebra
apply (cut_tac right_complemented_monoid_algebra)
by simp
end

sublocale pseudo_hoop_algebra <
pseudo_hoop_dual: pseudo_hoop_algebra "λ a b . b * a" "(⊓)" "(r→)" "(≤)" "(<)" 1 "(l→)"
apply unfold_locales
apply simp

context pseudo_hoop_algebra begin
lemma commutative_ps: "(∀ a b . a * b = b * a) = ((l→) = (r→))"
apply safe
apply (rule order.antisym)
apply (simp add: right_residual [THEN sym])
apply (subgoal_tac "x * (x l→ xa) =  (x l→ xa) * x")
apply (drule drop_assumption)
apply simp
apply simp
apply (simp add: left_residual [THEN sym])
apply (rule order.antisym)
apply (simp add: right_residual [THEN sym])
by (simp add: right_residual [THEN sym])

lemma lemma_2_4_5: "a l→ b ≤ (c l→ a) l→ (c l→ b)"
apply (simp add: left_residual [THEN sym] mult.assoc)
apply (rule_tac y = "(a l→ b) * a" in order_trans)
apply (rule mult_left_mono)

end

context pseudo_hoop_algebra begin

lemma lemma_2_4_6: "a r→ b ≤ (c r→ a) r→ (c r→ b)"
by (rule pseudo_hoop_dual.lemma_2_4_5)

primrec
imp_power_l:: "'a => nat ⇒ 'a ⇒ 'a" ("(_) l-(_)→ (_)" [65,0,65] 65) where
"a l-0→ b = b" |
"a l-(Suc n)→ b = (a l→ (a l-n→ b))"

primrec
imp_power_r:: "'a => nat ⇒ 'a ⇒ 'a" ("(_) r-(_)→ (_)" [65,0,65] 65) where
"a r-0→ b = b" |
"a r-(Suc n)→ b = (a r→ (a r-n→ b))"

lemma lemma_2_4_7_a: "a l-n→ b = a ^ n l→ b"
apply (induct_tac n)

lemma lemma_2_4_7_b: "a r-n→ b = a ^ n r→ b"
apply (induct_tac n)
by (simp_all add: right_impl_ded [THEN sym] power_commutes)

lemma lemma_2_5_8_a [simp]: "a * b ≤ a"
by (rule dual_algebra.H)

lemma lemma_2_5_8_b [simp]: "a * b ≤ b"
by (rule H)

lemma lemma_2_5_9_a: "a ≤ b l→ a"
by (simp add: left_residual [THEN sym] dual_algebra.H)

lemma lemma_2_5_9_b: "a ≤ b r→ a"
by (simp add: right_residual [THEN sym] H)

lemma lemma_2_5_11: "a * b ≤ a ⊓ b"
by simp

lemma lemma_2_5_12_a: "a ≤ b ⟹  c l→ a ≤ c l→ b"
apply (subst left_residual [THEN sym])
apply (subst left_impl_times)
apply (rule_tac y = "(a l→ c) * b" in order_trans)
by (rule H)

lemma lemma_2_5_13_a: "a ≤ b ⟹  b l→ c ≤ a l→ c"
apply (simp add: left_residual [THEN sym])
apply (rule_tac y = "(b l→ c) * b" in order_trans)

lemma lemma_2_5_14: "(b l→ c) * (a l→ b) ≤ a l→ c"
apply (simp add: left_residual [THEN sym])
apply (subst left_impl_times)
apply (subst mult.assoc [THEN sym])
apply (subst left_residual)
by (rule dual_algebra.H)

lemma lemma_2_5_16: "(a l→ b) ≤  (b l→ c) r→ (a l→ c)"
apply (simp add: right_residual [THEN sym])
by (rule lemma_2_5_14)

lemma lemma_2_5_18: "(a l→ b) ≤  a * c l→ b * c"
apply (simp add: left_residual  [THEN sym])
apply (subst mult.assoc  [THEN sym])
apply (rule mult_right_mono)
apply (subst left_impl_times)
by (rule H)

end

context pseudo_hoop_algebra begin

lemma lemma_2_5_12_b: "a ≤ b ⟹  c r→ a ≤ c r→ b"
by (rule pseudo_hoop_dual.lemma_2_5_12_a)

lemma lemma_2_5_13_b: "a ≤ b ⟹  b r→ c ≤ a r→ c"
by (rule pseudo_hoop_dual.lemma_2_5_13_a)

lemma lemma_2_5_15: "(a r→ b) * (b r→ c) ≤ a r→ c"
by (rule pseudo_hoop_dual.lemma_2_5_14)

lemma lemma_2_5_17: "(a r→ b) ≤  (b r→ c) l→ (a r→ c)"
by (rule pseudo_hoop_dual.lemma_2_5_16)

lemma lemma_2_5_19: "(a r→ b) ≤  c * a r→ c * b"
by (rule pseudo_hoop_dual.lemma_2_5_18)

definition
"lower_bound A = {a . ∀ x ∈ A . a ≤ x}"

definition
"infimum A = {a ∈ lower_bound A . (∀ x ∈ lower_bound A . x ≤ a)}"

lemma infimum_unique: "(infimum A = {x}) = (x ∈ infimum A)"
apply safe
apply simp
apply (rule order.antisym)

lemma lemma_2_6_20:
"a ∈ infimum A ⟹ b l→ a ∈ infimum (((l→) b)A)"
apply (subst infimum_def)
apply safe
apply (simp add: infimum_def lower_bound_def lemma_2_5_12_a)
by (simp add: infimum_def lower_bound_def left_residual  [THEN sym])

end

context pseudo_hoop_algebra begin

lemma lemma_2_6_21:
"a ∈ infimum A ⟹ b r→ a ∈ infimum (((r→) b)A)"
by (rule pseudo_hoop_dual.lemma_2_6_20)

lemma infimum_pair: "a ∈ infimum {x . x = b ∨ x = c} = (a = b ⊓ c)"
apply safe
apply (rule order.antisym)
by simp_all

lemma lemma_2_6_20_a:
"a l→ (b ⊓ c) = (a l→ b) ⊓ (a l→ c)"
apply (subgoal_tac "b ⊓ c ∈ infimum {x . x = b ∨ x = c}")
apply (drule_tac b = a in lemma_2_6_20)
apply (case_tac "((l→) a)  {x . ((x = b) ∨ (x = c))} = {x . x = a l→ b ∨ x = a l→ c}")
by auto
end

context pseudo_hoop_algebra begin

lemma lemma_2_6_21_a:
"a r→ (b ⊓ c) = (a r→ b) ⊓ (a r→ c)"
by (rule pseudo_hoop_dual.lemma_2_6_20_a)

lemma mult_mono: "a ≤ b ⟹ c ≤ d ⟹ a * c ≤ b * d"
apply (rule_tac y = "a * d" in order_trans)

lemma lemma_2_7_22: "(a l→ b) * (c l→ d) ≤ (a ⊓ c) l→ (b ⊓ d)"
apply (rule_tac y = "(a ⊓ c l→ b) * (a ⊓ c l→ d)" in order_trans)
apply (rule mult_mono)
apply (rule_tac y = "(a ⊓ c l→ b) ⊓ (a ⊓ c l→ d)" in order_trans)
apply (rule lemma_2_5_11)

end

context pseudo_hoop_algebra begin
lemma lemma_2_7_23: "(a r→ b) * (c r→ d) ≤ (a ⊓ c) r→ (b ⊓ d)"
apply (rule_tac y = "(c ⊓ a) r→ (d ⊓ b)" in order_trans)
apply (rule pseudo_hoop_dual.lemma_2_7_22)

definition
"upper_bound A = {a . ∀ x ∈ A . x ≤ a}"

definition
"supremum A = {a ∈ upper_bound A . (∀ x ∈ upper_bound A . a ≤ x)}"

lemma supremum_unique:
"a ∈ supremum A ⟹ b ∈ supremum A ⟹ a = b"
apply (rule order.antisym)
by auto

lemma lemma_2_8_i:
"a ∈ supremum A ⟹ a l→ b ∈ infimum ((λ x . x l→ b)A)"
apply (subst infimum_def)
apply safe
apply (simp add: supremum_def upper_bound_def lower_bound_def lemma_2_5_13_a)
apply (simp add: supremum_def upper_bound_def lower_bound_def left_residual  [THEN sym])

end

context pseudo_hoop_algebra begin

lemma lemma_2_8_i1:
"a ∈ supremum A ⟹ a r→ b ∈ infimum ((λ x . x r→ b)A)"
by (fact pseudo_hoop_dual.lemma_2_8_i)

definition
times_set :: "'a set ⇒ 'a set ⇒ 'a set"  (infixl "**" 70) where
"(A ** B) = {a . ∃ x ∈ A . ∃ y ∈ B . a = x * y}"

lemma times_set_assoc: "A ** (B ** C) = (A ** B) ** C"
apply safe
apply (rule_tac x = "xa * xb" in exI)
apply safe
apply (rule_tac x = xa in bexI)
apply (rule_tac x = xb in bexI)
apply simp_all
apply (subst mult.assoc)
apply (rule_tac x = ya in bexI)
apply simp_all
apply (rule_tac x = xb in bexI)
apply simp_all
apply (rule_tac x = "ya * y" in exI)
apply (subst mult.assoc)
apply simp
by auto

primrec power_set :: "'a set ⇒ nat ⇒ 'a set" (infixr "*^" 80) where
power_set_0: "(A *^ 0) = {1}"
| power_set_Suc: "(A *^ (Suc n)) = (A ** (A *^ n))"

lemma infimum_singleton [simp]: "infimum {a} = {a}"
by auto

lemma lemma_2_8_ii:
"a ∈ supremum A ⟹ (a ^ n) l→ b ∈ infimum ((λ x . x l→ b)(A *^ n))"
apply (induct_tac n)
apply simp
apply (drule_tac a = "a ^ n l→ b" and b = a in lemma_2_6_20)
apply (simp add: infimum_def lower_bound_def times_set_def)
apply safe
apply (drule_tac b = "y l→ b" in lemma_2_8_i)
apply (simp add: infimum_def lower_bound_def times_set_def left_impl_ded)
apply (rule_tac y = "a l→ y l→ b" in order_trans)
apply simp_all
apply (subgoal_tac "(∀xa ∈ A *^ n. x ≤ a l→ xa l→ b)")
apply simp
apply safe
apply (drule_tac b = "xa l→ b" in lemma_2_8_i)
apply safe
apply (subgoal_tac "(∀xb ∈ A. x ≤ xb l→ xa l→ b)")
apply simp
apply safe
apply (subgoal_tac "x ≤ xb * xa l→ b")
apply (subgoal_tac "(∃x ∈ A. ∃y ∈ A *^ n. xb * xa = x * y)")
by auto

lemma power_set_Suc2:
"A *^ (Suc n) = A *^ n ** A"
apply (induct_tac n)
apply simp
apply (subst times_set_assoc)
by simp

"A *^ (n + m) = (A *^ n) ** (A *^ m)"
apply (induct_tac m)
apply simp
apply simp
apply (subst times_set_assoc)
apply (subst times_set_assoc)
apply (subst power_set_Suc2 [THEN sym])
by simp
end

context pseudo_hoop_algebra begin

lemma lemma_2_8_ii1:
"a ∈ supremum A ⟹ (a ^ n) r→ b ∈ infimum ((λ x . x r→ b)(A *^ n))"
apply (induct_tac n)
apply simp
apply (subst power_Suc2)
apply (subst power_set_Suc2)
apply (drule_tac a = "a ^ n r→ b" and b = a in lemma_2_6_21)
apply (simp add: infimum_def lower_bound_def times_set_def)
apply safe
apply (drule_tac b = "xa r→ b" in lemma_2_8_i1)
apply (simp add: infimum_def lower_bound_def times_set_def right_impl_ded)
apply (rule_tac y = "a r→ xa r→ b" in order_trans)
apply simp_all
apply (subgoal_tac "(∀xa ∈ A *^ n. x ≤ a r→ xa r→ b)")
apply simp
apply safe
apply (drule_tac b = "xa r→ b" in lemma_2_8_i1)
apply safe
apply (subgoal_tac "(∀xb ∈ A. x ≤ xb r→ xa r→ b)")
apply simp
apply safe
apply (subgoal_tac "x ≤ xa * xb r→ b")
apply (subgoal_tac "(∃x ∈ A *^ n. ∃y ∈ A . xa * xb = x * y)")
by auto

lemma lemma_2_9_i:
"b ∈ supremum A ⟹ a * b ∈ supremum ((*) a  A)"
apply safe

lemma lemma_2_9_i1:
"b ∈ supremum A ⟹ b * a ∈ supremum ((λ x . x * a)  A)"
apply safe

lemma lemma_2_9_ii:
"b ∈ supremum A ⟹ a ⊓ b ∈ supremum ((⊓) a  A)"
apply (subst supremum_def)
apply safe
apply safe
apply (rule_tac y = x in order_trans)
apply simp_all
apply (subst inf_commute)
apply (subst inf_l_def)
apply (subst left_right_impl_times)
apply (frule_tac a = "(b r→ a)" in lemma_2_9_i1)
apply safe
apply (subgoal_tac "(∀xa ∈ A. b r→ a ≤ xa r→ x)")
apply simp
apply safe
apply (rule_tac y = "xa r→  b * (b r→ a)" in order_trans)
apply simp
apply (rule lemma_2_5_12_b)
apply (subst left_residual)
apply (subgoal_tac "(∀xa∈A. xa ≤ (b r→ a) l→ x)")
apply simp
apply safe
apply (subst left_residual [THEN sym])
apply (rule_tac y = "xaa * (xaa r→ a)" in order_trans)
apply (rule mult_left_mono)
apply (rule lemma_2_5_13_b)
apply simp
apply (subst right_impl_times)
by simp

lemma lemma_2_10_24:
"a ≤ (a l→ b) r→ b"
by (simp add: right_residual [THEN sym] inf_l_def [THEN sym])

lemma lemma_2_10_25:
"a ≤ (a l→ b) r→ a"
by (rule lemma_2_5_9_b)
end

context pseudo_hoop_algebra begin
lemma lemma_2_10_26:
"a ≤ (a r→ b) l→ b"
by (rule pseudo_hoop_dual.lemma_2_10_24)

lemma lemma_2_10_27:
"a ≤ (a r→ b) l→ a"
by (rule lemma_2_5_9_a)

lemma lemma_2_10_28:
"b l→ ((a l→ b) r→ a) = b l→ a"
apply (rule order.antisym)
apply (subst left_residual [THEN sym])
apply (rule_tac y = "((a l→ b) r→ a) ⊓ a" in order_trans)
apply (subst inf_l_def)
apply (rule_tac y = "(((a l→ b) r→ a) l→ b) * ((a l→ b) r→ a)" in order_trans)
apply (subst left_impl_times)
apply simp_all
apply (rule mult_right_mono)
apply (rule_tac y = "a l→ b" in order_trans)
apply (rule lemma_2_5_13_a)
apply (fact lemma_2_10_25)
apply (fact lemma_2_10_26)
apply (rule lemma_2_5_12_a)
by (fact lemma_2_10_25)

end

context pseudo_hoop_algebra begin

lemma lemma_2_10_29:
"b r→ ((a r→ b) l→ a) = b r→ a"
by (rule pseudo_hoop_dual.lemma_2_10_28)

lemma lemma_2_10_30:
"((b l→ a) r→ a) l→ a = b l→ a"
apply (rule order.antisym)
apply (rule lemma_2_5_13_a)
by (rule lemma_2_10_24)

end

context pseudo_hoop_algebra begin

lemma lemma_2_10_31:
"((b r→ a) l→ a) r→ a = b r→ a"
by (rule pseudo_hoop_dual.lemma_2_10_30)

lemma lemma_2_10_32:
"(((b l→ a) r→ a) l→ b) l→ (b l→ a) = b l→ a"
proof -
have "((((b l→ a) r→ a) l→ b) l→ (b l→ a) = (((b l→ a) r→ a) l→ b) l→ (((b l→ a) r→ a) l→ a))"
also have "… = ((((b l→ a) r→ a) l→ b) * ((b l→ a) r→ a) l→ a)"
also have "… = (((b l→ a) r→ a) ⊓ b) l→ a"
also have "… = b l→ a" apply (subgoal_tac "((b l→ a) r→ a) ⊓ b = b", simp, rule order.antisym)
finally show ?thesis .
qed

end

context pseudo_hoop_algebra begin

lemma lemma_2_10_33:
"(((b r→ a) l→ a) r→ b) r→ (b r→ a) = b r→ a"
by (rule pseudo_hoop_dual.lemma_2_10_32)
end

class pseudo_hoop_sup_algebra = pseudo_hoop_algebra + sup +
assumes
sup_comute: "a ⊔ b = b ⊔ a"
and sup_le [simp]: "a ≤ a ⊔ b"
and le_sup_equiv: "(a ≤ b) = (a ⊔ b = b)"
begin
lemma sup_le_2 [simp]:
"b ≤ a ⊔ b"
by (subst sup_comute, simp)

lemma le_sup_equiv_r:
"(a ⊔ b = b) = (a ≤ b)"

lemma sup_idemp [simp]:
"a ⊔ a = a"
end

class pseudo_hoop_sup1_algebra = pseudo_hoop_algebra + sup +
assumes
sup_def: "a ⊔ b = ((a l→ b) r→ b) ⊓ ((b l→ a) r→ a)"
begin

lemma sup_comute1: "a ⊔ b = b ⊔ a"
apply (rule order.antisym)
by simp_all

lemma sup_le1 [simp]: "a ≤ a ⊔ b"
by (simp add: sup_def lemma_2_10_24 lemma_2_5_9_b)

lemma le_sup_equiv1: "(a ≤ b) = (a ⊔ b = b)"
apply safe
apply (rule order.antisym)
apply (subgoal_tac "(a ⊓ b = a ⊓ (a ⊔ b)) ∧ (a ⊓ (a ⊔ b) = a)")
apply simp
apply safe
apply simp
apply (rule order.antisym)
apply simp
apply (drule drop_assumption)

subclass pseudo_hoop_sup_algebra
apply unfold_locales
apply simp
end

class pseudo_hoop_sup2_algebra = pseudo_hoop_algebra + sup +
assumes
sup_2_def: "a ⊔ b = ((a r→ b) l→ b) ⊓ ((b r→ a) l→ a)"

context pseudo_hoop_sup1_algebra begin end

sublocale pseudo_hoop_sup2_algebra < sup1_dual: pseudo_hoop_sup1_algebra "(⊔)" "λ a b . b * a" "(⊓)" "(r→)" "(≤)" "(<)" 1 "(l→)"
apply unfold_locales

context pseudo_hoop_sup2_algebra begin

lemma sup_comute_2: "a ⊔ b = b ⊔ a"
by (rule  sup1_dual.sup_comute)

lemma sup_le2 [simp]: "a ≤ a ⊔ b"
by (rule sup1_dual.sup_le)

lemma le_sup_equiv2: "(a ≤ b) = (a ⊔ b = b)"
by (rule sup1_dual.le_sup_equiv)

subclass pseudo_hoop_sup_algebra
apply unfold_locales
apply simp

end

class pseudo_hoop_lattice_a = pseudo_hoop_sup_algebra +
assumes sup_inf_le_distr: "a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)"
begin
lemma sup_lower_upper_bound [simp]:
"a ≤ c ⟹ b ≤ c ⟹ a ⊔ b ≤ c"
apply (subst le_iff_inf)
apply (subgoal_tac "(a ⊔ b) ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) ∧ a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c) ∧ a ⊔ (b ⊓ c) = a ⊔ b")
apply (rule order.antisym)
apply simp
apply safe
apply auto[1]
apply (rule sup_inf_le_distr)
end

sublocale pseudo_hoop_lattice_a <  lattice "(⊓)" "(≤)" "(<)" "(⊔)"
by (unfold_locales, simp_all)

class pseudo_hoop_lattice_b = pseudo_hoop_sup_algebra +
assumes le_sup_cong: "a ≤ b ⟹ a ⊔ c ≤ b ⊔ c"

begin
lemma sup_lower_upper_bound_b [simp]:
"a ≤ c ⟹ b ≤ c ⟹ a ⊔ b ≤ c"
proof -
assume A: "a ≤ c"
assume B: "b ≤ c"
have "a ⊔ b ≤ c ⊔ b" by (cut_tac A, simp add: le_sup_cong)
also have "… = b ⊔ c" by (simp add: sup_comute)
also have "… ≤ c ⊔ c" by (cut_tac B, rule le_sup_cong, simp)
also have "… = c"  by simp
finally show ?thesis .
qed

lemma  sup_inf_le_distr_b:
"a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)"
apply (rule sup_lower_upper_bound_b)
apply simp
apply simp
apply safe
apply (subst sup_comute)
apply (rule_tac y = "b" in order_trans)
apply simp_all
apply (rule_tac y = "c" in order_trans)
by simp_all
end

context pseudo_hoop_lattice_a begin end

sublocale pseudo_hoop_lattice_b <  pseudo_hoop_lattice_a "(⊔)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
by (unfold_locales, rule sup_inf_le_distr_b)

class pseudo_hoop_lattice = pseudo_hoop_sup_algebra +
assumes sup_assoc_1: "a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c"
begin
lemma le_sup_cong_c:
"a ≤ b ⟹ a ⊔ c ≤ b ⊔ c"
proof -
assume A: "a ≤ b"
have "a ⊔ c ⊔ (b ⊔ c) = a ⊔ (c ⊔ (b ⊔ c))" by (simp add: sup_assoc_1)
also have "… = a ⊔ ((b ⊔ c) ⊔ c)" by (simp add: sup_comute)
also have "… = a ⊔ (b ⊔ (c ⊔ c))" by (simp add: sup_assoc_1 [THEN sym])
also have "… = (a ⊔ b) ⊔ c" by (simp add: sup_assoc_1)
also have "… = b ⊔ c" by (cut_tac A, simp add: le_sup_equiv)
finally show ?thesis by (simp add: le_sup_equiv)
qed
end

sublocale pseudo_hoop_lattice <  pseudo_hoop_lattice_b "(⊔)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
by (unfold_locales, rule le_sup_cong_c)

sublocale pseudo_hoop_lattice <  semilattice_sup "(⊔)" "(≤)" "(<)"
by (unfold_locales, simp_all)

sublocale pseudo_hoop_lattice <  lattice "(⊓)" "(≤)" "(<)" "(⊔)"
by unfold_locales

lemma (in pseudo_hoop_lattice_a) supremum_pair [simp]:
"supremum {a, b} = {a ⊔ b}"
apply safe
apply simp_all
apply (rule order.antisym)
by simp_all

sublocale pseudo_hoop_lattice <  distrib_lattice "(⊓)" "(≤)" "(<)" "(⊔)"
apply unfold_locales
apply (rule distrib_imp1)
apply (case_tac "xa ⊓ (ya ⊔ za) ∈ supremum ((⊓) xa  {ya, za})")
apply (erule notE)
apply (rule lemma_2_9_ii)

class bounded_semilattice_inf_top = semilattice_inf + order_top
begin
lemma inf_eq_top_iff [simp]:
"(inf x y = top) = (x = top ∧ y = top)"
end

sublocale pseudo_hoop_algebra < bounded_semilattice_inf_top "(⊓)" "(≤)" "(<)" "1"
by unfold_locales simp

definition (in pseudo_hoop_algebra)
sup1::"'a ⇒ 'a ⇒ 'a" (infixl "⊔1" 70) where
"a ⊔1 b = ((a l→ b) r→ b) ⊓ ((b l→ a) r→ a)"

sublocale pseudo_hoop_algebra < sup1: pseudo_hoop_sup1_algebra "(⊔1)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales

definition (in pseudo_hoop_algebra)
sup2::"'a ⇒ 'a ⇒ 'a" (infixl "⊔2" 70) where
"a ⊔2 b = ((a r→ b) l→ b) ⊓ ((b r→ a) l→ a)"

sublocale pseudo_hoop_algebra < sup2: pseudo_hoop_sup2_algebra "(⊔2)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
apply unfold_locales

context pseudo_hoop_algebra
begin
lemma lemma_2_15_i:
"1 ∈ supremum {a, b} ⟹ a * b = a ⊓ b"
apply (rule order.antisym)
apply (rule lemma_2_5_11)
apply (subst left_impl_times)
apply (rule mult_right_mono)
apply (subst right_lesseq)
apply (subgoal_tac "a ⊔1 b = 1")
apply (rule order.antisym)
apply simp

lemma lemma_2_15_ii:
"1 ∈ supremum {a, b} ⟹ a ≤ c ⟹ b ≤ d ⟹ 1 ∈ supremum {c, d}"
apply safe
apply (drule_tac x = x in spec)
apply safe
by simp_all

lemma sup_union:
"a ∈ supremum A ⟹ b ∈ supremum B ⟹ supremum {a, b} = supremum (A ∪ B)"
apply safe
apply safe
apply auto
apply (subgoal_tac "(∀x ∈ A ∪ B. x ≤ xa)")
by auto

lemma sup_singleton [simp]: "a ∈ supremum {a}"

lemma sup_union_singleton: "a ∈ supremum X ⟹ supremum {a, b} = supremum (X ∪ {b})"
apply (rule_tac B = "{b}" in  sup_union)
by simp_all

lemma sup_le_union [simp]: "a ≤ b ⟹ supremum (A ∪ {a, b}) = supremum (A ∪ {b})"
by auto

lemma sup_sup_union: "a ∈ supremum A ⟹ b ∈ supremum (B ∪ {a}) ⟹ b ∈ supremum (A ∪ B)"
by auto

end

(*
context monoid_mult
begin
lemma "a ^ 2 = a * a"
end
*)

lemma [simp]:
"n ≤ 2 ^ n"
apply (induct_tac n)
apply auto
apply (rule_tac y = "1 + 2 ^ n" in order_trans)
by auto

context pseudo_hoop_algebra
begin

lemma sup_le_union_2:
"a ≤ b ⟹ a ∈ A ⟹ b ∈ A ⟹ supremum A = supremum ((A - {a}) ∪ {b})"
apply (case_tac "supremum ((A - {a , b}) ∪ {a, b}) = supremum ((A - {a, b}) ∪ {b})")
apply (case_tac "((A - {a, b}) ∪ {a, b} = A) ∧ ((A - {a, b}) ∪ {b} = (A - {a}) ∪ {b})")
apply safe[1]
apply simp
apply simp
apply (erule notE)
apply safe [1]
apply (erule notE)
apply (rule sup_le_union)
by simp

lemma lemma_2_15_iii_0:
"1 ∈ supremum {a, b} ⟹ 1 ∈ supremum {a ^ 2, b ^ 2}"
apply (frule_tac a = a in lemma_2_9_i)
apply simp
apply (frule_tac a = a and b = b in sup_union_singleton)
apply (subgoal_tac "supremum ({a * a, a * b} ∪ {b}) = supremum ({a * a, b})")
apply simp_all
apply (frule_tac a = b in lemma_2_9_i)
apply simp
apply (drule_tac a = b and A = "{b * (a * a), b * b}" and b = 1 and B = "{a * a}" in sup_sup_union)
apply simp
apply (case_tac "{a * a, b} = {b, a * a}")
apply simp
apply auto [1]
apply simp
apply (subgoal_tac "supremum {a * a, b * (a * a), b * b} = supremum {a * a, b * b}")
apply (case_tac "b * (a * a) = b * b")
apply auto[1]
apply (cut_tac  A = "{a * a, b * (a * a), b * b}" and a = "b * (a * a)" and b = "a * a" in  sup_le_union_2)
apply simp
apply simp
apply simp
apply (subgoal_tac "({a * a, b * (a * a), b * b} - {b * (a * a)} ∪ {a * a}) = {a * a, b * b}")
apply simp
apply auto[1]
apply (case_tac "a * a = a * b")
apply (subgoal_tac "{b, a * a, a * b} = {a * a, b}")
apply simp
apply auto[1]
apply (cut_tac  A = "{b, a * a, a * b}" and a = "a * b" and b = "b" in  sup_le_union_2)
apply simp
apply simp
apply simp
apply (subgoal_tac "{b, a * a, a * b} - {a * b} ∪ {b} = {a * a, b}")
apply simp
by auto

lemma [simp]: "m ≤ n ⟹ a ^ n ≤ a ^ m"
apply (subgoal_tac "a ^ n = (a ^ m) * (a ^ (n-m))")
apply simp
apply (cut_tac a = a and m = "m" and n = "n - m" in power_add)
by simp

lemma [simp]: "a ^ (2 ^ n) ≤ a ^ n"
by simp

lemma lemma_2_15_iii_1: "1 ∈ supremum {a, b} ⟹ 1 ∈ supremum {a ^ (2 ^ n), b ^ (2 ^ n)}"
apply (induct_tac n)
apply auto[1]
apply (drule drop_assumption)
apply (drule lemma_2_15_iii_0)
apply (subgoal_tac "∀a . (a ^ (2::nat) ^ n)⇧2 = a ^ (2::nat) ^ Suc n")
apply simp
apply safe
apply (cut_tac a = aa and m = "2 ^ n" and n = 2 in  power_mult)
apply auto
apply (subgoal_tac "((2::nat) ^ n * (2::nat)) = ((2::nat) * (2::nat) ^ n)")
by simp_all

lemma lemma_2_15_iii:
"1 ∈ supremum {a, b} ⟹ 1 ∈ supremum {a ^ n, b ^ n}"
apply (drule_tac n = n in lemma_2_15_iii_1)
apply safe
apply (drule_tac x = x in spec)
apply safe
apply (rule_tac y = "a ^ n" in order_trans)
apply simp_all
apply (rule_tac y = "b ^ n" in order_trans)
by simp_all
end

end



# Theory PseudoHoopFilters

section‹Filters and Congruences›

theory PseudoHoopFilters
imports PseudoHoops
begin

context pseudo_hoop_algebra
begin
definition
"filters = {F . F ≠ {} ∧ (∀ a b . a ∈ F ∧ b ∈ F ⟶ a * b ∈ F) ∧ (∀ a b . a ∈ F ∧ a ≤ b ⟶ b ∈ F)}"

definition
"properfilters = {F . F ∈ filters ∧ F ≠ UNIV}"

definition
"maximalfilters = {F . F ∈ filters ∧ (∀ A . A ∈ filters ∧ F ⊆ A ⟶ A = F ∨ A = UNIV)}"

definition
"ultrafilters = properfilters ∩ maximalfilters"

lemma filter_i: "F ∈ filters ⟹ a ∈ F ⟹ b ∈ F ⟹ a * b ∈ F"

lemma filter_ii: "F ∈ filters ⟹ a ∈ F ⟹ a ≤ b ⟹ b ∈ F"

lemma filter_iii [simp]: "F ∈ filters ⟹ 1 ∈ F"

lemma filter_left_impl:
"(F ∈ filters) = ((1 ∈ F) ∧ (∀ a b . a ∈ F ∧ a l→ b ∈ F ⟶ b ∈ F))"
apply safe
apply simp
apply (frule_tac a = "a l→ b" and b = a in filter_i)
apply simp
apply simp
apply (rule_tac a = "(a l→ b) * a" in filter_ii)
apply simp
apply simp
apply (simp add: inf_l_def [THEN sym])
apply (subst filters_def)
apply safe
apply (subgoal_tac "a l→ (b l→ a * b) ∈ F")
apply blast
apply (subst left_impl_ded [THEN sym])
apply (subst left_impl_one)
apply safe
apply (subst (asm) left_lesseq)
by blast

lemma filter_right_impl:
"(F ∈ filters) = ((1 ∈ F) ∧ (∀ a b . a ∈ F ∧ a r→ b ∈ F ⟶ b ∈ F))"
apply safe
apply simp
apply (frule_tac a = a and b = "a r→ b" in filter_i)
apply simp
apply simp
apply (rule_tac a = "a * (a r→ b)" in filter_ii)
apply simp
apply simp
apply (simp add: inf_r_def [THEN sym])
apply (subst filters_def)
apply safe
apply (subgoal_tac "b r→ (a r→ a * b) ∈ F")
apply blast
apply (subst right_impl_ded [THEN sym])
apply (subst right_impl_one)
apply safe
apply (subst (asm) right_lesseq)
by blast

lemma [simp]: "A ⊆ filters ⟹ ⋂ A ∈ filters"
apply safe
apply (drule_tac x = "1" in spec)
apply safe
apply (erule notE)
apply (subgoal_tac "x ∈ filters")
apply simp
apply blast
apply (frule rev_subsetD)
apply simp
apply simp
apply (frule rev_subsetD)
apply simp
apply (subgoal_tac "a ∈ X")
apply blast
by blast

definition
"filterof X = ⋂ {F . F ∈ filters ∧ X ⊆ F}"

lemma [simp]: "filterof X ∈ filters"

lemma times_le_mono [simp]: "x ≤ y ⟹ u ≤ v ⟹ x * u ≤ y * v"
apply (rule_tac y = "x * v" in order_trans)

lemma prop_3_2_i:
"filterof X = {a . ∃ n x . x ∈ X *^ n ∧ x ≤ a}"
apply safe
apply (subgoal_tac "{a . ∃ n x . x ∈ X *^ n ∧ x ≤ a} ∈ filters")
apply (drule_tac x = "{a::'a. ∃(n::nat) x::'a. x ∈ X *^ n ∧ x ≤ a}" in spec)
apply safe
apply (rule_tac x = "1::nat" in exI)
apply (rule_tac x = "xa" in exI)
apply (drule drop_assumption)
apply safe
apply (rule_tac x = "1" in exI)
apply (rule_tac x = "0" in exI)
apply (rule_tac x = "1" in exI)
apply simp
apply (rule_tac x = "n + na" in exI)
apply (rule_tac x = "x * xa" in exI)
apply safe
apply blast
apply simp
apply (rule_tac x = "n" in exI)
apply (rule_tac x = "x" in exI)
apply simp
apply safe
apply (rule filter_ii)
apply simp_all
apply (subgoal_tac "∀x . x ∈ X *^ n ⟶ x ∈ xb")
apply simp
apply (induct_tac n)
apply safe
apply (rule filter_i)
apply simp_all
by blast

lemma ultrafilter_union:
"ultrafilters = {F . F ∈ filters ∧ F ≠ UNIV ∧ (∀ x . x ∉ F ⟶ filterof (F ∪ {x}) = UNIV)}"
apply (simp add: ultrafilters_def maximalfilters_def properfilters_def filterof_def)
by auto

lemma filterof_sub: "F ∈ filters ⟹ X ⊆ F ⟹ filterof X ⊆ F"
by blast

lemma filterof_elem [simp]: "x ∈ X ⟹ x ∈  filterof X"
by blast

lemma [simp]: "filterof X ∈ filters"
apply safe
apply (rule_tac x = 1 in exI)
apply (rule_tac x = 0 in exI)
apply (rule_tac x = 1 in exI)
apply auto [1]
apply (rule_tac x = "n + na" in exI)
apply (rule_tac x = "x * xa" in exI)
apply safe
apply auto [1]
apply (rule_tac y = "x * b" in order_trans)
apply (rule mult_left_mono)
apply simp
apply (rule_tac x = n in exI)
apply (rule_tac x = x in exI)
by simp

lemma singleton_power [simp]: "{a} *^ n = {b . b = a ^ n}"
apply (induct_tac n)
apply auto [1]

lemma power_pair: "x ∈ {a, b} *^ n ⟹ ∃ i j . i + j = n ∧ x ≤ a ^ i ∧ x ≤ b ^ j"
apply (subgoal_tac "∀ x . x ∈ {a, b} *^ n ⟶ (∃ i j . i + j = n ∧ x ≤ a ^ i ∧ x ≤ b ^ j)")
apply auto[1]
apply (drule drop_assumption)
apply (induct_tac n)
apply auto [1]
apply safe
apply safe
apply (drule_tac x = y in spec)
apply safe
apply (rule_tac x = "i + 1" in exI)
apply (rule_tac x = "j" in exI)
apply simp
apply (rule_tac y = y in order_trans)
apply simp_all
apply (drule_tac x = y in spec)
apply safe
apply (rule_tac x = "i" in exI)
apply (rule_tac x = "j+1" in exI)
apply simp
apply (rule_tac y = y in order_trans)
by simp_all

lemma filterof_supremum:
"c ∈ supremum {a, b} ⟹ filterof {c} = filterof {a} ∩ filterof {b}"
apply safe
apply (cut_tac X = "{c}" and F = "filterof {a}" in filterof_sub)
apply simp_all
apply safe
apply (rule_tac  a = a in filter_ii)
apply simp_all
apply blast
apply (cut_tac X = "{c}" and F = "filterof {b}" in filterof_sub)
apply simp_all
apply safe
apply (rule_tac  a = b in filter_ii)
apply simp_all
apply blast
apply (subst (asm) prop_3_2_i)
apply simp
apply (subst (asm) prop_3_2_i)
apply simp
apply safe
apply (cut_tac A = "{a, b}" and a = c and b = x and n = "n + na" in  lemma_2_8_ii1)
apply simp
apply (subst prop_3_2_i)
apply simp
apply (rule_tac x = "n + na" in exI)
apply (subgoal_tac "infimum ((λxa::'a. xa r→ x)  ({a, b} *^ (n + na))) = {1}")
apply simp
apply (subst infimum_unique)
apply (subst infimum_def lower_bound_def)
apply (subst lower_bound_def)
apply safe
apply simp_all
apply (drule power_pair)
apply safe
apply (subst right_residual [THEN sym])
apply simp
apply (case_tac "n ≤ i")
apply (rule_tac y = "a ^ n" in order_trans)
apply (rule_tac y = "a ^ i" in order_trans)
apply simp_all
apply (subgoal_tac "na ≤ j")
apply (rule_tac y = "b ^ na" in order_trans)
apply (rule_tac y = "b ^ j" in order_trans)
by simp_all

definition "d1 a b = (a l→ b) * (b l→ a)"
definition "d2 a b = (a r→ b) * (b r→ a)"

definition "d3 a b = d1 b a"
definition "d4 a b = d2 b a"

lemma [simp]: "(a * b = 1) = (a = 1 ∧ b = 1)"
apply (rule iffI)
apply (rule conjI)
apply (rule order.antisym)
apply simp
apply (rule_tac y = "a*b" in order_trans)
apply simp
apply (drule drop_assumption)
apply simp
apply (rule order.antisym)
apply simp
apply (rule_tac y = "a*b" in order_trans)
apply simp
apply (drule drop_assumption)
apply simp
by simp

lemma lemma_3_5_i_1: "(d1 a b = 1) = (a = b)"
apply (simp add: d1_def left_lesseq [THEN sym])
by auto

lemma lemma_3_5_i_2: "(d2 a b = 1) = (a = b)"
apply (simp add: d2_def right_lesseq [THEN sym])
by auto

lemma lemma_3_5_i_3: "(d3 a b = 1) = (a = b)"
by auto

lemma lemma_3_5_i_4: "(d4 a b = 1) = (a = b)"
by auto

lemma lemma_3_5_ii_1 [simp]: "d1 a a = 1"
apply (subst lemma_3_5_i_1)
by simp

lemma lemma_3_5_ii_2 [simp]: "d2 a a = 1"
apply (subst lemma_3_5_i_2)
by simp

lemma lemma_3_5_ii_3 [simp]: "d3 a a = 1"
apply (subst lemma_3_5_i_3)
by simp

lemma lemma_3_5_ii_4 [simp]: "d4 a a = 1"
apply (subst lemma_3_5_i_4)
by simp

lemma [simp]: "(a l→ 1) = 1"
by (simp add: left_lesseq [THEN sym])

end

context pseudo_hoop_algebra begin

lemma [simp]: "(a r→ 1) = 1"
by simp

lemma lemma_3_5_iii_1 [simp]: "d1 a 1 = a"

lemma lemma_3_5_iii_2 [simp]: "d2 a 1 = a"

lemma lemma_3_5_iii_3 [simp]: "d3 a 1 = a"

lemma lemma_3_5_iii_4 [simp]: "d4 a 1 = a"

lemma lemma_3_5_iv_1: "(d1 b c) * (d1 a b) * (d1 b c) ≤ d1 a c"
apply (subgoal_tac "(b l→ c) * (c l→ b) * ((a l→ b) * (b l→ a)) * ((b l→ c) * (c l→ b)) =
((b l→ c) * (c l→ b) * (a l→ b)) * ((b l→ a) * (b l→ c) * (c l→ b))")
apply simp
apply (rule mult_mono)
apply (rule_tac y = "(b l→ c) * (a l→ b)" in order_trans)
apply (rule mult_right_mono)
apply simp
apply (rule_tac y = "(b l→ a) * (c l→ b)" in order_trans)
apply (rule mult_right_mono)
apply simp

lemma lemma_3_5_iv_2: "(d2 a b) * (d2 b c) * (d2 a b) ≤ d2 a c"
apply (subgoal_tac "(a r→ b) * (b r→ a) * ((b r→ c) * (c r→ b)) * ((a r→ b) * (b r→ a)) =
((a r→ b) * (b r→ a) * (b r→ c)) * ((c r→ b) * (a r→ b) * (b r→ a))")
apply simp
apply (rule mult_mono)
apply (rule_tac y = "(a r→ b) * (b r→ c)" in order_trans)
apply (rule mult_right_mono)
apply simp
apply (rule_tac y = "(c r→ b) * (b r→ a)" in order_trans)
apply (rule mult_right_mono)
apply simp

lemma lemma_3_5_iv_3: "(d3 a b) * (d3 b c) * (d3 a b) ≤ d3 a c"

lemma lemma_3_5_iv_4: "(d4 b c) * (d4 a b) * (d4 b c) ≤ d4 a c"

definition
"cong_r F a b ≡ d1 a b ∈ F"

definition
"cong_l F a b ≡ d2 a b ∈ F"

lemma cong_r_filter: "F ∈ filters ⟹ (cong_r F a b) = (a l→ b ∈ F ∧ b l→ a ∈ F)"
apply safe
apply (rule filter_ii)
apply simp_all
apply simp
apply (rule filter_ii)
apply simp_all
apply simp

lemma cong_r_symmetric: "F ∈ filters ⟹ (cong_r F a b) = (cong_r F b a)"
by blast

lemma cong_r_d3: "F ∈ filters ⟹ (cong_r F a b) = (d3 a b ∈ F)"
apply (subst cong_r_symmetric)

lemma cong_l_filter: "F ∈ filters ⟹ (cong_l F a b) = (a r→ b ∈ F ∧ b r→ a ∈ F)"
apply safe
apply (rule filter_ii)
apply simp_all
apply simp
apply (rule filter_ii)
apply simp_all
apply simp

lemma cong_l_symmetric: "F ∈ filters ⟹ (cong_l F a b) = (cong_l F b a)"
by blast

lemma cong_l_d4: "F ∈ filters ⟹ (cong_l F a b) = (d4 a b ∈ F)"
apply (subst cong_l_symmetric)

lemma cong_r_reflexive: "F ∈ filters ⟹ cong_r F a a"

lemma cong_r_transitive: "F ∈ filters ⟹ cong_r F a b ⟹ cong_r F b c ⟹ cong_r F a c"
apply safe
apply (rule_tac a = "(b l→ c) * (a l→ b)" in filter_ii)
apply simp_all
apply (rule filter_i)
apply simp_all
apply (rule_tac a = "(b l→ a) * (c l→ b)" in filter_ii)
apply simp_all
apply (rule filter_i)
apply simp_all

lemma cong_l_reflexive: "F ∈ filters ⟹ cong_l F a a"

lemma cong_l_transitive: "F ∈ filters ⟹ cong_l F a b ⟹ cong_l F b c ⟹ cong_l F a c"
apply safe
apply (rule_tac a = "(a r→ b) * (b r→ c)" in filter_ii)
apply simp_all
apply (rule filter_i)
apply simp_all
apply (rule_tac a = "(c r→ b) * (b r→ a)" in filter_ii)
apply simp_all
apply (rule filter_i)
apply simp_all

lemma lemma_3_7_i: "F ∈ filters ⟹ F = {a . cong_r F a 1}"

lemma lemma_3_7_ii: "F ∈ filters ⟹ F = {a . cong_l F a 1}"

lemma lemma_3_8_i: "F ∈ filters ⟹ (cong_r F a b) = (∃ x y . x ∈ F ∧ y ∈ F ∧ x * a = y * b)"
apply (subst cong_r_filter)
apply safe
apply (rule_tac x = "a l→ b" in exI)
apply (rule_tac x = "b l→ a" in exI)
apply (subgoal_tac "x ≤ a l→ b")
apply (simp add: left_residual [THEN sym])
apply (subgoal_tac "y ≤ b l→ a")
apply (simp add: left_residual [THEN sym])
apply (subgoal_tac "y * b = x * a")
by simp_all

lemma lemma_3_8_ii: "F ∈ filters ⟹ (cong_l F a b) = (∃ x y . x ∈ F ∧ y ∈ F ∧ a * x = b * y)"
apply (subst cong_l_filter)
apply safe
apply (rule_tac x = "a r→ b" in exI)
apply (rule_tac x = "b r→ a" in exI)
apply (subgoal_tac "x ≤ a r→ b")
apply (simp add: right_residual [THEN sym])
apply (subgoal_tac "y ≤ b r→ a")
apply (simp add: right_residual [THEN sym])
apply (subgoal_tac "b * y = a * x")
by simp_all

lemma lemma_3_9_i: "F ∈ filters ⟹ cong_r F a b  ⟹ cong_r F c d ⟹ (a l→ c ∈ F) = (b l→ d ∈ F)"
apply safe
apply (rule_tac a = "(a l→ d) * (b l→ a)" in filter_ii)
apply (rule_tac a = "((c l→ d) * (a l→ c)) * (b l→ a)" in filter_ii)
apply simp_all
apply (rule mult_right_mono)

apply (rule_tac a = "(b l→ c) * (a l→ b)" in filter_ii)
apply (rule_tac a = "((d l→ c) * (b l→ d)) * (a l→ b)" in filter_ii)
apply simp_all
apply (rule mult_right_mono)

lemma lemma_3_9_ii: "F ∈ filters ⟹ cong_l F a b  ⟹ cong_l F c d ⟹ (a r→ c ∈ F) = (b r→ d ∈ F)"
apply safe
apply (rule_tac a = "(b r→ a) * (a r→ d)" in filter_ii)
apply (rule_tac a = "(b r→ a) * ((a r→ c) * (c r→ d))" in filter_ii)
apply simp_all
apply (rule mult_left_mono)

apply (rule_tac a = "(a r→ b) * (b r→ c)" in filter_ii)
apply (rule_tac a = "(a r→ b) * ((b r→ d) * (d r→ c))" in filter_ii)
apply simp_all
apply (rule mult_left_mono)

definition
"normalfilters = {F . F ∈ filters ∧ (∀ a b . (a l→ b ∈ F) = (a r→ b ∈ F))}"

lemma normalfilter_i:
"H ∈ normalfilters ⟹ a l→ b ∈ H ⟹ a r→ b ∈ H"

lemma normalfilter_ii:
"H ∈ normalfilters ⟹ a r→ b ∈ H ⟹ a l→ b ∈ H"

lemma [simp]: "H ∈ normalfilters ⟹ H ∈ filters"

lemma lemma_3_10_i_ii:
"H ∈ normalfilters ⟹ {a} ** H = H ** {a}"
apply safe
apply simp
apply (rule_tac x = "a l→ a * y" in bexI)
apply (simp add: inf_l_def [THEN sym])
apply (rule order.antisym)
apply simp
apply simp
apply (rule normalfilter_ii)
apply simp_all
apply (rule_tac a = "y" in filter_ii)
apply simp_all
apply (simp add: right_residual [THEN sym])

apply (rule_tac x = "a r→ xa * a" in bexI)
apply (simp add: inf_r_def [THEN sym])
apply (rule order.antisym)
apply simp
apply simp
apply (rule normalfilter_i)
apply simp_all
apply (rule_tac a = "xa" in filter_ii)
apply simp_all
by (simp add: left_residual [THEN sym])

lemma lemma_3_10_ii_iii:
"H ∈ filters ⟹ (∀ a . {a} ** H = H ** {a}) ⟹ cong_r H = cong_l H"
apply (subst fun_eq_iff)
apply (subst fun_eq_iff)
apply safe
apply (subst (asm) lemma_3_8_i)
apply simp_all
apply safe
apply (subst lemma_3_8_ii)
apply simp_all
apply (subgoal_tac "xb * x ∈ {x} ** H")
apply (subgoal_tac "y * xa ∈ {xa} ** H")
apply (drule drop_assumption)
apply (drule drop_assumption)
apply safe
apply (rule_tac x = ya in exI)
apply simp
apply (rule_tac x = yb in exI)
apply simp
apply (drule_tac x = xa in spec)
apply auto[1]
apply (drule_tac x = x in spec)
apply simp
apply (rule_tac x = xb in bexI)
apply simp_all

apply (subst (asm) lemma_3_8_ii)
apply simp_all
apply safe
apply (subst lemma_3_8_i)
apply simp_all
apply (subgoal_tac "x * xb ∈ H ** {x}")
apply (subgoal_tac "xa * y ∈ H ** {xa}")
apply (drule drop_assumption)
apply (drule drop_assumption)
apply safe
apply (rule_tac x = xc in exI)
apply simp
apply (rule_tac x = xd in exI)
apply simp
apply (drule_tac x = xa in spec)
apply auto[1]
apply (drule_tac x = x in spec)
apply (subgoal_tac "x * xb ∈ {x} ** H")
apply simp
apply (subst times_set_def)
by blast

lemma lemma_3_10_i_iii:
"H ∈ normalfilters ⟹ cong_r H = cong_l H"

lemma order_impl_l [simp]: "a ≤ b ⟹ a l→ b = 1"

end

context pseudo_hoop_algebra begin

lemma impl_l_d1: "(a l→ b) = d1 a (a ⊓ b)"
by (simp add: d1_def lemma_2_6_20_a )

lemma impl_r_d2: "(a r→ b) = d2 a (a ⊓ b)"

lemma lemma_3_10_iii_i:
"H ∈ filters ⟹ cong_r H = cong_l H ⟹ H ∈ normalfilters"
apply (unfold normalfilters_def)
apply safe
apply (subgoal_tac  "cong_r H a (a ⊓ b)")
apply simp
apply (subst (asm) cong_l_def)
apply simp
apply (subst cong_r_def)
apply simp
apply (subgoal_tac  "cong_r H a (a ⊓ b)")
apply (subst (asm) cong_r_def)
apply simp
apply simp
apply (subst cong_l_def)
by simp

lemma lemma_3_10_ii_i:
"H ∈ filters ⟹  (∀ a . {a} ** H = H ** {a}) ⟹ H ∈ normalfilters"
apply (rule lemma_3_10_iii_i)
apply simp
apply (rule lemma_3_10_ii_iii)
by simp_all

definition
"allpowers x n = {y . ∃ i. i < n ∧ y = x ^ i}"

lemma times_set_in: "a ∈ A ⟹ b ∈ B ⟹ c = a * b ⟹ c ∈ A ** B"
by auto

lemma power_set_power: "a ∈ A ⟹ a ^ n ∈ A *^ n"
apply (induct_tac n)
apply simp
apply simp
apply (rule_tac a = a and b = "a ^ n" in times_set_in)
by simp_all

lemma normal_filter_union: "H ∈ normalfilters ⟹ (H ∪ {x}) *^ n = (H ** (allpowers x n)) ∪ {x ^ n} "
apply (induct_tac n)
apply safe
apply simp
apply safe
apply safe
apply (subgoal_tac "x * xa ∈ H ** {x}")
apply safe
apply (drule_tac x = "xb" in bspec)
apply simp
apply (drule_tac x = "x ^ (i + 1)" in spec)
apply simp
apply safe
apply (erule notE)
apply (rule_tac x = "i + 1" in exI)
apply simp
apply (erule notE)
apply (simp add: mult.assoc [THEN sym])
apply (drule_tac a = x in lemma_3_10_i_ii)
apply (subgoal_tac "H ** {x} = {x} ** H")
apply simp
apply auto[1]
apply simp
apply (drule_tac x = "xaa" in bspec)
apply simp
apply (drule_tac x = "x ^ n" in bspec)
apply blast
apply simp
apply (drule_tac x = "xaa * xb" in bspec)
apply (drule_tac x = "ya" in bspec)
apply safe
apply (rule_tac x = i in exI)
apply simp
apply simp
apply (subst (asm)  times_set_def)
apply (subst (asm)  times_set_def)
apply simp
apply safe
apply (subst (asm) allpowers_def)
apply (subst (asm) allpowers_def)
apply safe
apply (case_tac "i = 0")
apply simp
apply (rule_tac a = xa and b = 1 in times_set_in)
apply blast
apply safe
apply simp
apply (drule_tac x = 1 in bspec)
apply simp
apply (drule_tac x = 1 in spec)
apply simp
apply (drule_tac x = 0 in spec)
apply auto[1]
apply simp
apply (rule_tac a = xaa and b = "x ^ i" in times_set_in)
apply blast
apply (case_tac "i = n")
apply simp
apply safe
apply (subgoal_tac "x ^ i ∈  H ** {y . ∃i<n. y = x ^ i}")
apply simp
apply (rule_tac a = 1 and b = "x ^ i" in times_set_in)
apply simp
apply simp
apply (rule_tac x = i in exI)
apply simp
apply simp
apply (rule power_set_power)
by simp

lemma lemma_3_11_i: "H ∈ normalfilters ⟹ filterof (H ∪ {x}) = {a . ∃ n h . h ∈ H ∧ h * x ^ n ≤ a}"
apply (subst prop_3_2_i)
apply (subst normal_filter_union)
apply simp_all
apply safe
apply (rule_tac x = n in exI)
apply (rule_tac x = 1 in exI)
apply simp
apply safe
apply (rule_tac x = i in exI)
apply (rule_tac x = xb in exI)
apply simp
apply (rule_tac x = "n + 1" in exI)
apply (rule_tac x = "h * x ^ n" in exI)
apply safe
apply (erule notE)
apply (rule_tac x = h in bexI)
apply (rule_tac x = "x ^ n" in exI)
by auto

lemma lemma_3_11_ii: "H ∈ normalfilters ⟹ filterof (H ∪ {x}) = {a . ∃ n h . h ∈ H ∧ (x ^ n) * h ≤ a}"
apply (subst lemma_3_11_i)
apply simp_all
apply safe
apply (rule_tac x = n in exI)
apply (subgoal_tac "h * x ^ n ∈ {x ^ n} ** H")
apply auto[1]
apply (drule_tac a = "x ^ n" in lemma_3_10_i_ii)
apply simp
apply auto[1]
apply (rule_tac x = n in exI)
apply (subgoal_tac "(x ^ n) * h ∈ H ** {x ^ n}")
apply auto[1]
apply (drule_tac a = "x ^ n" in lemma_3_10_i_ii)
apply (drule_tac sym)
apply simp
by auto

lemma lemma_3_12_i_ii:
"H ∈ normalfilters ⟹ H ∈ ultrafilters ⟹ x ∉ H ⟹ (∃ n . x ^ n l→ a ∈ H)"
apply (subst (asm) ultrafilter_union)
apply clarify
apply (drule_tac x = x in spec)
apply clarify
apply (subst (asm) lemma_3_11_i)
apply assumption
apply (subgoal_tac "a ∈ {a::'a. ∃(n::nat) h::'a. h ∈ H ∧ h * x ^ n ≤ a}")
apply clarify
apply (rule_tac x = n in exI)
apply (rule filter_ii)
by simp_all

lemma lemma_3_12_ii_i:
"H ∈ normalfilters ⟹ H ∈ properfilters ⟹ (∀ x a . x ∉ H ⟶ (∃ n . x ^ n l→ a ∈ H)) ⟹ H ∈ maximalfilters"
apply (subgoal_tac "H ∈ ultrafilters")
apply (subst ultrafilter_union)
apply clarify
apply (subst (asm) properfilters_def)
apply clarify
apply (subst lemma_3_11_i)
apply simp_all
apply safe
apply simp_all
apply (drule_tac x = x in spec)
apply clarify
apply (drule_tac x = xb in spec)
apply clarify
apply (rule_tac x = n in exI)
apply (rule_tac x = "x ^ n l→ xb" in exI)
apply clarify
apply (subst inf_l_def [THEN sym])
by simp

lemma lemma_3_12_i_iii:
"H ∈ normalfilters ⟹ H ∈ ultrafilters ⟹ x ∉ H ⟹ (∃ n . x ^ n r→ a ∈ H)"
apply (subst (asm) ultrafilter_union)
apply clarify
apply (drule_tac x = x in spec)
apply clarify
apply (subst (asm) lemma_3_11_ii)
apply assumption
apply (subgoal_tac "a ∈ {a::'a. ∃(n::nat) h::'a. h ∈ H ∧ (x ^ n) * h ≤ a}")
apply clarify
apply (rule_tac x = n in exI)
apply (rule filter_ii)
by simp_all

lemma lemma_3_12_iii_i:
"H ∈ normalfilters ⟹ H ∈ properfilters ⟹ (∀ x a . x ∉ H ⟶ (∃ n . x ^ n r→ a ∈ H)) ⟹ H ∈ maximalfilters"
apply (subgoal_tac "H ∈ ultrafilters")
apply (subst ultrafilter_union)
apply clarify
apply (subst (asm) properfilters_def)
apply clarify
apply (subst lemma_3_11_ii)
apply simp_all
apply safe
apply simp_all
apply (drule_tac x = x in spec)
apply clarify
apply (drule_tac x = xb in spec)
apply clarify
apply (rule_tac x = n in exI)
apply (rule_tac x = "x ^ n r→ xb" in exI)
apply clarify
apply (subst inf_r_def [THEN sym])
by simp

definition
"cong H = (λ x y . cong_l H x y ∧ cong_r H x y)"

definition
"congruences = {R . equivp R ∧ (∀ a b c d . R a b ∧ R c d ⟶ R (a * c) (b * d) ∧  R (a l→ c) (b l→ d) ∧  R (a r→ c) (b r→ d))}"

lemma cong_l: "H ∈ normalfilters ⟹ cong H = cong_l H"

lemma cong_r: "H ∈ normalfilters ⟹ cong H = cong_r H"

lemma cong_equiv: "H ∈ normalfilters ⟹ equivp (cong H)"
apply (simp add: equivp_reflp_symp_transp reflp_def refl_on_def cong_l_reflexive cong_l_symmetric symp_def sym_def transp_def trans_def)
apply safe
apply (rule cong_l_transitive)
by simp_all

lemma cong_trans: "H ∈ normalfilters ⟹ cong H x y ⟹ cong H y z ⟹ cong H x z"
apply (drule cong_equiv)
apply (drule equivp_transp)
by simp_all

lemma lemma_3_13 [simp]:
"H ∈ normalfilters ⟹ cong H ∈ congruences"
apply (subst congruences_def)
apply safe
apply (rule_tac y = "b * c" in cong_trans)
apply simp_all
apply safe
apply (rule_tac x = x in exI)
apply simp
apply (rule_tac x = y in exI)
apply (simp add: mult.assoc [THEN sym])
apply safe
apply (rule_tac x = xa in exI)
apply simp
apply (rule_tac x = ya in exI)
apply (rule_tac y = "a l→ d" in cong_trans)
apply simp
apply safe
apply (rule_tac a = "c l→ d" in filter_ii)
apply simp_all
apply (subst left_residual [THEN sym])
apply (rule_tac a = "d l→ c" in filter_ii)
apply simp_all
apply (subst left_residual [THEN sym])
apply (subst cong_l)
apply simp
apply (simp add: cong_r cong_r_filter cong_l_filter)
apply safe
apply (rule_tac a = "b l→ a" in filter_ii)
apply simp_all
apply (subst right_residual [THEN sym])
apply (rule_tac a = "a l→ b" in filter_ii)
apply simp_all
apply (subst right_residual [THEN sym])

apply (rule_tac y = "a r→ d" in cong_trans)
apply simp
apply safe
apply (rule_tac a = "c r→ d" in filter_ii)
apply simp_all
apply (subst right_residual [THEN sym])
apply (rule_tac a = "d r→ c" in filter_ii)
apply simp_all
apply (subst right_residual [THEN sym])

apply (subst cong_r)
apply simp
apply (simp add: cong_l cong_l_filter cong_r_filter)
apply safe
apply (rule_tac a = "b r→ a" in filter_ii)
apply simp_all
apply (subst left_residual [THEN sym])
apply (rule_tac a = "a r→ b" in filter_ii)
apply simp_all
apply (subst left_residual [THEN sym])

lemma cong_times: "R ∈ congruences ⟹ R a b ⟹ R c d ⟹ R (a * c) (b * d)"

lemma cong_impl_l: "R ∈ congruences ⟹ R a b ⟹ R c d ⟹ R (a l→ c) (b l→ d)"

lemma cong_impl_r: "R ∈ congruences ⟹ R a b ⟹ R c d ⟹ R (a r→ c) (b r→ d)"

lemma cong_refl [simp]: "R ∈ congruences ⟹ R a a"

lemma cong_trans_a: "R ∈ congruences ⟹ R a b ⟹ R b c ⟹ R a c"
apply (rule_tac y = b in equivp_transp)
by simp_all

lemma cong_sym: "R ∈ congruences ⟹ R a b ⟹ R b a"

definition
"normalfilter R = {a . R a 1}"

lemma lemma_3_14 [simp]:
"R ∈ congruences ⟹ (normalfilter R) ∈ normalfilters"
apply (unfold normalfilters_def)
apply safe
apply safe
apply (drule_tac x = 1 in spec)
apply (drule_tac a = a and c = b and b = 1 and d = 1 and R = R in cong_times)
apply simp_all
apply (cut_tac R = R and a = a and b = 1 and c = b and d = b in cong_impl_l)
apply simp_all
apply (cut_tac R = R and a = "a l→ b" and b = 1 and c = a and d = a in cong_times)
apply simp_all
apply (simp add: inf_l_def [THEN sym])
apply (cut_tac R = R and a = a and b = "a ⊓ b" and c = b and d = b in cong_impl_r)
apply simp_all
apply (cut_tac R = R and c = "a r→ b" and d = 1 and a = a and b = a in cong_times)
apply simp_all
apply (simp add: inf_r_def [THEN sym])
apply (cut_tac R = R and a = a and b = "a ⊓ b" and c = b and d = b in cong_impl_l)
apply simp_all

lemma lemma_3_15_i:
"H ∈ normalfilters ⟹ normalfilter (cong H) = H"
by (simp add: normalfilter_def cong_r cong_r_filter)

lemma lemma_3_15_ii:
"R ∈ congruences ⟹ cong (normalfilter R) = R"
apply (simp add: fun_eq_iff cong_r cong_r_filter)
apply safe
apply (cut_tac R = R and a = "x l→ xa" and b = 1 and c = x and d = x in cong_times)
apply simp_all
apply (cut_tac R = R and a = "xa l→ x" and b = 1 and c = xa and d = xa in cong_times)
apply simp_all
apply (simp add: inf_l_def [THEN sym])
apply (rule_tac b = "x ⊓ xa" in cong_trans_a)
apply simp_all
apply (subst cong_sym)
apply simp_all
apply (subst inf.commute)
apply simp_all
apply (cut_tac R = R and a = x and b = xa and c = xa and d = xa in cong_impl_l)
apply simp_all
apply (cut_tac R = R and a = xa and b = xa and c = x and d = xa in cong_impl_l)
by simp_all

lemma lemma_3_15_iii: "H1 ∈ normalfilters ⟹ H2 ∈ normalfilters ⟹ (H1 ⊆ H2) = (cong H1 ≤ cong H2)"
apply safe
apply blast
apply (subgoal_tac "cong H2 x 1")
apply (subgoal_tac "cong H1 x 1")
apply blast

definition
"p x y z = ((x l→ y) r→ z) ⊓ ((z l→ y) r→ x)"

lemma lemma_3_16_i: "p x x y = y ∧ p x y y = x"
apply safe
apply (rule order.antisym)
apply (rule order.antisym)

definition "M x y z = ((y l→ x) r→ x) ⊓ ((z l→ y) r→ y) ⊓ ((x l→ z) r→ z)"

lemma "M x x y = x ∧ M x y x = x ∧ M y x x = x"
apply safe
apply (rule order.antisym)
apply (rule order.antisym)
apply (rule order.antisym)
end

end


# Theory PseudoWaisbergAlgebra

section‹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 (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 (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 (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
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 (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
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"

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 (subst W2c)
apply (rule P8_a)
apply (subst P7 [THEN sym])
apply (rule_tac y = "(z l→ x) r→ x" in P5_a)
apply (subst W2a)

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 (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 (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 (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 (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 (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 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 (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 (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 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)"

lemma order_r: "(a ≤ b) = (a r→ b = 1)"

lemma P11_a: "a ≤ b l→ a"

lemma P11_b: "a ≤ b r→ a"

lemma P12: "(a ≤ b l→ c) = (b ≤ a r→ c)"
apply (subst order_r)
apply (subst order_l)

lemma P13_a: "a ≤ b ⟹ b l→ c ≤ a l→ c"
apply (subst order_r)
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 (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 (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 (cut_tac x = a and y = b and z = c in P8_b)
by simp

subclass order
apply (subgoal_tac "(≤) = lesseq_a ∧ (<) = 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"

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)

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)

lemma C2_a [simp]: "0 l→ x = 1"

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 order.antisym)
qed

lemma C3_b: "x r→ 0 = -r x"
apply (rule order.antisym)
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)

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 order.antisym)
apply (cut_tac a = "-r y" and b = "-r x" in W5a)

lemma C5_b: "-l x r→ -l y = y l→ x"
apply (rule order.antisym)
apply (cut_tac a = "-l y" and b = "-l x" in W5b)

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)

lemma C7_b: "(x ≤ y) = (-r y ≤ -r x)"
apply (subst order_r)
apply (subst order_l)

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 "(≤)" "(<)"
apply unfold_locales
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)"
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)"
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)"
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)"
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)
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 "(≤)" "(<)"
apply unfold_locales
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)"
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)"
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)"
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)"
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)
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 clarify
apply (rule order.antisym)
by simp_all

end
end


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

apply (simp add: right_residual [THEN sym])
apply (rule_tac y = "((a r→ b) ⊔ (b r→ a)) r→ c" in bounded_lattice.order_trans)

end

class product_pseudo_hoop_algebra = basic_pseudo_hoop_algebra +
assumes P1: "b l→ b * b ≤ (a ⊓ (a l→ b)) l→ b"
and P2: "b r→ b * b ≤ (a ⊓ (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 (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_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 (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 (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)
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])

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

end

lemma (in pseudo_hoop_algebra) [simp]: "{1} ∈ filters"
apply safe
apply (rule order.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 safe
apply simp_all
apply (case_tac "xb = 1")
apply simp
apply (cut_tac a = xb in strong_simple_a)
apply simp
apply blast
apply (cut_tac proper)
by blast
end

sublocale strong_simple_pseudo_hoop_algebra < strong_simple_pseudo_hoop_algebra_a
apply unfold_locales

lemma (in pseudo_hoop_algebra) power_impl: "b l→ a = a ⟹ b ^ n l→ a = a"
apply (induct_tac n)
apply simp

lemma (in pseudo_hoop_algebra) power_impr: "b r→ a = a ⟹ b ^ n r→ a = a"
apply (induct_tac n)
apply simp

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)
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 (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: 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 (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: right_lesseq [THEN sym])
apply safe
apply (erule notE)
by simp

subclass wajsberg_pseudo_hoop_algebra
apply unfold_locales
apply (rule order.antisym)
apply simp_all
apply (rule order.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

subclass wajsberg_pseudo_hoop_algebra
by unfold_locales

end

end


# Theory Examples

section‹Examples of Pseudo-Hoops›

theory Examples
imports SpecialPseudoHoops LatticeProperties.Lattice_Ordered_Group
begin

declare add_uminus_conv_diff [simp del] right_minus [simp]

context lgroup
begin
lemma (in lgroup) less_eq_inf_2: "(x ≤ y) = (inf y x = x)"
end

class lgroup_with_const = lgroup +
fixes u::'a
assumes [simp]: "0 ≤ u"

definition "G = {a::'a::lgroup_with_const. (0 ≤ a ∧ a ≤ u)}"
typedef (overloaded) 'a G = "G::'a::lgroup_with_const set"
proof
show "0 ∈ G" by (simp add: G_def)
qed

instantiation "G" :: (lgroup_with_const) bounded_wajsberg_pseudo_hoop_algebra
begin

definition
times_def: "a * b ≡ Abs_G (sup (Rep_G a - u + Rep_G b) 0)"

lemma [simp]: "sup (Rep_G a - u + Rep_G b) 0 ∈ G"
apply (cut_tac x = a in Rep_G)
apply (cut_tac x = b in Rep_G)
apply (unfold G_def)
apply safe
apply (rule right_move_to_right)
apply (rule_tac y = 0 in order_trans)
apply (rule right_move_to_right)
apply simp
apply (rule right_move_to_left)
by simp

definition
impl_def: "a l→ b ≡ Abs_G ((Rep_G b - Rep_G a + u) ⊓ u)"

lemma [simp]: "inf (Rep_G (b::'a G) - Rep_G a + u) u ∈ G"
apply (cut_tac x = a in Rep_G)
apply (cut_tac x = b in Rep_G)
apply (unfold G_def)
apply safe
apply (rule right_move_to_left)
apply (rule right_move_to_left)
apply simp
apply (rule_tac y = 0 in order_trans)
apply (rule left_move_to_right)
by simp_all

definition
impr_def: "a r→ b ≡ Abs_G (inf (u - Rep_G a + Rep_G b) u)"

lemma [simp]: "inf (u - Rep_G a + Rep_G b) u ∈ G"
apply (cut_tac x = a in Rep_G)
apply (cut_tac x = b in Rep_G)
apply (unfold G_def)
apply safe
apply (rule right_move_to_left)
apply (rule right_move_to_left)
apply simp
apply (rule left_move_to_right)
apply (rule_tac y = u in order_trans)
apply  simp_all
apply (rule right_move_to_left)
by simp_all

definition
one_def: "1 ≡ Abs_G u"

definition
zero_def: "0 ≡ Abs_G 0"

definition
order_def: "((a::'a G) ≤ b) ≡ (a l→ b = 1)"

definition
strict_order_def: "(a::'a G) < b ≡ (a ≤ b ∧ ¬ b ≤ a)"

definition
inf_def: "(a::'a G) ⊓ b = ((a l→ b) * a)"

lemma [simp]: "(u::'a) ∈ G"
apply (