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