Theory Order_Lattice_Props_Loc

(* 
  Title: Locale-Based Duality
  Author: Georg Struth 
  Maintainer:Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Locale-Based Duality›

theory Order_Lattice_Props_Loc
  imports Main 
begin

unbundle lattice_syntax

text ‹This section explores order and lattice duality based on locales. Used within the context of a class or locale, 
this is very effective, though more opaque than the previous approach. Outside of such a context, however, it apparently
cannot be used for dualising theorems. Examples are properties of  functions between orderings or lattices.›

definition Fix :: "('a  'a)  'a set" where 
  "Fix f = {x. f x = x}"

context ord
begin

definition min_set :: "'a set  'a set" where 
 "min_set X = {y  X. x  X. x  y  x = y}"

definition max_set :: "'a set  'a set" where 
 "max_set X = {x  X. y  X. x  y  x = y}"

definition directed :: "'a set  bool" where
 "directed X = (Y. finite Y  Y  X  (x  X. y  Y. y  x))"

definition filtered :: "'a set  bool" where
 "filtered X = (Y. finite Y  Y  X  (x  X. y  Y. x  y))"

definition downset_set :: "'a set  'a set" ("") where
  "X = {y. x  X. y  x}"

definition upset_set :: "'a set  'a set" ("") where
 "X = {y. x  X. x  y}"

definition downset :: "'a  'a set" ("") where 
  " =   (λx. {x})"

definition upset :: "'a  'a set" ("") where 
  " =   (λx. {x})"

definition downsets :: "'a set set" where  
  "downsets = Fix "
 
definition upsets :: "'a set set" where
  "upsets = Fix "

abbreviation "downset_setp X  X  downsets"

abbreviation "upset_setp X  X  upsets"

definition ideals :: "'a set set" where
  "ideals = {X. X  {}  downset_setp X  directed X}"

definition filters :: "'a  set set" where
  "filters = {X. X  {}  upset_setp X  filtered X}"

abbreviation "idealp X  X  ideals"

abbreviation "filterp X  X  filters"

end

abbreviation Sup_pres :: "('a::Sup  'b::Sup)  bool" where
  "Sup_pres f  f  Sup = Sup  (`) f"

abbreviation Inf_pres :: "('a::Inf  'b::Inf)  bool" where
  "Inf_pres f  f  Inf = Inf  (`) f"

abbreviation sup_pres :: "('a::sup  'b::sup)  bool" where
  "sup_pres f  (x y. f (x  y) = f x  f y)"

abbreviation inf_pres :: "('a::inf  'b::inf)  bool" where
 "inf_pres f  (x y. f (x  y) = f x  f y)"

abbreviation bot_pres :: "('a::bot  'b::bot)  bool" where
  "bot_pres f  f  = "

abbreviation top_pres :: "('a::top  'b::top)  bool" where
  "top_pres f  f  = "

abbreviation Sup_dual :: "('a::Sup  'b::Inf)  bool" where
  "Sup_dual f  f  Sup = Inf  (`) f"

abbreviation Inf_dual :: "('a::Inf  'b::Sup)  bool" where
  "Inf_dual f  f  Inf = Sup  (`) f"

abbreviation sup_dual :: "('a::sup  'b::inf)  bool" where
  "sup_dual f  (x y. f (x  y) = f x  f y)"

abbreviation inf_dual :: "('a::inf  'b::sup)  bool" where
 "inf_dual f  (x y. f (x  y) = f x  f y)"

abbreviation bot_dual :: "('a::bot  'b::top)  bool" where 
 "bot_dual f  f  = "

abbreviation top_dual :: "('a::top  'b::bot)  bool" where 
  "top_dual f  f  = "


subsection ‹Duality via Locales›

sublocale ord  dual_ord: ord "(≥)" "(>)"
  rewrites dual_max_set: "max_set = dual_ord.min_set"
  and dual_filtered: "filtered = dual_ord.directed"
  and dual_upset_set: "upset_set = dual_ord.downset_set"
  and dual_upset: "upset = dual_ord.downset"
  and dual_upsets: "upsets = dual_ord.downsets"
  and dual_filters: "filters = dual_ord.ideals"
       apply unfold_locales
  unfolding max_set_def ord.min_set_def fun_eq_iff apply blast
  unfolding filtered_def ord.directed_def apply simp 
  unfolding upset_set_def ord.downset_set_def apply simp
  apply (simp add: ord.downset_def ord.downset_set_def ord.upset_def ord.upset_set_def)
  unfolding upsets_def ord.downsets_def apply (metis ord.downset_set_def upset_set_def)
  unfolding filters_def ord.ideals_def Fix_def ord.downsets_def upsets_def ord.downset_set_def upset_set_def ord.directed_def filtered_def
  by simp

sublocale preorder  dual_preorder: preorder "(≥)" "(>)"
  apply unfold_locales
  apply (simp add: less_le_not_le)
  apply simp
  using order_trans by blast

sublocale order  dual_order: order "(≥)" "(>)"
  by (unfold_locales, simp)

sublocale lattice  dual_lattice: lattice sup "(≥)" "(>)" inf
  by (unfold_locales, simp_all)

sublocale bounded_lattice  dual_bounded_lattice: bounded_lattice sup "(≥)" "(>)" inf  
  by (unfold_locales, simp_all)

sublocale boolean_algebra  dual_boolean_algebra: boolean_algebra "λx y. x  -y" uminus sup "(≥)" "(>)" inf  
  by (unfold_locales, simp_all add: inf_sup_distrib1)

sublocale complete_lattice  dual_complete_lattice: complete_lattice Sup Inf sup "(≥)" "(>)" inf  
  rewrites dual_gfp: "gfp = dual_complete_lattice.lfp"  
proof-
  show "class.complete_lattice Sup Inf sup (≥) (>) inf  "
    by (unfold_locales, simp_all add: Sup_upper Sup_least Inf_lower Inf_greatest)
  then interpret dual_complete_lattice: complete_lattice Sup Inf sup "(≥)" "(>)" inf  .
  show "gfp = dual_complete_lattice.lfp"  
    unfolding gfp_def dual_complete_lattice.lfp_def fun_eq_iff by simp
qed

context ord
begin

lemma dual_min_set: "min_set = dual_ord.max_set"
  by (simp add: dual_ord.dual_max_set)

lemma dual_directed: "directed = dual_ord.filtered"
  by (simp add:dual_ord.dual_filtered)

lemma dual_downset: "downset = dual_ord.upset"
  by (simp add: dual_ord.dual_upset)

lemma dual_downset_set: "downset_set = dual_ord.upset_set"
  by (simp add: dual_ord.dual_upset_set)

lemma dual_downsets: "downsets = dual_ord.upsets"
  by (simp add: dual_ord.dual_upsets)

lemma dual_ideals: "ideals = dual_ord.filters"
  by (simp add: dual_ord.dual_filters)

end

context complete_lattice
begin

lemma dual_lfp: "lfp = dual_complete_lattice.gfp"
  by (simp add: dual_complete_lattice.dual_gfp)

end

subsection ‹Properties of Orderings, Again›

context ord
begin

lemma directed_nonempty: "directed X  X  {}"
  unfolding directed_def by fastforce

lemma directed_ub: "directed X  (x  X. y  X. z  X. x  z  y  z)"
  by (meson empty_subsetI directed_def finite.emptyI finite_insert insert_subset order_refl)

lemma downset_set_prop: " = Union  (`) "
  unfolding downset_set_def downset_def fun_eq_iff by fastforce

lemma downset_set_prop_var: "X = (x  X. x)"
  by (simp add: downset_set_prop)

lemma downset_prop: "x = {y. y  x}"
  unfolding downset_def downset_set_def fun_eq_iff comp_def by fastforce

end

context preorder
begin

lemma directed_prop: "X  {}  (x  X. y  X. z  X. x  z  y  z)  directed X"
proof-
  assume h1: "X  {}"
  and h2: "x  X. y  X. z  X. x  z  y  z"
  {fix Y
  have "finite Y  Y  X  (x  X. y  Y. y  x)"
  proof (induct rule: finite_induct)
    case empty
    then show ?case
      using h1 by blast 
  next
    case (insert x F)
    then show ?case
      by (metis h2 insert_iff insert_subset order_trans) 
  qed}
  thus ?thesis
    by (simp add: directed_def)
qed

lemma directed_alt: "directed X = (X  {}  (x  X. y  X. z  X. x  z  y  z))"
  by (metis directed_prop directed_nonempty directed_ub)

lemma downset_set_ext: "id  "
  unfolding le_fun_def id_def downset_set_def by auto 

lemma downset_set_iso: "mono "
  unfolding mono_def downset_set_def by blast

lemma downset_set_idem [simp]: "   = "
  unfolding fun_eq_iff downset_set_def comp_def using order_trans by auto

lemma downset_faithful: "x  y  x  y"
  by (simp add: downset_prop subset_eq)

lemma downset_iso_iff: "(x  y) = (x  y)"
  using atMost_iff downset_prop order_trans by blast

lemma downset_directed_downset_var [simp]: "directed (X) = directed X"
proof
  assume h1: "directed X"
  {fix Y
  assume h2: "finite Y" and h3: "Y  X"
  hence "y. x. y  Y  x  X   y  x"
    by (force simp: downset_set_def)
  hence "f. y. y  Y   f y  X  y  f y"
    by (rule choice)
  hence "f. finite (f ` Y)  f ` Y  X  (y  Y. y  f y)"
    by (metis finite_imageI h2 image_subsetI)
  hence "Z. finite Z  Z  X  (y  Y.  z  Z. y  z)"
    by fastforce
  hence "Z. finite Z  Z  X  (y  Y.  z  Z. y  z)  (x  X.  z  Z. z  x)"
    by (metis directed_def h1)
  hence "x  X. y  Y. y  x"
    by (meson order_trans)}
  thus "directed (X)"
    unfolding directed_def downset_set_def by fastforce
next 
  assume "directed (X)"
  thus "directed X"
    unfolding directed_def downset_set_def 
    apply clarsimp
    by (smt (verit) Ball_Collect order_refl order_trans subsetCE)
qed

lemma downset_directed_downset [simp]: "directed   = directed"
  unfolding fun_eq_iff comp_def by simp

lemma directed_downset_ideals: "directed (X) = (X  ideals)"
  by (metis (mono_tags, lifting) Fix_def comp_apply directed_alt downset_set_idem downsets_def ideals_def mem_Collect_eq)

end

lemma downset_iso: "mono (::'a::order  'a set)"
  by (simp add: downset_iso_iff mono_def)

context order
begin

lemma downset_inj: "inj "
  by (metis injI downset_iso_iff order.eq_iff)

end

context lattice
begin

lemma lat_ideals: "X  ideals = (X  {}  X  downsets  (x  X.  y  X. x  y  X))"
  unfolding ideals_def directed_alt downsets_def Fix_def downset_set_def 
  using local.sup.bounded_iff by blast

end

context bounded_lattice
begin

lemma bot_ideal: "X  ideals    X"
  unfolding ideals_def downsets_def Fix_def downset_set_def by fastforce

end

context complete_lattice
begin

lemma Sup_downset_id [simp]: "Sup   = id"
  using Sup_atMost atMost_def downset_prop by fastforce

lemma downset_Sup_id: "id    Sup"
  by (simp add: Sup_upper downset_prop le_funI subsetI)

lemma Inf_Sup_var: "(x  X. x) = X"
  unfolding downset_prop by (simp add: Collect_ball_eq Inf_eq_Sup)

lemma Inf_pres_downset_var: "(x  X. x) = (X)"
  unfolding downset_prop by (safe, simp_all add: le_Inf_iff)

end

lemma lfp_in_Fix: 
  fixes f :: "'a::complete_lattice  'a"
  shows "mono f  lfp f  Fix f"
  using Fix_def lfp_unfold by fastforce

lemma gfp_in_Fix: 
  fixes f :: "'a::complete_lattice  'a"
  shows "mono f  gfp f  Fix f"
  using Fix_def gfp_unfold by fastforce

lemma nonempty_Fix: 
  fixes f :: "'a::complete_lattice  'a"
  shows "mono f  Fix f  {}"
  using lfp_in_Fix by fastforce


subsection ‹Dual Properties of Orderings from Locales›

text ‹These properties can be proved very smoothly overall. But only within the context of a class
or locale!›

context ord
begin

lemma filtered_nonempty: "filtered X  X  {}"
  by (simp add: dual_filtered dual_ord.directed_nonempty)

lemma filtered_lb: "filtered X  (x  X. y  X. z  X. z  x  z  y)"
  by (simp add: dual_filtered dual_ord.directed_ub)

lemma upset_set_prop: " = Union  (`) "
  by (simp add: dual_ord.downset_set_prop dual_upset dual_upset_set)

lemma upset_set_prop_var: "X = (x  X. x)"
  by (simp add: dual_ord.downset_set_prop_var dual_upset dual_upset_set)

lemma upset_prop: "x = {y. x  y}"
  by (simp add: dual_ord.downset_prop dual_upset)

end

context preorder
begin

lemma filtered_prop: "X  {}  (x  X. y  X. z  X. z  x  z  y)  filtered X"
  by (simp add: dual_filtered dual_preorder.directed_prop)

lemma filtered_alt: "filtered X = (X  {}  (x  X. y  X. z  X. z  x  z  y))"
  by (simp add: dual_filtered dual_preorder.directed_alt)

lemma upset_set_ext: "id  "
  by (simp add: dual_preorder.downset_set_ext dual_upset_set)

lemma upset_set_anti: "mono "
  by (simp add: dual_preorder.downset_set_iso dual_upset_set) 

lemma up_set_idem [simp]: "   = "
  by (simp add: dual_upset_set)

lemma upset_faithful: "x  y  y  x"
  by (metis dual_preorder.downset_faithful dual_upset)

lemma upset_anti_iff: "(y  x) = (x  y)"
  by (simp add: dual_preorder.downset_iso_iff dual_upset)

lemma upset_filtered_upset [simp]: "filtered   = filtered"
  by (simp add: dual_filtered dual_upset_set)

lemma filtered_upset_filters: "filtered (X) = (X  filters)"
  using dual_filtered dual_preorder.directed_downset_ideals dual_upset_set ord.dual_filters by fastforce

end

context order
begin

lemma upset_inj: "inj "
  by (simp add: dual_order.downset_inj dual_upset)

end

context lattice
begin

lemma lat_filters: "X  filters = (X  {}  X  upsets  (x  X.  y  X. x  y  X))"
  by (simp add: dual_filters dual_lattice.lat_ideals dual_ord.downsets_def dual_upset_set upsets_def)

end

context bounded_lattice
begin

lemma top_filter: "X  filters    X"
  by (simp add: dual_bounded_lattice.bot_ideal dual_filters)

end

context complete_lattice
begin

lemma Inf_upset_id [simp]: "Inf   = id"
  by (simp add:  dual_upset)

lemma upset_Inf_id: "id    Inf"
  by (simp add: dual_complete_lattice.downset_Sup_id dual_upset)

lemma Sup_Inf_var: " (x  X. x) = X"
  by (simp add: dual_complete_lattice.Inf_Sup_var dual_upset)

lemma Sup_dual_upset_var: "(x  X. x) = (X)"
  by (simp add: dual_complete_lattice.Inf_pres_downset_var dual_upset)

end

subsection ‹Examples that Do Not Dualise›

lemma upset_anti: "antimono (::'a::order  'a set)"
  by (simp add: antimono_def upset_anti_iff)

context complete_lattice 
begin

lemma fSup_unfold: "(f::nat  'a) 0  (n. f (Suc n)) = (n. f n)"
  apply (intro order.antisym sup_least)
    apply (rule Sup_upper, force)
   apply (rule Sup_mono, force)
  apply (safe intro!: Sup_least)
 by (case_tac n, simp_all add: Sup_upper le_supI2)


lemma fInf_unfold: "(f::nat  'a) 0  (n. f (Suc n)) = (n. f n)"
  apply (intro order.antisym inf_greatest)
  apply (rule Inf_greatest, safe)
  apply (case_tac n)
   apply simp_all
  using Inf_lower inf.coboundedI2 apply force
   apply (simp add: Inf_lower)
  by (auto intro: Inf_mono)

end

lemma fun_isol: "mono f  mono ((∘) f)"
  by (simp add: le_fun_def mono_def)

lemma fun_isor: "mono f  mono (λx. x  f)"
  by (simp add: le_fun_def mono_def)

lemma Sup_sup_pres: 
  fixes f :: "'a::complete_lattice  'b::complete_lattice"
  shows "Sup_pres f  sup_pres f"
  by (metis (no_types, opaque_lifting) Sup_empty Sup_insert comp_apply image_insert sup_bot.right_neutral)

lemma Inf_inf_pres: 
  fixes f :: "'a::complete_lattice  'b::complete_lattice"
  shows"Inf_pres f  inf_pres f"
  by (smt (verit) INF_insert comp_eq_elim dual_complete_lattice.Sup_empty dual_complete_lattice.Sup_insert inf_top.right_neutral)

lemma Sup_bot_pres: 
  fixes f :: "'a::complete_lattice  'b::complete_lattice"
  shows "Sup_pres f  bot_pres f"
  by (metis SUP_empty Sup_empty comp_eq_elim)

lemma Inf_top_pres: 
  fixes f :: "'a::complete_lattice  'b::complete_lattice"
  shows "Inf_pres f  top_pres f"
  by (metis INF_empty comp_eq_elim dual_complete_lattice.Sup_empty)

context complete_lattice
begin

lemma iso_Inf_subdistl: 
  assumes "mono (f::'a  'b::complete_lattice)"
  shows "f  Inf  Inf  (`) f"
  by (simp add: assms complete_lattice_class.le_Inf_iff le_funI Inf_lower monoD)

lemma iso_Sup_supdistl: 
  assumes "mono (f::'a  'b::complete_lattice)"
  shows "Sup  (`) f  f  Sup"
  by (simp add: assms complete_lattice_class.SUP_le_iff le_funI dual_complete_lattice.Inf_lower monoD)

lemma Inf_subdistl_iso: 
  fixes f :: "'a  'b::complete_lattice"
  shows "f  Inf  Inf  (`) f  mono f"
  unfolding mono_def le_fun_def comp_def by (metis complete_lattice_class.le_INF_iff Inf_atLeast atLeast_iff)

lemma Sup_supdistl_iso: 
  fixes f :: "'a  'b::complete_lattice"
  shows "Sup  (`) f  f  Sup  mono f"
  unfolding mono_def le_fun_def comp_def by (metis complete_lattice_class.SUP_le_iff Sup_atMost atMost_iff)

lemma supdistl_iso: 
  fixes f :: "'a  'b::complete_lattice"
  shows "(Sup  (`) f  f  Sup) = mono f"
  using Sup_supdistl_iso iso_Sup_supdistl by force

lemma subdistl_iso: 
  fixes f :: "'a  'b::complete_lattice"
  shows "(f  Inf  Inf  (`) f) = mono f"
  using Inf_subdistl_iso iso_Inf_subdistl by force

end

lemma fSup_distr: "Sup_pres (λx. x  f)"
  unfolding fun_eq_iff comp_def
  by (smt (verit) Inf.INF_cong SUP_apply Sup_apply)

lemma fSup_distr_var: "F  g = (f  F. f  g)"
  unfolding fun_eq_iff comp_def
  by (smt (verit) Inf.INF_cong SUP_apply Sup_apply)

lemma fInf_distr: "Inf_pres (λx. x  f)"
  unfolding fun_eq_iff comp_def
  by (smt (verit) INF_apply Inf.INF_cong Inf_apply)

lemma fInf_distr_var: "F  g = (f  F. f  g)"
  unfolding fun_eq_iff comp_def
  by (smt (verit) INF_apply Inf.INF_cong Inf_apply)

lemma fSup_subdistl: 
  assumes "mono (f::'a::complete_lattice  'b::complete_lattice)"
  shows "Sup  (`) ((∘) f)  (∘) f  Sup"
  using assms by (simp add: SUP_least Sup_upper le_fun_def monoD image_comp)

lemma fSup_subdistl_var: 
  fixes f :: "'a::complete_lattice  'b::complete_lattice"
  shows  "mono f  (g  G. f  g)  f  G"
  by (simp add: SUP_least Sup_upper le_fun_def monoD image_comp)

lemma fInf_subdistl: 
  fixes f :: "'a::complete_lattice  'b::complete_lattice"
  shows  "mono f  (∘) f  Inf  Inf  (`) ((∘) f)"
  by (simp add: INF_greatest Inf_lower le_fun_def monoD image_comp)

lemma fInf_subdistl_var: 
  fixes f :: "'a::complete_lattice  'b::complete_lattice"
  shows "mono f  f  G  (g  G. f  g)"
  by (simp add: INF_greatest Inf_lower le_fun_def monoD image_comp)

lemma Inf_pres_downset: "Inf_pres (::'a::complete_lattice  'a set)"
  unfolding downset_prop fun_eq_iff comp_def
  by (safe, simp_all add: le_Inf_iff)
 
lemma Sup_dual_upset: "Sup_dual (::'a::complete_lattice  'a set)"
  unfolding upset_prop fun_eq_iff comp_def
  by (safe, simp_all add: Sup_le_iff)

text ‹This approach could probably be combined with the explicit functor-based one. This may be good for proofs, but seems conceptually rather ugly.›

end