# Theory SML_Complete_Lattices

```(* Title: Examples/SML_Relativization/Lattices/SML_Complete_Lattices.thy
Author: Mihails Milehins
*)
section‹Relativization of the results about complete lattices›
theory SML_Complete_Lattices
imports SML_Lattices
begin

subsection‹Simple complete lattices›

subsubsection‹Definitions and common properties›

locale Inf_ow =
fixes U :: "'al set" and Inf (‹⨅⇩o⇩w›)
assumes Inf_closed[simp]: "⨅⇩o⇩w ` Pow U ⊆ U"
begin

notation Inf (‹⨅⇩o⇩w›)

lemma Inf_closed'[simp]: "∀x⊆U. ⨅⇩o⇩w x ∈ U" using Inf_closed by blast

end

locale Inf_pair_ow = Inf⇩1: Inf_ow U⇩1 Inf⇩1 + Inf⇩2: Inf_ow U⇩2 Inf⇩2
for U⇩1 :: "'al set" and Inf⇩1 and U⇩2 :: "'bl set" and Inf⇩2
begin

notation Inf⇩1 (‹⨅⇩o⇩w⇩.⇩1›)
notation Inf⇩2 (‹⨅⇩o⇩w⇩.⇩2›)

end

locale Sup_ow =
fixes U :: "'al set" and Sup (‹⨆⇩o⇩w›)
assumes Sup_closed[simp]: "⨆⇩o⇩w ` Pow U ⊆ U"
begin

notation Sup (‹⨆⇩o⇩w›)

lemma Sup_closed'[simp]: "∀x⊆U. ⨆⇩o⇩w x ∈ U" using Sup_closed by blast

end

locale Sup_pair_ow = Sup⇩1: Sup_ow U⇩1 Sup⇩1 + Sup⇩2: Sup_ow U⇩2 Sup⇩2
for U⇩1 :: "'al set" and Sup⇩1 and U⇩2 :: "'bl set" and Sup⇩2
begin

notation Sup⇩1 (‹⨆⇩o⇩w⇩.⇩1›)
notation Sup⇩2 (‹⨆⇩o⇩w⇩.⇩2›)

end

locale complete_lattice_ow =
lattice_ow U inf le ls sup +
Inf_ow U Inf +
Sup_ow U Sup +
bot_ow U bot +
top_ow U top
for U :: "'al set" and Inf  Sup inf le ls sup bot top +
assumes Inf_lower: "⟦ A ⊆ U; x ∈ A ⟧ ⟹ ⨅⇩o⇩w A ≤⇩o⇩w x"
and Inf_greatest:
"⟦ A ⊆ U; z ∈ U; (⋀x. x ∈ A ⟹ z ≤⇩o⇩w x) ⟧ ⟹ z ≤⇩o⇩w ⨅⇩o⇩w A"
and Sup_upper: "⟦ x ∈ A; A ⊆ U ⟧ ⟹ x ≤⇩o⇩w ⨆⇩o⇩w A"
and Sup_least:
"⟦ A ⊆ U; z ∈ U; (⋀x. x ∈ A ⟹ x ≤⇩o⇩w z) ⟧ ⟹ ⨆⇩o⇩w A ≤⇩o⇩w z"
and Inf_empty[simp]: "⨅⇩o⇩w {} = ⊤⇩o⇩w"
and Sup_empty[simp]: "⨆⇩o⇩w {} = ⊥⇩o⇩w"
begin

sublocale bounded_lattice_ow U ‹(⊓⇩o⇩w)› ‹(≤⇩o⇩w)› ‹(<⇩o⇩w)› ‹(⊔⇩o⇩w)› ‹⊥⇩o⇩w› ‹⊤⇩o⇩w›
apply standard
subgoal using Sup_least by force
subgoal using Inf_greatest by fastforce
done

tts_register_sbts ‹⊥⇩o⇩w› | U
proof-
assume ALA: "Domainp ALA = (λx. x ∈ U)"
have "Domainp ALA ⊥⇩o⇩w" unfolding ALA by simp
then obtain bot' where "ALA ⊥⇩o⇩w bot'" by blast
then show "∃bot'. ALA ⊥⇩o⇩w bot'" by auto
qed

tts_register_sbts ‹⊤⇩o⇩w› | U
proof-
assume ALA: "Domainp ALA = (λx. x ∈ U)"
have "Domainp ALA ⊤⇩o⇩w" unfolding ALA by simp
then obtain top' where "ALA ⊤⇩o⇩w top'" by blast
then show "∃top'. ALA ⊤⇩o⇩w top'" by auto
qed

end

locale complete_lattice_pair_ow =
cl⇩1: complete_lattice_ow U⇩1 Inf⇩1 Sup⇩1 inf⇩1 le⇩1 ls⇩1 sup⇩1 bot⇩1 top⇩1 +
cl⇩2: complete_lattice_ow U⇩2 Inf⇩2 Sup⇩2 inf⇩2 le⇩2 ls⇩2 sup⇩2 bot⇩2 top⇩2
for U⇩1 :: "'al set" and Inf⇩1 Sup⇩1 inf⇩1 le⇩1 ls⇩1 sup⇩1 bot⇩1 top⇩1
and U⇩2 :: "'bl set" and Inf⇩2 Sup⇩2 inf⇩2 le⇩2 ls⇩2 sup⇩2 bot⇩2 top⇩2
begin

sublocale bounded_lattice_pair_ow ..
sublocale Inf_pair_ow ..
sublocale Sup_pair_ow ..

end

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

lemma complete_lattice_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"(
(rel_set A ===> A) ===>
(rel_set A ===> A) ===>
(A ===> A ===> A) ===>
(A ===> A ===> (=)) ===>
(A ===> A ===> (=)) ===>
(A ===> A ===> A) ===>
A ===> A ===>
(=)
)
(complete_lattice_ow (Collect (Domainp A))) class.complete_lattice"
proof-
let ?P =
"(
(rel_set A ===> A) ===>
(rel_set A ===> A) ===>
(A ===> A ===> A) ===>
(A ===> A ===> (=)) ===>
(A ===> A ===> (=)) ===>
(A ===> A ===> A) ===>
A ===> A ===>
(=)
)"
let ?complete_lattice_ow = "(complete_lattice_ow (Collect (Domainp A)))"
let ?Inf_Sup_UNIV =
"(λF'::'b set ⇒ 'b. (F' ` Pow UNIV ⊆ UNIV))"
have rrng:
"((A2 ∧ A3 ∧ A4 ∧ A5 ∧ A1 ∧ A6 ∧ A7 ∧ A8 ∧ A9 ∧ A10 ∧ A11) = F') ⟹
((A1 ∧ A2 ∧ A3 ∧ A4 ∧ A5 ∧ A6 ∧ A7 ∧ A8 ∧ A9 ∧ A10 ∧ A11) = F')"
for A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 F'
by auto
have
"?P
?complete_lattice_ow
(
λInf Sup inf le ls sup bot top.
?Inf_Sup_UNIV Inf ∧ ?Inf_Sup_UNIV Sup ∧ bot ∈ UNIV ∧ top ∈ UNIV ∧
class.complete_lattice Inf Sup inf le ls sup bot top
)"
unfolding
complete_lattice_ow_def class.complete_lattice_def
complete_lattice_ow_axioms_def class.complete_lattice_axioms_def
Inf_ow_def Sup_ow_def bot_ow_def top_ow_def
apply transfer_prover_start
apply transfer_step+
apply(simp, intro ext, rule rrng, intro arg_cong2[where f="(∧)"])
subgoal unfolding Ball_Collect by simp
subgoal unfolding Ball_Collect by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal unfolding Ball_Collect[symmetric] by auto
subgoal unfolding Ball_Collect[symmetric] by metis
subgoal unfolding Ball_Collect[symmetric] by auto
subgoal unfolding Ball_Collect[symmetric] by metis
subgoal by simp
subgoal by simp
done
then show ?thesis by simp
qed

end

subsubsection‹Relativization›

context complete_lattice_ow
begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating ‹?a ∈ ?A› and ‹?A ⊆ ?B› through auto
applying [OF Inf_closed' Sup_closed' inf_closed' sup_closed']
begin

tts_lemma Inf_atLeast:
assumes "x ∈ U"
shows "⨅⇩o⇩w {x..⇩o⇩w} = x"
is complete_lattice_class.Inf_atLeast.

tts_lemma Inf_atMost:
assumes "x ∈ U"
shows "⨅⇩o⇩w {..⇩o⇩wx} = ⊥⇩o⇩w"
is complete_lattice_class.Inf_atMost.

tts_lemma Sup_atLeast:
assumes "x ∈ U"
shows "⨆⇩o⇩w {x..⇩o⇩w} = ⊤⇩o⇩w"
is complete_lattice_class.Sup_atLeast.

tts_lemma Sup_atMost:
assumes "y ∈ U"
shows "⨆⇩o⇩w {..⇩o⇩wy} = y"
is complete_lattice_class.Sup_atMost.

tts_lemma Inf_insert:
assumes "a ∈ U" and "A ⊆ U"
shows "⨅⇩o⇩w (insert a A) = a ⊓⇩o⇩w ⨅⇩o⇩w A"
is complete_lattice_class.Inf_insert.

tts_lemma Sup_insert:
assumes "a ∈ U" and "A ⊆ U"
shows "⨆⇩o⇩w (insert a A) = a ⊔⇩o⇩w ⨆⇩o⇩w A"
is complete_lattice_class.Sup_insert.

tts_lemma Inf_atMostLessThan:
assumes "x ∈ U" and "⊤⇩o⇩w <⇩o⇩w x"
shows "⨅⇩o⇩w {..<⇩o⇩wx} = ⊥⇩o⇩w"
is complete_lattice_class.Inf_atMostLessThan.

tts_lemma Sup_greaterThanAtLeast:
assumes "x ∈ U" and "x <⇩o⇩w ⊤⇩o⇩w"
shows "⨆⇩o⇩w {x<⇩o⇩w..} = ⊤⇩o⇩w"
is complete_lattice_class.Sup_greaterThanAtLeast.

tts_lemma le_Inf_iff:
assumes "b ∈ U" and "A ⊆ U"
shows "(b ≤⇩o⇩w ⨅⇩o⇩w A) = Ball A ((≤⇩o⇩w) b)"
is complete_lattice_class.le_Inf_iff.

tts_lemma Sup_le_iff:
assumes "A ⊆ U" and "b ∈ U"
shows "(⨆⇩o⇩w A ≤⇩o⇩w b) = (∀x∈A. x ≤⇩o⇩w b)"
is complete_lattice_class.Sup_le_iff.

tts_lemma Inf_atLeastLessThan:
assumes "x ∈ U" and "y ∈ U" and "x <⇩o⇩w y"
shows "⨅⇩o⇩w (on U with (≤⇩o⇩w) (<⇩o⇩w) : {x..<y}) = x"
is complete_lattice_class.Inf_atLeastLessThan.

tts_lemma Sup_greaterThanAtMost:
assumes "x ∈ U" and "y ∈ U" and "x <⇩o⇩w y"
shows "⨆⇩o⇩w {x<⇩o⇩w..y} = y"
is complete_lattice_class.Sup_greaterThanAtMost.

tts_lemma Inf_atLeastAtMost:
assumes "x ∈ U" and "y ∈ U" and "x ≤⇩o⇩w y"
shows "⨅⇩o⇩w {x..⇩o⇩wy} = x"
is complete_lattice_class.Inf_atLeastAtMost.

tts_lemma Sup_atLeastAtMost:
assumes "x ∈ U" and "y ∈ U" and "x ≤⇩o⇩w y"
shows "⨆⇩o⇩w {x..⇩o⇩wy} = y"
is complete_lattice_class.Sup_atLeastAtMost.

tts_lemma Inf_lower2:
assumes "A ⊆ U" and "v ∈ U" and "u ∈ A" and "u ≤⇩o⇩w v"
shows "⨅⇩o⇩w A ≤⇩o⇩w v"
is complete_lattice_class.Inf_lower2.

tts_lemma Sup_upper2:
assumes "A ⊆ U" and "v ∈ U" and "u ∈ A" and "v ≤⇩o⇩w u"
shows "v ≤⇩o⇩w ⨆⇩o⇩w A"
is complete_lattice_class.Sup_upper2.

tts_lemma Inf_less_eq:
assumes "A ⊆ U" and "u ∈ U" and "⋀v. v ∈ A ⟹ v ≤⇩o⇩w u" and "A ≠ {}"
shows "⨅⇩o⇩w A ≤⇩o⇩w u"
given complete_lattice_class.Inf_less_eq by auto

tts_lemma less_eq_Sup:
assumes "A ⊆ U" and "u ∈ U" and "⋀v. v ∈ A ⟹ u ≤⇩o⇩w v" and "A ≠ {}"
shows "u ≤⇩o⇩w ⨆⇩o⇩w A"
given complete_lattice_class.less_eq_Sup by auto

tts_lemma Sup_eqI:
assumes "A ⊆ U"
and "x ∈ U"
and "⋀y. y ∈ A ⟹ y ≤⇩o⇩w x"
and "⋀y. ⟦y ∈ U; ⋀z. z ∈ A ⟹ z ≤⇩o⇩w y⟧ ⟹ x ≤⇩o⇩w y"
shows "⨆⇩o⇩w A = x"
given complete_lattice_class.Sup_eqI
by (simp add: Sup_least Sup_upper order.antisym)

tts_lemma Inf_eqI:
assumes "A ⊆ U"
and "x ∈ U"
and "⋀i. i ∈ A ⟹ x ≤⇩o⇩w i"
and "⋀y. ⟦y ∈ U; ⋀i. i ∈ A ⟹ y ≤⇩o⇩w i⟧ ⟹ y ≤⇩o⇩w x"
shows "⨅⇩o⇩w A = x"
given complete_lattice_class.Inf_eqI

tts_lemma Inf_union_distrib:
assumes "A ⊆ U" and "B ⊆ U"
shows "⨅⇩o⇩w (A ∪ B) = ⨅⇩o⇩w A ⊓⇩o⇩w ⨅⇩o⇩w B"
is complete_lattice_class.Inf_union_distrib.

tts_lemma Sup_union_distrib:
assumes "A ⊆ U" and "B ⊆ U"
shows "⨆⇩o⇩w (A ∪ B) = ⨆⇩o⇩w A ⊔⇩o⇩w ⨆⇩o⇩w B"
is complete_lattice_class.Sup_union_distrib.

tts_lemma Sup_inter_less_eq:
assumes "A ⊆ U" and "B ⊆ U"
shows "⨆⇩o⇩w (A ∩ B) ≤⇩o⇩w ⨆⇩o⇩w A ⊓⇩o⇩w ⨆⇩o⇩w B"
is complete_lattice_class.Sup_inter_less_eq.

tts_lemma less_eq_Inf_inter:
assumes "A ⊆ U" and "B ⊆ U"
shows "⨅⇩o⇩w A ⊔⇩o⇩w ⨅⇩o⇩w B ≤⇩o⇩w ⨅⇩o⇩w (A ∩ B)"
is complete_lattice_class.less_eq_Inf_inter.

tts_lemma Sup_subset_mono:
assumes "B ⊆ U" and "A ⊆ B"
shows "⨆⇩o⇩w A ≤⇩o⇩w ⨆⇩o⇩w B"
is complete_lattice_class.Sup_subset_mono.

tts_lemma Inf_superset_mono:
assumes "A ⊆ U" and "B ⊆ A"
shows "⨅⇩o⇩w A ≤⇩o⇩w ⨅⇩o⇩w B"
is complete_lattice_class.Inf_superset_mono.

tts_lemma Sup_bot_conv:
assumes "A ⊆ U"
shows
"(⨆⇩o⇩w A = ⊥⇩o⇩w) = (∀x∈A. x = ⊥⇩o⇩w)"
"(⊥⇩o⇩w = ⨆⇩o⇩w A) = (∀x∈A. x = ⊥⇩o⇩w)"
is complete_lattice_class.Sup_bot_conv.

tts_lemma Inf_top_conv:
assumes "A ⊆ U"
shows
"(⨅⇩o⇩w A = ⊤⇩o⇩w) = (∀x∈A. x = ⊤⇩o⇩w)"
"(⊤⇩o⇩w = ⨅⇩o⇩w A) = (∀x∈A. x = ⊤⇩o⇩w)"
is complete_lattice_class.Inf_top_conv.

tts_lemma Inf_le_Sup:
assumes "A ⊆ U" and "A ≠ {}"
shows "⨅⇩o⇩w A ≤⇩o⇩w ⨆⇩o⇩w A"
is complete_lattice_class.Inf_le_Sup.

tts_lemma INF_UNIV_bool_expand:
assumes "range A ⊆ U"
shows "⨅⇩o⇩w (range A) = A True ⊓⇩o⇩w A False"
is complete_lattice_class.INF_UNIV_bool_expand.

tts_lemma SUP_UNIV_bool_expand:
assumes "range A ⊆ U"
shows "⨆⇩o⇩w (range A) = A True ⊔⇩o⇩w A False"
is complete_lattice_class.SUP_UNIV_bool_expand.

tts_lemma Sup_mono:
assumes "A ⊆ U" and "B ⊆ U" and "⋀a. a ∈ A ⟹ Bex B ((≤⇩o⇩w) a)"
shows "⨆⇩o⇩w A ≤⇩o⇩w ⨆⇩o⇩w B"
given complete_lattice_class.Sup_mono by simp

tts_lemma Inf_mono:
assumes "B ⊆ U"
and "A ⊆ U"
and "⋀b. b ∈ B ⟹ ∃x∈A. x ≤⇩o⇩w b"
shows "⨅⇩o⇩w A ≤⇩o⇩w ⨅⇩o⇩w B"
given complete_lattice_class.Inf_mono by simp

tts_lemma Sup_Inf_le:
assumes "A ⊆ Pow U"
shows "⨆⇩o⇩w
(
⨅⇩o⇩w ` {x. x ⊆ U ∧ (∃f∈{f. f ` Pow U ⊆ U}. x = f ` A ∧ (∀Y∈A. f Y ∈ Y))}
) ≤⇩o⇩w ⨅⇩o⇩w (⨆⇩o⇩w ` A)"
is complete_lattice_class.Sup_Inf_le.

end

tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
applying [
OF Inf_closed' Sup_closed' inf_closed' sup_closed' bot_closed top_closed
]
begin

tts_lemma Inf_UNIV: "⨅⇩o⇩w U = ⊥⇩o⇩w"
is complete_lattice_class.Inf_UNIV.

tts_lemma Sup_UNIV: "⨆⇩o⇩w U = ⊤⇩o⇩w"
is complete_lattice_class.Sup_UNIV.

end

context
fixes U⇩2 :: "'b set"
begin

lemmas [transfer_rule] =
image_transfer[where ?'a='b]

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through (insert Sup_least, auto)
begin

tts_lemma SUP_upper2:
assumes "A ⊆ U⇩2"
and "u ∈ U"
and "∀x∈U⇩2. f x ∈ U"
and "i ∈ A"
and "u ≤⇩o⇩w f i"
shows "u ≤⇩o⇩w ⨆⇩o⇩w (f ` A)"
is complete_lattice_class.SUP_upper2.

tts_lemma INF_lower2:
assumes "A ⊆ U⇩2"
and "∀x∈U⇩2. f x ∈ U"
and "u ∈ U"
and "i ∈ A"
and "f i ≤⇩o⇩w u"
shows "⨅⇩o⇩w (f ` A) ≤⇩o⇩w u"
is complete_lattice_class.INF_lower2.

tts_lemma less_INF_D:
assumes "y ∈ U"
and "∀x∈U⇩2. f x ∈ U"
and "A ⊆ U⇩2"
and "y <⇩o⇩w ⨅⇩o⇩w (f ` A)"
and "i ∈ A"
shows "y <⇩o⇩w f i"
is complete_lattice_class.less_INF_D.

tts_lemma SUP_lessD:
assumes "∀x∈U⇩2. f x ∈ U"
and "A ⊆ U⇩2"
and "y ∈ U"
and "⨆⇩o⇩w (f ` A) <⇩o⇩w y"
and "i ∈ A"
shows "f i <⇩o⇩w y"
is complete_lattice_class.SUP_lessD.

tts_lemma SUP_le_iff:
assumes "∀x∈U⇩2. f x ∈ U" and "A ⊆ U⇩2" and "u ∈ U"
shows "(⨆⇩o⇩w (f ` A) ≤⇩o⇩w u) = (∀x∈A. f x ≤⇩o⇩w u)"
is complete_lattice_class.SUP_le_iff.

end

end

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through (auto dest: top_le)
begin

tts_lemma INF_eqI:
assumes "A ⊆ U⇩2"
and "x ∈ U"
and "∀x∈U⇩2. f x ∈ U"
and "⋀i. ⟦i ∈ U⇩2; i ∈ A⟧ ⟹ x ≤⇩o⇩w f i"
and "⋀y. ⟦y ∈ U; ⋀i. ⟦i ∈ U⇩2; i ∈ A⟧ ⟹ y ≤⇩o⇩w f i⟧ ⟹ y ≤⇩o⇩w x"
shows "⨅⇩o⇩w (f ` A) = x"
is complete_lattice_class.INF_eqI.

end

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through (auto simp: order.eq_iff)
begin

tts_lemma SUP_eqI:
assumes "A ⊆ U⇩2"
and "∀x∈U⇩2. f x ∈ U"
and "x ∈ U"
and "⋀i. ⟦i ∈ U⇩2; i ∈ A⟧ ⟹ f i ≤⇩o⇩w x"
and "⋀y. ⟦y ∈ U; ⋀i. ⟦i ∈ U⇩2; i ∈ A⟧ ⟹ f i ≤⇩o⇩w y⟧ ⟹ x ≤⇩o⇩w y"
shows "⨆⇩o⇩w (f ` A) = x"
is complete_lattice_class.SUP_eqI.

end

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through simp
begin

tts_lemma INF_le_SUP:
assumes "A ⊆ U⇩2" and "∀x∈U⇩2. f x ∈ U" and "A ≠ {}"
shows "⨅⇩o⇩w (f ` A) ≤⇩o⇩w ⨆⇩o⇩w (f ` A)"
is complete_lattice_class.INF_le_SUP.

tts_lemma INF_inf_const1:
assumes "I ⊆ U⇩2" and "x ∈ U" and "∀x∈U⇩2. f x ∈ U" and "I ≠ {}"
shows "⨅⇩o⇩w ((λi. x ⊓⇩o⇩w f i) ` I) = x ⊓⇩o⇩w ⨅⇩o⇩w (f ` I)"
is complete_lattice_class.INF_inf_const1.

tts_lemma INF_inf_const2:
assumes "I ⊆ U⇩2" and "∀x∈U⇩2. f x ∈ U" and "x ∈ U" and "I ≠ {}"
shows "⨅⇩o⇩w ((λi. f i ⊓⇩o⇩w x) ` I) = ⨅⇩o⇩w (f ` I) ⊓⇩o⇩w x"
is complete_lattice_class.INF_inf_const2.

end

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through auto
begin

tts_lemma INF_eq_const:
assumes "I ⊆ U⇩2"
and "∀x∈U⇩2. f x ∈ U"
and "I ≠ {}"
and "⋀i. i ∈ I ⟹ f i = x"
shows "⨅⇩o⇩w (f ` I) = x"
given complete_lattice_class.INF_eq_const
proof-
assume
"⟦I ⊆ U⇩2; ∀x∈U⇩2. f x ∈ U; I ≠ {}; ⋀i. ⟦i ∈ U⇩2; i ∈ I⟧ ⟹ f i = x⟧ ⟹
⨅⇩o⇩w (f ` I) = x"
for I :: "'a set" and U⇩2 f x
then have
"⟦I ⊆ U⇩2; ∀x∈U⇩2. f x ∈ U; I ≠ {}; ⋀i. i ∈ I ⟹ f i = x⟧ ⟹
⨅⇩o⇩w (f ` I) = x"
by presburger
then show "⨅⇩o⇩w (f ` I) = x" using assms by simp
qed

tts_lemma SUP_eq_const:
assumes "I ⊆ U⇩2"
and "∀x∈U⇩2. f x ∈ U"
and "I ≠ {}"
and "⋀i. i ∈ I ⟹ f i = x"
shows "⨆⇩o⇩w (f ` I) = x"
given complete_lattice_class.SUP_eq_const
proof-
assume
"⟦I ⊆ U⇩2; ∀x∈U⇩2. f x ∈ U; I ≠ {}; ⋀i. ⟦i ∈ U⇩2; i ∈ I⟧ ⟹ f i = x⟧ ⟹
⨆⇩o⇩w (f ` I) = x"
for I :: "'a set" and U⇩2 f x
then have
"⟦I ⊆ U⇩2; ∀x∈U⇩2. f x ∈ U; I ≠ {}; ⋀i. i ∈ I ⟹ f i = x⟧ ⟹
⨆⇩o⇩w (f ` I) = x"
by presburger
then show "⨆⇩o⇩w (f ` I) = x" using assms by simp
qed

tts_lemma SUP_eq_iff:
assumes "I ⊆ U⇩2"
and "c ∈ U"
and "∀x∈U⇩2. f x ∈ U"
and "I ≠ {}"
and "⋀i. i ∈ I ⟹ c ≤⇩o⇩w f i"
shows "(⨆⇩o⇩w (f ` I) = c) = (∀x∈I. f x = c)"
given complete_lattice_class.SUP_eq_iff
proof-
assume
"⟦
I ⊆ U⇩2;
c ∈ U; ∀x∈U⇩2. f x ∈ U;
I ≠ {};
⋀i. ⟦i ∈ U⇩2; i ∈ I⟧ ⟹ c ≤⇩o⇩w f i
⟧ ⟹  (⨆⇩o⇩w (f ` I) = c) = (∀x∈I. f x = c)"
for I :: "'a set" and U⇩2 c f
then have
"⟦
I ⊆ U⇩2;
c ∈ U; ∀x∈U⇩2. f x ∈ U;
I ≠ {};
⋀i. i ∈ I ⟹ c ≤⇩o⇩w f i
⟧ ⟹ (⨆⇩o⇩w (f ` I) = c) = (∀x∈I. f x = c)"
by presburger
then show "(⨆⇩o⇩w (f ` I) = c) = (∀x∈I. f x = c)" using assms by auto
qed

tts_lemma INF_eq_iff:
assumes "I ⊆ U⇩2"
and "∀x∈U⇩2. f x ∈ U"
and "c ∈ U"
and "I ≠ {}"
and "⋀i. i ∈ I ⟹ f i ≤⇩o⇩w c"
shows "(⨅⇩o⇩w (f ` I) = c) = (∀x∈I. f x = c)"
given complete_lattice_class.INF_eq_iff
proof-
assume
"⟦
I ⊆ U⇩2;
∀x∈U⇩2. f x ∈ U; c ∈ U;
I ≠ {};
⋀i. ⟦i ∈ U⇩2; i ∈ I⟧ ⟹ f i ≤⇩o⇩w c
⟧ ⟹ (⨅⇩o⇩w (f ` I) = c) = (∀x∈I. f x = c)"
for I :: "'a set" and U⇩2 f c
then have
"⟦
I ⊆ U⇩2;
∀x∈U⇩2. f x ∈ U; c ∈ U;
I ≠ {};
⋀i. i ∈ I ⟹ f i ≤⇩o⇩w c
⟧ ⟹ (⨅⇩o⇩w (f ` I) = c) = (∀x∈I. f x = c)"
by presburger
then show "(⨅⇩o⇩w (f ` I) = c) = (∀x∈I. f x = c)" using assms by auto
qed

end

context
fixes U⇩2 :: "'b set"
begin

lemmas [transfer_rule] =
image_transfer[where ?'a='b]

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through (auto simp: sup_bot.top_unique top_le intro: Sup_least)
begin

tts_lemma INF_insert:
assumes "∀x∈U⇩2. f x ∈ U" and "a ∈ U⇩2" and "A ⊆ U⇩2"
shows "⨅⇩o⇩w (f ` insert a A) = f a ⊓⇩o⇩w ⨅⇩o⇩w (f ` A)"
is complete_lattice_class.INF_insert.

tts_lemma SUP_insert:
assumes "∀x∈U⇩2. f x ∈ U" and "a ∈ U⇩2" and "A ⊆ U⇩2"
shows "⨆⇩o⇩w (f ` insert a A) = f a ⊔⇩o⇩w ⨆⇩o⇩w (f ` A)"
is complete_lattice_class.SUP_insert.

tts_lemma le_INF_iff:
assumes "u ∈ U" and "∀x∈U⇩2. f x ∈ U" and "A ⊆ U⇩2"
shows "(u ≤⇩o⇩w ⨅⇩o⇩w (f ` A)) = (∀x∈A. u ≤⇩o⇩w f x)"
is complete_lattice_class.le_INF_iff.

tts_lemma INF_union:
assumes "∀x∈U⇩2. M x ∈ U" and "A ⊆ U⇩2" and "B ⊆ U⇩2"
shows "⨅⇩o⇩w (M ` (A ∪ B)) = ⨅⇩o⇩w (M ` A) ⊓⇩o⇩w ⨅⇩o⇩w (M ` B)"
is complete_lattice_class.INF_union.

tts_lemma SUP_union:
assumes "∀x∈U⇩2. M x ∈ U" and "A ⊆ U⇩2" and "B ⊆ U⇩2"
shows "⨆⇩o⇩w (M ` (A ∪ B)) = ⨆⇩o⇩w (M ` A) ⊔⇩o⇩w ⨆⇩o⇩w (M ` B)"
is complete_lattice_class.SUP_union.

tts_lemma SUP_bot_conv:
assumes "∀x∈U⇩2. B x ∈ U" and "A ⊆ U⇩2"
shows
"(⨆⇩o⇩w (B ` A) = ⊥⇩o⇩w) = (∀x∈A. B x = ⊥⇩o⇩w)"
"(⊥⇩o⇩w = ⨆⇩o⇩w (B ` A)) = (∀x∈A. B x = ⊥⇩o⇩w)"
is complete_lattice_class.SUP_bot_conv.

tts_lemma INF_top_conv:
assumes "∀x∈U⇩2. B x ∈ U" and "A ⊆ U⇩2"
shows
"(⨅⇩o⇩w (B ` A) = ⊤⇩o⇩w) = (∀x∈A. B x = ⊤⇩o⇩w)"
"(⊤⇩o⇩w = ⨅⇩o⇩w (B ` A)) = (∀x∈A. B x = ⊤⇩o⇩w)"
is complete_lattice_class.INF_top_conv.

tts_lemma SUP_upper:
assumes "A ⊆ U⇩2" and "∀x∈U⇩2. f x ∈ U" and "i ∈ A"
shows "f i ≤⇩o⇩w ⨆⇩o⇩w (f ` A)"
is complete_lattice_class.SUP_upper.

tts_lemma INF_lower:
assumes "A ⊆ U⇩2" and "∀x∈U⇩2. f x ∈ U" and "i ∈ A"
shows "⨅⇩o⇩w (f ` A) ≤⇩o⇩w f i"
is complete_lattice_class.INF_lower.

tts_lemma INF_inf_distrib:
assumes "∀x∈U⇩2. f x ∈ U" and "A ⊆ U⇩2" and "∀x∈U⇩2. g x ∈ U"
shows "⨅⇩o⇩w (f ` A) ⊓⇩o⇩w ⨅⇩o⇩w (g ` A) = ⨅⇩o⇩w ((λa. f a ⊓⇩o⇩w g a) ` A)"
is complete_lattice_class.INF_inf_distrib.

tts_lemma SUP_sup_distrib:
assumes "∀x∈U⇩2. f x ∈ U" and "A ⊆ U⇩2" and "∀x∈U⇩2. g x ∈ U"
shows "⨆⇩o⇩w (f ` A) ⊔⇩o⇩w ⨆⇩o⇩w (g ` A) = ⨆⇩o⇩w ((λa. f a ⊔⇩o⇩w g a) ` A)"
is complete_lattice_class.SUP_sup_distrib.

tts_lemma SUP_subset_mono:
assumes "B ⊆ U⇩2"
and "∀x∈U⇩2. f x ∈ U"
and "∀x∈U⇩2. g x ∈ U"
and "A ⊆ B"
and "⋀x. x ∈ A ⟹ f x ≤⇩o⇩w g x"
shows "⨆⇩o⇩w (f ` A) ≤⇩o⇩w ⨆⇩o⇩w (g ` B)"
given complete_lattice_class.SUP_subset_mono
proof-
assume
"⟦
B ⊆ U⇩2;
∀x∈U⇩2. f x ∈ U;
∀x∈U⇩2. g x ∈ U;
A ⊆ B;
⋀x. ⟦x ∈ U⇩2; x ∈ A⟧ ⟹ f x ≤⇩o⇩w g x
⟧ ⟹ ⨆⇩o⇩w (f ` A) ≤⇩o⇩w ⨆⇩o⇩w (g ` B)"
for B :: "'b set" and f g A
then have
"⟦
B ⊆ U⇩2;
∀x∈U⇩2. f x ∈ U;
∀x∈U⇩2. g x ∈ U;
A ⊆ B;
⋀x. x ∈ A ⟹ f x ≤⇩o⇩w g x
⟧ ⟹ ⨆⇩o⇩w (f ` A) ≤⇩o⇩w ⨆⇩o⇩w (g ` B)"
by auto
then show "⨆⇩o⇩w (f ` A) ≤⇩o⇩w ⨆⇩o⇩w (g ` B)" using assms by blast
qed

tts_lemma INF_superset_mono:
assumes "A ⊆ U⇩2"
and "∀x∈U⇩2. f x ∈ U"
and "∀x∈U⇩2. g x ∈ U"
and "B ⊆ A"
and "⋀x. ⟦x ∈ U⇩2; x ∈ B⟧ ⟹ f x ≤⇩o⇩w g x"
shows "⨅⇩o⇩w (f ` A) ≤⇩o⇩w ⨅⇩o⇩w (g ` B)"
given complete_lattice_class.INF_superset_mono
proof-
assume
"⟦
A ⊆ U⇩2;
∀x∈U⇩2. f x ∈ U;
∀x∈U⇩2. g x ∈ U;
B ⊆ A;
⋀x. ⟦x ∈ U⇩2; x ∈ B⟧ ⟹ f x ≤⇩o⇩w g x
⟧ ⟹ ⨅⇩o⇩w (f ` A) ≤⇩o⇩w ⨅⇩o⇩w (g ` B)"
for A :: "'b set" and f g B
then have
"⟦
A ⊆ U⇩2;
∀x∈U⇩2. f x ∈ U;
∀x∈U⇩2. g x ∈ U;
B ⊆ A;
⋀x. x ∈ B ⟹ f x ≤⇩o⇩w g x
⟧ ⟹ ⨅⇩o⇩w (f ` A) ≤⇩o⇩w ⨅⇩o⇩w (g ` B)"
by auto
then show "⨅⇩o⇩w (f ` A) ≤⇩o⇩w ⨅⇩o⇩w (g ` B)" using assms by blast
qed

tts_lemma INF_absorb:
assumes "I ⊆ U⇩2" and "∀x∈U⇩2. A x ∈ U" and "k ∈ I"
shows "A k ⊓⇩o⇩w ⨅⇩o⇩w (A ` I) = ⨅⇩o⇩w (A ` I)"
is complete_lattice_class.INF_absorb.

tts_lemma SUP_absorb:
assumes "I ⊆ U⇩2" and "∀x∈U⇩2. A x ∈ U" and "k ∈ I"
shows "A k ⊔⇩o⇩w ⨆⇩o⇩w (A ` I) = ⨆⇩o⇩w (A ` I)"
is complete_lattice_class.SUP_absorb.

end

end

context
fixes f :: "'b ⇒ 'al" and U⇩2 :: "'b set"
assumes f[transfer_rule]: "∀x ∈ U⇩2. f x = ⊥⇩o⇩w"
begin

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
sbterms: (‹Orderings.bot::?'a::complete_lattice› to ‹⊥⇩o⇩w›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through simp
begin

tts_lemma SUP_bot:
assumes "A ⊆ U⇩2"
shows "⨆⇩o⇩w (f ` A) = ⊥⇩o⇩w"
is complete_lattice_class.SUP_bot[folded const_fun_def].

end

end

context
fixes f :: "'b ⇒ 'al" and U⇩2 :: "'b set"
assumes f[transfer_rule]: "∀x ∈ U⇩2. f x = ⊤⇩o⇩w"
begin

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
sbterms: (‹Orderings.top::?'a::complete_lattice› to ‹⊤⇩o⇩w›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through simp
begin

tts_lemma INF_top:
assumes "A ⊆ U⇩2"
shows "⨅⇩o⇩w (f ` A) = ⊤⇩o⇩w"
is complete_lattice_class.INF_top[folded const_fun_def].

end

end

context
fixes f :: "'b ⇒ 'al" and c and F and U⇩2 :: "'b set"
assumes c_closed[transfer_rule]: "c ∈ U"
assumes f[transfer_rule]: "∀x ∈ U⇩2. f x = c"
begin

tts_register_sbts ‹c› | U
proof-
assume ALC: "Domainp ALC = (λx. x ∈ U)"
have "Domainp ALC c" unfolding ALC by (simp add: c_closed)
then obtain c' where "ALC c c'" by blast
then show "∃c'. ALC c c'" by auto
qed

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
sbterms: (‹?c::?'a::complete_lattice› to ‹c›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through simp
begin

tts_lemma INF_constant:
assumes "A ⊆ U⇩2"
shows "⨅⇩o⇩w (f ` A) = (if A = {} then ⊤⇩o⇩w else c)"
is complete_lattice_class.INF_constant[folded const_fun_def].

tts_lemma SUP_constant:
assumes "A ⊆ U⇩2"
shows "⨆⇩o⇩w (f ` A) = (if A = {} then ⊥⇩o⇩w else c)"
is complete_lattice_class.SUP_constant[folded const_fun_def].

end

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›)
sbterms: (‹?f::?'a::complete_lattice› to ‹c›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating through simp
begin

tts_lemma INF_const:
assumes "A ⊆ U⇩2" and "A ≠ {}"
shows "⨅⇩o⇩w ((λi. c) ` A) = c"
is complete_lattice_class.INF_const.

tts_lemma SUP_const:
assumes "A ⊆ U⇩2" and "A ≠ {}"
shows "⨆⇩o⇩w ((λi. c) ` A) = c"
is complete_lattice_class.SUP_const.

end

end

end

context complete_lattice_ow
begin

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›) and (?'c to ‹U⇩3::'c set›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
eliminating ‹?U ≠ {}› through (force simp: subset_iff INF_top equals0D)
applying [
OF Inf_closed' Sup_closed' inf_closed' sup_closed' bot_closed top_closed
]
begin

tts_lemma SUP_eq:
assumes "A ⊆ U⇩2"
and "B ⊆ U⇩3"
and "∀x∈U⇩2. f (x::'a) ∈ U"
and "∀x∈U⇩3. g x ∈ U"
and "⋀i. i ∈ A ⟹ ∃x∈B. f i ≤⇩o⇩w g x"
and "⋀j. j ∈ B ⟹ ∃x∈A. g j ≤⇩o⇩w f x"
shows "⨆⇩o⇩w (f ` A) = ⨆⇩o⇩w (g ` B)"
given complete_lattice_class.SUP_eq
proof-
assume
"⟦
A ⊆ U⇩2;
B ⊆ U⇩3;
∀x∈U⇩2. f x ∈ U;
∀x∈U⇩3. g x ∈ U;
⋀i. ⟦i ∈ U⇩2; i ∈ A⟧ ⟹ ∃x∈B. f i ≤⇩o⇩w g x;
⋀j. ⟦j ∈ U⇩3; j ∈ B⟧ ⟹ ∃x∈A. g j ≤⇩o⇩w f x
⟧ ⟹ ⨆⇩o⇩w (f ` A) = ⨆⇩o⇩w (g ` B)"
for A :: "'a set" and U⇩2 and B :: "'b set" and U⇩3 f g
then have
"⟦
A ⊆ U⇩2;
B ⊆ U⇩3;
∀x∈U⇩2. f x ∈ U;
∀x∈U⇩3. g x ∈ U;
⋀i. i ∈ A ⟹ ∃x∈B. f i ≤⇩o⇩w g x;
⋀j. j ∈ B ⟹ ∃x∈A. g j ≤⇩o⇩w f x
⟧ ⟹ ⨆⇩o⇩w (f ` A) = ⨆⇩o⇩w (g ` B)"
by simp
then show "⨆⇩o⇩w (f ` A) = ⨆⇩o⇩w (g ` B)" using assms by simp
qed

tts_lemma INF_eq:
assumes "A ⊆ U⇩2"
and "B ⊆ U⇩3"
and "∀x∈U⇩3. g x ∈ U"
and "∀x∈U⇩2. f (x::'a) ∈ U"
and "⋀i. i ∈ A ⟹ ∃x∈B. g x ≤⇩o⇩w f i"
and "⋀j. j ∈ B ⟹ ∃x∈A. f x ≤⇩o⇩w g j"
shows "⨅⇩o⇩w (f ` A) = ⨅⇩o⇩w (g ` B)"
given complete_lattice_class.INF_eq
proof-
assume
"⟦
A ⊆ U⇩2;
B ⊆ U⇩3;
∀x∈U⇩3. g x ∈ U;
∀x∈U⇩2. f x ∈ U;
⋀i. ⟦i ∈ U⇩2; i ∈ A⟧ ⟹ ∃x∈B. g x ≤⇩o⇩w f i;
⋀j. ⟦j ∈ U⇩3; j ∈ B⟧ ⟹ ∃x∈A. f x ≤⇩o⇩w g j
⟧ ⟹ ⨅⇩o⇩w (f ` A) = ⨅⇩o⇩w (g ` B)"
for A :: "'a set" and U⇩2 and B :: "'b set" and U⇩3 g f
then have
"⟦
A ⊆ U⇩2;
B ⊆ U⇩3;
∀x∈U⇩3. g x ∈ U;
∀x∈U⇩2. f x ∈ U;
⋀i. i ∈ A ⟹ ∃x∈B. g x ≤⇩o⇩w f i;
⋀j. j ∈ B ⟹ ∃x∈A. f x ≤⇩o⇩w g j
⟧ ⟹ ⨅⇩o⇩w (f ` A) = ⨅⇩o⇩w (g ` B)"
by simp
then show "⨅⇩o⇩w (f ` A) = ⨅⇩o⇩w (g ` B)" using assms by simp
qed

end

end

context complete_lattice_ow
begin

context
fixes U⇩2 :: "'b set" and U⇩3 :: "'c set"
begin

lemmas [transfer_rule] =
image_transfer[where ?'a='b]
image_transfer[where ?'a='c]

tts_context
tts: (?'a to U) and (?'b to ‹U⇩2::'b set›) and (?'c to ‹U⇩3::'c set›)
rewriting ctr_simps
substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty
applying [
OF _ _ Inf_closed' Sup_closed' inf_closed' sup_closed' bot_closed top_closed
]
begin

tts_lemma ne_INF_commute:
assumes "U⇩2 ≠ {}"
and "U⇩3 ≠ {}"
and "∀x∈U⇩2. ∀y∈U⇩3. f (x::'b) y ∈ U"
and "B ⊆ U⇩3"
and "A ⊆ U⇩2"
shows "⨅⇩o⇩w ((λi. ⨅⇩o⇩w (f i ` B)) ` A) = ⨅⇩o⇩w ((λj. ⨅⇩o⇩w ((λi. f i j) ` A)) ` B)"
is complete_lattice_class.INF_commute.

tts_lemma ne_SUP_commute:
assumes "U⇩2 ≠ {}"
and "U⇩3 ≠ {}"
and "∀x∈U⇩2. ∀y∈U⇩3. f (x::'b) y ∈ U"
and "B ⊆ U⇩3"
and "A ⊆ U⇩2"
shows "⨆⇩o⇩w ((λi. ⨆⇩o⇩w (f i ` B)) ` A) = ⨆⇩o⇩w ((λj. ⨆⇩o⇩w ((λi. f i j) ` A)) ` B)"
is complete_lattice_class.SUP_commute.

tts_lemma ne_SUP_mono:
assumes "U⇩2 ≠ {}"
and "U⇩3 ≠ {}"
and "A ⊆ U⇩2"
and "B ⊆ U⇩3"
and "∀x∈U⇩2. f (x::'b) ∈ U"
and "∀x∈U⇩3. g x ∈ U"
and "⋀n. ⟦n ∈ U⇩2; n ∈ A⟧ ⟹ ∃x∈B. f n ≤⇩o⇩w g x"
shows "⨆⇩o⇩w (f ` A) ≤⇩o⇩w ⨆⇩o⇩w (g ` B)"
is complete_lattice_class.SUP_mono.

tts_lemma ne_INF_mono:
assumes "U⇩2 ≠ {}"
and "U⇩3 ≠ {}"
and "B ⊆ U⇩2"
and "A ⊆ U⇩3"
and "∀x∈U⇩3. f x ∈ U"
and "∀x∈U⇩2. g (x::'b) ∈ U"
and "⋀m. ⟦m ∈ U⇩2; m ∈ B⟧ ⟹ ∃x∈A. f x ≤⇩o⇩w g m"
shows "⨅⇩o⇩w (f ` A) ≤⇩o⇩w ⨅⇩o⇩w (g ` B)"
is complete_lattice_class.INF_mono.

end

end

lemma INF_commute:
assumes "∀x∈U⇩2. ∀y∈U⇩3. f x y ∈ U" and "B ⊆ U⇩3" and "A ⊆ U⇩2"
shows
"⨅⇩o⇩w ((λx. ⨅⇩o⇩w (f x ` B)) ` A) = ⨅⇩o⇩w ((λj. ⨅⇩o⇩w ((λi. f i j) ` A)) ` B)"
proof(cases ‹U⇩2 = {}›)
case True then show ?thesis
using assms by (simp add: inf_top.sl_neut.neutral_map Inf_top_conv(2))
next
case ne_U⇩2: False show ?thesis
proof(cases ‹U⇩3 = {}›)
case True show ?thesis
proof-
from assms(2) have "B = {}" unfolding True by simp
from assms(1) show ?thesis
unfolding ‹B = {}› by (force intro: INF_top)
qed
next
case False
from ne_U⇩2 False assms show ?thesis by (rule ne_INF_commute)
qed
qed

lemma SUP_commute:
assumes "∀x∈U⇩2. ∀y∈U⇩3. f x y ∈ U" and "B ⊆ U⇩3" and "A ⊆ U⇩2"
shows
"⨆⇩o⇩w ((λx. ⨆⇩o⇩w (f x ` B)) ` A) = ⨆⇩o⇩w ((λj. ⨆⇩o⇩w ((λi. f i j) ` A)) ` B)"
proof(cases ‹U⇩2 = {}›)
case True show ?thesis
proof-
from assms(3) have "A = {}" unfolding True by simp
from assms(2) show ?thesis
unfolding ‹A = {}›
by (simp add: sup_bot.sl_neut.neutral_map inf_absorb1 SUP_bot)
qed
next
case ne_U⇩2: False show ?thesis
proof(cases ‹U⇩3 = {}›)
case True show ?thesis
proof-
from assms(2) have "B = {}" unfolding True by simp
from assms(1) show ?thesis
unfolding ‹B = {}›
qed
next
case False
from ne_U⇩2 False assms show ?thesis by (rule ne_SUP_commute)
qed
qed

lemma SUP_mono:
assumes "A ⊆ U⇩2"
and "B ⊆ U⇩3"
and "∀x∈U⇩2. f x ∈ U"
and "∀x∈U⇩3. g x ∈ U"
and "⋀n. n ∈ A ⟹ ∃m∈B. f n ≤⇩o⇩w g m"
shows "⨆⇩o⇩w (f ` A) ≤⇩o⇩w ⨆⇩o⇩w (g ` B)"
proof(cases ‹U⇩2 = {}›)
case True show ?thesis
proof-
from assms(1) have "A = {}" unfolding True by simp
have "f ` A = {}" unfolding ‹A = {}› by simp
from assms(2,4) show ?thesis
unfolding ‹f ` A = {}› by (simp add: image_subset_iff in_mono)
qed
next
case ne_U⇩2: False show ?thesis
proof(cases ‹U⇩3 = {}›)
case True show ?thesis
proof-
from assms(2) have "B = {}" unfolding True by simp
have "g ` B = {}" unfolding ‹B = {}› by simp
from assms(1,3,5) show ?thesis
unfolding ‹g ` B = {}› ‹B = {}› by (force simp: subset_iff)
qed
next
case False
from ne_U⇩2 False assms show ?thesis by (rule ne_SUP_mono)
qed
qed

lemma INF_mono:
assumes "B ⊆ U⇩2"
and "A ⊆ U⇩3"
and "∀x∈U⇩3. f x ∈ U"
and "∀x∈U⇩2. g x ∈ U"
and "⋀m. m ∈ B ⟹ ∃n∈A. f n ≤⇩o⇩w g m"
shows "⨅⇩o⇩w (f ` A) ≤⇩o⇩w ⨅⇩o⇩w (g ` B)"
proof(cases ‹U⇩2 = {}›)
case True show ?thesis
proof-
from assms(1) have "B = {}" unfolding True by simp
have "g ` B = {}" unfolding ‹B = {}› by simp
from assms(2,3) show ?thesis
unfolding ‹g ` B = {}› by (simp add: image_subset_iff in_mono)
qed
next
case ne_U⇩2: False show ?thesis
proof(cases ‹U⇩3 = {}›)
case True show ?thesis
proof-
from assms(2) have "A = {}" unfolding True by simp
have "f ` A = {}" unfolding ‹A = {}› by simp
from assms show ?thesis
unfolding ‹f ` A = {}› ‹A = {}› by (auto simp: subset_iff) fastforce
qed
next
case False from ne_U⇩2 False assms show ?thesis by (rule ne_INF_mono)
qed
qed

end

context complete_lattice_pair_ow
begin

context
fixes U⇩3 :: "'c set"
begin

lemmas [transfer_rule] =
image_transfer[where ?'a='c]

end

end

text‹\newpage›

end```