# Theory Examples

Up to index of Isabelle/HOL/LatticeProperties/PseudoHoops

theory Examples
imports SpecialPseudoHoops Lattice_Ordered_Group
`header{* Examples of Pseudo-Hoops *}theory Examplesimports SpecialPseudoHoops "../LatticeProperties/Lattice_Ordered_Group"begincontext lgroupbeginlemma (in lgroup) less_eq_inf_2: "(x ≤ y) = (inf y x = x)"  by (simp add: le_iff_inf inf_commute)endclass lgroup_with_const = lgroup +  fixes u::'a  assumes [simp]: "0 ≤ u"definition "G = {a::'a::lgroup_with_const. (0 ≤ a ∧ a ≤ u)}"typedef 'a G = "G::'a::lgroup_with_const set"proof  show "0 ∈ G" by (simp add: G_def)qedinstantiation "G" :: (lgroup_with_const) bounded_wajsberg_pseudo_hoop_algebrabegindefinition  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 (simp_all add: diff_minus)  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) \<sqinter> 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 (simp_all add: diff_minus)  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 (simp_all add: diff_minus)  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_alldefinition  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) \<sqinter> b = ((a l-> b) * a)"lemma [simp]: "(u::'a) ∈ G"  by (simp add: G_def)lemma [simp]: "(1::'a G) * a = a"  apply (simp add: one_def times_def)  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 (simp add: Rep_G_inverse)  apply (cut_tac x = a in Rep_G)  apply (rule antisym)  apply (simp add: G_def)  by simplemma [simp]: "a * (1::'a G) = a"  apply (simp add: one_def times_def)  apply (cut_tac y = "u::'a" in Abs_G_inverse)  apply (simp_all add: diff_minus add_assoc)  apply (subgoal_tac "sup (Rep_G a) (0::'a) = Rep_G a")  apply (simp add: Rep_G_inverse)  apply (cut_tac x = a in Rep_G)  apply (rule antisym)  by (simp_all add: G_def)lemma [simp]: "a l-> a = (1::'a G)"  by (simp add: one_def impl_def)lemma [simp]: "a r-> a = (1::'a G)"  by (simp add: one_def impr_def diff_minus add_assoc)lemma [simp]: "a ∈ G ==> Rep_G (Abs_G a) = a"  apply (rule Abs_G_inverse)  by simplemma inf_def_1: "((a::'a G) l-> b) * a = Abs_G (inf (Rep_G a) (Rep_G b))"  apply (simp add: times_def impl_def)  apply (simp add: diff_minus add_assoc)  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 (simp add: G_def)  apply (subgoal_tac "inf (Rep_G a) (Rep_G b) = inf (Rep_G b) (Rep_G a)")  apply simp  apply (rule antisym)  by simp_alllemma inf_def_2: "(a::'a G) * (a r-> b) = Abs_G (inf (Rep_G a) (Rep_G b))"  apply (simp add: times_def impr_def)  apply (simp add: diff_minus add_assoc [THEN sym])  apply (simp add: add_assoc)  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 (simp add: G_def)  apply (subgoal_tac "inf (Rep_G a) (Rep_G b) = inf (Rep_G b) (Rep_G a)")  apply simp  apply (rule antisym)  by simp_alllemma 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 (simp add: diff_minus)  apply (drule_tac a = "u" and b = " Rep_G b + - Rep_G a + u" and v = "-u" in add_order_preserving_right)  apply (simp add: add_assoc)  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 add: add_assoc)  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 (simp add: diff_minus)  apply (rule right_move_to_left)  by simplemma ded_left: "((a::'a G) * b) l-> c = a l-> b l-> c"  apply (simp add: times_def impl_def)  apply (simp add: diff_minus minus_add)  apply (simp add: add_assoc [THEN sym])  apply (simp add: inf_assoc)  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 (simp add: add_assoc)  apply (rule add_pos)  apply (cut_tac x = a in Rep_G)  apply (simp add: G_def)  apply (rule left_move_to_left)  apply simp  apply (rule antisym)  apply simp  apply simp  apply (rule add_pos_left)  apply (cut_tac x = c in Rep_G)  by (simp add: G_def)lemma ded_right: "((a::'a G) * b) r-> c = b r-> a r-> c"  apply (simp add: times_def impr_def)  apply (simp add: diff_minus minus_add)  apply (simp add: add_assoc [THEN sym])  apply (simp add: inf_assoc)  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 (simp add: add_assoc)  apply (rule add_pos)  apply (cut_tac x = b in Rep_G)  apply (simp add: G_def)  apply (rule left_move_to_left)  apply simp  apply (rule antisym)  apply simp  apply simp  apply (rule add_pos)  apply (cut_tac x = c in Rep_G)  by (simp add: G_def)lemma [simp]: "0 ∈ G"  by (simp add: G_def)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   apply (rule add_pos_left)  by simplemma lemma_W1: "((a::'a G) l-> b) r-> b = (b l-> a) r-> a"  apply (simp add: impl_def impr_def)   apply (simp add: diff_minus minus_add)  apply (simp add: add_assoc)  apply (simp add: add_assoc [THEN sym])  apply (subgoal_tac "Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a")  apply simp  apply (rule antisym)  by simp_all  (*by (simp add: sup_commute)*)lemma lemma_W2: "((a::'a G) r-> b) l-> b = (b r-> a) l-> a"  apply (simp add: impl_def impr_def)   apply (simp add: diff_minus minus_add)  apply (simp add: add_assoc)  apply (simp add: add_assoc [THEN sym])  apply (subgoal_tac "Rep_G a \<squnion> Rep_G b = Rep_G b \<squnion> Rep_G a")  apply simp  apply (rule antisym)  by simp_all  (*by (simp add: sup_commute)*)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 simpnext  fix a b have a: "((a::'a G) l-> b) * a = (b l-> a) * b"     by (simp add: inf_def_1 inf_commute)   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 simpnext  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 simpnext  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 \<sqinter> b = (a l-> b) * a" by (rule inf_def)next  fix a b::"'a G" show "a \<sqinter> b = a * (a r-> b)" by (simp add: inf_def inf_def_2 inf_def_1) qedendcontext orderbegindefinition  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}"endcontext group_addbegindefinition  "subgroup = {A . 0 ∈ A ∧ (∀ a b . a ∈ A ∧ b ∈ A --> a + b ∈ A ∧ -a ∈ A)}"lemma [simp]: "A ∈ subgroup ==> 0 ∈ A"  by (simp add: subgroup_def)lemma [simp]: "A ∈ subgroup ==> a ∈ A ==> b ∈ A ==> a + b ∈ A"  apply (subst (asm) subgroup_def)  by simplemma minus_subgroup: "A ∈ subgroup ==> -a ∈ A ==> a ∈ A"  apply (subst (asm) subgroup_def)  apply safe  apply (drule_tac x="-a" in spec)   by simpdefinition  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)}"endcontext lgroupbegindefinition  "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"  by (simp add: lsubgroup_def)lemma sup_lsubgroup:  "A ∈ lsubgroup ==> a ∈ A ==> b ∈ A ==> sup a b ∈ A"  by (simp add: lsubgroup_def)enddefinition  "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 (simp add: normal_def F_def)  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 (simp add: add_set_def)  apply safe  apply (subgoal_tac "- Rep_G x + u = - Rep_G x + Rep_G x + b")  apply simp  apply (subst add_assoc)  apply simp  apply (subst add_set_def)  apply simp  apply (rule_tac x = "u - Rep_G x" in bexI)  apply (simp add: diff_minus add_assoc)  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 (simp add: add_set_def)  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 (subst add_assoc [THEN sym])  apply simp  apply simp  apply (subst add_set_def)  apply simp  apply (rule_tac x = "- Rep_G x + u" in bexI)  apply (simp add: add_assoc [THEN sym])  by simpcontext lgroup beginlemma sup_assoc_lgroup: "a \<squnion> b \<squnion> c = a \<squnion> (b \<squnion> c)"  by (rule sup_assoc)endlemma 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 (subst (asm) add_set_def)  apply simp  apply safe  apply (simp add: times_set_def)  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 (simp add: times_def)  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 (simp add: diff_minus add_assoc)  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 add: G_def)  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 (simp add: G_def)  apply (rule left_move_to_right)  apply simp  apply (rule right_move_to_left)  apply simp  apply (simp add: G_def)  apply (simp add: diff_minus)  apply (simp add: add_assoc)  apply (simp add: F_def)  apply (subgoal_tac "inf (sup (aa + u) (0::'a)) u ∈ G")  apply simp  apply (simp add: diff_minus minus_add add_assoc [THEN sym])  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 (simp add: G_def)  apply (subst (asm) normal_def)  apply simp  apply (drule drop_assumption)  apply (simp add: add_set_def)  apply (rule_tac x = "-u + Rep_G y" in bexI)  apply (simp add: diff_minus add_assoc)  apply simp  apply (rule minus_subgroup)  apply (simp add: lsubgroup_def)  by (simp add: minus_add)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 (subgoal_tac "Rep_G x - u ∈ K")  apply (subgoal_tac "Rep_G x - u + Rep_G a ∈ {Rep_G a} +++ K")  apply (subst (asm) add_set_def)  apply simp  apply safe  apply (simp add: times_set_def)  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 (simp add: times_def)  apply (simp add: diff_minus add_assoc)  apply (simp add: add_assoc [THEN sym])  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 add: G_def)  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 (simp add: G_def)  apply (rule right_move_to_right)  apply simp  apply (rule left_move_to_left)  apply simp  apply (simp add: G_def)  apply (simp add: diff_minus)  apply (simp add: add_assoc)  apply (simp add: add_assoc [THEN sym])  apply (simp add: F_def2)  apply (subgoal_tac "inf (sup (u + b) (0::'a)) u ∈ G")  apply simp  apply (simp add: diff_minus minus_add add_assoc [THEN sym])  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 (simp add: add_assoc)  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 (simp add: G_def)  apply (subgoal_tac  "{Rep_G a} +++ K = K +++ {Rep_G a}")  apply simp  apply (simp add: add_set_def)  apply (subst (asm) normal_def)  apply simp  apply (rule minus_subgroup)  apply (simp add: lsubgroup_def)  by (simp add: diff_minus minus_add)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 (simp add: F_def)  apply (simp add: convex_def)  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 (simp add: closed_interval_def)  apply safe  apply (cut_tac x = "a * b" in Rep_G)  apply (simp add: G_def diff_minus)  apply (rule right_move_to_left)  apply simp  apply (simp add: times_def)  apply (subgoal_tac "(u - (Rep_G a - u + Rep_G b)) = u - Rep_G b + (u - Rep_G a)")  apply simp  apply (simp add: diff_minus add_assoc minus_add)  apply (subst (asm) Rep_G_order)  apply (simp add: F_def)  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 (simp add: G_def)  apply (safe)  apply (simp add: diff_minus)  apply (rule right_move_to_left)  apply simp  apply (simp add: diff_minus)  apply (rule add_order_preserving_left)  apply (rule minus_order)  apply simp  apply (simp add: lsubgroup_def)  apply (rule normal_1)   apply simp_all  apply (rule normal_2)   by simp_all    definition "N = {a::'a::lgroup. a ≤ 0}"typedef ('a::lgroup) N = "N :: 'a::lgroup set"proof  show "0 ∈ N" by (simp add: N_def)qedclass cancel_product_pseudo_hoop_algebra = cancel_pseudo_hoop_algebra + product_pseudo_hoop_algebracontext group_addbeginsubclass cancel_semigroup_addproof qed(*  fix a b c :: 'a  assume "a + b = a + c"  then have "- a + a + b = - a + a + c"    unfolding add_assoc by simp  then show "b = c" by simpnext  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 simpqed*)end  instantiation "N" :: (lgroup) pseudo_hoop_algebrabegindefinition  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 (simp add: N_def)  apply (rule_tac left_move_to_right)  apply (rule_tac y = 0 in order_trans)  apply simp_all  apply (rule_tac minus_order)  by simpdefinition  impl_N_def: "a l-> b ≡ Abs_N (inf (Rep_N b - Rep_N a) 0)"definition   inf_N_def: "(a:: 'a N) \<sqinter> 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)  by (simp add: N_def)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)  by (simp add: N_def)definition  one_N_def: "1 ≡ Abs_N 0"lemma [simp]: "0 ∈ N"  by (simp add: N_def)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 (simp add: impl_N_def one_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 (simp add: Abs_N_inverse)  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 (simp add: diff_minus add_assoc)  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 (simp add: diff_minus)  apply (rule right_move_to_left)  apply simp  apply simp  by (simp add: Abs_N_inverse)lemma order_Abs_N:  "a ∈ N ==> b ∈ N ==> (a ≤ b) = (Abs_N a ≤ Abs_N b)"  apply (subst order_N_def)  apply (simp add: impl_N_def one_N_def)  apply (simp add: Abs_N_inverse)  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 (simp add: Abs_N_inverse)  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 (simp add: diff_minus)  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 (simp add: diff_minus add_assoc)  apply (rule_tac y = "inf (b - a) (0::'a)" in order_trans)  apply simp  apply (drule drop_assumption)  apply simp  apply (simp add: Abs_N_inverse)  by (simp add: N_def)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)  apply simp_all  by (simp_all add: diff_minus add_assoc) lemma impr_times: "a * (a r-> b) = (b::'a N) * (b r-> a)"  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 a + Rep_N b)) (Rep_N a) = inf (Rep_N b + (- Rep_N b + Rep_N a)) (Rep_N b)")  apply simp  apply (simp add: add_assoc [THEN sym])  apply (rule antisym)  by simp_alllemma impr_impl_times: "(a l-> b) * a = (a::'a N) * (a r-> b)"  apply (simp add: impr_N_def 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 a + Rep_N b)) (Rep_N a)")  apply simp  apply (simp add: add_assoc diff_minus)  by (simp add: add_assoc [THEN sym])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 (simp add: diff_minus minus_add add_assoc)  apply (rule_tac y = "0" in order_trans)  apply simp  apply (cut_tac x = a in "Rep_N")  apply (simp add: N_def)  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  by (simp add: diff_minus minus_add add_assoc)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 (simp add: diff_minus minus_add add_assoc)  apply (rule_tac y = "0" in order_trans)  apply simp  apply (cut_tac x = b in "Rep_N")  apply (simp add: N_def)  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  by (simp add: diff_minus minus_add add_assoc)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 simpnext  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 \<sqinter> b = (a l-> b) * a" by (simp add: inf_N_def)next  fix a b::"'a N" show "a \<sqinter> b = a * (a r-> b)" by (simp add: inf_N_def impr_impl_times)qedendlemma Rep_N_inf: "Rep_N ((a::'a::lgroup N) \<sqinter> b) = (Rep_N a) \<sqinter> (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 \<sqinter> b" in Rep_N)  apply (simp add: N_def)  apply (simp add: Rep_N_inverse)  apply safe  apply (subst order_Rep_N)  apply (simp add: Abs_N_inverse)  apply (subst order_Rep_N)  apply (simp add: Abs_N_inverse)  apply (simp add: N_def)  apply (rule_tac y = "Rep_N a" in order_trans)  apply simp  apply (cut_tac x = a in Rep_N)   by (simp add: N_def)context lgroup beginlemma sup_inf_distrib2_lgroup: "(b \<sqinter> c) \<squnion> a = (b \<squnion> a) \<sqinter> (c \<squnion> a)"  by (rule sup_inf_distrib2)lemma inf_sup_distrib2_lgroup: "(b \<squnion> c) \<sqinter> a = (b \<sqinter> a) \<squnion> (c \<sqinter> a)"  by (rule inf_sup_distrib2)endinstantiation "N" :: (lgroup) cancel_product_pseudo_hoop_algebrabeginlemma 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 (simp add: Abs_N_inverse)  apply (subgoal_tac "Abs_N (Rep_N b) = Abs_N (Rep_N c)")  apply (drule drop_assumption)  apply (simp add: Rep_N_inverse)  by simp_alllemma 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 (simp add: Abs_N_inverse)  apply (subgoal_tac "Abs_N (Rep_N b) = Abs_N (Rep_N c)")  apply (drule drop_assumption)  apply (simp add: Rep_N_inverse)  by simp_alllemma 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 (simp add: diff_minus minus_add)  (*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 add_order_preserving_left)  apply (simp add: add_assoc)  apply (rule add_order_preserving_left)  apply (rule left_move_to_left)  apply simp  apply (cut_tac x = c in Rep_N)  apply (simp add: N_def)  apply (rule minus_order)  by simplemma 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_add)  apply (subst minus_minus)  apply (subst minus_zero)  apply (rule left_move_to_right)  apply (subst minus_minus)  apply simp  apply (simp add: minus_add)  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 add_order_preserving_right)  apply (simp add: add_assoc [THEN sym])  apply (rule add_order_preserving_right)  apply (rule left_move_to_left)  apply (rule right_move_to_right)  apply simp  apply (cut_tac x = c in Rep_N)  by (simp add: N_def)  lemma prod_3: "(b::'a N) l-> b * b ≤ a \<sqinter> (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 (simp add: add_assoc N_def)  apply (subst Abs_N_inverse)  apply (simp add: add_assoc N_def)  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 (simp add: add_assoc)  apply (rule_tac y = "Rep_N b" in order_trans)  by simp_alllemma prod_4: "(b::'a N) r-> b * b ≤ a \<sqinter> (a r-> b) r-> b"  apply (simp add: impr_N_def times_N_def Abs_N_inverse Rep_N_inverse Rep_N_inf minus_add)  apply (subst order_Abs_N [THEN sym])  apply (simp add:  N_def)  apply (simp add:  N_def)  apply simp  apply (simp add: add_assoc [THEN sym])  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)  by (simp add: N_def)lemma prod_5: "(((a::'a N) l-> b) l-> b) * (c * a l-> f * a) * (c * b l-> f * b) ≤ c l-> f"  apply (simp add: impl_N_def times_N_def Abs_N_inverse Rep_N_inverse Rep_N_inf minus_add)  apply (subst Abs_N_inverse)  apply (simp add: N_def)  apply (subst Abs_N_inverse)  apply (simp add: N_def)  apply (subst Abs_N_inverse)  apply (simp add: N_def)  apply (subst order_Abs_N [THEN sym])  apply (simp add: N_def inf_assoc [THEN sym])  apply (simp add: N_def)  apply (simp only: diff_minus minus_add minus_minus add_assoc)  apply (subst (4) add_assoc [THEN sym])  apply (subst (5) add_assoc [THEN sym])  apply (simp only: right_minus add_0_left)  apply (rule right_move_to_right)  apply (simp only: minus_add add_assoc [THEN sym] add_0_left right_minus)  by (simp add: minus_add)lemma prod_6: "(((a::'a N) r-> b) r-> b) * (a * c r-> a * f) * (b * c r-> b * f) ≤ c r-> f"  apply (simp add: impr_N_def times_N_def Abs_N_inverse Rep_N_inverse Rep_N_inf minus_add)  apply (subst Abs_N_inverse)  apply (simp add: N_def)  apply (subst Abs_N_inverse)  apply (simp add: N_def)  apply (subst Abs_N_inverse)  apply (simp add: N_def)  apply (subst order_Abs_N [THEN sym])  apply (simp add: N_def inf_assoc [THEN sym])  apply (simp add: N_def)  apply (simp only: diff_minus minus_add minus_minus add_assoc)  apply (subst (4) add_assoc [THEN sym])  apply (subst (5) add_assoc [THEN sym])  apply (simp only: left_minus add_0_left)  apply (rule right_move_to_right)  apply (simp only: minus_add add_assoc [THEN sym] add_0_left right_minus)  by (simp add: minus_add)instanceapply intro_classesby (fact cancel_times_left cancel_times_right prod_1 prod_2 prod_3 prod_4 prod_5 prod_6)+enddefinition "OrdSum =  {x. (∃a::'a::pseudo_hoop_algebra. x = (a, 1::'b::pseudo_hoop_algebra)) ∨ (∃b::'b. x = (1::'a, b))}"typedef ('a, 'b) OrdSum = "OrdSum :: ('a::pseudo_hoop_algebra × 'b::pseudo_hoop_algebra) set"proof  show "(1, 1) ∈ OrdSum" by (simp add: OrdSum_def)qedlemma [simp]: "(1, b) ∈ OrdSum"  by (simp add: OrdSum_def)lemma [simp]: "(a, 1) ∈ OrdSum"  by (simp add: OrdSum_def)definition  "first x = fst (Rep_OrdSum x)"definition  "second x = snd (Rep_OrdSum x)" instantiation "OrdSum" :: (pseudo_hoop_algebra, pseudo_hoop_algebra) pseudo_hoop_algebrabegindefinition  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) \<sqinter> 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"  by (simp add: OrdSum_def)lemma OrdSum_second [simp]: "(1, b) ∈ OrdSum"  by (simp add: OrdSum_def)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)  apply (simp add: Rep_OrdSum_inverse)  by simplemma 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_alllemma if_unfold_left: "((if a then b else c) = d) = ((a--> b = d) ∧ (¬ a --> c = d))"  apply auto  donelemma if_unfold_right: "(d = (if a then b else c)) = ((a --> d = b) ∧ (¬ a --> d = c))"  apply auto  donelemma 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_alllemma [simp]: "fst (Rep_OrdSum a) ≠ 1 ==> (snd (Rep_OrdSum a) ≠ 1 = False)"  apply (cut_tac x = a in Rep_OrdSum)  apply (simp add: OrdSum_def)  by autolemma fst_not_one_snd: "fst (Rep_OrdSum a) ≠ 1 ==> (snd (Rep_OrdSum a) = 1)"  apply (cut_tac x = a in Rep_OrdSum)  apply (simp add: OrdSum_def)  by autolemma snd_not_one_fst: "snd (Rep_OrdSum a) ≠ 1 ==> (fst (Rep_OrdSum a) = 1)"  apply (cut_tac x = a in Rep_OrdSum)  apply (simp add: OrdSum_def)  by autolemma fst_not_one_simp [simp]: "fst (Rep_OrdSum c) ≠ 1 ==> Abs_OrdSum (fst (Rep_OrdSum c), 1) = c"  apply (rule  Rep_OrdSum_eq)  apply (simp add: Abs_OrdSum_inverse)  apply (rule fst_snd_eq)  apply simp_all  by (simp add: fst_not_one_snd)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 (simp add: Abs_OrdSum_inverse)  apply (rule fst_snd_eq)  apply simp_all  by (simp add: snd_not_one_fst)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_allinstanceprooffix 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)nextfix 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)nextfix a::"('a, 'b) OrdSum" show "a l-> a = 1"   by (simp add: one_OrdSum_def impl_OrdSum_def)nextfix a::"('a, 'b) OrdSum" show "a r-> a = 1"   by (simp add: one_OrdSum_def impr_OrdSum_def)nextfix 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 )nextfix 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 )nextfix a b::"('a, 'b) OrdSum" show "(a l-> b) * a = a * (a r-> b)" by (rule A)nextfix 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: impl_OrdSum_def)  apply (simp_all add: first_def second_def)  apply (simp_all add: Abs_OrdSum_inverse Rep_OrdSum_inverse)  apply (simp_all add: fst_snd_eq)  apply (simp_all add: Abs_OrdSum_inverse Rep_OrdSum_inverse)  apply (simp_all add: left_impl_ded)  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 autonextfix 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 autonext  fix a b::"('a, 'b) OrdSum" show "(a ≤ b) = (a l-> b = 1)"    by (simp add:  order_OrdSum_def)next  fix a b::"('a, 'b) OrdSum" show "(a < b) = (a ≤ b ∧ ¬ b ≤ a)"    by (simp add:  strict_order_OrdSum_def)next  fix a b::"('a, 'b) OrdSum" show "a \<sqinter> b = (a l-> b) * a" by (simp add: inf_OrdSum_def)next  fix a b::"('a, 'b) OrdSum" show "a \<sqinter> b = a * (a r-> b)" by (simp add: inf_OrdSum_def A)  qeddefinition   "Second = {x . ∃ b . x =  Abs_OrdSum(1::'a, b::'b)}"endlemma "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 (simp add: Abs_OrdSum_inverse Rep_OrdSum_inverse)  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 add: Abs_OrdSum_inverse Rep_OrdSum_inverse)  apply simp  apply simp  apply (simp add: Abs_OrdSum_inverse Rep_OrdSum_inverse)  apply (case_tac "fst (Rep_OrdSum b) = (1::'a)")  apply simp  apply simp  apply (simp add: Abs_OrdSum_inverse Rep_OrdSum_inverse)  apply (case_tac "snd (Rep_OrdSum b) = (1::'b)")  apply simp_all  apply (simp add: Abs_OrdSum_inverse Rep_OrdSum_inverse)  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 simpclass linear_pseudo_hoop_algebra = pseudo_hoop_algebra + linorderinstantiation "OrdSum" :: (linear_pseudo_hoop_algebra, linear_pseudo_hoop_algebra) linear_pseudo_hoop_algebrabegininstanceproof  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)    apply (simp add: left_lesseq)    by auto [1]qedendinstantiation bool:: pseudo_hoop_algebrabegindefinition 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) \<sqinter> 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 autoendcontext cancel_pseudo_hoop_algebra begin endlemma "¬ class.cancel_pseudo_hoop_algebra op * op \<sqinter>  op l-> op ≤ op < (1:: bool) op 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)  by (simp add: times_bool_def)context pseudo_hoop_algebra beginlemma classorder: "class.order op ≤ op <"  proof qedendlemma 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_allcontext pseudo_hoop_algebra begin endcontext linear_pseudo_hoop_algebra begin endcontext basic_pseudo_hoop_algebra begin endlemma "class.pseudo_hoop_algebra op * op \<sqinter> op l-> op ≤ op < (1::'a::pseudo_hoop_algebra) op r->          ==> ¬ (class.linear_pseudo_hoop_algebra op ≤ op <  op * op \<sqinter> op l-> (1::'a) op r->)          ==> ¬ class.basic_pseudo_hoop_algebra op * op \<sqinter> op l-> op ≤ op < (1::('a, bool) OrdSum) op 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")  apply (simp add: impl_OrdSum_first_second)  apply (unfold order_OrdSum_def one_OrdSum_def one_bool_def impl_OrdSum_second impl_bool_def ) [1]  apply simp  apply (cut_tac x = "(1::'a, False)" and y = "(1::'a, True)" in  Abs_OrdSum_eq)  apply simp_all  apply (unfold left_lesseq)  by simpend`