Theory SML_Lattices

(* Title: Examples/SML_Relativization/Lattices/SML_Lattices.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Relativization of the results about lattices›
theory SML_Lattices
  imports SML_Semilattices
begin



subsection‹Simple lattices›


subsubsection‹Definitions and common properties›

locale lattice_ow = 
  semilattice_inf_ow U inf le ls + semilattice_sup_ow U sup le ls 
  for U :: "'al set" and inf le ls sup

locale lattice_pair_ow = 
  lattice1: lattice_ow U1 inf1 le1 ls1 sup1 +
  lattice2: lattice_ow U2 inf2 le2 ls2 sup2
  for U1 :: "'al set" and inf1 le1 ls1 sup1
    and U2 :: "'bl set" and inf2 le2 ls2 sup2
begin

sublocale semilattice_inf_pair_ow ..
sublocale semilattice_sup_pair_ow ..

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma lattice_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> A) ===> 
      (=)
    )
    (lattice_ow (Collect (Domainp A))) class.lattice"
  unfolding class.lattice_def lattice_ow_def by transfer_prover
  
end


subsubsection‹Relativization›

context lattice_ow 
begin

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

tts_lemma inf_sup_aci:
  assumes "x ∈ U" and "y ∈ U"
  shows 
    "x ⊓ow y = y ⊓ow x"
    "z ∈ U ⟹ x ⊓ow y ⊓ow z = x ⊓ow (y ⊓ow z)"
    "z ∈ U ⟹ x ⊓ow (y ⊓ow z) = y ⊓ow (x ⊓ow z)"
    "x ⊓ow (x ⊓ow y) = x ⊓ow y"
    "x ⊔ow y = y ⊔ow x"
    "z ∈ U ⟹ x ⊔ow y ⊔ow z = x ⊔ow (y ⊔ow z)"
    "z ∈ U ⟹ x ⊔ow (y ⊔ow z) = y ⊔ow (x ⊔ow z)"
    "x ⊔ow (x ⊔ow y) = x ⊔ow y"
    is lattice_class.inf_sup_aci.
    
tts_lemma inf_sup_absorb:
  assumes "x ∈ U" and "y ∈ U"
  shows "x ⊓ow (x ⊔ow y) = x"
    is lattice_class.inf_sup_absorb.

tts_lemma sup_inf_absorb:
  assumes "x ∈ U" and "y ∈ U"
  shows "x ⊔ow (x ⊓ow y) = x"
    is lattice_class.sup_inf_absorb.
    
tts_lemma bdd_above_insert:
  assumes "a ∈ U" and "A ⊆ U"
  shows "local.bdd_above (insert a A) = local.bdd_above A"
    is lattice_class.bdd_above_insert.

tts_lemma bdd_below_insert:
  assumes "a ∈ U" and "A ⊆ U"
  shows "local.bdd_below (insert a A) = local.bdd_below A"
  is lattice_class.bdd_below_insert.
    
tts_lemma distrib_sup_le:
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U"
  shows "x ⊔ow (y ⊓ow z) ≤ow x ⊔ow y ⊓ow (x ⊔ow z)"
    is lattice_class.distrib_sup_le.

tts_lemma distrib_inf_le:
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U"
  shows "x ⊓ow y ⊔ow (x ⊓ow z) ≤ow x ⊓ow (y ⊔ow z)"
    is lattice_class.distrib_inf_le.

tts_lemma distrib_imp1:
  assumes "x ∈ U"
    and "y ∈ U"
    and "z ∈ U"
    and 
      "⋀x y z. ⟦x ∈ U; y ∈ U; z ∈ U⟧ ⟹ 
        x ⊓ow (y ⊔ow z) = x ⊓ow y ⊔ow (x ⊓ow z)"
  shows "x ⊔ow (y ⊓ow z) = x ⊔ow y ⊓ow (x ⊔ow z)"
    is lattice_class.distrib_imp1.

tts_lemma distrib_imp2:
  assumes "x ∈ U"
    and "y ∈ U"
    and "z ∈ U"
    and 
      "⋀x y z. ⟦x ∈ U; y ∈ U; z ∈ U⟧ ⟹ 
        x ⊔ow (y ⊓ow z) = x ⊔ow y ⊓ow (x ⊔ow z)"
  shows "x ⊓ow (y ⊔ow z) = x ⊓ow y ⊔ow (x ⊓ow z)"
    is lattice_class.distrib_imp2.

tts_lemma bdd_above_Un:
  assumes "A ⊆ U" and "B ⊆ U"
  shows "local.bdd_above (A ∪ B) = (local.bdd_above A ∧ local.bdd_above B)"
    is lattice_class.bdd_above_Un.

tts_lemma bdd_below_Un:
  assumes "A ⊆ U" and "B ⊆ U"
  shows "local.bdd_below (A ∪ B) = (local.bdd_below A ∧ local.bdd_below B)"
    is lattice_class.bdd_below_Un.

tts_lemma bdd_above_image_sup:
  assumes "range f ⊆ U" and "range g ⊆ U"
  shows "local.bdd_above ((λx. f x ⊔ow g x) ` A) = 
    (local.bdd_above (f ` A) ∧ local.bdd_above (g ` A))"
    is lattice_class.bdd_above_image_sup.

tts_lemma bdd_below_image_inf:
  assumes "range f ⊆ U" and "range g ⊆ U"
  shows "local.bdd_below ((λx. f x ⊓ow g x) ` A) = 
    (local.bdd_below (f ` A) ∧ local.bdd_below (g ` A))"
    is lattice_class.bdd_below_image_inf.

end

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

tts_lemma bdd_above_UN:
  assumes "U ≠ {}" and "range A ⊆ Pow U" and "finite I"
  shows "bdd_above (⋃ (A ` I)) = (∀x∈I. bdd_above (A x))"
    is lattice_class.bdd_above_UN .

tts_lemma bdd_below_UN:
  assumes "U ≠ {}" and "range A ⊆ Pow U" and "finite I"
  shows "local.bdd_below (⋃ (A ` I)) = (∀x∈I. local.bdd_below (A x))"
    is lattice_class.bdd_below_UN.
    
tts_lemma bdd_above_finite:
  assumes "U ≠ {}" and "A ⊆ U" and "finite A"
  shows "local.bdd_above A"
    is lattice_class.bdd_above_finite.

tts_lemma bdd_below_finite:
  assumes "U ≠ {}" and "A ⊆ U" and "finite A"
  shows "local.bdd_below A"
    is lattice_class.bdd_below_finite.

end

end



subsection‹Bounded lattices›


subsubsection‹Definitions and common properties›

locale bounded_lattice_bot_ow = 
  lattice_ow U inf le ls sup + order_bot_ow U bot le ls
  for U :: "'al set" and inf le ls sup bot
begin

sublocale bounded_semilattice_sup_bot_ow U ‹(⊔ow)› ‹(≤ow)› ‹(<ow)› ‹⊥ow› ..

end

locale bounded_lattice_bot_pair_ow = 
  blb1: bounded_lattice_bot_ow U1 inf1 le1 ls1 sup1 bot1 +
  blb2: bounded_lattice_bot_ow U2 inf2 le2 ls2 sup2 bot2
  for U1 :: "'al set" and inf1 le1 ls1 sup1 bot1
    and U2 :: "'bl set" and inf2 le2 ls2 sup2 bot2
begin

sublocale lattice_pair_ow ..
sublocale order_bot_pair_ow U1 bot1 le1 ls1 U2 bot2 le2 ls2 ..

end

locale bounded_lattice_top_ow = 
  lattice_ow U inf le ls sup + order_top_ow U le ls top
  for U :: "'al set" and inf le ls sup top 
begin

sublocale bounded_semilattice_inf_top_ow U ‹(⊓ow)› ‹(≤ow)› ‹(<ow)› ‹⊤ow› ..

end

locale bounded_lattice_top_pair_ow = 
  blb1: bounded_lattice_top_ow U1 inf1 le1 ls1 sup1 top1 +
  blb2: bounded_lattice_top_ow U2 inf2 le2 ls2 sup2 top2
  for U1 :: "'al set" and inf1 le1 ls1 sup1 top1
    and U2 :: "'bl set" and inf2 le2 ls2 sup2 top2
begin

sublocale lattice_pair_ow ..
sublocale order_top_pair_ow U1 le1 ls1 top1 U2 le2 ls2 top2 ..

end

locale bounded_lattice_ow = 
  lattice_ow U inf le ls sup + 
  order_bot_ow U bot le ls + 
  order_top_ow U le ls top
  for U :: "'al set" and inf le ls sup bot top
begin

sublocale bounded_lattice_bot_ow U ‹(⊓ow)› ‹(≤ow)› ‹(<ow)› ‹(⊔ow)› ‹⊥ow› ..
sublocale bounded_lattice_top_ow U ‹(⊓ow)› ‹(≤ow)› ‹(<ow)› ‹(⊔ow)› ‹⊤ow› ..

end

locale bounded_lattice_pair_ow = 
  bl1: bounded_lattice_ow U1 inf1 le1 ls1 sup1 bot1 top1 +
  bl2: bounded_lattice_ow U2 inf2 le2 ls2 sup2 bot2 top2
  for U1 :: "'al set" and inf1 le1 ls1 sup1 bot1 top1 
    and U2 :: "'bl set" and inf2 le2 ls2 sup2 bot2 top2
begin

sublocale bounded_lattice_bot_pair_ow ..
sublocale bounded_lattice_top_pair_ow ..

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma bounded_lattice_bot_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> A) ===> 
      A ===> 
      (=)
    ) 
    (bounded_lattice_bot_ow (Collect (Domainp A))) 
    class.bounded_lattice_bot"
  unfolding bounded_lattice_bot_ow_def class.bounded_lattice_bot_def
  by transfer_prover

lemma bounded_lattice_top_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "
    (
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> A) ===> 
      A ===> 
      (=)
    ) 
      (bounded_lattice_top_ow (Collect (Domainp A))) 
      class.bounded_lattice_top"
  unfolding bounded_lattice_top_ow_def class.bounded_lattice_top_def
  by transfer_prover

lemma bounded_lattice_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> (=)) ===> 
      (A ===> A ===> A) ===> 
      A ===> 
      A ===> 
      (=)
    ) 
    (bounded_lattice_ow (Collect (Domainp A))) class.bounded_lattice"
  unfolding bounded_lattice_ow_def class.bounded_lattice_def by transfer_prover

end


subsubsection‹Relativization›

context bounded_lattice_bot_ow
begin

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

tts_lemma inf_bot_left:
  assumes "x ∈ U"
  shows "⊥ow ⊓ow x = ⊥ow"
    is bounded_lattice_bot_class.inf_bot_left.

tts_lemma inf_bot_right:
  assumes "x ∈ U"
  shows "x ⊓ow ⊥ow = ⊥ow"
    is bounded_lattice_bot_class.inf_bot_right.

end

end

context bounded_lattice_top_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting bounded_lattice_top_ow_axioms and inf_top.sl_neut.not_empty
  applying [OF inf_closed' sup_closed' top_closed]
begin
    
tts_lemma sup_top_left:
  assumes "x ∈ U"
  shows "⊤ow ⊔ow x = ⊤ow"
    is bounded_lattice_top_class.sup_top_left.
    
tts_lemma sup_top_right:
  assumes "x ∈ U"
  shows "x ⊔ow ⊤ow = ⊤ow"
    is bounded_lattice_top_class.sup_top_right.
    
end

end

context bounded_lattice_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting bounded_lattice_ow_axioms 
  applying [OF sup_bot.sl_neut.not_empty, simplified]
begin

tts_lemma atLeastAtMost_eq_UNIV_iff:
  assumes "x ∈ U" and "y ∈ U"
  shows "({x..owy} = U) = (x = ⊥ow ∧ y = ⊤ow)"
    is bounded_lattice_class.atLeastAtMost_eq_UNIV_iff.

end

end



subsection‹Distributive lattices›


subsubsection‹Definitions and common properties›

locale distrib_lattice_ow =
  lattice_ow U inf le ls sup for U :: "'al set" and inf le ls sup  +
  assumes sup_inf_distrib1: 
    "⟦ x ∈ U; y ∈ U; z ∈ U ⟧ ⟹ x ⊔ow (y ⊓ow z) = (x ⊔ow y) ⊓ow (x ⊔ow z)"


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma distrib_lattice_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> (=)) ===>
      (A ===> A ===> (=)) ===>
      (A ===> A ===> A) ===> 
      (=)
    )
    (distrib_lattice_ow (Collect (Domainp A))) class.distrib_lattice"
  unfolding 
    distrib_lattice_ow_def class.distrib_lattice_def  
    class.distrib_lattice_axioms_def distrib_lattice_ow_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by simp
  
end


subsubsection‹Relativization›

context distrib_lattice_ow 
begin

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

tts_lemma inf_sup_distrib1:
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U"
  shows "x ⊓ow (y ⊔ow z) = x ⊓ow y ⊔ow (x ⊓ow z)"
  is distrib_lattice_class.inf_sup_distrib1.

tts_lemma inf_sup_distrib2:
  assumes "y ∈ U" and "z ∈ U" and "x ∈ U"
  shows "y ⊔ow z ⊓ow x = y ⊓ow x ⊔ow (z ⊓ow x)"
    is distrib_lattice_class.inf_sup_distrib2.

tts_lemma sup_inf_distrib2:
  assumes "y ∈ U" and "z ∈ U" and "x ∈ U"
  shows "y ⊓ow z ⊔ow x = y ⊔ow x ⊓ow (z ⊔ow x)"
    is distrib_lattice_class.sup_inf_distrib2.

end

end

text‹\newpage›

end