Session PseudoHoops

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])
    by (simp add: inf_commute)

  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)

    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)
    by (simp_all add: left_residual)
  
  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)
    by (simp_all add: C B)

  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 (simp add: left_impl_times)
    apply (simp add: left_impl_ded)
    apply (case_tac "c  1")
    apply (simp add: left_lesseq)
    by (simp add: D)


  lemma F: "(a * b) * c l→ z = a * (b * c) l→ z"
    by (simp add: left_impl_ded)

  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)
    apply (simp add: F)
    by (simp add: F [THEN sym])

  lemma H: "a * b  b"
    apply (simp add: less_eq)
    by auto

  lemma I: "a * b l→ b = 1"
    apply (case_tac "a * b  b")
    apply (simp add: left_lesseq)
    by (simp add: H)

  lemma K: "a  b  a * c  b * c"
    apply (unfold less_eq)
    apply clarify
    apply (rule_tac x = "ca" in exI)
    by (simp add: associativity) 

  lemma L: "(x * a  b) = (x  a l→ b)"
    by (simp add: left_lesseq left_impl_ded)

  subclass left_complemented_monoid 
    apply unfold_locales 
    apply (simp_all add:  less_def D associativity K)
    apply (simp add: L)
    by (simp add: less_eq)
  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)
  apply (simp add: right_residual)
  by (simp add: left_divisibility)

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
  apply (simp add: dual_algebra.mult.assoc)
  apply (simp add: dual_algebra.mult_right_mono)
  apply (simp add: dual_algebra.left_residual)
  by (simp add: dual_algebra.right_divisibility)
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 (simp add: less_r_def);
  apply (simp add: inf_rr_def);
  apply (rule right_impl_times, rule right_impl_ded);
  by (simp add: lesseq_r_def);
*)

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 (simp add: less_r_def)
  apply (simp add: inf_rr_def)
  apply (rule right_impl_times, rule right_impl_ded)
  by (simp add: lesseq_r_def)

  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 add: inf_l_def)
  apply simp
  apply (simp add: left_impl_times)
  apply (simp add: left_impl_ded)
  by (simp add: left_right_impl_times)

context pseudo_hoop_algebra begin
lemma commutative_ps: "( a b . a * b = b * a) = ((l→) = (r→))"
  apply (simp add: fun_eq_iff)
  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 add: left_residual)
  apply simp
  apply (simp add: left_residual [THEN sym])
  apply (simp add: right_residual)
  apply (rule order.antisym)
  apply (simp add: left_residual)
  apply (simp add: right_residual [THEN sym])
  apply (simp add: left_residual)
  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)
  by (simp_all add: left_residual)

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)
  by (simp_all add: left_impl_ded)

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)
  apply (simp add: mult_left_mono)
  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)
  apply (simp add: mult_left_mono)
  by (simp add: left_residual)

lemma lemma_2_5_14: "(b l→ c) * (a l→ b)  a l→ c"
  apply (simp add: left_residual [THEN sym])
  apply (simp add: mult.assoc)
  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)
  by (simp_all add: infimum_def)

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 (simp add: infimum_def lower_bound_def)
  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}")
  apply (simp_all add: infimum_pair)
  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)
  by (simp_all add: mult_right_mono mult_left_mono)

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 (simp_all add: lemma_2_5_13_a)
  apply (rule_tac y = "(a  c l→ b)  (a  c l→ d)" in order_trans)
  apply (rule lemma_2_5_11)
  by (simp add: lemma_2_6_20_a)

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)
  by (simp add: inf_commute)

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 (simp add: supremum_def upper_bound_def)
  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])
  by (simp add: right_residual)

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 (simp add: times_set_def)
  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}"
  apply (simp add: infimum_def lower_bound_def)
  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 (simp add: left_impl_ded)
  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 (simp add: infimum_def lower_bound_def)
  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 (simp add: left_impl_ded)
  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 add: times_set_def)
  apply simp
  apply (subst times_set_assoc)
  by simp

lemma power_set_add:
  "A *^ (n + m) = (A *^ n) ** (A *^ m)"
  apply (induct_tac m)
  apply simp
  apply (simp add: times_set_def)
  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 (simp add: right_impl_ded)
  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 (simp add: infimum_def lower_bound_def)
  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 (simp add: right_impl_ded)
  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 (simp add: supremum_def upper_bound_def)
  apply safe
  apply (simp add: mult_left_mono)
  by (simp add: right_residual)
 
lemma lemma_2_9_i1:
  "b  supremum A  b * a  supremum ((λ x . x * a) ` A)"
  apply (simp add: supremum_def upper_bound_def)
  apply safe
  apply (simp add: mult_right_mono)
  by (simp add: left_residual)


lemma lemma_2_9_ii:
  "b  supremum A  a  b  supremum ((⊓) a ` A)"
  apply (subst supremum_def)
  apply safe
  apply (simp add: supremum_def upper_bound_def)
  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 (simp add: right_residual)
  apply (simp add: supremum_def upper_bound_def)
  apply (simp add: right_residual)
  apply safe
  apply (subgoal_tac "(xa  A. b r→ a  xa r→ x)")
  apply simp
  apply safe
  apply (simp add: inf_l_def)
  apply (simp add: left_right_impl_times)
  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 "(xaA. 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 (simp_all add: lemma_2_10_26)
  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))"
      by (simp add: lemma_2_10_30)
    also have " = ((((b l→ a) r→ a) l→ b) * ((b l→ a) r→ a) l→ a)"
      by (simp add: left_impl_ded)
    also have " = (((b l→ a) r→ a)  b) l→ a"
      by (simp add: inf_l_def)
    also have " = b l→ a" apply (subgoal_tac "((b l→ a) r→ a)  b = b", simp, rule order.antisym) 
      by (simp_all add: lemma_2_10_24)
    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)"
    by (simp add: le_sup_equiv)

  lemma sup_idemp [simp]: 
    "a  a = a"
    by (simp add: le_sup_equiv_r)
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 (simp add: sup_def)
  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 (simp add: left_lesseq)
  apply (rule order.antisym)
  apply (simp add: sup_def)
  apply (simp add: sup_def)
  apply (simp_all add: lemma_2_10_24)
  apply (simp add:  le_iff_inf)
  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)
  by (simp add: sup_comute1)
  
subclass pseudo_hoop_sup_algebra
  apply unfold_locales
  apply (simp add: sup_comute1)
  apply simp
  by (simp add: le_sup_equiv1)
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
  by (simp add: sup_2_def)

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 add: sup_comute_2)
  apply simp
  by (simp add: le_sup_equiv2)

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 (simp add:  le_sup_equiv)
    apply (rule sup_inf_le_distr)
    by (simp add: le_iff_inf)
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 (simp add: supremum_def upper_bound_def)
  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 (simp add: supremum_pair)
  apply (erule notE)
  apply (rule lemma_2_9_ii)
  by (simp add: supremum_pair)

class bounded_semilattice_inf_top = semilattice_inf + order_top
begin
lemma inf_eq_top_iff [simp]:
  "(inf x y = top) = (x = top  y = top)"
  by (simp add: order.eq_iff)
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 
  by (simp add: sup1_def)



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 
  by (simp add: sup2_def)

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 (simp add: inf_l_def)
    apply (subst left_impl_times)
    apply (rule mult_right_mono)
    apply (subst right_lesseq)
    apply (subgoal_tac "a ⊔1 b = 1")
    apply (simp add: sup1_def)
    apply (rule order.antisym)
    apply simp
    by (simp add: supremum_def upper_bound_def)

    
  lemma lemma_2_15_ii:
    "1  supremum {a, b}  a  c  b  d  1  supremum {c, d}"
    apply (simp add: supremum_def upper_bound_def)
    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 (simp_all add: supremum_def upper_bound_def)
  apply safe
  apply auto
  apply (subgoal_tac "(x  A  B. x  xa)")
  by auto

lemma sup_singleton [simp]: "a  supremum {a}"
  by (simp add: supremum_def upper_bound_def)
 

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})"
  apply (simp add: supremum_def upper_bound_def)
  by auto

lemma sup_sup_union: "a  supremum A  b  supremum (B  {a})  b  supremum (A  B)"
  apply (simp add: supremum_def upper_bound_def)
  by auto
  
end

(*
context monoid_mult
begin
lemma "a ^ 2 = a * a"
  by (simp add: power2_eq_square)
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(simp add: power2_eq_square)
    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 (simp add: supremum_def upper_bound_def)
    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"
  by (simp add: filters_def)

lemma filter_ii: "F  filters  a  F  a  b  b  F"
 by (simp add: filters_def)

lemma filter_iii [simp]: "F  filters  1  F"
  by (auto simp add: filters_def)

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 (simp add: filters_def)
  apply safe
  apply (simp add: Inter_eq)
  apply (drule_tac x = "1" in spec)
  apply safe
  apply (erule notE)
  apply (subgoal_tac "x  filters")
  apply simp
  apply (simp add: filters_def)
  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"
  by (auto simp add: filterof_def)

lemma times_le_mono [simp]: "x  y  u  v  x * u  y * v"
  apply (rule_tac y = "x * v" in order_trans)
  by (simp_all add: mult_left_mono mult_right_mono)

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 (simp add: filterof_def)
  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 (simp add: times_set_def)
  apply (drule drop_assumption)
  apply (simp add: filters_def)
  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 (simp add: power_set_add times_set_def)
  apply blast
  apply simp
  apply (rule_tac x = "n" in exI)
  apply (rule_tac x = "x" in exI)
  apply simp
  apply (simp add: filterof_def)
  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 (simp add: power_set_0)
  apply (simp add: power_set_Suc times_set_def)
  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"
  apply (simp add: filterof_def)
  by blast

lemma filterof_elem [simp]: "x  X  x   filterof X"
  apply (simp add: filterof_def)
  by blast

lemma [simp]: "filterof X  filters"
  apply (simp add: filters_def  prop_3_2_i)
  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 (unfold power_set_add)
  apply (simp add: times_set_def)
  apply auto [1]
  apply (rule_tac y = "x * b" in order_trans)
  apply (rule mult_left_mono)
  apply simp
  apply (simp add: mult_right_mono)
  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]
  by (simp add: times_set_def)

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 (simp add: times_set_def)
  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 (simp add: supremum_def upper_bound_def)
  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 (simp add: supremum_def upper_bound_def)
  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 (simp add: right_lesseq)
  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)"
  apply (simp add: d3_def lemma_3_5_i_1)
  by auto

lemma lemma_3_5_i_4: "(d4 a b = 1) = (a = b)"
  apply (simp add: d4_def lemma_3_5_i_2)
  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"
  by (simp add: d1_def)

lemma lemma_3_5_iii_2 [simp]: "d2 a 1 = a"
  by (simp add: d2_def)

lemma lemma_3_5_iii_3 [simp]: "d3 a 1 = a"
  by (simp add: d3_def d1_def)

lemma lemma_3_5_iii_4 [simp]: "d4 a 1 = a"
  by (simp add: d4_def d2_def)

lemma lemma_3_5_iv_1: "(d1 b c) * (d1 a b) * (d1 b c)  d1 a c"
  apply (simp add: d1_def)
  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 (simp add: lemma_2_5_14)
  apply (rule_tac y = "(b l→ a) * (c l→ b)" in order_trans)
  apply (rule mult_right_mono)
  apply simp
  apply (simp add: lemma_2_5_14)
  by (simp add: mult.assoc)

lemma lemma_3_5_iv_2: "(d2 a b) * (d2 b c) * (d2 a b)  d2 a c"
  apply (simp add: d2_def)
  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 (simp add: lemma_2_5_15)
  apply (rule_tac y = "(c r→ b) * (b r→ a)" in order_trans)
  apply (rule mult_right_mono)
  apply simp
  apply (simp add: lemma_2_5_15)
  by (simp add: mult.assoc)



lemma lemma_3_5_iv_3: "(d3 a b) * (d3 b c) * (d3 a b)  d3 a c"
  by (simp add: d3_def lemma_3_5_iv_1)

lemma lemma_3_5_iv_4: "(d4 b c) * (d4 a b) * (d4 b c)  d4 a c"
  by (simp add: d4_def lemma_3_5_iv_2)

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 (simp add: cong_r_def d1_def)
  apply safe
  apply (rule filter_ii)
  apply simp_all
  apply simp
  apply (rule filter_ii)
  apply simp_all
  apply simp
  by (simp add: filter_i)

lemma cong_r_symmetric: "F  filters  (cong_r F a b) = (cong_r F b a)"
  apply (simp add: cong_r_filter)
  by blast

lemma cong_r_d3: "F  filters  (cong_r F a b) = (d3 a b  F)"
  apply (simp add: d3_def)
  apply (subst cong_r_symmetric)
  by (simp_all add: cong_r_def)


lemma cong_l_filter: "F  filters  (cong_l F a b) = (a r→ b  F  b r→ a  F)"
  apply (simp add: cong_l_def d2_def)
  apply safe
  apply (rule filter_ii)
  apply simp_all
  apply simp
  apply (rule filter_ii)
  apply simp_all
  apply simp
  by (simp add: filter_i)

lemma cong_l_symmetric: "F  filters  (cong_l F a b) = (cong_l F b a)"
  apply (simp add: cong_l_filter)
  by blast

lemma cong_l_d4: "F  filters  (cong_l F a b) = (d4 a b  F)"
  apply (simp add: d4_def)
  apply (subst cong_l_symmetric)
  by (simp_all add: cong_l_def)

lemma cong_r_reflexive: "F  filters  cong_r F a a"
  by (simp add: cong_r_def)

lemma cong_r_transitive: "F  filters  cong_r F a b  cong_r F b c  cong_r F a c"
  apply (simp add: cong_r_filter)
  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 (simp add: lemma_2_5_14)
  apply (rule_tac a = "(b l→ a) * (c l→ b)" in filter_ii)
  apply simp_all
  apply (rule filter_i)
  apply simp_all
  by (simp add: lemma_2_5_14)



lemma cong_l_reflexive: "F  filters  cong_l F a a"
  by (simp add: cong_l_def)

lemma cong_l_transitive: "F  filters  cong_l F a b  cong_l F b c  cong_l F a c"
  apply (simp add: cong_l_filter)
  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 (simp add: lemma_2_5_15)
  apply (rule_tac a = "(c r→ b) * (b r→ a)" in filter_ii)
  apply simp_all
  apply (rule filter_i)
  apply simp_all
  by (simp add: lemma_2_5_15)

lemma lemma_3_7_i: "F  filters  F = {a . cong_r F a 1}"
  by (simp add: cong_r_def)

lemma lemma_3_7_ii: "F  filters  F = {a . cong_l F a 1}"
  by (simp add: cong_l_def)

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 (simp add: left_impl_times)
  apply (subgoal_tac "x  a l→ b")
  apply (simp add: filter_ii)
  apply (simp add: left_residual [THEN sym])
  apply (subgoal_tac "y  b l→ a")
  apply (simp add: filter_ii)
  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 (simp add: right_impl_times)
  apply (subgoal_tac "x  a r→ b")
  apply (simp add: filter_ii)
  apply (simp add: right_residual [THEN sym])
  apply (subgoal_tac "y  b r→ a")
  apply (simp add: filter_ii)
  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 (simp add: cong_r_filter)
  apply safe
  apply (rule_tac a = "(a l→ d) * (b l→ a)" in filter_ii)
  apply (simp_all add: lemma_2_5_14)
  apply (rule_tac a = "((c l→ d) * (a l→ c)) * (b l→ a)" in filter_ii)
  apply simp_all
  apply (simp add: filter_i)
  apply (rule mult_right_mono)
  apply (simp_all add: lemma_2_5_14)

  apply (rule_tac a = "(b l→ c) * (a l→ b)" in filter_ii)
  apply (simp_all add: lemma_2_5_14)
  apply (rule_tac a = "((d l→ c) * (b l→ d)) * (a l→ b)" in filter_ii)
  apply simp_all
  apply (simp add: filter_i)
  apply (rule mult_right_mono)
  by (simp_all add: lemma_2_5_14)

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 (simp add: cong_l_filter)
  apply safe
  apply (rule_tac a = "(b r→ a) * (a r→ d)" in filter_ii)
  apply (simp_all add: lemma_2_5_15)
  apply (rule_tac a = "(b r→ a) * ((a r→ c) * (c r→ d))" in filter_ii)
  apply simp_all
  apply (simp add: filter_i)
  apply (rule mult_left_mono)
  apply (simp_all add: lemma_2_5_15)

  apply (rule_tac a = "(a r→ b) * (b r→ c)" in filter_ii)
  apply (simp_all add: lemma_2_5_15)
  apply (rule_tac a = "(a r→ b) * ((b r→ d) * (d r→ c))" in filter_ii)
  apply simp_all
  apply (simp add: filter_i)
  apply (rule mult_left_mono)
  by (simp_all add: lemma_2_5_15)

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"
  by (simp add: normalfilters_def)


lemma normalfilter_ii:
  "H  normalfilters  a r→ b  H  a l→ b  H"
  by (simp add: normalfilters_def)

lemma [simp]: "H  normalfilters  H  filters" 
  by (simp add: normalfilters_def)

lemma lemma_3_10_i_ii:
  "H  normalfilters  {a} ** H = H ** {a}"
  apply (simp add: times_set_def)
  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 (simp add: times_set_def)
  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 (simp add: times_set_def)
  apply auto[1]
  apply (drule_tac x = x in spec)
  apply simp
  apply (simp add: times_set_def)
  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 (simp add: times_set_def)
  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 (simp add: times_set_def)
  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"
  by (simp add: lemma_3_10_i_ii lemma_3_10_ii_iii)

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

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)"
  by (simp add: d2_def lemma_2_6_21_a)

lemma lemma_3_10_iii_i:
  "H  filters  cong_r H = cong_l H  H  normalfilters"
  apply (unfold normalfilters_def)
  apply (simp add: impl_l_d1 impl_r_d2)
  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" 
  apply (simp add: times_set_def)
  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 (simp add: times_set_def allpowers_def)
  apply safe
  apply simp
  apply (simp add:  times_set_def)
  apply safe
  apply (simp add:  allpowers_def)
  apply safe
  apply (subgoal_tac "x * xa  H ** {x}")
  apply (simp add: times_set_def)
  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 (simp add: times_set_def)
  apply auto[1]
  apply simp
  apply (drule_tac x = "xaa" in bspec)
  apply simp
  apply (drule_tac x = "x ^ n" in bspec)
  apply (simp add: allpowers_def)
  apply blast
  apply simp
  apply (drule_tac x = "xaa * xb" in bspec)
  apply (simp add: filter_i)
  apply (simp add: mult.assoc)
  apply (drule_tac x = "ya" in bspec)
  apply (simp add: allpowers_def)
  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 (simp add: allpowers_def times_set_def)
  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 (simp add: allpowers_def)
  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 (simp_all add: allpowers_def times_set_def)
  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 (simp add: times_set_def)
  apply auto[1]
  apply (drule_tac a = "x ^ n" in lemma_3_10_i_ii)
  apply simp
  apply (simp add: times_set_def)
  apply auto[1]
  apply (rule_tac x = n in exI)
  apply (subgoal_tac "(x ^ n) * h  H ** {x ^ n}")
  apply (simp add: times_set_def)
  apply auto[1]
  apply (drule_tac a = "x ^ n" in lemma_3_10_i_ii)
  apply (drule_tac sym)
  apply simp
  apply (simp add: times_set_def)
  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 (simp add: left_residual)
  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 (simp add: ultrafilters_def)
  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 (simp add: right_residual)
  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 (simp add: ultrafilters_def)
  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"
  by (simp add: cong_def lemma_3_10_i_iii)
  
lemma cong_r: "H  normalfilters  cong H = cong_r H"
  by (simp add: cong_def lemma_3_10_i_iii)

lemma cong_equiv: "H  normalfilters  equivp (cong H)"
  apply (simp add: cong_l)
  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 (simp add: cong_equiv)
  apply (rule_tac y = "b * c" in cong_trans)
  apply simp_all
  apply (simp add: cong_r lemma_3_8_i)
  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 (simp add: cong_l lemma_3_8_ii)
  apply safe
  apply (rule_tac x = xa in exI)
  apply simp
  apply (rule_tac x = ya in exI)
  apply (simp add: mult.assoc)
  apply (rule_tac y = "a l→ d" in cong_trans)
  apply simp
  apply (simp add: cong_r cong_r_filter)
  apply safe
  apply (rule_tac a = "c l→ d" in filter_ii)
  apply simp_all
  apply (subst left_residual [THEN sym])
  apply (simp add: lemma_2_5_14)
  apply (rule_tac a = "d l→ c" in filter_ii)
  apply simp_all
  apply (subst left_residual [THEN sym])
  apply (simp add: lemma_2_5_14)
  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 (simp add: lemma_2_5_14)
  apply (rule_tac a = "a l→ b" in filter_ii)
  apply simp_all
  apply (subst right_residual [THEN sym])
  apply (simp add: lemma_2_5_14)

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

  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 (simp add: lemma_2_5_15)
  apply (rule_tac a = "a r→ b" in filter_ii)
  apply simp_all
  apply (subst left_residual [THEN sym])
  by (simp add: lemma_2_5_15)

lemma cong_times: "R  congruences  R a b  R c d  R (a * c) (b * d)"
  by (simp add: congruences_def)

lemma cong_impl_l: "R  congruences  R a b  R c d  R (a l→ c) (b l→ d)"
  by (simp add: congruences_def)

lemma cong_impl_r: "R  congruences  R a b  R c d  R (a r→ c) (b r→ d)"
  by (simp add: congruences_def)

lemma cong_refl [simp]: "R  congruences  R a a"
  by (simp add: congruences_def equivp_reflp)

lemma cong_trans_a: "R  congruences  R a b  R b c  R a c"
  apply (simp add: congruences_def)
  apply (rule_tac y = b in equivp_transp)
  by simp_all

lemma cong_sym: "R  congruences  R a b  R b a"
  by (simp add: congruences_def equivp_symp)

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

lemma lemma_3_14 [simp]:
  "R  congruences  (normalfilter R)  normalfilters"
  apply (unfold normalfilters_def)
  apply safe
  apply (simp add: filters_def)
  apply safe
  apply (simp add: normalfilter_def)
  apply (drule_tac x = 1 in spec)
  apply (simp add: congruences_def  equivp_reflp)
  apply (simp add: normalfilter_def)
  apply (drule_tac a = a and c = b and b = 1 and d = 1 and R = R in cong_times)
  apply simp_all
  apply (simp add: normalfilter_def)
  apply (simp add: left_lesseq)
  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 (simp add: cong_sym)
  apply (simp_all add: normalfilter_def)
  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 (simp add: cong_sym)
  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
  by (simp add: cong_sym)
 
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 (simp add: normalfilter_def)
  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 (simp add: cong_l cong_l_filter)
  apply blast
  apply (subgoal_tac "cong H2 x 1")
  apply (simp add: cong_l cong_l_def)
  apply (subgoal_tac "cong H1 x 1")
  apply blast
  by (simp add: cong_l cong_l_def)

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 (simp_all add: p_def)
  apply (rule order.antisym)
  apply (simp_all add: lemma_2_10_24)
  apply (rule order.antisym)
  by (simp_all add: lemma_2_10_24)

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 (simp add: M_def)
  apply safe
  apply (rule order.antisym)
  apply (simp_all add: lemma_2_10_24 lemma_2_5_9_b) 
  apply (rule order.antisym)
  apply (simp_all add: lemma_2_10_24 lemma_2_5_9_b) 
  apply (rule order.antisym)
  by (simp_all add: lemma_2_10_24 lemma_2_5_9_b) 
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 (simp add: P3_a)
  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 (simp add: P3_b)
  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 (simp add: P6_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
      by (simp add: W3a)
    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 (simp add: P6_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
      by (simp add: W3b)
    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"
  by (simp add: W3b P7)

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 (simp add: P6_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 (simp add: P6_a)
  apply (subst W2a)
  by (simp add: P8_b)

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 (simp add: less_a_def)
  apply (simp_all add: lesseq_a_def)
  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 (simp add: less_b_def)
  apply (simp_all add: lesseq_b_def)
  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 (simp_all add: lesseq_a_def sup_a_def)
  apply (simp add: P9)
  apply (simp add: P9)
  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 (simp add: W2a)
  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 (simp add: W3b)
  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_all add: lesseq_b_def sup_a_def)
  apply (simp_all add: W2b)
  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 (simp add: W2c)
  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 (simp add: W3a)
  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 (simp add: fun_eq_iff)
  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)"
  by (simp add: order)

lemma order_r: "(a  b) = (a r→ b = 1)"
  by (simp add: order P10)

lemma P11_a: "a  b l→ a"
  by (simp add: order_r P6_b)

lemma P11_b: "a  b r→ a"
  by (simp add: order_l P6_a)

lemma P12: "(a  b l→ c) = (b  a r→ c)" 
  apply (subst order_r)
  apply (subst order_l)
  by (simp add: P7)

lemma P13_a: "a  b  b l→ c  a l→ c"
  apply (subst order_r)
  apply (simp add: order_l)
  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 (simp add: order_r)
  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 (simp add: order_l)
  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 (simp add: order_r)
  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"
  by (simp add: zero_def W4)

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)
  by (simp add: P10)

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) 
  by (simp add: P6_b)
  
lemma C2_a [simp]: "0 l→ x = 1"
  by (simp add: P10)

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)
      apply (simp add: order_r B) 
      by (simp add: order_l A)
    qed

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

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 (simp add: order_l W5b)
  apply (cut_tac a = "-r y" and b = "-r x" in W5a)
  by (simp add: order_l)
  
  
lemma C5_b: "-l x r→ -l y = y l→ x"
  apply (rule order.antisym)
  apply (simp add: order_l W5a)
  apply (cut_tac a = "-l y" and b = "-l x" in W5b)
  by (simp add: order_l)

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)
  by (simp add: C5_b)
 
lemma C7_b: "(x  y) = (-r y  -r x)"
  apply (subst order_r)
  apply (subst order_l)
  by (simp add: C5_a)

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 (simp_all add: inf_a_def)
  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)"
      by (simp add: C)
    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)"
      by (simp add: C5_b)
    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)"
      by (simp add: W2c)
    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)"
      by (simp add: C5_b)
    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)
      by (simp add: B)
    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 (simp_all add: inf_b_def)
  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)"
      by (simp add: C)
    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)"
      by (simp add: C5_a)
    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)"
      by (simp add: W2a)
    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)"
      by (simp add: C5_a)
    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)
      by (simp add: A)
    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 (simp add: fun_eq_iff)
  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)
  apply (simp add: cancel_left_a)
  by (simp add: left_impl_ded)

lemma lemma_4_2_ii: "a r→ b = (c * a) r→ (c * b)"
  apply (subgoal_tac "a r→ b = a r→ (c r→ (c * b))  a r→ (c r→ (c * b)) = (c * a) r→ (c * b)")
  apply simp
  apply (rule conjI)
  apply (simp add: cancel_right_a)
  by (simp add: right_impl_ded)

lemma lemma_4_2_iii: "(a * c  b * c) = (a  b)"
  by (simp add: left_lesseq lemma_4_2_i [THEN sym])

lemma lemma_4_2_iv: "(c * a  c * b) = (a  b)"
  by (simp add: right_lesseq lemma_4_2_ii [THEN sym])

end

class wajsberg_pseudo_hoop_algebra = pseudo_hoop_algebra +
  assumes wajsberg1: "(a l→ b) r→ b = (b l→ a) r→ a"
  and wajsberg2: "(a r→ b) l→ b = (b r→ a) l→ a"



context wajsberg_pseudo_hoop_algebra
begin

lemma lemma_4_3_i_a: "a ⊔1 b = (a l→ b) r→ b"
  by (simp add: sup1_def wajsberg1)

lemma lemma_4_3_i_b: "a ⊔1 b = (b l→ a) r→ a"
  by (simp add: sup1_def wajsberg1)

lemma lemma_4_3_ii_a: "a ⊔2 b = (a r→ b) l→ b"
  by (simp add: sup2_def wajsberg2)

lemma lemma_4_3_ii_b: "a ⊔2 b = (b r→ a) l→ a"
  by (simp add: sup2_def wajsberg2)
end


sublocale wajsberg_pseudo_hoop_algebra < lattice1:pseudo_hoop_lattice_b "(⊔1)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
  apply unfold_locales
  apply (simp add: lemma_4_3_i_a)
  by (simp add: lemma_2_5_13_b lemma_2_5_13_a)

class zero_one = zero + one


class bounded_wajsberg_pseudo_hoop_algebra = zero_one + wajsberg_pseudo_hoop_algebra +
  assumes zero_smallest [simp]: "0  a"
begin 
end


sublocale wajsberg_pseudo_hoop_algebra < lattice2:pseudo_hoop_lattice_b "(⊔2)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
  apply unfold_locales
  apply (simp add: lemma_4_3_ii_a)
  by (simp add: lemma_2_5_13_b lemma_2_5_13_a)

lemma (in wajsberg_pseudo_hoop_algebra) sup1_eq_sup2: "(⊔1) = (⊔2)"
  apply (simp add: fun_eq_iff)
  apply safe
  apply (cut_tac a = x and b = xa in lattice1.supremum_pair)
  apply (cut_tac a = x and b = xa in lattice2.supremum_pair)
  by blast

context bounded_wajsberg_pseudo_hoop_algebra
begin
definition
  "negl a = a l→ 0"
  
definition
  "negr a = a r→ 0"

lemma [simp]: "0 l→ a = 1"
  by (simp add: order [THEN sym])
  
lemma [simp]: "0 r→ a = 1"
  by (simp add: order_r [THEN sym])
end

sublocale bounded_wajsberg_pseudo_hoop_algebra < wajsberg: pseudo_wajsberg_algebra "1"  "(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 (simp add: lemma_2_5_16)
  apply (subst right_lesseq [THEN sym])
  apply (simp add: lemma_2_5_17)
  apply (simp add: left_lesseq)
  apply (simp add: less_def)
  apply (simp_all add: negl_def negr_def) 
  apply (subst left_lesseq [THEN sym])
  apply (subgoal_tac "b l→ a = ((b l→ 0) r→ 0) l→ ((a l→ 0) r→ 0)")
  apply (simp add: lemma_2_5_17)
  apply (subst wajsberg1)
  apply simp
  apply (subst wajsberg1)
  apply simp
  apply (subst left_lesseq [THEN sym])
  apply (subgoal_tac "b r→ a = ((b r→ 0) l→ 0) r→ ((a r→ 0) l→ 0)")
  apply (simp add: lemma_2_5_16)
  apply (subst wajsberg2)
  apply simp
  apply (subst wajsberg2)
  apply simp
  apply (simp add: left_impl_ded [THEN sym])
  apply (simp add: right_impl_ded [THEN sym])
  apply (simp add:  lemma_4_3_i_a [THEN sym] lemma_4_3_ii_a [THEN sym])
  apply (rule 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 add: strict)
  apply (simp_all add: mult_def order_l strict) 
  apply (simp add: zero_def [THEN sym] C3_a)
  apply (simp add: W6 inf_a_def [THEN sym])
  apply (rule 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: W6)
  apply (simp add: C6 [THEN sym])
  apply (simp add: P9 C5_a)
  apply (simp add: inf_b_def [THEN sym])
  apply (simp add: W6 inf_a_def [THEN sym])
  apply (rule order.antisym)
  apply simp_all
  apply (simp add: W2a)
  by (simp add: W2c)

end

class basic_pseudo_hoop_algebra = pseudo_hoop_algebra +
  assumes B1: "(a l→ b) l→ c  ((b l→ a) l→ c) l→ c"
  and B2: "(a r→ b) r→ c  ((b r→ a) r→ c) r→ c"
begin
lemma lemma_4_5_i: "(a l→ b) ⊔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 (simp add: sup1_def)
  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 (simp add: sup2_def)
  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 (simp add: mult.assoc)
  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 (simp add: mult.assoc)
  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 (simp add: mult.assoc)
  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 (simp add: mult.assoc)
  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)
  by (simp_all add: lemma_4_5_a lemma_4_5_b)
end

sublocale basic_pseudo_hoop_algebra <  basic_lattice:lattice "(⊓)" "(≤)" "(<)" "(⊔1)"
  apply unfold_locales
  by (simp_all add: lemma_4_5_a)

context pseudo_hoop_lattice begin end

sublocale basic_pseudo_hoop_algebra <  pseudo_hoop_lattice "(⊔1)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
  apply unfold_locales
  by (simp_all add: basic_lattice.sup_assoc)

class sup_assoc_pseudo_hoop_algebra = pseudo_hoop_algebra +
  assumes sup1_assoc: "a ⊔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
  by (simp add: sup1_assoc)

sublocale sup_assoc_pseudo_hoop_algebra <  sup2_lattice: pseudo_hoop_lattice "(⊔2)" "(*)" "(⊓)" "(l→)" "(≤)" "(<)" 1 "(r→)"
  apply unfold_locales
  by (simp add: sup2_assoc)


class sup_assoc_pseudo_hoop_algebra_1 = sup_assoc_pseudo_hoop_algebra +
  assumes union_impl: "(a l→ b) ⊔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 (simp add: infimum_def lower_bound_def)
  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 (simp add: lemma_2_5_11)
  apply (simp add: union_impl)
   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)
  apply (simp add: lemma_2_5_11)
  by (simp add: union_impr)

context basic_pseudo_hoop_algebra
begin

lemma lemma_4_8_i: "a * (b  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: lemma_4_5 lemma_4_5_ii)
  apply (simp add: mult.assoc [THEN sym])  
  apply safe
  apply (rule_tac y = "a * b * (b r→ c)" in order_trans)
  apply simp
  apply simp
  apply (rule_tac y = "a * c * (c r→ b)" in order_trans)
  apply simp
  apply simp
  apply (simp add: inf_r_def [THEN sym])
  apply (subgoal_tac "b  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 (simp add: lemma_4_5_i)
  apply (simp add: mult.assoc)  
  apply safe
  apply (rule_tac y = "(b l→ c) * (b * a)" in order_trans)
  apply simp_all
  apply (rule_tac y = "(c l→ b) * (c * a)" in order_trans)
  apply simp_all
  apply (simp add: inf_l_def [THEN sym])
  apply (subgoal_tac "b  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)
  by (simp add: lemma_2_5_9_a)

 lemma lemma_4_8_iv: "(a r→ b) r→ (b r→ a) = b r→ a"
  apply (rule order.antisym)
  apply (cut_tac a = a and b = b in lemma_4_5_ii)
  apply (unfold sup2_def left_lesseq, simp)
  by (simp add: lemma_2_5_9_b)

end

context wajsberg_pseudo_hoop_algebra
begin
subclass sup_assoc_pseudo_hoop_algebra_1
  apply unfold_locales
  apply (simp add: lattice1.sup_assoc)
  apply (simp add: lattice2.sup_assoc)
  apply (simp add: lemma_4_3_i_a)
  apply (subgoal_tac "(a l→ b) l→ (b l→ a) = b l→ a")
  apply simp
  apply (subst lemma_2_10_30 [THEN sym])
  apply (subst wajsberg1)
  apply (simp add: lemma_2_10_32)
  apply (subst sup1_eq_sup2)
  apply (simp add: lemma_4_3_ii_a)
  apply (subgoal_tac "(a r→ b) r→ (b r→ a) = b r→ a")
  apply simp
  apply (subst lemma_2_10_31 [THEN sym])
  apply (subst wajsberg2)
  by (simp add: lemma_2_10_33)
end

class bounded_basic_pseudo_hoop_algebra = zero_one + basic_pseudo_hoop_algebra +
  assumes zero_smallest [simp]: "0  a"

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)  
  apply (simp add: lemma_4_5) 
  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 (simp add: left_residual_bl)
    apply (rule conjI)
    apply (simp add: left_residual_bl)
    apply (rule conjI)
    apply (simp add: mult.assoc)
    apply (simp add: left_residual_bl)
    apply (simp add: left_residual_bl [THEN sym])
    apply (rule_tac y="(b l→ c) * b" in bounded_lattice.order_trans)
    apply (simp add: mult.assoc [THEN sym]) 
    apply (subst inf_l_bl_def [THEN sym])
    apply (subst bounded_lattice.inf_commute)
    apply (subst inf_l_bl_def)
    apply (subst mult.assoc) 
    apply (subst left_residual_bl) 
    apply simp
    apply (subst left_residual_bl) 
    by simp

  lemma impr_ded_bl: "(b * a r→ c) = (a r→ (b r→ c))"
    apply (rule bounded_lattice.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 (simp add: right_residual_bl)
    apply (rule conjI)
    apply (simp add: right_residual_bl)
    apply (rule conjI)
    apply (simp add: mult.assoc)
    apply (simp add: right_residual_bl)
    apply (simp add: right_residual_bl [THEN sym])
    apply (rule_tac y="b * (b r→ c)" in bounded_lattice.order_trans)
    apply (simp add: mult.assoc) 
    apply (subst inf_r_bl_def [THEN sym])
    apply (subst bounded_lattice.inf_commute)
    apply (subst inf_r_bl_def)
    apply (subst mult.assoc [THEN sym]) 
    apply (subst right_residual_bl) 
    apply simp
    apply (subst right_residual_bl) 
    by simp

  lemma lesseq_impl_bl: "(a  b) = (a l→ b = 1)"
    apply (rule iffI)
    apply (rule  bounded_lattice.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: bounded_lattice.less_le_not_le)
  apply (simp add: mult_1_left)
  apply (simp add: mult_1_right)
  apply (simp add: impl_one_bl)
  apply (simp add: inf_l_bl_def [THEN sym])
  apply (rule bounded_lattice.inf_commute)
  apply (rule impl_ded_bl)
  apply (rule lesseq_impl_bl)
  apply (rule inf_r_bl_def)
  apply (simp add: impr_one_bl)
  apply (simp add: inf_r_bl_def [THEN sym])
  apply (rule bounded_lattice.inf_commute)
  apply (rule impr_ded_bl)
  apply (simp add: inf_r_bl_def [THEN sym] inf_l_bl_def [THEN sym])
  apply (rule bounded_lattice.sup_commute)
  apply simp
  apply safe
  apply (rule bounded_lattice.order.antisym)
  apply simp_all
  apply (subgoal_tac "a   a  b")
  apply simp
  apply (drule drop_assumption)
  apply simp
  by (simp add: bounded_lattice.sup_assoc)

subclass bounded_basic_pseudo_hoop_algebra
  apply unfold_locales
  apply simp_all
  apply (simp add: left_residual [THEN sym])
  apply (rule_tac y = "((a l→ b)  (b l→ a)) l→ c" in bounded_lattice.order_trans)
  apply (simp add: sup_impl_inf)
  apply (simp add: impl_sup_bl)

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

end

class product_pseudo_hoop_algebra = basic_pseudo_hoop_algebra +
  assumes P1: "b l→ b * b  (a  (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 (simp add: lemma_2_5_9_a)

  apply (rule_tac y = "1 r→ b" in order_trans)
  apply (cut_tac a = 1 and b = b and c = b in lemma_4_2_ii)
  apply simp
  apply (simp add: lemma_2_5_9_b)
  apply (simp add: lemma_4_2_i [THEN sym])
  by (simp add: lemma_4_2_ii [THEN sym])

end

class simple_pseudo_hoop_algebra = pseudo_hoop_algebra +
  assumes simple: "normalfilters  properfilters = {{1}}"

class proper = one +
  assumes proper: " a . a  1"

class strong_simple_pseudo_hoop_algebra = pseudo_hoop_algebra +
  assumes strong_simple: "properfilters = {{1}}"
begin

subclass proper
  apply unfold_locales
  apply (cut_tac strong_simple)
  apply (simp add: properfilters_def)
  apply (case_tac "{1} = UNIV")
  apply blast
  by blast

lemma lemma_4_12_i_ii: "a  1  filterof({a}) = UNIV"
  apply (cut_tac strong_simple)
  apply (simp add: properfilters_def)
  apply (subgoal_tac "filterof {a}  {F  filters. F  UNIV}")
  apply (drule drop_assumption)
  apply (drule drop_assumption)
  apply simp
  apply simp
  apply safe
  apply (subgoal_tac "a  filterof {a}")
  apply simp
  apply (subst filterof_def)
  by simp

lemma lemma_4_12_i_iii: "a  1  ( n . a ^ n  b)"
  apply (drule lemma_4_12_i_ii)
  apply (simp add: prop_3_2_i)
  by blast

lemma lemma_4_12_i_iv: "a  1  ( n . a l-n b = 1)"
  apply (subst lemma_2_4_7_a)
  apply (subst left_lesseq [THEN sym])
  by (simp add: lemma_4_12_i_iii)

lemma lemma_4_12_i_v: "a  1  ( n . a r-n b = 1)"
  apply (subst lemma_2_4_7_b)
  apply (subst right_lesseq [THEN sym])
  by (simp add: lemma_4_12_i_iii)

end

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

sublocale strong_simple_pseudo_hoop_algebra < strong_simple_pseudo_hoop_algebra_a
  apply unfold_locales
  by (simp add: lemma_4_12_i_ii)

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

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

context strong_simple_pseudo_hoop_algebra
begin

lemma lemma_4_13_i: "b l→ a = a  a = 1  b = 1"
  apply safe
  apply (drule_tac a = b and b = a in lemma_4_12_i_iii)
  apply safe
  apply (subst (asm) left_lesseq)
  apply (drule_tac n = n in power_impl)
  by simp

lemma lemma_4_13_ii: "b r→ a = a  a = 1  b = 1"
  apply safe
  apply (drule_tac a = b and b = a in lemma_4_12_i_iii)
  apply safe
  apply (subst (asm) right_lesseq)
  apply (drule_tac n = n in power_impr)
  by simp
end

class basic_pseudo_hoop_algebra_A = basic_pseudo_hoop_algebra + 
  assumes left_impl_one: "b l→ a = a  a = 1  b = 1"
  and right_impl_one: "b r→ a = a  a = 1  b = 1"
begin
subclass linorder
  apply unfold_locales
  apply (cut_tac a = "x" and b = "y" in lemma_4_8_iii)
  apply (drule left_impl_one)
  apply (simp add: left_lesseq)
  by blast

lemma [simp]: "(a l→ b) r→ b  (b l→ a) r→ a"
  apply (case_tac "a = b")
  apply simp
  apply (cut_tac x = a and y =b in linear) 
  apply safe
  apply (subst (asm) left_lesseq)
  apply (simp add: lemma_2_10_24)
  apply (subst (asm) left_lesseq)
  apply simp
  apply (subst left_lesseq)
  apply (cut_tac b = "((a l→ b) r→ b) l→ a" and a = "a l→ b" in left_impl_one)
  apply (simp add: lemma_2_10_32)
  apply (simp add: left_lesseq [THEN sym])
  apply safe
  apply (erule notE)
  by simp

end

context basic_pseudo_hoop_algebra_A begin

lemma [simp]: "(a r→ b) l→ b  (b r→ a) l→ a"
  apply (case_tac "a = b")
  apply simp
  apply (cut_tac x = a and y =b in linear) 
  apply safe
  apply (subst (asm) right_lesseq)
  apply simp
  apply (simp add: lemma_2_10_26)
  apply (unfold right_lesseq)
  apply (cut_tac b = "((a r→ b) l→ b) r→ a" and a = "a r→ b" in right_impl_one)
  apply (simp add: lemma_2_10_33)
  apply (simp add: right_lesseq [THEN sym])
  apply safe
  apply (erule notE)
  by simp

subclass wajsberg_pseudo_hoop_algebra
  apply unfold_locales
  apply (rule 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
  apply (simp add: lemma_4_13_i)
  by (simp add: lemma_4_13_ii)

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]
lemmas diff_minus = diff_conv_add_uminus

context lgroup
begin
lemma (in lgroup) less_eq_inf_2: "(x  y) = (inf y x = x)"
  by (simp add: le_iff_inf inf_commute)
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 (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)  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_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"
  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 (