Theory SML_Complete_Lattices

(* Title: Examples/SML_Relativization/Lattices/SML_Complete_Lattices.thy
   Author: Mihails Milehins
   Copyright 2021 (C) 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 (‹⨅ow›)
  assumes Inf_closed[simp]: "⨅ow ` Pow U ⊆ U"
begin

notation Inf (‹⨅ow›)

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

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 (‹⨅ow.1›)
notation Inf2 (‹⨅ow.2›)

end

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

notation Sup (‹⨆ow›)

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

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 (‹⨆ow.1›)
notation Sup2 (‹⨆ow.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 ⟧ ⟹ ⨅ow A ≤ow x"
    and Inf_greatest: 
      "⟦ A ⊆ U; z ∈ U; (⋀x. x ∈ A ⟹ z ≤ow x) ⟧ ⟹ z ≤ow ⨅ow A"
    and Sup_upper: "⟦ x ∈ A; A ⊆ U ⟧ ⟹ x ≤ow ⨆ow A"
    and Sup_least: 
      "⟦ A ⊆ U; z ∈ U; (⋀x. x ∈ A ⟹ x ≤ow z) ⟧ ⟹ ⨆ow A ≤ow z"
    and Inf_empty[simp]: "⨅ow {} = ⊤ow"
    and Sup_empty[simp]: "⨆ow {} = ⊥ow"
begin

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

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

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

end

locale complete_lattice_pair_ow = 
  cl1: complete_lattice_ow U1 Inf1 Sup1 inf1 le1 ls1 sup1 bot1 top1 + 
  cl2: complete_lattice_ow U2 Inf2 Sup2 inf2 le2 ls2 sup2 bot2 top2 
  for U1 :: "'al set" and Inf1 Sup1 inf1 le1 ls1 sup1 bot1 top1
    and U2 :: "'bl set" and Inf2 Sup2 inf2 le2 ls2 sup2 bot2 top2
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 "⨅ow {x..ow} = x"
  is complete_lattice_class.Inf_atLeast.
    
tts_lemma Inf_atMost:
  assumes "x ∈ U"
  shows "⨅ow {..owx} = ⊥ow"
    is complete_lattice_class.Inf_atMost.
    
tts_lemma Sup_atLeast:
  assumes "x ∈ U"
  shows "⨆ow {x..ow} = ⊤ow"
  is complete_lattice_class.Sup_atLeast.
    
tts_lemma Sup_atMost:
  assumes "y ∈ U"
  shows "⨆ow {..owy} = y"
    is complete_lattice_class.Sup_atMost.
    
tts_lemma Inf_insert:
  assumes "a ∈ U" and "A ⊆ U"
  shows "⨅ow (insert a A) = a ⊓ow ⨅ow A"
    is complete_lattice_class.Inf_insert.
    
tts_lemma Sup_insert:
  assumes "a ∈ U" and "A ⊆ U"
  shows "⨆ow (insert a A) = a ⊔ow ⨆ow A"
    is complete_lattice_class.Sup_insert.
    
tts_lemma Inf_atMostLessThan:
  assumes "x ∈ U" and "⊤ow <ow x"
  shows "⨅ow {..<owx} = ⊥ow"
    is complete_lattice_class.Inf_atMostLessThan.
    
tts_lemma Sup_greaterThanAtLeast:
  assumes "x ∈ U" and "x <ow ⊤ow"
  shows "⨆ow {x<ow..} = ⊤ow"
    is complete_lattice_class.Sup_greaterThanAtLeast.
    
tts_lemma le_Inf_iff:
  assumes "b ∈ U" and "A ⊆ U"
  shows "(b ≤ow ⨅ow A) = Ball A ((≤ow) b)"
    is complete_lattice_class.le_Inf_iff.
    
tts_lemma Sup_le_iff:
  assumes "A ⊆ U" and "b ∈ U"
  shows "(⨆ow A ≤ow b) = (∀x∈A. x ≤ow b)"
    is complete_lattice_class.Sup_le_iff.
    
tts_lemma Inf_atLeastLessThan:
  assumes "x ∈ U" and "y ∈ U" and "x <ow y"
  shows "⨅ow (on U with (≤ow) (<ow) : {x..<y}) = x"
    is complete_lattice_class.Inf_atLeastLessThan.
    
tts_lemma Sup_greaterThanAtMost:
  assumes "x ∈ U" and "y ∈ U" and "x <ow y"
  shows "⨆ow {x<ow..y} = y"
    is complete_lattice_class.Sup_greaterThanAtMost.
    
tts_lemma Inf_atLeastAtMost:
  assumes "x ∈ U" and "y ∈ U" and "x ≤ow y"
  shows "⨅ow {x..owy} = x"
is complete_lattice_class.Inf_atLeastAtMost.
    
tts_lemma Sup_atLeastAtMost:
  assumes "x ∈ U" and "y ∈ U" and "x ≤ow y"
  shows "⨆ow {x..owy} = y"
    is complete_lattice_class.Sup_atLeastAtMost.
    
tts_lemma Inf_lower2:
  assumes "A ⊆ U" and "v ∈ U" and "u ∈ A" and "u ≤ow v"
  shows "⨅ow A ≤ow v"
  is complete_lattice_class.Inf_lower2.
    
tts_lemma Sup_upper2:
  assumes "A ⊆ U" and "v ∈ U" and "u ∈ A" and "v ≤ow u"
  shows "v ≤ow ⨆ow A"
    is complete_lattice_class.Sup_upper2.
    
tts_lemma Inf_less_eq:
  assumes "A ⊆ U" and "u ∈ U" and "⋀v. v ∈ A ⟹ v ≤ow u" and "A ≠ {}"
  shows "⨅ow A ≤ow 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 ≤ow v" and "A ≠ {}"
  shows "u ≤ow ⨆ow 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 ≤ow x"
    and "⋀y. ⟦y ∈ U; ⋀z. z ∈ A ⟹ z ≤ow y⟧ ⟹ x ≤ow y"
  shows "⨆ow 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 ≤ow i"
    and "⋀y. ⟦y ∈ U; ⋀i. i ∈ A ⟹ y ≤ow i⟧ ⟹ y ≤ow x"
  shows "⨅ow A = x"
    given complete_lattice_class.Inf_eqI 
  by (simp add: subset_eq)

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

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

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

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

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

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

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

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

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

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

tts_lemma SUP_UNIV_bool_expand:
  assumes "range A ⊆ U"
  shows "⨆ow (range A) = A True ⊔ow 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 ((≤ow) a)"
  shows "⨆ow A ≤ow ⨆ow 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 ≤ow b"
  shows "⨅ow A ≤ow ⨅ow B"
    given complete_lattice_class.Inf_mono by simp

tts_lemma Sup_Inf_le:
  assumes "A ⊆ Pow U"
  shows "⨆ow 
    (
      ⨅ow ` {x. x ⊆ U ∧ (∃f∈{f. f ` Pow U ⊆ U}. x = f ` A ∧ (∀Y∈A. f Y ∈ Y))}
    ) ≤ow ⨅ow (⨆ow ` 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: "⨅ow U = ⊥ow"
    is complete_lattice_class.Inf_UNIV.

tts_lemma Sup_UNIV: "⨆ow U = ⊤ow"
    is complete_lattice_class.Sup_UNIV.

end

context 
  fixes U2 :: "'b set"
begin

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

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'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 ⊆ U2"
    and "u ∈ U"
    and "∀x∈U2. f x ∈ U"
    and "i ∈ A"
    and "u ≤ow f i"
  shows "u ≤ow ⨆ow (f ` A)"
  is complete_lattice_class.SUP_upper2.

tts_lemma INF_lower2:
  assumes "A ⊆ U2"
    and "∀x∈U2. f x ∈ U"
    and "u ∈ U"
    and "i ∈ A"
    and "f i ≤ow u"
  shows "⨅ow (f ` A) ≤ow u"
  is complete_lattice_class.INF_lower2.
    
tts_lemma less_INF_D:
  assumes "y ∈ U"
    and "∀x∈U2. f x ∈ U"
    and "A ⊆ U2"
    and "y <ow ⨅ow (f ` A)"
    and "i ∈ A"
  shows "y <ow f i"
  is complete_lattice_class.less_INF_D.
    
tts_lemma SUP_lessD:
  assumes "∀x∈U2. f x ∈ U"
    and "A ⊆ U2"
    and "y ∈ U"
    and "⨆ow (f ` A) <ow y"
    and "i ∈ A"
  shows "f i <ow y"
  is complete_lattice_class.SUP_lessD.

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

end

end

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'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 ⊆ U2"
    and "x ∈ U"
    and "∀x∈U2. f x ∈ U"
    and "⋀i. ⟦i ∈ U2; i ∈ A⟧ ⟹ x ≤ow f i"
    and "⋀y. ⟦y ∈ U; ⋀i. ⟦i ∈ U2; i ∈ A⟧ ⟹ y ≤ow f i⟧ ⟹ y ≤ow x"
  shows "⨅ow (f ` A) = x"
  is complete_lattice_class.INF_eqI.

end

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'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 ⊆ U2"
    and "∀x∈U2. f x ∈ U"
    and "x ∈ U"
    and "⋀i. ⟦i ∈ U2; i ∈ A⟧ ⟹ f i ≤ow x"
    and "⋀y. ⟦y ∈ U; ⋀i. ⟦i ∈ U2; i ∈ A⟧ ⟹ f i ≤ow y⟧ ⟹ x ≤ow y"
  shows "⨆ow (f ` A) = x"
    is complete_lattice_class.SUP_eqI.
    
end

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'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 ⊆ U2" and "∀x∈U2. f x ∈ U" and "A ≠ {}"
  shows "⨅ow (f ` A) ≤ow ⨆ow (f ` A)"
  is complete_lattice_class.INF_le_SUP.
    
tts_lemma INF_inf_const1:
  assumes "I ⊆ U2" and "x ∈ U" and "∀x∈U2. f x ∈ U" and "I ≠ {}"
  shows "⨅ow ((λi. x ⊓ow f i) ` I) = x ⊓ow ⨅ow (f ` I)"
    is complete_lattice_class.INF_inf_const1.
    
tts_lemma INF_inf_const2:
  assumes "I ⊆ U2" and "∀x∈U2. f x ∈ U" and "x ∈ U" and "I ≠ {}"
  shows "⨅ow ((λi. f i ⊓ow x) ` I) = ⨅ow (f ` I) ⊓ow x"
    is complete_lattice_class.INF_inf_const2.    

end

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'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 ⊆ U2" 
    and "∀x∈U2. f x ∈ U" 
    and "I ≠ {}"
    and "⋀i. i ∈ I ⟹ f i = x"
  shows "⨅ow (f ` I) = x"
    given complete_lattice_class.INF_eq_const
proof-
  assume 
    "⟦I ⊆ U2; ∀x∈U2. f x ∈ U; I ≠ {}; ⋀i. ⟦i ∈ U2; i ∈ I⟧ ⟹ f i = x⟧ ⟹ 
      ⨅ow (f ` I) = x"
    for I :: "'a set" and U2 f x
  then have 
    "⟦I ⊆ U2; ∀x∈U2. f x ∈ U; I ≠ {}; ⋀i. i ∈ I ⟹ f i = x⟧ ⟹ 
      ⨅ow (f ` I) = x"
    by presburger
  then show "⨅ow (f ` I) = x" using assms by simp
qed
    
tts_lemma SUP_eq_const:
  assumes "I ⊆ U2"
    and "∀x∈U2. f x ∈ U"
    and "I ≠ {}"
    and "⋀i. i ∈ I ⟹ f i = x"
  shows "⨆ow (f ` I) = x"
    given complete_lattice_class.SUP_eq_const
proof-
  assume 
    "⟦I ⊆ U2; ∀x∈U2. f x ∈ U; I ≠ {}; ⋀i. ⟦i ∈ U2; i ∈ I⟧ ⟹ f i = x⟧ ⟹ 
      ⨆ow (f ` I) = x"
    for I :: "'a set" and U2 f x
  then have 
    "⟦I ⊆ U2; ∀x∈U2. f x ∈ U; I ≠ {}; ⋀i. i ∈ I ⟹ f i = x⟧ ⟹ 
      ⨆ow (f ` I) = x"
    by presburger
  then show "⨆ow (f ` I) = x" using assms by simp
qed
    
tts_lemma SUP_eq_iff:
  assumes "I ⊆ U2"
    and "c ∈ U"
    and "∀x∈U2. f x ∈ U"
    and "I ≠ {}"
    and "⋀i. i ∈ I ⟹ c ≤ow f i"
  shows "(⨆ow (f ` I) = c) = (∀x∈I. f x = c)"
    given complete_lattice_class.SUP_eq_iff
proof-
  assume 
    "⟦
      I ⊆ U2; 
      c ∈ U; ∀x∈U2. f x ∈ U; 
      I ≠ {}; 
      ⋀i. ⟦i ∈ U2; i ∈ I⟧ ⟹ c ≤ow f i
    ⟧ ⟹  (⨆ow (f ` I) = c) = (∀x∈I. f x = c)"
    for I :: "'a set" and U2 c f
  then have 
    "⟦
      I ⊆ U2; 
      c ∈ U; ∀x∈U2. f x ∈ U; 
      I ≠ {}; 
      ⋀i. i ∈ I ⟹ c ≤ow f i
    ⟧ ⟹ (⨆ow (f ` I) = c) = (∀x∈I. f x = c)"
    by presburger
  then show "(⨆ow (f ` I) = c) = (∀x∈I. f x = c)" using assms by auto
qed
    
tts_lemma INF_eq_iff:
  assumes "I ⊆ U2"
    and "∀x∈U2. f x ∈ U"
    and "c ∈ U"
    and "I ≠ {}"
    and "⋀i. i ∈ I ⟹ f i ≤ow c"
  shows "(⨅ow (f ` I) = c) = (∀x∈I. f x = c)"
    given complete_lattice_class.INF_eq_iff
proof-
  assume 
    "⟦
      I ⊆ U2; 
      ∀x∈U2. f x ∈ U; c ∈ U; 
      I ≠ {}; 
      ⋀i. ⟦i ∈ U2; i ∈ I⟧ ⟹ f i ≤ow c
    ⟧ ⟹ (⨅ow (f ` I) = c) = (∀x∈I. f x = c)"
    for I :: "'a set" and U2 f c
  then have 
    "⟦
      I ⊆ U2; 
      ∀x∈U2. f x ∈ U; c ∈ U; 
      I ≠ {}; 
      ⋀i. i ∈ I ⟹ f i ≤ow c
    ⟧ ⟹ (⨅ow (f ` I) = c) = (∀x∈I. f x = c)"
    by presburger
  then show "(⨅ow (f ` I) = c) = (∀x∈I. f x = c)" using assms by auto
qed

end


context 
  fixes U2 :: "'b set"
begin

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

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'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∈U2. f x ∈ U" and "a ∈ U2" and "A ⊆ U2"
  shows "⨅ow (f ` insert a A) = f a ⊓ow ⨅ow (f ` A)"
  is complete_lattice_class.INF_insert.
    
tts_lemma SUP_insert:
  assumes "∀x∈U2. f x ∈ U" and "a ∈ U2" and "A ⊆ U2"
  shows "⨆ow (f ` insert a A) = f a ⊔ow ⨆ow (f ` A)"
    is complete_lattice_class.SUP_insert.
    
tts_lemma le_INF_iff:
  assumes "u ∈ U" and "∀x∈U2. f x ∈ U" and "A ⊆ U2"
  shows "(u ≤ow ⨅ow (f ` A)) = (∀x∈A. u ≤ow f x)"
  is complete_lattice_class.le_INF_iff.
    
tts_lemma INF_union:
  assumes "∀x∈U2. M x ∈ U" and "A ⊆ U2" and "B ⊆ U2"
  shows "⨅ow (M ` (A ∪ B)) = ⨅ow (M ` A) ⊓ow ⨅ow (M ` B)"
    is complete_lattice_class.INF_union.
    
tts_lemma SUP_union:
  assumes "∀x∈U2. M x ∈ U" and "A ⊆ U2" and "B ⊆ U2"
  shows "⨆ow (M ` (A ∪ B)) = ⨆ow (M ` A) ⊔ow ⨆ow (M ` B)"
  is complete_lattice_class.SUP_union.
    
tts_lemma SUP_bot_conv:
  assumes "∀x∈U2. B x ∈ U" and "A ⊆ U2"
  shows 
    "(⨆ow (B ` A) = ⊥ow) = (∀x∈A. B x = ⊥ow)"
    "(⊥ow = ⨆ow (B ` A)) = (∀x∈A. B x = ⊥ow)"
  is complete_lattice_class.SUP_bot_conv.
    
tts_lemma INF_top_conv:
  assumes "∀x∈U2. B x ∈ U" and "A ⊆ U2"
  shows 
    "(⨅ow (B ` A) = ⊤ow) = (∀x∈A. B x = ⊤ow)"
    "(⊤ow = ⨅ow (B ` A)) = (∀x∈A. B x = ⊤ow)"
  is complete_lattice_class.INF_top_conv.
    
tts_lemma SUP_upper:
  assumes "A ⊆ U2" and "∀x∈U2. f x ∈ U" and "i ∈ A"
  shows "f i ≤ow ⨆ow (f ` A)"
  is complete_lattice_class.SUP_upper.
    
tts_lemma INF_lower:
  assumes "A ⊆ U2" and "∀x∈U2. f x ∈ U" and "i ∈ A"
  shows "⨅ow (f ` A) ≤ow f i"
  is complete_lattice_class.INF_lower.

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

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

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

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

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

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

end

end

context 
  fixes f :: "'b ⇒ 'al" and U2 :: "'b set"
  assumes f[transfer_rule]: "∀x ∈ U2. f x = ⊥ow"
begin

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'b set›)
  sbterms: (‹Orderings.bot::?'a::complete_lattice› to ‹⊥ow›)
  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 ⊆ U2"
  shows "⨆ow (f ` A) = ⊥ow"
    is complete_lattice_class.SUP_bot[folded const_fun_def].

end

end

context 
  fixes f :: "'b ⇒ 'al" and U2 :: "'b set"
  assumes f[transfer_rule]: "∀x ∈ U2. f x = ⊤ow"
begin

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'b set›)
  sbterms: (‹Orderings.top::?'a::complete_lattice› to ‹⊤ow›)
  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 ⊆ U2"
  shows "⨅ow (f ` A) = ⊤ow"
  is complete_lattice_class.INF_top[folded const_fun_def].

end

end

context 
  fixes f :: "'b ⇒ 'al" and c and F and U2 :: "'b set"
  assumes c_closed[transfer_rule]: "c ∈ U"
  assumes f[transfer_rule]: "∀x ∈ U2. 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 ‹U2::'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 ⊆ U2"
  shows "⨅ow (f ` A) = (if A = {} then ⊤ow else c)"
    is complete_lattice_class.INF_constant[folded const_fun_def].

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

end

tts_context
  tts: (?'a to U) and (?'b to ‹U2::'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 ⊆ U2" and "A ≠ {}"
  shows "⨅ow ((λi. c) ` A) = c"
    is complete_lattice_class.INF_const.
    
tts_lemma SUP_const:
  assumes "A ⊆ U2" and "A ≠ {}"
  shows "⨆ow ((λ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 ‹U2::'b set›) and (?'c to ‹U3::'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 ⊆ U2"
    and "B ⊆ U3"
    and "∀x∈U2. f (x::'a) ∈ U"
    and "∀x∈U3. g x ∈ U"
    and "⋀i. i ∈ A ⟹ ∃x∈B. f i ≤ow g x"
    and "⋀j. j ∈ B ⟹ ∃x∈A. g j ≤ow f x"
  shows "⨆ow (f ` A) = ⨆ow (g ` B)"
    given complete_lattice_class.SUP_eq
proof-
  assume 
    "⟦
      A ⊆ U2; 
      B ⊆ U3; 
      ∀x∈U2. f x ∈ U; 
      ∀x∈U3. g x ∈ U; 
      ⋀i. ⟦i ∈ U2; i ∈ A⟧ ⟹ ∃x∈B. f i ≤ow g x; 
      ⋀j. ⟦j ∈ U3; j ∈ B⟧ ⟹ ∃x∈A. g j ≤ow f x
    ⟧ ⟹ ⨆ow (f ` A) = ⨆ow (g ` B)"
    for A :: "'a set" and U2 and B :: "'b set" and U3 f g
  then have
    "⟦
      A ⊆ U2; 
      B ⊆ U3; 
      ∀x∈U2. f x ∈ U; 
      ∀x∈U3. g x ∈ U; 
      ⋀i. i ∈ A ⟹ ∃x∈B. f i ≤ow g x; 
      ⋀j. j ∈ B ⟹ ∃x∈A. g j ≤ow f x
    ⟧ ⟹ ⨆ow (f ` A) = ⨆ow (g ` B)"
    by simp
  then show "⨆ow (f ` A) = ⨆ow (g ` B)" using assms by simp
qed

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

end

end

context complete_lattice_ow
begin

context 
  fixes U2 :: "'b set" and U3 :: "'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 ‹U2::'b set›) and (?'c to ‹U3::'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 "U2 ≠ {}"
    and "U3 ≠ {}"
    and "∀x∈U2. ∀y∈U3. f (x::'b) y ∈ U"
    and "B ⊆ U3"
    and "A ⊆ U2"
  shows "⨅ow ((λi. ⨅ow (f i ` B)) ` A) = ⨅ow ((λj. ⨅ow ((λi. f i j) ` A)) ` B)"
    is complete_lattice_class.INF_commute.
    
tts_lemma ne_SUP_commute:
  assumes "U2 ≠ {}"
    and "U3 ≠ {}"
    and "∀x∈U2. ∀y∈U3. f (x::'b) y ∈ U"
    and "B ⊆ U3"
    and "A ⊆ U2"
  shows "⨆ow ((λi. ⨆ow (f i ` B)) ` A) = ⨆ow ((λj. ⨆ow ((λi. f i j) ` A)) ` B)"
    is complete_lattice_class.SUP_commute.
    
tts_lemma ne_SUP_mono:
  assumes "U2 ≠ {}"
    and "U3 ≠ {}"
    and "A ⊆ U2"
    and "B ⊆ U3"
    and "∀x∈U2. f (x::'b) ∈ U"
    and "∀x∈U3. g x ∈ U"
    and "⋀n. ⟦n ∈ U2; n ∈ A⟧ ⟹ ∃x∈B. f n ≤ow g x"
  shows "⨆ow (f ` A) ≤ow ⨆ow (g ` B)"
    is complete_lattice_class.SUP_mono.
    
tts_lemma ne_INF_mono:
  assumes "U2 ≠ {}"
    and "U3 ≠ {}"
    and "B ⊆ U2"
    and "A ⊆ U3"
    and "∀x∈U3. f x ∈ U"
    and "∀x∈U2. g (x::'b) ∈ U"
    and "⋀m. ⟦m ∈ U2; m ∈ B⟧ ⟹ ∃x∈A. f x ≤ow g m"
  shows "⨅ow (f ` A) ≤ow ⨅ow (g ` B)"
    is complete_lattice_class.INF_mono.

end

end

lemma INF_commute:
  assumes "∀x∈U2. ∀y∈U3. f x y ∈ U" and "B ⊆ U3" and "A ⊆ U2" 
  shows 
    "⨅ow ((λx. ⨅ow (f x ` B)) ` A) = ⨅ow ((λj. ⨅ow ((λi. f i j) ` A)) ` B)"
proof(cases ‹U2 = {}›)
  case True then show ?thesis 
    using assms by (simp add: inf_top.sl_neut.neutral_map Inf_top_conv(2)) 
next
  case ne_U2: False show ?thesis
  proof(cases ‹U3 = {}›)
    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_U2 False assms show ?thesis by (rule ne_INF_commute)
  qed
qed

lemma SUP_commute:
  assumes "∀x∈U2. ∀y∈U3. f x y ∈ U" and "B ⊆ U3" and "A ⊆ U2"
  shows 
    "⨆ow ((λx. ⨆ow (f x ` B)) ` A) = ⨆ow ((λj. ⨆ow ((λi. f i j) ` A)) ` B)"
proof(cases ‹U2 = {}›)
  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_U2: False show ?thesis
  proof(cases ‹U3 = {}›)
    case True show ?thesis
    proof-
      from assms(2) have "B = {}" unfolding True by simp
      from assms(1) show ?thesis 
        unfolding ‹B = {}› 
        by (simp add: sup_bot.sl_neut.neutral_map Sup_bot_conv(1))
    qed
  next
    case False 
    from ne_U2 False assms show ?thesis by (rule ne_SUP_commute)
  qed
qed

lemma SUP_mono:
  assumes "A ⊆ U2" 
    and "B ⊆ U3" 
    and "∀x∈U2. f x ∈ U" 
    and "∀x∈U3. g x ∈ U"
    and "⋀n. n ∈ A ⟹ ∃m∈B. f n ≤ow g m" 
  shows "⨆ow (f ` A) ≤ow ⨆ow (g ` B)"
proof(cases ‹U2 = {}›)
  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_U2: False show ?thesis
  proof(cases ‹U3 = {}›)
    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_U2 False assms show ?thesis by (rule ne_SUP_mono)
  qed
qed

lemma INF_mono:
  assumes "B ⊆ U2" 
    and "A ⊆ U3" 
    and "∀x∈U3. f x ∈ U" 
    and "∀x∈U2. g x ∈ U"
    and "⋀m. m ∈ B ⟹ ∃n∈A. f n ≤ow g m" 
  shows "⨅ow (f ` A) ≤ow ⨅ow (g ` B)"
proof(cases ‹U2 = {}›)
  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_U2: False show ?thesis
  proof(cases ‹U3 = {}›)
    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_U2 False assms show ?thesis by (rule ne_INF_mono)
  qed                                                              
qed

end

context complete_lattice_pair_ow
begin

context 
  fixes U3 :: "'c set"
begin

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

end

end

text‹\newpage›

end