Theory SML_Semilattices

(* Title: Examples/SML_Relativization/Lattices/SML_Semilattices.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Relativization of the results about semilattices›
theory SML_Semilattices
  imports 
    "../Simple_Orders/SML_Simple_Orders"
    "../Algebra/SML_Monoids"
begin



subsection‹Commutative bands›


subsubsection‹Definitions and common properties›

locale semilattice_ow = abel_semigroup_ow U f 
  for U :: "'al set" and f +
  assumes idem[simp]: "x ∈ U ⟹ x *ow x = x"

locale semilattice_set_ow = 
  semilattice_ow U f for U :: "'al set" and f (infixl ‹*ow› 70)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma semilattice_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> (=)) 
      (λf. semilattice_ow (Collect (Domainp A)) f) semilattice"
  unfolding
    semilattice_ow_def semilattice_def 
    semilattice_ow_axioms_def semilattice_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by simp

lemma semilattice_set_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> (=)) 
      (λf. semilattice_set_ow (Collect (Domainp A)) f) semilattice_set"
  unfolding semilattice_set_ow_def semilattice_set_def by transfer_prover

end


subsubsection‹Relativization›

context semilattice_ow 
begin

tts_context
  tts: (?'a to U)
  substituting semilattice_ow_axioms
  eliminating through simp
begin

tts_lemma left_idem:
  assumes "a ∈ U" and "b ∈ U"
  shows "a *ow (a *ow b) = a *ow b"
    is semilattice.left_idem.

tts_lemma right_idem:
  assumes "a ∈ U" and "b ∈ U"
  shows "a *ow b *ow b = a *ow b"
    is semilattice.right_idem.

end

end



subsection‹Simple upper and lower semilattices›


subsubsection‹Definitions and common properties›

locale semilattice_order_ow = semilattice_ow U f 
  for U :: "'al set" and f  +
  fixes le :: "['al, 'al] ⇒ bool" (infix ‹≤ow› 50)
    and ls :: "['al, 'al] ⇒ bool" (infix ‹<ow› 50)
  assumes order_iff: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a ≤ow b ⟷ a = a *ow b"
    and strict_order_iff: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a <ow b ⟷ a = a *ow b ∧ a ≠ b"
begin

sublocale ordering_ow U ‹(≤ow)› ‹(<ow)›
proof
  show "⟦a ∈ U; b ∈ U⟧ ⟹ (a <ow b) = (a ≤ow b ∧ a ≠ b)" for a b
    apply standard
    subgoal by (auto simp: commute order_iff strict_order_iff)
    subgoal by (auto simp: order_iff strict_order_iff)
    done
  show "x ∈ U ⟹ x ≤ow x" for x by (simp add: order_iff)
  show "⟦ x ∈ U; y ∈ U; z ∈ U; x ≤ow y; y ≤ow z ⟧ ⟹ x ≤ow z" for x y z
  proof-
    assume "x ∈ U" and "y ∈ U" and "z ∈ U" and "x ≤ow y" and "y ≤ow z"
    note xy = order_iff[THEN iffD1, OF ‹x ∈ U› ‹y ∈ U› ‹x ≤ow y›]
    note yz = order_iff[THEN iffD1, OF ‹y ∈ U› ‹z ∈ U› ‹y ≤ow z›]
    note xz = assoc[OF ‹x ∈ U› ‹y ∈ U› ‹z ∈ U›, folded xy yz, symmetric]
    show ?thesis by (rule order_iff[THEN iffD2, OF ‹x ∈ U› ‹z ∈ U› xz])
  qed
  show "⟦ x ∈ U; y ∈ U; x ≤ow y; y ≤ow x ⟧ ⟹ x = y" for x y
    by (fastforce simp: commute order_iff)
qed

notation le (infix "≤ow" 50)
  and ls (infix "<ow" 50)

end

locale semilattice_order_set_ow = 
  semilattice_order_ow U f le ls + semilattice_set_ow U f
  for U :: "'al set" and f le ls  

locale inf_ow =
  fixes U :: "'al set" and inf (infixl ‹⊓ow› 70)
  assumes inf_closed[simp]: "⟦ x ∈ U; y ∈ U ⟧ ⟹ x ⊓ow y ∈ U"
begin

notation inf (infixl ‹⊓ow› 70)

lemma inf_closed'[simp]: "∀x∈U. ∀y∈U. x ⊓ow y ∈ U" by simp

end

locale inf_pair_ow = inf1: inf_ow U1 inf1 + inf2: inf_ow U2 inf2
  for U1 :: "'al set" and inf1
    and U2 :: "'bl set" and inf2
begin

notation inf1 (infixl ‹⊓ow.1› 70)
notation inf2 (infixl ‹⊓ow.2› 70)

end

locale semilattice_inf_ow = inf_ow U inf + order_ow U le ls 
  for U :: "'al set" and inf le ls  +
  assumes inf_le1[simp]: "⟦ x ∈ U; y ∈ U ⟧ ⟹ x ⊓ow y ≤ow x"
    and inf_le2[simp]: "⟦ x ∈ U; y ∈ U ⟧ ⟹ x ⊓ow y ≤ow y"
    and inf_greatest: 
      "⟦ x ∈ U; y ∈ U; z ∈ U; x ≤ow y; x ≤ow z ⟧ ⟹ x ≤ow y ⊓ow z"
begin

sublocale inf: semilattice_order_ow U ‹(⊓ow)› ‹(≤ow)› ‹(<ow)›
proof

  show *: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a ⊓ow b ∈ U" for a b by simp

  show **: "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a ⊓ow b ⊓ow c = a ⊓ow (b ⊓ow c)" 
    for a b c
  proof -
    
    assume "a ∈ U" and "b ∈ U" and "c ∈ U"
    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have ab_c: "a ⊓ow b ⊓ow c ∈ U" by simp
    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have a_bc: "a ⊓ow (b ⊓ow c) ∈ U" by simp

    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "a ⊓ow b ⊓ow c ≤ow b" 
      by (meson * inf_le1 inf_le2 order_trans)
    moreover from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "a ⊓ow b ⊓ow c ≤ow c" by simp
    ultimately have abc_le_bc: "a ⊓ow b ⊓ow c ≤ow b ⊓ow c"
      by (rule inf_greatest[OF ab_c ‹b ∈ U› ‹c ∈ U›])
    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have abc_le_a: "a ⊓ow b ⊓ow c ≤ow a" 
      by (meson inf_le1 order_trans inf_closed)
    note lhs = 
      inf_greatest[OF ab_c ‹a ∈ U› *[OF ‹b ∈ U› ‹c ∈ U›] abc_le_a abc_le_bc]

    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "a ⊓ow (b ⊓ow c) ≤ow a" 
      by (meson * inf_le1 order_trans)
    moreover from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "a ⊓ow (b ⊓ow c) ≤ow b" 
      by (meson * inf_le1 inf_le2 order_trans)
    ultimately have abc_le_bc: "a ⊓ow (b ⊓ow c) ≤ow a ⊓ow b"
      by (rule inf_greatest[OF a_bc ‹a ∈ U› ‹b ∈ U›])
    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have abc_le_a: "a ⊓ow (b ⊓ow c) ≤ow c" 
      by (meson inf_le2 order_trans inf_closed)
    note rhs =
      inf_greatest[OF a_bc *[OF ‹a ∈ U› ‹b ∈ U›] ‹c ∈ U› abc_le_bc abc_le_a] 
    show "a ⊓ow b ⊓ow c = a ⊓ow (b ⊓ow c)" 
      by (rule antisym[OF ab_c a_bc lhs rhs])
 
  qed

  show ***: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a ⊓ow b = b ⊓ow a" for a b
    by (simp add: inf_greatest xt1(5))

  show ****: "x ∈ U ⟹ x ⊓ow x = x" for x
  proof-
    assume "x ∈ U"
    have "x ⊓ow x ≤ow x" by (simp add: ‹x ∈ U›)
    moreover have "x ≤ow x ⊓ow x" by (simp add: ‹x ∈ U› inf_greatest)
    ultimately show "x ⊓ow x = x" by (simp add: ‹x ∈ U› antisym)
  qed

  show *****: "⟦ a ∈ U; b ∈ U ⟧ ⟹ (a ≤ow b) = (a = a ⊓ow b)" for a b
    by (metis * *** inf_greatest inf_le2 order.eq_iff)
  
  show "⟦ a ∈ U; b ∈ U ⟧ ⟹ (a <ow b) = (a = a ⊓ow b ∧ a ≠ b)" for a b
    by (simp add: ***** less_le)

qed

sublocale Inf_fin: semilattice_order_set_ow U ‹(⊓ow)› ‹(≤ow)› ‹(<ow)› ..

end

locale semilattice_inf_pair_ow = 
  sl_inf1: semilattice_inf_ow U1 inf1 le1 ls1 +
  sl_inf2: semilattice_inf_ow U2 inf2 le2 ls2
  for U1 :: "'al set" and inf1 le1 ls1
    and U2 :: "'bl set" and inf2 le2 ls2
begin

sublocale inf_pair_ow ..
sublocale order_pair_ow ..

end

locale sup_ow =
  fixes U :: "'ao set" and sup :: "['ao, 'ao] ⇒ 'ao" (infixl ‹⊔ow› 70)
  assumes sup_closed[simp]: "⟦ x ∈ U; y ∈ U ⟧ ⟹ sup x y ∈ U"
begin

notation sup (infixl ‹⊔ow› 70)

lemma sup_closed'[simp]: "∀x∈U. ∀y∈U. x ⊔ow y ∈ U" by simp

end

locale sup_pair_ow = sup1: sup_ow U1 sup1 + sup2: sup_ow U2 sup2
  for U1 :: "'al set" and sup1
    and U2 :: "'bl set" and sup2
begin

notation sup1 (infixl ‹⊔ow.1› 70)
notation sup2 (infixl ‹⊔ow.2› 70)

end

locale semilattice_sup_ow = sup_ow U sup + order_ow U le ls 
  for U :: "'al set" and sup le ls + 
  assumes sup_ge1[simp]: "⟦ x ∈ U; y ∈ U ⟧ ⟹ x ≤ow x ⊔ow y"
    and sup_ge2[simp]: "⟦ y ∈ U; x ∈ U ⟧ ⟹ y ≤ow x ⊔ow y"
    and sup_least: 
      "⟦ y ∈ U; x ∈ U; z ∈ U; y ≤ow x; z ≤ow x ⟧ ⟹ y ⊔ow z ≤ow x"
begin

sublocale sup: semilattice_order_ow U ‹(⊔ow)› ‹(≥ow)› ‹(>ow)›
proof

  show *: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a ⊔ow b ∈ U" for a b by simp

  show **: 
    "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a ⊔ow b ⊔ow c = a ⊔ow (b ⊔ow c)" for a b c
  proof -
    
    assume "a ∈ U" and "b ∈ U" and "c ∈ U"
    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have ab_c: "a ⊔ow b ⊔ow c ∈ U" by simp
    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have a_bc: "a ⊔ow (b ⊔ow c) ∈ U" by simp

    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "b ≤ow a ⊔ow b ⊔ow c"
      by (meson order_trans sup_ge1 sup_ge2 sup_closed')
    moreover from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "c ≤ow a ⊔ow b ⊔ow c" by simp
    ultimately have ab_le_abc: "b ⊔ow c ≤ow a ⊔ow b ⊔ow c"
      by (rule sup_least[OF ‹b ∈ U› ab_c ‹c ∈ U›])
    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have a_le_abc: "a ≤ow a ⊔ow b ⊔ow c" 
      by (meson "*" order_trans sup_ge1)
    note rhs = 
      sup_least[OF ‹a ∈ U› ab_c *[OF ‹b ∈ U› ‹c ∈ U›] a_le_abc ab_le_abc]

    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "a ≤ow a ⊔ow (b ⊔ow c)" by simp
    moreover from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "b ≤ow a ⊔ow (b ⊔ow c)" 
      by (meson order_trans sup_ge1 sup_ge2 sup_closed')
    ultimately have ab_le_abc: "a ⊔ow b ≤ow a ⊔ow (b ⊔ow c)"
      by (rule sup_least[OF ‹a ∈ U› a_bc ‹b ∈ U›])
    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have c_le_abc: "c ≤ow a ⊔ow (b ⊔ow c)" 
      by (meson "*" order_trans sup_ge2)
    note lhs =
      sup_least[OF *[OF ‹a ∈ U› ‹b ∈ U›] a_bc ‹c ∈ U› ab_le_abc c_le_abc]  
    show "a ⊔ow b ⊔ow c = a ⊔ow (b ⊔ow c)"
      by (rule antisym[OF ab_c a_bc lhs rhs])
 
  qed

  show ***: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a ⊔ow b = b ⊔ow a" for a b
    by (simp add: antisym sup_least)

  show ****: "x ∈ U ⟹ x ⊔ow x = x" for x
  proof-
    assume "x ∈ U"
    have "x ≤ow x ⊔ow x" by (simp add: ‹x ∈ U›)
    moreover have "x ⊔ow x ≤ow x" by (simp add: ‹x ∈ U› sup_least)
    ultimately show "x ⊔ow x = x" by (simp add: ‹x ∈ U› antisym)
  qed

  show *****: "⟦ a ∈ U; b ∈ U ⟧ ⟹ (a ≥ow b) = (a = a ⊔ow b)" for a b 
    by (metis *** order.eq_iff sup_ge2 sup_least sup_closed)

  show "⟦ a ∈ U; b ∈ U ⟧ ⟹ (a >ow b) = (a = a ⊔ow b ∧ a ≠ b)" for a b
    by (auto simp: ***** less_le)

qed

sublocale Sup_fin: semilattice_order_set_ow U sup "(≥ow)" "(>ow)" ..

end


locale semilattice_sup_pair_ow = 
  sl_sup1: semilattice_sup_ow U1 sup1 le1 ls1 +
  sl_sup2: semilattice_sup_ow U2 sup2 le2 ls2
  for U1 :: "'al set" and sup1 le1 ls1
    and U2 :: "'bl set" and sup2 le2 ls2
begin

sublocale sup_pair_ow ..
sublocale order_pair_ow ..

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma semilattice_order_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (=)
    ) (semilattice_order_ow (Collect (Domainp A))) semilattice_order"
  unfolding
    semilattice_order_ow_def semilattice_order_def 
    semilattice_order_ow_axioms_def semilattice_order_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by simp

lemma semilattice_order_set_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (=)
    ) (semilattice_order_set_ow (Collect (Domainp A))) semilattice_order_set"
  unfolding semilattice_order_set_ow_def semilattice_order_set_def 
  apply transfer_prover_start
  apply transfer_step+
  by simp

lemma semilattice_inf_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (=)
    ) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf"
proof -
  let ?P = 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (=)
    )"
  let ?semilattice_ow = "semilattice_inf_ow (Collect (Domainp A))"
  let ?rf_UNIV = 
    "(λinf::['b, 'b] ⇒ 'b. (∀x y. x ∈ UNIV ⟶ y ∈ UNIV ⟶ inf x y ∈ UNIV))"
  have 
    "?P 
    ?semilattice_ow 
    (λinf le ls. ?rf_UNIV inf ∧ class.semilattice_inf inf le ls)"
    unfolding 
      class.semilattice_inf_def semilattice_inf_ow_def 
      class.semilattice_inf_axioms_def semilattice_inf_ow_axioms_def
      inf_ow_def
    apply transfer_prover_start
    apply transfer_step+
    unfolding Ball_def by fastforce
  then show ?thesis by simp
qed

lemma semilattice_sup_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (=)
    ) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup"
proof -
  let ?P = 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (=)
    )"
  let ?semilattice_ow = "semilattice_sup_ow (Collect (Domainp A))"
  let ?rf_UNIV = 
    "(λsup::['b, 'b] ⇒ 'b. (∀x y. x ∈ UNIV ⟶ y ∈ UNIV ⟶ sup x y ∈ UNIV))"
  have 
    "?P 
    ?semilattice_ow 
    (λsup le ls. ?rf_UNIV sup ∧ class.semilattice_sup sup le ls)"
  unfolding 
    class.semilattice_sup_def semilattice_sup_ow_def 
    class.semilattice_sup_axioms_def semilattice_sup_ow_axioms_def
    sup_ow_def
  apply transfer_prover_start
  apply transfer_step+
  unfolding Ball_def by fastforce
  then show ?thesis by simp
qed

end


subsubsection‹Relativization›

context semilattice_order_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting semilattice_order_ow_axioms
  eliminating through simp
begin

tts_lemma cobounded1:
  assumes "a ∈ U" and "b ∈ U"
  shows "a *ow b ≤ow a"
    is semilattice_order.cobounded1.
    
tts_lemma cobounded2:
  assumes "a ∈ U" and "b ∈ U"
  shows "a *ow b ≤ow b"
    is semilattice_order.cobounded2.

tts_lemma absorb_iff1:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a ≤ow b) = (a *ow b = a)"
    is semilattice_order.absorb_iff1.

tts_lemma absorb_iff2:
  assumes "b ∈ U" and "a ∈ U"
  shows "(b ≤ow a) = (a *ow b = b)"
    is semilattice_order.absorb_iff2.

tts_lemma strict_coboundedI1:
  assumes "a ∈ U" and "c ∈ U" and "b ∈ U" and "a <ow c"
  shows "a *ow b <ow c"
    is semilattice_order.strict_coboundedI1.

tts_lemma strict_coboundedI2:
  assumes "b ∈ U" and "c ∈ U" and "a ∈ U" and "b <ow c"
  shows "a *ow b <ow c"
    is semilattice_order.strict_coboundedI2.

tts_lemma absorb1:
  assumes "a ∈ U" and "b ∈ U" and "a ≤ow b"
  shows "a *ow b = a"
    is semilattice_order.absorb1.

tts_lemma coboundedI1:
  assumes "a ∈ U" and "c ∈ U" and "b ∈ U" and "a ≤ow c"
  shows "a *ow b ≤ow c"
    is semilattice_order.coboundedI1.

tts_lemma absorb2:
  assumes "b ∈ U" and "a ∈ U" and "b ≤ow a"
  shows "a *ow b = b"
    is semilattice_order.absorb2.

tts_lemma coboundedI2:
  assumes "b ∈ U" and "c ∈ U" and "a ∈ U" and "b ≤ow c"
  shows "a *ow b ≤ow c"
    is semilattice_order.coboundedI2.

tts_lemma orderI:
  assumes "a ∈ U" and "b ∈ U" and "a = a *ow b"
  shows "a ≤ow b"
    is semilattice_order.orderI.

tts_lemma bounded_iff:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "(a ≤ow b *ow c) = (a ≤ow b ∧ a ≤ow c)"
    is semilattice_order.bounded_iff.

tts_lemma boundedI:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a ≤ow b" and "a ≤ow c"
  shows "a ≤ow b *ow c"
    is semilattice_order.boundedI.

tts_lemma orderE:
  assumes "a ∈ U" and "b ∈ U"  and "a ≤ow b" and "a = a *ow b ⟹ thesis"
  shows thesis
    is semilattice_order.orderE.

tts_lemma mono:
  assumes "a ∈ U"
    and "c ∈ U"
    and "b ∈ U"
    and "d ∈ U"
    and "a ≤ow c"
    and "b ≤ow d"
  shows "a *ow b ≤ow c *ow d"
    is semilattice_order.mono.

tts_lemma strict_boundedE:
  assumes "a ∈ U"
    and "b ∈ U"
    and "c ∈ U"
    and "a <ow b *ow c"
  obtains "a <ow b" and "a <ow c"
    given semilattice_order.strict_boundedE by auto

tts_lemma boundedE:
  assumes "a ∈ U"
    and "b ∈ U"
    and "c ∈ U"
    and "a ≤ow b *ow c"
  obtains "a ≤ow b" and "a ≤ow c"
    given semilattice_order.boundedE by auto

end

end

context semilattice_inf_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting semilattice_inf_ow_axioms
  eliminating through simp
begin

tts_lemma le_iff_inf:
  assumes "x ∈ U" and "y ∈ U"
  shows "(x ≤ow y) = (x ⊓ow y = x)"
    is semilattice_inf_class.le_iff_inf.
    
tts_lemma less_infI1:
  assumes "a ∈ U" and "x ∈ U" and "b ∈ U" and "a <ow x"
  shows "a ⊓ow b <ow x"
    is semilattice_inf_class.less_infI1.

tts_lemma less_infI2:
  assumes "b ∈ U" and "x ∈ U" and "a ∈ U" and "b <ow x"
  shows "a ⊓ow b <ow x"
    is semilattice_inf_class.less_infI2.

tts_lemma le_infI1:
  assumes "a ∈ U" and "x ∈ U" and "b ∈ U" and "a ≤ow x"
  shows "a ⊓ow b ≤ow x"
    is semilattice_inf_class.le_infI1.

tts_lemma le_infI2:
  assumes "b ∈ U" and "x ∈ U" and "a ∈ U" and "b ≤ow x"
  shows "a ⊓ow b ≤ow x"
    is semilattice_inf_class.le_infI2.

tts_lemma le_inf_iff:
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U"
  shows "(x ≤ow y ⊓ow z) = (x ≤ow y ∧ x ≤ow z)"
    is semilattice_inf_class.le_inf_iff.

tts_lemma le_infI:
  assumes "x ∈ U" and "a ∈ U" and "b ∈ U" and "x ≤ow a" and "x ≤ow b"
  shows "x ≤ow a ⊓ow b"
    is semilattice_inf_class.le_infI.

tts_lemma le_infE:
  assumes "x ∈ U"
    and "a ∈ U"
    and "b ∈ U"
    and "x ≤ow a ⊓ow b"
    and "⟦x ≤ow a; x ≤ow b⟧ ⟹ P"
  shows P
    is semilattice_inf_class.le_infE.

tts_lemma inf_mono:
  assumes "a ∈ U"
    and "c ∈ U"
    and "b ∈ U"
    and "d ∈ U"
    and "a ≤ow c"
    and "b ≤ow d"
  shows "a ⊓ow b ≤ow c ⊓ow d"
    is semilattice_inf_class.inf_mono.

end

end

context semilattice_sup_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting semilattice_sup_ow_axioms
  eliminating through simp
begin

tts_lemma le_iff_sup:
  assumes "x ∈ U" and "y ∈ U"
  shows "(x ≤ow y) = (x ⊔ow y = y)"
    is semilattice_sup_class.le_iff_sup.

tts_lemma less_supI1:
  assumes "x ∈ U" and "a ∈ U" and "b ∈ U" and "x <ow a"
  shows "x <ow a ⊔ow b"
    is semilattice_sup_class.less_supI1.

tts_lemma less_supI2:
  assumes "x ∈ U" and "b ∈ U" and "a ∈ U" and "x <ow b"
  shows "x <ow a ⊔ow b"
    is semilattice_sup_class.less_supI2.

tts_lemma le_supI1:
  assumes "x ∈ U" and "a ∈ U" and "b ∈ U" and "x ≤ow a"
  shows "x ≤ow a ⊔ow b"
    is semilattice_sup_class.le_supI1.

tts_lemma le_supI2:
  assumes "x ∈ U" and "b ∈ U" and "a ∈ U" and "x ≤ow b"
  shows "x ≤ow a ⊔ow b"
    is semilattice_sup_class.le_supI2.

tts_lemma le_sup_iff:
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U"
  shows "(x ⊔ow y ≤ow z) = (x ≤ow z ∧ y ≤ow z)"
    is semilattice_sup_class.le_sup_iff.

tts_lemma le_supI:
  assumes "a ∈ U" and "x ∈ U" and "b ∈ U" and "a ≤ow x" and "b ≤ow x"
  shows "a ⊔ow b ≤ow x"
    is semilattice_sup_class.le_supI.

tts_lemma le_supE:
  assumes "a ∈ U"
    and "b ∈ U"
    and "x ∈ U"
    and "a ⊔ow b ≤ow x"
    and "⟦a ≤ow x; b ≤ow x⟧ ⟹ P"
  shows P
    is semilattice_sup_class.le_supE.

tts_lemma sup_unique:
  assumes "∀x∈U. ∀y∈U. f x y ∈ U"
    and "x ∈ U"
    and "y ∈ U"
    and "⋀x y. ⟦x ∈ U; y ∈ U⟧ ⟹ x ≤ow f x y"
    and "⋀x y. ⟦x ∈ U; y ∈ U⟧ ⟹ y ≤ow f x y"
    and "⋀x y z. ⟦x ∈ U; y ∈ U; z ∈ U; y ≤ow x; z ≤ow x⟧ ⟹ f y z ≤ow x"
  shows "x ⊔ow y = f x y"
    is semilattice_sup_class.sup_unique.

tts_lemma sup_mono:
  assumes "a ∈ U"
    and "c ∈ U"
    and "b ∈ U"
    and "d ∈ U"
    and "a ≤ow c"
    and "b ≤ow d"
  shows "a ⊔ow b ≤ow c ⊔ow d"
    is semilattice_sup_class.sup_mono.

end

end



subsection‹Bounded semilattices›


subsubsection‹Definitions and common properties›

locale semilattice_neutral_ow = semilattice_ow U f + comm_monoid_ow U f z
  for U :: "'al set" and f z

locale semilattice_neutral_order_ow = 
  sl_neut: semilattice_neutral_ow U f z + 
  sl_ord: semilattice_order_ow U f le ls
  for U :: "'al set" and f z le ls 
begin

sublocale order_top_ow U ‹(≤ow)› ‹(<ow)› ‹1ow›
  apply unfold_locales
  subgoal by (auto simp: antisym sl_ord.strict_iff_order sl_ord.antisym)
  subgoal by (auto simp: sl_ord.order_iff)
  subgoal by (auto intro: sl_ord.trans)
  subgoal by (auto simp: sl_ord.antisym)
  subgoal by auto
  subgoal by (simp add: sl_ord.absorb_iff1)
  done

end

locale bounded_semilattice_inf_top_ow =
  semilattice_inf_ow U inf le ls + order_top_ow U le ls top
  for U :: "'al set" and inf le ls top 
begin

sublocale inf_top: semilattice_neutral_order_ow U ‹(⊓ow)› ‹⊤ow› ‹(≤ow)› ‹(<ow)›
  apply unfold_locales
  subgoal by simp
  subgoal using top_greatest by (simp add: inf.order_iff)
  done

end

locale bounded_semilattice_sup_bot_ow = 
  semilattice_sup_ow U sup le ls + order_bot_ow U bot le ls
  for U :: "'al set" and sup le ls bot
begin

sublocale sup_bot: semilattice_neutral_order_ow U ‹(⊔ow)› ‹⊥ow› ‹(≥ow)› ‹(>ow)›
  by unfold_locales (simp_all add: sup.absorb1)

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma semilattice_neutral_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (=))
      (semilattice_neutral_ow (Collect (Domainp A))) semilattice_neutr"
  unfolding semilattice_neutral_ow_def semilattice_neutr_def by transfer_prover
  
lemma semilattice_neutr_order_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      A ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (=)
    )
    (semilattice_neutral_order_ow (Collect (Domainp A))) 
    semilattice_neutr_order"
  unfolding semilattice_neutral_order_ow_def semilattice_neutr_order_def 
  by transfer_prover

lemma bounded_semilattice_inf_top_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      A ===> 
      (=)
    ) 
    (bounded_semilattice_inf_top_ow (Collect (Domainp A))) 
    class.bounded_semilattice_inf_top"
  unfolding
    bounded_semilattice_inf_top_ow_def class.bounded_semilattice_inf_top_def
  by transfer_prover

lemma bounded_semilattice_sup_bot_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      A ===> 
      (=)
    ) 
    (bounded_semilattice_sup_bot_ow (Collect (Domainp A))) 
    class.bounded_semilattice_sup_bot"
  unfolding
    bounded_semilattice_sup_bot_ow_def class.bounded_semilattice_sup_bot_def
  by transfer_prover

end

text‹\newpage›

end