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

lemma [simp]: "(1::'a G) * a = a"
apply (cut_tac y = "u::'a" in Abs_G_inverse)
apply simp_all
apply (subgoal_tac "sup (Rep_G a) (0::'a) = Rep_G a")
apply (cut_tac x = a in Rep_G)
apply (rule antisym)
by simp

lemma [simp]: "a * (1::'a G) = a"
apply (cut_tac y = "u::'a" in Abs_G_inverse)
apply (subgoal_tac "sup (Rep_G a) (0::'a) = Rep_G a")
apply (cut_tac x = a in Rep_G)
apply (rule antisym)

lemma [simp]: "a l→ a = (1::'a G)"

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

lemma [simp]: "a ∈ G ⟹ Rep_G (Abs_G a) = a"
apply (rule Abs_G_inverse)
by simp

lemma inf_def_1: "((a::'a G) l→ b) * a = Abs_G (inf (Rep_G a) (Rep_G b))"
apply (subgoal_tac "sup (inf (Rep_G b) (Rep_G a)) 0 = inf (Rep_G a) (Rep_G b)")
apply simp
apply (rule antisym)
apply (cut_tac x = "a" in Rep_G)
apply (cut_tac x = "b" in Rep_G)
apply (subgoal_tac "inf (Rep_G a) (Rep_G b) = inf (Rep_G b) (Rep_G a)")
apply simp
apply (rule antisym)
by simp_all

lemma inf_def_2: "(a::'a G) * (a r→ b) = Abs_G (inf (Rep_G a) (Rep_G b))"
apply (subgoal_tac "sup (inf (Rep_G b) (Rep_G a)) 0 = inf (Rep_G a) (Rep_G b)")
apply simp
apply (rule antisym)
apply (cut_tac x = "a" in Rep_G)
apply (cut_tac x = "b" in Rep_G)
apply (subgoal_tac "inf (Rep_G a) (Rep_G b) = inf (Rep_G b) (Rep_G a)")
apply simp
apply (rule antisym)
by simp_all

lemma Rep_G_order: "(a ≤ b) = (Rep_G a ≤ Rep_G b)"
apply (simp add: order_def impl_def one_def)
apply safe
apply (subgoal_tac "Rep_G (Abs_G (inf (Rep_G b - Rep_G a + u) u)) = Rep_G (Abs_G u)")
apply (drule drop_assumption)
apply simp
apply (subst (asm) less_eq_inf_2 [THEN sym])
apply (drule_tac a = "u" and b = " Rep_G b + - Rep_G a + u" and v = "-u" in add_order_preserving_right)
apply (drule_tac a = "0" and b = " Rep_G b + - Rep_G a" and v = "Rep_G a" in add_order_preserving_right)
apply simp
apply (subgoal_tac "Rep_G (Abs_G (inf (Rep_G b - Rep_G a + u) u)) = Rep_G (Abs_G u)")
apply simp
apply simp
apply (subst less_eq_inf_2 [THEN sym])
apply (rule right_move_to_left)
apply simp
apply (rule right_move_to_left)
by simp

lemma ded_left: "((a::'a G) * b) l→ c = a l→ b l→ c"
apply (subgoal_tac "inf (Rep_G c + u) u = u")
apply (subgoal_tac "inf (u + - Rep_G a + u) u = u")
apply simp
apply (rule antisym)
apply simp
apply simp
apply (cut_tac x = a in Rep_G)
apply (rule left_move_to_left)
apply simp
apply (rule antisym)
apply simp
apply simp
apply (cut_tac x = c in Rep_G)

lemma ded_right: "((a::'a G) * b) r→ c = b r→ a r→ c"
apply (subgoal_tac "inf (u + Rep_G c) u = u")
apply (subgoal_tac "inf (u + - Rep_G b + u) u = u")
apply simp
apply (rule antisym)
apply simp
apply simp
apply (cut_tac x = b in Rep_G)
apply (rule left_move_to_left)
apply simp
apply (rule antisym)
apply simp
apply simp
apply (cut_tac x = c in Rep_G)

lemma [simp]: "0 ∈ G"

lemma [simp]: "0 ≤ (a::'a G)"
apply (simp add: order_def impl_def zero_def one_def diff_minus)
apply (subgoal_tac "inf (Rep_G a + u) u = u")
apply simp
apply (rule antisym)
apply simp
apply (cut_tac x = a in Rep_G)
apply (unfold G_def)
apply simp
by simp

lemma lemma_W1: "((a::'a G) l→ b) r→ b = (b l→ a) r→ a"
apply (subgoal_tac "Rep_G a ⊔ Rep_G b = Rep_G b ⊔ Rep_G a")
apply simp
apply (rule antisym)
by simp_all

lemma lemma_W2: "((a::'a G) r→ b) l→ b = (b r→ a) l→ a"
apply (subgoal_tac "Rep_G a ⊔ Rep_G b = Rep_G b ⊔ Rep_G a")
apply simp
apply (rule antisym)
by simp_all

instance proof
fix a show "(1::'a G) * a = a" by simp
fix a show "a * (1::'a G) = a" by simp
fix a show "a l→ a = (1::'a G)" by simp
fix a show "a r→ a = (1::'a G)" by simp
next
fix a b have a: "((a::'a G) l→ b) * a = (b l→ a) * b"
show "((a::'a G) l→ b) * a = (b l→ a) * b" by (rule a)
next
fix a b have a: "a * ((a::'a G) r→ b) = b * (b r→ a)" by (simp add: inf_def_2 inf_commute)
show "a * ((a::'a G) r→ b) = b * (b r→ a)" by (rule a)
next
fix a b have "!!a b . ((a::'a G) l→ b) * a = a * (a r→ b)" by (simp add: inf_def_2 inf_def_1)
from this show "((a::'a G) l→ b) * a = a * (a r→ b)"  by simp
next
fix a b c show "(a::'a G) * b l→ c = a l→ b l→ c" by (rule ded_left)
next
fix a b c show "(a::'a G) * b r→ c = b r→ a r→ c" by (rule ded_right)
next
fix a::"'a G" have "0 ≤ a" by simp
from this show "0 ≤ a" by simp
next
fix a b::"'a G" show "(a ≤ b) = (a l→ b = 1)" by (simp add: order_def)
next
fix a b::"'a G" show "(a < b) = (a ≤ b ∧ ¬ b ≤ a)" by (simp add: strict_order_def)
next
fix a b::"'a G" show "(a l→ b) r→ b = (b l→ a) r→ a" by (rule lemma_W1)
next
fix a b::"'a G" show "(a r→ b) l→ b = (b r→ a) l→ a" by (rule lemma_W2)
next
fix a b::"'a G" show "a ⊓ b = (a l→ b) * a" by (rule inf_def)
next
fix a b::"'a G" show "a ⊓ b = a * (a r→ b)" by (simp add: inf_def inf_def_2 inf_def_1)
qed

end

context order
begin
definition
closed_interval::"'a⇒'a⇒'a set" ("|[ _ , _ ]|" [0, 0] 900) where
"closed_interval a b = {c . a ≤ c ∧ c ≤ b}"

definition
"convex = {A . ∀ a b . a ∈ A ∧ b ∈ A ⟶ |[a, b]| ⊆ A}"

end

begin
definition
"subgroup = {A . 0 ∈ A ∧ (∀ a b . a ∈ A ∧ b ∈ A ⟶ a + b ∈ A ∧ -a ∈ A)}"

lemma [simp]: "A ∈ subgroup ⟹ 0 ∈ A"

lemma [simp]: "A ∈ subgroup ⟹ a ∈ A ⟹ b ∈ A ⟹ a + b ∈ A"
apply (subst (asm) subgroup_def)
by simp

lemma minus_subgroup: "A ∈ subgroup ⟹ -a ∈ A ⟹ a ∈ A"
apply (subst (asm) subgroup_def)
apply safe
apply (drule_tac x="-a" in spec)
by simp

definition
add_set:: "'a set ⇒ 'a set ⇒ 'a set" (infixl "+++" 70) where
"add_set A B = {c . ∃ a ∈ A .∃ b ∈ B . c = a + b}"

definition
"normal = {A . (∀ a . A +++ {a} = {a} +++ A)}"
end

context lgroup
begin
definition
"lsubgroup = {A . A ∈ subgroup ∧ (∀ a b . a ∈ A ∧ b ∈ A ⟶ inf a b ∈ A ∧ sup a b ∈ A)}"

lemma inf_lsubgroup:
"A ∈ lsubgroup ⟹ a ∈ A ⟹ b ∈ A ⟹ inf a b ∈ A"

lemma sup_lsubgroup:
"A ∈ lsubgroup ⟹ a ∈ A ⟹ b ∈ A ⟹ sup a b ∈ A"
end

definition
"F K = {a:: 'a G . (u::'a::lgroup_with_const) - Rep_G a ∈ K}"

lemma F_def2: "K ∈ normal ⟹ F K = {a:: 'a G . - Rep_G a + (u::'a::lgroup_with_const) ∈ K}"
apply safe
apply (drule_tac x = "Rep_G x" in spec)
apply (subgoal_tac "u ∈ K +++ {Rep_G x}")
apply simp
apply (drule drop_assumption)
apply (drule drop_assumption)
apply safe
apply (subgoal_tac "- Rep_G x + u = - Rep_G x + Rep_G x + b")
apply simp
apply simp
apply simp
apply (rule_tac x = "u - Rep_G x" in bexI)
apply simp
apply (drule_tac x = "Rep_G x" in spec)
apply (subgoal_tac "u ∈ K +++ {Rep_G x}")
apply (drule drop_assumption)
apply (drule drop_assumption)
apply safe
apply (subgoal_tac "u - Rep_G x = a +  (Rep_G x -  Rep_G x)")
apply simp
apply (subst diff_minus)
apply (subst diff_minus)
apply simp
apply simp
apply simp
apply (rule_tac x = "- Rep_G x + u" in bexI)
by simp

context lgroup begin
lemma sup_assoc_lgroup: "a ⊔ b ⊔ c = a ⊔ (b ⊔ c)"
by (rule sup_assoc)

end

lemma normal_1: "K ∈ normal ⟹ K ∈ convex ⟹ K ∈ lsubgroup ⟹ x ∈ {a} ** F K ⟹ x ∈ F K ** {a}"
apply (subst (asm) times_set_def)
apply simp
apply safe
apply (subst (asm) F_def2)
apply simp_all
apply (subgoal_tac "-u + Rep_G y ∈ K")
apply (subgoal_tac "Rep_G a - u + Rep_G y ∈ K +++ {Rep_G a}")
apply simp
apply safe
apply (rule_tac x = "Abs_G (inf (sup (aa + u) 0) u)" in bexI)
apply (subgoal_tac "aa =  Rep_G a - u + Rep_G y - Rep_G a")
apply (subgoal_tac "inf (sup (aa + u) (0::'a)) u ∈ G")
apply safe
apply simp
apply (subgoal_tac "(sup (Rep_G a - u + Rep_G y) 0) = (sup (inf (sup (Rep_G a - u + Rep_G y - Rep_G a + u - u + Rep_G a) (- u + Rep_G a)) (Rep_G a)) 0)")
apply simp
apply (subgoal_tac "inf (sup (Rep_G a + (- u + Rep_G y)) (- u + Rep_G a)) (Rep_G a) = (sup (Rep_G a + (- u + Rep_G y)) (- u + Rep_G a))")
apply simp
(*apply (subst sup_assoc) - why it does not work*)
apply (subst sup_assoc_lgroup)
apply (subgoal_tac "(sup (- u + Rep_G a) (0::'a)) = 0")
apply simp
apply (rule antisym)
apply simp
apply (rule left_move_to_right)
apply simp
apply (cut_tac x = a in Rep_G)
apply simp
apply (rule antisym)
apply simp
apply simp
apply safe
apply (rule left_move_to_right)
apply simp
apply (rule left_move_to_right)
apply simp
apply (cut_tac x = y in Rep_G)
apply (rule left_move_to_right)
apply simp
apply (rule right_move_to_left)
apply simp
apply (subgoal_tac "inf (sup (aa + u) (0::'a)) u ∈ G")
apply simp
apply (subst (asm) convex_def)
apply simp
apply (drule_tac x = 0 in spec)
apply (drule_tac x = "sup (- aa) 0" in spec)
apply safe
apply (subst (asm) lsubgroup_def)
apply simp
apply (rule sup_lsubgroup)
apply simp
apply (rule minus_subgroup)
apply (subst (asm) lsubgroup_def)
apply simp
apply simp
apply (subst (asm) lsubgroup_def)
apply simp
apply (subgoal_tac "sup (inf (- aa) u) (0::'a) ∈ |[ 0::'a , sup (- aa) (0::'a) ]|")
apply blast
apply (subst closed_interval_def)
apply safe
apply simp
apply simp
(*
apply (rule_tac y = "-aa" in order_trans)
apply simp
apply simp
*)
apply (subst (asm) normal_def)
apply simp
apply (drule drop_assumption)
apply (rule_tac x = "-u + Rep_G y" in bexI)
apply simp
apply (rule minus_subgroup)

lemma normal_2: "K ∈ normal ⟹ K ∈ convex ⟹ K ∈ lsubgroup ⟹ x ∈ F K ** {a} ⟹ x ∈ {a} ** F K"
apply (subst (asm) times_set_def)
apply simp
apply safe
apply (subst (asm) F_def)
apply simp_all
apply hypsubst_thin
apply (subgoal_tac "Rep_G x - u ∈ K")
apply (subgoal_tac "Rep_G x - u + Rep_G a ∈ {Rep_G a} +++ K")
apply simp
apply safe
apply (rule_tac x = "Abs_G (inf (sup (u + b) 0) u)" in bexI)
apply (subgoal_tac "b =  - Rep_G a + Rep_G x - u + Rep_G a")
apply (subgoal_tac "inf (sup (u + b) 0) u ∈ G")
apply safe
apply simp
apply (subgoal_tac "sup (Rep_G x + - u + Rep_G a) 0 = sup (inf (sup (Rep_G x + - u + Rep_G a) (Rep_G a + - u)) (Rep_G a)) 0")
apply simp
apply (subgoal_tac "inf (sup (Rep_G x + - u + Rep_G a) (Rep_G a + - u)) (Rep_G a) = sup (Rep_G x + - u + Rep_G a) (Rep_G a + - u)")
apply simp
(*apply (subst sup_assoc) - why it does not work*)
apply (subst sup_assoc_lgroup)
apply (subgoal_tac "(sup (Rep_G a + - u) (0::'a)) = 0")
apply simp
apply (rule antisym)
apply simp
apply (rule right_move_to_right)
apply simp
apply (cut_tac x = a in Rep_G)
apply simp
apply (rule antisym)
apply simp
apply simp
apply safe
apply (rule right_move_to_right)
apply simp
apply (rule right_move_to_right)
apply simp
apply (cut_tac x = x in Rep_G)
apply (rule right_move_to_right)
apply simp
apply (rule left_move_to_left)
apply simp
apply (subgoal_tac "inf (sup (u + b) (0::'a)) u ∈ G")
apply simp
apply (subst (asm) convex_def)
apply simp
apply (drule_tac x = 0 in spec)
apply (drule_tac x = "sup (- b) 0" in spec)
apply safe
apply (subst (asm) lsubgroup_def)
apply simp
apply (rule sup_lsubgroup)
apply simp
apply (rule minus_subgroup)
apply (subst (asm) lsubgroup_def)
apply simp
apply simp
apply (subst (asm) lsubgroup_def)
apply simp
apply (subgoal_tac "sup (inf (- b) u) (0::'a) ∈ |[ 0::'a , sup (-b) 0]|")
apply blast
apply (subst closed_interval_def)
apply safe
apply simp
apply simp
(*
apply (rule_tac y = "-b" in order_trans)
apply simp
apply simp
*)
apply (subgoal_tac  "{Rep_G a} +++ K = K +++ {Rep_G a}")
apply simp
apply (subst (asm) normal_def)
apply simp
apply (rule minus_subgroup)

lemma "K ∈ normal ⟹ K ∈ convex ⟹ K ∈ lsubgroup ⟹ F K ∈ normalfilters"
apply (rule lemma_3_10_ii_i)
apply (subgoal_tac "K ∈ subgroup")
apply (subst filters_def)
apply safe
apply (subgoal_tac "1 ∈ F K")
apply simp
apply (subst F_def)
apply safe
apply (subst one_def)
apply simp
apply (drule_tac x = 0 in spec)
apply (drule_tac x = "(u - Rep_G b) + (u - Rep_G a) " in spec)
apply simp
apply (subgoal_tac "u - Rep_G (a * b) ∈ |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]|")
apply blast
apply safe
apply (cut_tac x = "a * b" in Rep_G)
apply (rule right_move_to_left)
apply simp
apply (subgoal_tac "(u - (Rep_G a - u + Rep_G b)) = u - Rep_G b + (u - Rep_G a)")
apply simp
apply (subst (asm) Rep_G_order)

apply (subst (asm) convex_def)
apply simp
apply (drule_tac x = 0 in spec)
apply (drule_tac x = " u - Rep_G a" in spec)
apply simp
apply (subgoal_tac "u - Rep_G b ∈ |[ 0::'a , u - Rep_G a ]|")
apply blast
apply (subst closed_interval_def)
apply simp
apply safe
apply (cut_tac x = "b" in Rep_G)
apply (safe)
apply (rule right_move_to_left)
apply simp
apply (rule minus_order)
apply simp
apply (rule normal_1)
apply simp_all
apply (rule normal_2)
by simp_all

definition "N = {a::'a::lgroup. a ≤ 0}"
typedef (overloaded) ('a::lgroup) N = "N :: 'a::lgroup set"
proof
show "0 ∈ N" by (simp add: N_def)
qed

class cancel_product_pseudo_hoop_algebra = cancel_pseudo_hoop_algebra + product_pseudo_hoop_algebra

begin
proof qed
(*
fix a b c :: 'a
assume "a + b = a + c"
then have "- a + a + b = - a + a + c"
then show "b = c" by simp
next
fix a b c :: 'a
assume "b + a = c + a"
then have "b + a + - a = c + a  + - a" by simp
then show "b = c" unfolding add.assoc by simp
qed
*)
end

instantiation "N" :: (lgroup) pseudo_hoop_algebra
begin

definition
times_N_def: "a * b ≡ Abs_N (Rep_N a +  Rep_N b)"

lemma [simp]: "Rep_N a + Rep_N b ∈ N"
apply (cut_tac x = a in Rep_N)
apply (cut_tac x = b in Rep_N)
apply (rule_tac left_move_to_right)
apply (rule_tac y = 0 in order_trans)
apply simp_all
apply (rule_tac minus_order)
by simp

definition
impl_N_def: "a l→ b ≡ Abs_N (inf (Rep_N b - Rep_N a) 0)"

definition
inf_N_def: "(a:: 'a N) ⊓ b = (a l→ b) * a"

lemma [simp]: "inf (Rep_N b - Rep_N a) 0 ∈ N"
apply (cut_tac x = a in Rep_N)
apply (cut_tac x = b in Rep_N)

definition
impr_N_def: "a r→ b ≡ Abs_N (inf (- Rep_N a + Rep_N b) 0)"

lemma [simp]: "inf (- Rep_N a + Rep_N b) 0 ∈ N"
apply (cut_tac x = a in Rep_N)
apply (cut_tac x = b in Rep_N)

definition
one_N_def: "1 ≡ Abs_N 0"

lemma [simp]: "0 ∈ N"

definition
order_N_def: "((a::'a N) ≤ b) ≡ (a l→ b = 1)"

definition
strict_order_N_def: "(a::'a N) < b ≡ (a ≤ b ∧ ¬ b ≤ a)"

lemma order_Rep_N:
"((a::'a N) ≤ b) = (Rep_N a ≤ Rep_N b)"
apply (subst order_N_def)
apply (subgoal_tac "(Abs_N (inf (Rep_N b - Rep_N a) (0::'a)) = Abs_N (0::'a)) = ((Rep_N (Abs_N (inf (Rep_N b - Rep_N a) (0::'a))) = Rep_N(Abs_N (0::'a))))")
apply simp
apply (drule drop_assumption)
apply safe
apply (subgoal_tac "0 ≤ Rep_N b - Rep_N a")
apply (drule_tac v = "Rep_N a" in add_order_preserving_right)
apply (rule_tac y = "inf (Rep_N b - Rep_N a) (0::'a)" in order_trans)
apply simp
apply (drule drop_assumption)
apply simp
apply (rule antisym)
apply simp
apply simp
apply (rule right_move_to_left)
apply simp
apply simp

lemma order_Abs_N:
"a ∈ N ⟹ b ∈ N ⟹ (a ≤ b) = (Abs_N a ≤ Abs_N b)"
apply (subst order_N_def)
apply (subgoal_tac "inf (b - a) 0 ∈ N")
apply (subgoal_tac "(Abs_N (inf (b - a) (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N (inf (b - a) (0::'a))) = Rep_N (Abs_N (0::'a)))")
apply simp
apply (drule drop_assumption)
apply (drule drop_assumption)
apply (drule drop_assumption)
apply (drule drop_assumption)
apply simp
apply safe
apply (rule antisym)
apply simp_all
apply (rule right_move_to_left)
apply simp
apply (subgoal_tac "0 ≤ b - a")
apply (drule_tac v = "a" in add_order_preserving_right)
apply (rule_tac y = "inf (b - a) (0::'a)" in order_trans)
apply simp
apply (drule drop_assumption)
apply simp

lemma [simp]: "(1::'a N) * a = a"
by (simp add: one_N_def times_N_def Abs_N_inverse Rep_N_inverse)

lemma [simp]: "a * (1::'a N) = a"
by (simp add: one_N_def times_N_def Abs_N_inverse Rep_N_inverse)

lemma [simp]: "a l→ a = (1::'a N)"
by (simp add: impl_N_def one_N_def Abs_N_inverse Rep_N_inverse)

lemma [simp]: "a r→ a = (1::'a N)"
by (simp add: impr_N_def one_N_def Abs_N_inverse Rep_N_inverse)

lemma impl_times: "(a l→ b) * a = (b l→ a) * (b::'a N)"
apply (simp add: impl_N_def impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)
apply (subgoal_tac "inf (Rep_N b - Rep_N a + Rep_N a) (Rep_N a) = inf (Rep_N a - Rep_N b + Rep_N b) (Rep_N b)")
apply simp
apply (subgoal_tac "Rep_N b - Rep_N a + Rep_N a = Rep_N b ")
apply simp
apply (subgoal_tac "Rep_N a - Rep_N b + Rep_N b = Rep_N a")
apply simp
apply (rule antisym)
by simp_all

lemma impr_times: "a * (a r→ b) = (b::'a N) * (b r→ a)"
apply (simp add: impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)
apply (subgoal_tac "inf (Rep_N a + (- Rep_N a + Rep_N b)) (Rep_N a) = inf (Rep_N b + (- Rep_N b + Rep_N a)) (Rep_N b)")
apply simp
apply (rule antisym)
by simp_all

lemma impr_impl_times: "(a l→ b) * a = (a::'a N) * (a r→ b)"
by (simp add: impl_N_def impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)

lemma impl_ded: "(a::'a N) * b l→ c = a l→ b l→ c"
apply (simp add: impl_N_def impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)
apply (subgoal_tac "inf (Rep_N c - (Rep_N a + Rep_N b)) (0::'a) = inf (inf (Rep_N c - Rep_N b - Rep_N a) (- Rep_N a)) (0::'a)")
apply simp
apply (rule antisym)
apply simp_all
apply safe
apply (rule_tac y = "Rep_N c - (Rep_N a + Rep_N b)" in order_trans)
apply simp
apply (rule_tac y = "0" in order_trans)
apply simp
apply (cut_tac x = a in "Rep_N")
apply (drule_tac u = 0 and v = "- Rep_N a" in add_order_preserving)
apply simp
apply (rule_tac y = "inf (Rep_N c - Rep_N b - Rep_N a) (- Rep_N a)" in order_trans)
apply (rule inf_le1)
apply (rule_tac y = "Rep_N c - Rep_N b - Rep_N a" in order_trans)
apply simp

lemma impr_ded: "(a::'a N) * b r→ c = b r→ a r→ c"
apply (simp add: impr_N_def impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)
apply (subgoal_tac "inf (- (Rep_N a + Rep_N b) + Rep_N c) (0::'a) = inf (inf (- Rep_N b + (- Rep_N a + Rep_N c)) (- Rep_N b)) (0::'a)")
apply simp
apply (rule antisym)
apply simp_all
apply safe
apply (rule_tac y = "- (Rep_N a + Rep_N b) + Rep_N c" in order_trans)
apply simp
apply (rule_tac y = "0" in order_trans)
apply simp
apply (cut_tac x = b in "Rep_N")
apply (drule_tac u = 0 and v = "- Rep_N b" in add_order_preserving)
apply simp
apply (rule_tac y = "inf (- Rep_N b + (- Rep_N a + Rep_N c)) (- Rep_N b)" in order_trans)
apply (rule inf_le1)
apply (rule_tac y = "- Rep_N b + (- Rep_N a + Rep_N c)" in order_trans)
apply simp

instance proof
fix a show "(1::'a N) * a = a" by simp
fix a show "a * (1::'a N) = a" by simp
fix a show "a l→ a = (1::'a N)" by simp
fix a show "a r→ a = (1::'a N)" by simp
next
fix a b::"'a N" show "(a l→ b) * a = (b l→ a) * b" by (simp add: impl_times)
next
fix a b::"'a N" show "a * (a r→ b) = b * (b r→ a)" by (simp add: impr_times)
next
fix a b::"'a N" show "(a l→ b) * a = a * (a r→ b)" by (simp add: impr_impl_times)
next
fix a b c::"'a N" show "a * b l→ c = a l→ b l→ c" by (simp add: impl_ded)
fix a b c::"'a N" show "a * b r→ c = b r→ a r→ c" by (simp add: impr_ded)
next
fix a b::"'a N" show "(a ≤ b) = (a l→ b = 1)" by (simp add: order_N_def)
next
fix a b::"'a N" show "(a < b) = (a ≤ b ∧ ¬ b ≤ a)" by (simp add: strict_order_N_def)
next
fix a b::"'a N" show "a ⊓ b = (a l→ b) * a" by (simp add: inf_N_def)
next
fix a b::"'a N" show "a ⊓ b = a * (a r→ b)" by (simp add: inf_N_def impr_impl_times)
qed

end

lemma Rep_N_inf: "Rep_N ((a::'a::lgroup N) ⊓ b) = (Rep_N a) ⊓ (Rep_N b)"
apply (rule antisym)
apply simp_all
apply safe
apply (simp add: order_Rep_N [THEN sym])
apply (simp add: order_Rep_N [THEN sym])
apply (subgoal_tac "inf (Rep_N a) (Rep_N b) ∈ N")
apply (subst order_Abs_N)
apply simp_all
apply (cut_tac x = "a ⊓ b" in Rep_N)
apply safe
apply (subst order_Rep_N)
apply (subst order_Rep_N)
apply (rule_tac y = "Rep_N a" in order_trans)
apply simp
apply (cut_tac x = a in Rep_N)

context lgroup begin

lemma sup_inf_distrib2_lgroup: "(b ⊓ c) ⊔ a = (b ⊔ a) ⊓ (c ⊔ a)"
by (rule sup_inf_distrib2)

lemma inf_sup_distrib2_lgroup: "(b ⊔ c) ⊓ a = (b ⊓ a) ⊔ (c ⊓ a)"
by (rule inf_sup_distrib2)
end

instantiation "N" :: (lgroup) cancel_product_pseudo_hoop_algebra
begin

lemma cancel_times_left: "(a::'a N) * b = a * c ⟹ b = c"
apply (simp add: times_N_def Abs_N_inverse Rep_N_inverse)
apply (subgoal_tac "Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c))")
apply (drule drop_assumption)
apply (subgoal_tac "Abs_N (Rep_N b) = Abs_N (Rep_N c)")
apply (drule drop_assumption)
by simp_all

lemma cancel_times_right: "b * (a::'a N) = c * a ⟹ b = c"
apply (simp add: times_N_def Abs_N_inverse Rep_N_inverse)
apply (subgoal_tac "Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a))")
apply (drule drop_assumption)
apply (subgoal_tac "Abs_N (Rep_N b) = Abs_N (Rep_N c)")
apply (drule drop_assumption)
by simp_all

lemma prod_1: "((a::'a N) l→ b) l→ c ≤ ((b l→ a) l→ c) l→ c"
apply (unfold impl_N_def times_N_def Abs_N_inverse Rep_N_inverse order_N_def one_N_def)
apply (subst Abs_N_inverse)
apply simp
apply (subst Abs_N_inverse)
apply simp
apply (subst Abs_N_inverse)
apply simp
apply (subst Abs_N_inverse)
apply simp
apply (subst Abs_N_inverse)
apply simp
apply (subgoal_tac "inf (inf (Rep_N c - inf (Rep_N c - inf (Rep_N a - Rep_N b) 0) 0) 0 - inf (Rep_N c - inf (Rep_N b - Rep_N a) 0) 0) 0 = 0")
apply simp
apply (rule antisym)
apply simp
apply (rule inf_greatest)
apply (subst diff_minus)
apply (subst diff_minus)
apply (subst diff_minus)
apply (subst diff_minus)
apply (rule right_move_to_left)
apply simp_all
(*apply (subst sup_inf_distrib2) - why it does not work*)
apply (subst sup_inf_distrib2_lgroup)
apply simp
(*apply safe*)
(*apply (subst inf_sup_distrib2) - why it does not work*)
apply (subst inf_sup_distrib2_lgroup)
apply simp
(*apply safe*)
apply (rule_tac y="Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c)" in order_trans)
apply simp_all
apply (rule_tac y="Rep_N c + (Rep_N a + - Rep_N b)" in order_trans)
apply simp_all
apply (rule left_move_to_left)
apply simp
apply (cut_tac x = c in Rep_N)
apply (rule minus_order)
by simp

lemma prod_2: "((a::'a N) r→ b) r→ c ≤ ((b r→ a) r→ c) r→ c"
apply (unfold impr_N_def times_N_def Abs_N_inverse Rep_N_inverse right_lesseq one_N_def)
apply (subst Abs_N_inverse)
apply simp
apply (subst Abs_N_inverse)
apply simp
apply (subst Abs_N_inverse)
apply simp
apply (subst Abs_N_inverse)
apply simp
apply (subst Abs_N_inverse)
apply simp
apply (subgoal_tac "inf (- inf (- inf (- Rep_N a + Rep_N b) (0::'a) + Rep_N c) (0::'a) + inf (- inf (- inf (- Rep_N b + Rep_N a) (0::'a) + Rep_N c) (0::'a) + Rep_N c) (0::'a))
(0::'a) = 0")
apply simp
apply (rule antisym)
apply simp
apply (rule inf_greatest)
apply (rule minus_order)
apply (subst minus_minus)
apply (subst minus_zero)
apply (rule left_move_to_right)
apply (subst minus_minus)
apply simp
apply simp_all
(*apply (subst sup_inf_distrib2) - why it does not work*)
apply (subst sup_inf_distrib2_lgroup)
apply simp
(*  apply safe*)
(*apply (subst inf_sup_distrib2) - why it does not work*)
apply (subst inf_sup_distrib2_lgroup)
apply simp
(*  apply safe*)
apply (rule_tac y = "- Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c" in order_trans)
apply simp_all
apply (rule_tac y = "- Rep_N b + Rep_N a + Rep_N c" in order_trans)
apply simp_all
apply (rule left_move_to_left)
apply (rule right_move_to_right)
apply simp
apply (cut_tac x = c in Rep_N)

lemma prod_3: "(b::'a N) l→ b * b ≤ a ⊓ (a l→ b) l→ b"
apply (simp add: impl_N_def times_N_def Abs_N_inverse Rep_N_inverse order_N_def one_N_def Rep_N_inf)
apply (subst Abs_N_inverse)
apply (subst Abs_N_inverse)
apply (subgoal_tac "inf (inf (sup (Rep_N b - Rep_N a) (sup (Rep_N b - (Rep_N b - Rep_N a)) (Rep_N b))) (0::'a) - inf (Rep_N b + Rep_N b - Rep_N b) (0::'a)) (0::'a) = 0")
apply simp
apply (rule antisym)
apply simp
apply (subst diff_minus)
apply (subst diff_minus)
apply (subst diff_minus)
apply (subst diff_minus)
apply (subst diff_minus)
apply (rule inf_greatest)
apply (rule right_move_to_left)
apply (subst minus_minus)
apply simp_all
apply (rule_tac y = "Rep_N b" in order_trans)
by simp_all

lemma prod_4: "(b::'a N) r→ b * b ≤ a ⊓ (a r→ b) r→ b"
apply (subst order_Abs_N [THEN sym])
apply simp
apply (rule_tac y = "- Rep_N a + Rep_N b" in order_trans)
apply simp_all
apply (rule_tac y = "Rep_N b" in order_trans)
apply simp
apply (rule right_move_to_left)
apply simp
apply (rule minus_order)
apply simp
apply (cut_tac x = a in Rep_N)

lemma prod_5: "(((a::'a N) l→ b) l→ b) * (c * a l→ f * a) * (c * b l→ f * b) ≤ c l→ f"
apply (subst Abs_N_inverse)
apply (subst Abs_N_inverse)
apply (subst Abs_N_inverse)
apply (subst order_Abs_N [THEN sym])
apply (simp add: N_def inf_assoc [THEN sym])
apply (subst (4) add.assoc [THEN sym])
apply (subst (5) add.assoc [THEN sym])
apply (rule right_move_to_right)

lemma prod_6: "(((a::'a N) r→ b) r→ b) * (a * c r→ a * f) * (b * c r→ b * f) ≤ c r→ f"
apply (subst Abs_N_inverse)
apply (subst Abs_N_inverse)
apply (subst Abs_N_inverse)
apply (subst order_Abs_N [THEN sym])
apply (simp add: N_def inf_assoc [THEN sym])
apply (subst (4) add.assoc [THEN sym])
apply (subst (5) add.assoc [THEN sym])
apply (rule right_move_to_right)

instance
apply intro_classes
by (fact cancel_times_left cancel_times_right prod_1 prod_2 prod_3 prod_4 prod_5 prod_6)+

end

definition "OrdSum =
{x. (∃a::'a::pseudo_hoop_algebra. x = (a, 1::'b::pseudo_hoop_algebra)) ∨ (∃b::'b. x = (1::'a, b))}"
typedef (overloaded) ('a, 'b) OrdSum = "OrdSum :: ('a::pseudo_hoop_algebra × 'b::pseudo_hoop_algebra) set"
proof
show "(1, 1) ∈ OrdSum" by (simp add: OrdSum_def)
qed

lemma [simp]: "(1, b) ∈ OrdSum"

lemma [simp]: "(a, 1) ∈ OrdSum"

definition
"first x = fst (Rep_OrdSum x)"

definition
"second x = snd (Rep_OrdSum x)"

lemma if_unfold_left: "((if a then b else c) = d) = ((a⟶ b = d) ∧ (¬ a ⟶ c = d))"
apply auto
done

lemma if_unfold_right: "(d = (if a then b else c)) = ((a ⟶ d = b) ∧ (¬ a ⟶ d = c))"
apply auto
done

lemma fst_snd_eq: "fst a = x ⟹ snd a = y ⟹ (x, y) = a"
apply (subgoal_tac "x = fst a")
apply (subgoal_tac "y = snd a")
apply (drule drop_assumption)
apply (drule drop_assumption)
by simp_all

instantiation "OrdSum" :: (pseudo_hoop_algebra, pseudo_hoop_algebra) pseudo_hoop_algebra
begin

definition
times_OrdSum_def: "a * b ≡ (
if second a = 1 ∧ second b = 1 then
Abs_OrdSum (first a * first b, 1)
else if first a = 1 ∧ first b = 1 then
Abs_OrdSum (1, second a * second b)
else if first a = 1 ∧ second b = 1 then
b
else
a)"

definition
one_OrdSum_def: "1 ≡ Abs_OrdSum (1, 1)"

definition
impl_OrdSum_def: "a l→ b ≡
(if second a = 1 ∧ second b = 1 then
Abs_OrdSum (first a l→ first b, 1)
else if first a = 1 ∧ first b = 1 then
Abs_OrdSum (1, second a l→ second b)
else if first a = 1 ∧ second b = 1 then
b
else
1)"

definition
impr_OrdSum_def: "a r→ b ≡
(if second a = 1 ∧ second b = 1 then
Abs_OrdSum (first a r→ first b, 1)
else if first a = 1 ∧ first b = 1 then
Abs_OrdSum (1, second a r→ second b)
else if first a = 1 ∧ second b = 1 then
b
else
1)"

definition
order_OrdSum_def: "((a::('a, 'b) OrdSum) ≤ b) ≡ (a l→ b = 1)"

definition
inf_OrdSum_def: "(a::('a, 'b) OrdSum) ⊓ b = (a l→ b) * a"

definition
strict_order_OrdSum_def: "(a::('a, 'b) OrdSum) < b ≡ (a ≤ b ∧ ¬ b ≤ a)"

lemma OrdSum_first [simp]: "(a, 1) ∈ OrdSum"

lemma OrdSum_second [simp]: "(1, b) ∈ OrdSum"

lemma Rep_OrdSum_eq: "Rep_OrdSum x = Rep_OrdSum y ⟹ x = y"
apply (subgoal_tac "Abs_OrdSum (Rep_OrdSum x) = Abs_OrdSum (Rep_OrdSum y)")
apply (drule drop_assumption)
by simp

lemma Abs_OrdSum_eq: "x ∈ OrdSum ⟹ y ∈ OrdSum ⟹ Abs_OrdSum x = Abs_OrdSum y ⟹ x = y"
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)")
apply (unfold Abs_OrdSum_inverse) [1]
by simp_all

lemma [simp]: "fst (Rep_OrdSum a) ≠ 1 ⟹ (snd (Rep_OrdSum a) ≠ 1 = False)"
apply (cut_tac x = a in Rep_OrdSum)
by auto

lemma fst_not_one_snd: "fst (Rep_OrdSum a) ≠ 1 ⟹ (snd (Rep_OrdSum a) = 1)"
apply (cut_tac x = a in Rep_OrdSum)
by auto

lemma snd_not_one_fst: "snd (Rep_OrdSum a) ≠ 1 ⟹ (fst (Rep_OrdSum a) = 1)"
apply (cut_tac x = a in Rep_OrdSum)
by auto

lemma fst_not_one_simp [simp]: "fst (Rep_OrdSum c) ≠ 1 ⟹ Abs_OrdSum (fst (Rep_OrdSum c), 1) = c"
apply (rule  Rep_OrdSum_eq)
apply (rule fst_snd_eq)
apply simp_all

lemma snd_not_one_simp [simp]: "snd (Rep_OrdSum c) ≠ 1 ⟹ Abs_OrdSum (1, snd (Rep_OrdSum c)) = c"
apply (rule  Rep_OrdSum_eq)
apply (rule fst_snd_eq)
apply simp_all

lemma  A: fixes a b::"('a, 'b) OrdSum" shows "(a l→ b) * a = a * (a r→ b)"
apply (simp add: one_OrdSum_def impr_OrdSum_def impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply safe
apply (simp_all add: fst_snd_eq times_OrdSum_def left_right_impl_times first_def second_def Abs_OrdSum_inverse Rep_OrdSum_inverse )
apply safe
by simp_all

instance
proof
fix a::"('a, 'b) OrdSum" show "1 * a = a"
by (simp add: fst_snd_eq one_OrdSum_def times_OrdSum_def first_def second_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
next
fix a::"('a, 'b) OrdSum" show "a * 1 = a"
by (simp add: fst_snd_eq one_OrdSum_def times_OrdSum_def first_def second_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
next
fix a::"('a, 'b) OrdSum" show "a l→ a = 1"
next
fix a::"('a, 'b) OrdSum" show "a r→ a = 1"
next
fix a b::"('a, 'b) OrdSum" show "(a l→ b) * a = (b l→ a) * b"
apply (unfold one_OrdSum_def impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply simp
apply safe
by (simp_all add: times_OrdSum_def left_impl_times first_def second_def Abs_OrdSum_inverse Rep_OrdSum_inverse )
next
fix a b::"('a, 'b) OrdSum" show "a * (a r→ b) = b * (b r→ a)"
apply (unfold one_OrdSum_def impr_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (simp)
apply safe
by (simp_all add: fst_snd_eq times_OrdSum_def right_impl_times first_def second_def Abs_OrdSum_inverse Rep_OrdSum_inverse )
next
fix a b::"('a, 'b) OrdSum" show "(a l→ b) * a = a * (a r→ b)" by (rule A)
next
fix a b c::"('a, 'b) OrdSum" show "a * b l→ c = a l→ b l→ c"
apply (unfold times_OrdSum_def)
apply simp apply safe
apply (simp_all add: fst_snd_eq one_OrdSum_def times_OrdSum_def left_impl_ded impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
by auto
next
fix a b c::"('a, 'b) OrdSum" show "a * b r→ c = b r→ a r→ c"
apply (simp add: right_impl_ded impr_OrdSum_def second_def first_def one_OrdSum_def  times_OrdSum_def  second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
by auto
next
fix a b::"('a, 'b) OrdSum" show "(a ≤ b) = (a l→ b = 1)"
next
fix a b::"('a, 'b) OrdSum" show "(a < b) = (a ≤ b ∧ ¬ b ≤ a)"
next
fix a b::"('a, 'b) OrdSum" show "a ⊓ b = (a l→ b) * a" by (simp add: inf_OrdSum_def)
next
fix a b::"('a, 'b) OrdSum" show "a ⊓ b = a * (a r→ b)" by (simp add: inf_OrdSum_def A)

qed

definition
"Second = {x . ∃ b . x =  Abs_OrdSum(1::'a, b::'b)}"

end

lemma "Second ∈ normalfilters"
apply (unfold normalfilters_def)
apply safe
apply (unfold filters_def)
apply safe
apply (unfold Second_def)
apply auto
apply (rule_tac x = "ba * bb" in exI)
apply (simp add: times_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (rule_tac x = "second b" in exI)
apply (subgoal_tac "Abs_OrdSum (1::'a, second b) = Abs_OrdSum (first b, second b)")
apply simp
apply (simp add: first_def second_def Rep_OrdSum_inverse)
apply (subgoal_tac "first b = 1")
apply simp
apply (simp add: order_OrdSum_def one_OrdSum_def impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (unfold second_def first_def)
apply (case_tac "ba = (1::'b) ∧ snd (Rep_OrdSum b) = (1::'b)")
apply simp
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))")
apply (drule drop_assumption)
apply simp
apply simp
apply (case_tac "fst (Rep_OrdSum b) = (1::'a)")
apply simp
apply simp
apply (case_tac "snd (Rep_OrdSum b) = (1::'b)")
apply simp_all
apply (simp add: impr_OrdSum_def impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply safe
apply (unfold second_def first_def)
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (case_tac "snd (Rep_OrdSum a) = (1::'b)")
apply simp_all
apply auto
apply (case_tac "snd (Rep_OrdSum a) = (1::'b)")
apply auto
apply (rule_tac x = 1 in exI)
apply (rule Rep_OrdSum_eq)
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l→ fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))")
apply (drule drop_assumption)
apply (simp add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (simp add: left_lesseq [THEN sym] right_lesseq [THEN sym])
apply simp
apply (rule_tac x = 1 in exI)
apply (rule Rep_OrdSum_eq)
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l→ fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))")
apply (drule drop_assumption)
apply (simp add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (simp add: left_lesseq [THEN sym] right_lesseq [THEN sym])
apply simp

apply (simp add: impr_OrdSum_def impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply safe
apply (unfold second_def first_def)
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (case_tac "snd (Rep_OrdSum a) = (1::'b)")
apply simp_all
apply auto
apply (case_tac "snd (Rep_OrdSum a) = (1::'b)")
apply auto
apply (rule_tac x = 1 in exI)
apply (rule Rep_OrdSum_eq)
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r→ fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))")
apply (drule drop_assumption)
apply (simp add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (simp add: left_lesseq [THEN sym] right_lesseq [THEN sym])
apply simp
apply (rule_tac x = 1 in exI)
apply (rule Rep_OrdSum_eq)
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r→ fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))")
apply (drule drop_assumption)
apply (simp add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (simp add: left_lesseq [THEN sym] right_lesseq [THEN sym])
by simp

class linear_pseudo_hoop_algebra = pseudo_hoop_algebra + linorder

instantiation "OrdSum" :: (linear_pseudo_hoop_algebra, linear_pseudo_hoop_algebra) linear_pseudo_hoop_algebra
begin
instance
proof
fix x y::"('a, 'b) OrdSum" show "x ≤ y ∨ y ≤ x"
apply (simp add: order_OrdSum_def impl_OrdSum_def one_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
apply (cut_tac x = "fst (Rep_OrdSum x)" and y = "fst (Rep_OrdSum y)" in linear)
apply (cut_tac x = "snd (Rep_OrdSum x)" and y = "snd (Rep_OrdSum y)" in linear)
by auto [1]
qed
end

instantiation bool:: pseudo_hoop_algebra
begin
definition impl_bool_def:
"a l→ b = (a ⟶ b)"

definition impr_bool_def:
"a r→ b = (a ⟶ b)"

definition one_bool_def:
"1 = True"

definition times_bool_def:
"a * b = (a ∧ b)"

lemma inf_bool_def: "(a :: bool) ⊓ b = (a l→ b) * a"
by (auto simp add: times_bool_def impl_bool_def)

instance
apply intro_classes
apply (simp_all add: impl_bool_def impr_bool_def one_bool_def times_bool_def le_bool_def less_bool_def inf_bool_def)
by auto

end

context cancel_pseudo_hoop_algebra begin end

lemma "¬ class.cancel_pseudo_hoop_algebra (*) (⊓)  (l→) (≤) (<) (1:: bool) (r→) "
apply (unfold  class.cancel_pseudo_hoop_algebra_def)
apply (unfold  class.cancel_pseudo_hoop_algebra_axioms_def)
apply safe
apply (drule drop_assumption)
apply (drule_tac x = "False" in spec)
apply (drule drop_assumption)
apply (drule_tac x = "True" in spec)
apply (drule_tac x = "False" in spec)

context pseudo_hoop_algebra begin
lemma classorder: "class.order (≤) (<)"
proof qed
end

lemma impl_OrdSum_first: "Abs_OrdSum (x, 1) l→ Abs_OrdSum (y, 1) = Abs_OrdSum (x l→ y, 1)"
by (simp add: impl_OrdSum_def first_def second_def  Abs_OrdSum_inverse Rep_OrdSum_inverse)

lemma impl_OrdSum_second: "Abs_OrdSum (1, x) l→ Abs_OrdSum (1, y) = Abs_OrdSum (1, x l→ y)"
by (simp add: impl_OrdSum_def first_def second_def  Abs_OrdSum_inverse Rep_OrdSum_inverse)

lemma impl_OrdSum_first_second: "x ≠ 1 ⟹ Abs_OrdSum (x, 1) l→ Abs_OrdSum (1, y) = 1"
by (simp add: one_OrdSum_def impl_OrdSum_def first_def second_def  Abs_OrdSum_inverse Rep_OrdSum_inverse)

lemma Abs_OrdSum_bijective: "x ∈ OrdSum ⟹ y ∈ OrdSum ⟹ (Abs_OrdSum x = Abs_OrdSum y) = (x = y)"
apply safe
apply (subgoal_tac  "Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)")
apply (unfold Abs_OrdSum_inverse) [1]
by simp_all

context pseudo_hoop_algebra begin end

context linear_pseudo_hoop_algebra begin end
context basic_pseudo_hoop_algebra begin end

lemma "class.pseudo_hoop_algebra (*) (⊓) (l→) (≤) (<) (1::'a::pseudo_hoop_algebra) (r→)
⟹ ¬ (class.linear_pseudo_hoop_algebra (≤) (<)  (*) (⊓) (l→) (1::'a) (r→))
⟹ ¬ class.basic_pseudo_hoop_algebra (*) (⊓) (l→) (≤) (<) (1::('a, bool) OrdSum) (r→)"
apply (unfold class.linear_pseudo_hoop_algebra_def)
apply (unfold class.linorder_def)
apply (unfold class.linorder_axioms_def)
apply safe
apply (rule classorder)
apply (unfold class.basic_pseudo_hoop_algebra_def) [1]
apply simp
apply (unfold class.basic_pseudo_hoop_algebra_axioms_def) [1]
apply safe
apply (subgoal_tac "(Abs_OrdSum (x, 1) l→ Abs_OrdSum (y, 1)) l→ Abs_OrdSum (1, False) ≤
((Abs_OrdSum (y, 1) l→ Abs_OrdSum (x, 1)) l→ Abs_OrdSum (1, False)) l→ Abs_OrdSum (1, False)")
apply (unfold impl_OrdSum_first) [1]
apply (case_tac "x l→ y ≠ 1 ∧ y l→ x ≠ 1")