Theory PseudoHoops

header{* 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 "op *" inf_rr "op 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 (op *) inf_rr (op 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 = op \<sqinter>"
    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 "op *" inf_rr "op r->"
      by (rule right_complemented_monoid_algebra)
(*
    find_theorems name: le_iff_inf
    thm A.dual_algebra.le_iff_inf
    have "!!x y. lesseq_r x y = (inf_rr x y = x)" by fact
    note `!!x y. lesseq_r x y = (inf_rr x y = x)`
*)
    show "lesseq_r a b = (a ≤ b)"
      apply (subst  le_iff_inf)
      apply (subst `lesseq_r a b = (inf_rr a b = a)`)
      apply (unfold inf_rr_inf [THEN sym])
      by simp
  qed
  lemma [simp]: "lesseq_r = op ≤"
    apply (unfold fun_eq_iff, simp add: lesseq_lesseq_r) done

  lemma [simp]: "less_r = op <"
    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" "op \<sqinter>" "op r->" "op ≤" "op <" 1 "op 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) = ((op l->) = (op r->))"
  apply (simp add: fun_eq_iff)
  apply safe
  apply (rule 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 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 \<sqinter> 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 antisym)
  by (simp_all add: infimum_def)

lemma lemma_2_6_20:
  "a ∈ infimum A ==> b l-> a ∈ infimum ((op 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 ((op r-> b)`A)"
  by (rule pseudo_hoop_dual.lemma_2_6_20)

lemma infimum_pair: "a ∈ infimum {x . x = b ∨ x = c} = (a = b \<sqinter> c)"
  apply (simp add: infimum_def lower_bound_def)
  apply safe
  apply (rule antisym)
  by simp_all
 
lemma lemma_2_6_20_a:
  "a l-> (b \<sqinter> c) = (a l-> b) \<sqinter> (a l-> c)"
  apply (subgoal_tac "b \<sqinter> c ∈ infimum {x . x = b ∨ x = c}")
  apply (drule_tac b = a in lemma_2_6_20)
  apply (case_tac "(op 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 \<sqinter> c) = (a r-> b) \<sqinter> (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 \<sqinter> c) l-> (b \<sqinter> d)"
  apply (rule_tac y = "(a \<sqinter> c l-> b) * (a \<sqinter> c l-> d)" in order_trans)
  apply (rule mult_mono)
  apply (simp_all add: lemma_2_5_13_a)
  apply (rule_tac y = "(a \<sqinter> c l-> b) \<sqinter> (a \<sqinter> 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 \<sqinter> c) r-> (b \<sqinter> d)"
  apply (rule_tac y = "(c \<sqinter> a) r-> (d \<sqinter> 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 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 (rule pseudo_hoop_dual.lemma_2_8_i, simp)

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 (op * 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 \<sqinter> b ∈ supremum (op \<sqinter> 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 "(∀xa∈A. xa ≤ (b r-> a) l-> x)")
  apply simp
  apply safe
  apply (subst left_residual [THEN sym])
  apply (rule_tac y = "xaa * (xaa r-> a)" in order_trans)
  apply (rule mult_left_mono)
  apply (rule lemma_2_5_13_b)
  apply simp
  apply (subst right_impl_times)
  by simp

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

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

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

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

lemma lemma_2_10_28:
  "b l-> ((a l-> b) r-> a) = b l-> a"
  apply (rule antisym)
  apply (subst left_residual [THEN sym])
  apply (rule_tac y = "((a l-> b) r-> a) \<sqinter> 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 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) \<sqinter> b) l-> a"
      by (simp add: inf_l_def)
    also have "… = b l-> a" apply (subgoal_tac "((b l-> a) r-> a) \<sqinter> b = b", simp, rule 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 \<squnion> b = b \<squnion> a"
    and sup_le [simp]: "a ≤ a \<squnion> b"
    and le_sup_equiv: "(a ≤ b) = (a \<squnion> b = b)"
begin
  lemma sup_le_2 [simp]:
    "b ≤ a \<squnion> b"
    by (subst sup_comute, simp)

  lemma le_sup_equiv_r:
    "(a \<squnion> b = b) = (a ≤ b)"
    by (simp add: le_sup_equiv)

  lemma sup_idemp [simp]: 
    "a \<squnion> a = a"
    by (simp add: le_sup_equiv_r)
end

class pseudo_hoop_sup1_algebra = pseudo_hoop_algebra + sup +
  assumes
  sup_def: "a \<squnion> b = ((a l-> b) r-> b) \<sqinter> ((b l-> a) r-> a)"
begin

lemma sup_comute1: "a \<squnion> b = b \<squnion> a"
  apply (simp add: sup_def)
  apply (rule antisym)
  by simp_all

lemma sup_le1 [simp]: "a ≤ a \<squnion> b"
  by (simp add: sup_def lemma_2_10_24 lemma_2_5_9_b)

lemma le_sup_equiv1: "(a ≤ b) = (a \<squnion> b = b)"
  apply safe
  apply (simp add: left_lesseq)
  apply (rule 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 \<sqinter> b = a \<sqinter> (a \<squnion> b)) ∧ (a \<sqinter> (a \<squnion> b) = a)")
  apply simp
  apply safe
  apply simp
  apply (rule 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 \<squnion> b = ((a r-> b) l-> b) \<sqinter> ((b r-> a) l-> a)"

context pseudo_hoop_sup1_algebra begin end

sublocale pseudo_hoop_sup2_algebra < sup1_dual!: pseudo_hoop_sup1_algebra "op \<squnion>" "λ a b . b * a" "op \<sqinter>" "op r->" "op ≤" "op <" 1 "op l->"
  apply unfold_locales
  by (simp add: sup_2_def)

context pseudo_hoop_sup2_algebra begin

lemma sup_comute_2: "a \<squnion> b = b \<squnion> a"
  by (rule  sup1_dual.sup_comute)

lemma sup_le2 [simp]: "a ≤ a \<squnion> b"
  by (rule sup1_dual.sup_le)

lemma le_sup_equiv2: "(a ≤ b) = (a \<squnion> 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 \<squnion> (b \<sqinter> c) ≤ (a \<squnion> b) \<sqinter> (a \<squnion> c)"
begin
  lemma sup_lower_upper_bound [simp]:
    "a ≤ c ==> b ≤ c ==> a \<squnion> b ≤ c"
    apply (subst le_iff_inf)
    apply (subgoal_tac "(a \<squnion> b) \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c) ∧ a \<squnion> (b \<sqinter> c) ≤ (a \<squnion> b) \<sqinter> (a \<squnion> c) ∧ a \<squnion> (b \<sqinter> c) = a \<squnion> b")
    apply (rule 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 "op \<sqinter>" "op ≤" "op <" "op \<squnion>"
  by (unfold_locales, simp_all)

class pseudo_hoop_lattice_b = pseudo_hoop_sup_algebra +
  assumes le_sup_cong: "a ≤ b ==> a \<squnion> c ≤ b \<squnion> c"

begin
  lemma sup_lower_upper_bound_b [simp]:
    "a ≤ c ==> b ≤ c ==> a \<squnion> b ≤ c"
    proof -
      assume A: "a ≤ c"
      assume B: "b ≤ c"
      have "a \<squnion> b ≤ c \<squnion> b" by (cut_tac A, simp add: le_sup_cong)
      also have "… = b \<squnion> c" by (simp add: sup_comute)
      also have "… ≤ c \<squnion> 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 \<squnion> (b \<sqinter> c) ≤ (a \<squnion> b) \<sqinter> (a \<squnion> 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 "op \<squnion>" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"
  by (unfold_locales, rule sup_inf_le_distr_b)

class pseudo_hoop_lattice = pseudo_hoop_sup_algebra +
  assumes sup_assoc_1: "a \<squnion> (b \<squnion> c) = (a \<squnion> b) \<squnion> c"
begin
  lemma le_sup_cong_c:
    "a ≤ b ==> a \<squnion> c ≤ b \<squnion> c"
    proof -
      assume A: "a ≤ b"
      have "a \<squnion> c \<squnion> (b \<squnion> c) = a \<squnion> (c \<squnion> (b \<squnion> c))" by (simp add: sup_assoc_1)
      also have "… = a \<squnion> ((b \<squnion> c) \<squnion> c)" by (simp add: sup_comute)
      also have "… = a \<squnion> (b \<squnion> (c \<squnion> c))" by (simp add: sup_assoc_1 [THEN sym])
      also have "… = (a \<squnion> b) \<squnion> c" by (simp add: sup_assoc_1)
      also have "… = b \<squnion> 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 "op \<squnion>" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"
  by (unfold_locales, rule le_sup_cong_c)


sublocale pseudo_hoop_lattice <  semilattice_sup "op \<squnion>" "op ≤" "op <"
  by (unfold_locales, simp_all)

sublocale pseudo_hoop_lattice <  lattice "op \<sqinter>" "op ≤" "op <" "op \<squnion>"
  by unfold_locales

lemma (in pseudo_hoop_lattice_a) supremum_pair [simp]:
  "supremum {a, b} = {a \<squnion> b}" 
  apply (simp add: supremum_def upper_bound_def)
  apply safe
  apply simp_all
  apply (rule antisym)
  by simp_all

sublocale pseudo_hoop_lattice <  distrib_lattice "op \<sqinter>" "op ≤" "op <" "op \<squnion>"
  apply unfold_locales
  apply (rule distrib_imp1)
  apply (case_tac "xa \<sqinter> (ya \<squnion> za) ∈ supremum (op \<sqinter> 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 + top
begin
lemma inf_eq_top_iff [simp]:
  "(inf x y = top) = (x = top ∧ y = top)"
  by (simp add: eq_iff)
end

sublocale pseudo_hoop_algebra < bounded_semilattice_inf_top "op \<sqinter>" "op ≤" "op <" "1"
  by unfold_locales simp

definition (in pseudo_hoop_algebra)
  sup1::"'a => 'a => 'a" (infixl "\<squnion>1" 70) where 
  "a \<squnion>1 b = ((a l-> b) r-> b) \<sqinter> ((b l-> a) r-> a)"

sublocale pseudo_hoop_algebra < sup1!: pseudo_hoop_sup1_algebra "op \<squnion>1" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op r->"
  apply unfold_locales 
  by (simp add: sup1_def)



definition (in pseudo_hoop_algebra)
  sup2::"'a => 'a => 'a" (infixl "\<squnion>2" 70) where 
  "a \<squnion>2 b = ((a r-> b) l-> b) \<sqinter> ((b r-> a) l-> a)"

sublocale pseudo_hoop_algebra < sup2!: pseudo_hoop_sup2_algebra "op \<squnion>2" "op *" "op \<sqinter>" "op l->" "op ≤" "op <" 1 "op 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 \<sqinter> b"
    apply (rule 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 \<squnion>1 b = 1")
    apply (simp add: sup1_def)
    apply (rule 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: local.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)² = 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