Theory Order_Lattice_Props_Wenzel

(* 
  Title: Duality Based on a Data Type
  Author: Georg Struth 
  Maintainer:Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Duality Based on a Data Type›

theory Order_Lattice_Props_Wenzel
  imports Main 
begin

unbundle lattice_syntax

subsection ‹Wenzel's Approach Revisited›

text ‹This approach is similar to, but inferior to the explicit class-based one. The main caveat is that duality is not involutive 
with this approach, and this allows dualising less theorems.›

text ‹I copy Wenzel's development \<^cite>‹"Wenzel"› in this subsection and extend it with additional properties. I show only the most important properties.›

datatype 'a dual = dual (un_dual: 'a) ("∂")

notation un_dual ("∂⇧-")

lemma dual_inj: "inj ∂"
  using injI by fastforce

lemma dual_surj: "surj ∂"
  using dual.exhaust_sel by blast

lemma dual_bij: "bij ∂"
  by (simp add: bijI dual_inj dual_surj)

text ‹Dual is not idempotent, and I see no way of imposing this condition. Yet at least an inverse exists --- namely un-dual..›

lemma dual_inv1 [simp]: "∂⇧- ∘ ∂ = id"
  by fastforce

lemma dual_inv2 [simp]: "∂ ∘ ∂⇧- = id"
  by fastforce

lemma dual_inv_inj: "inj ∂⇧-"
  by (simp add: dual.expand injI)

lemma dual_inv_surj: "surj ∂⇧-"
  by (metis dual.sel surj_def)

lemma dual_inv_bij: "bij ∂⇧-"
  by (simp add: bij_def dual_inv_inj dual_inv_surj)

lemma dual_iff: "(∂ x = y) ⟷ (x = ∂⇧- y)"
  by fastforce

text ‹Isabelle data types come with a number of generic functions.›

text ‹The functor map-dual lifts functions to dual types. Isabelle's generic definition is not straightforward to 
understand and use. Yet conceptually it can be explained as follows.›

lemma map_dual_def_var [simp]: "(map_dual::('a ⇒ 'b) ⇒ 'a dual ⇒ 'b dual) f = ∂ ∘ f ∘ ∂⇧-"  
  unfolding fun_eq_iff comp_def by (metis dual.map_sel dual_iff)

lemma map_dual_def_var2: "∂⇧- ∘ map_dual f = f ∘ ∂⇧-"
  by (simp add: rewriteL_comp_comp)

lemma map_dual_func1: "map_dual (f ∘ g) = map_dual f ∘ map_dual g"
  unfolding fun_eq_iff comp_def by (metis dual.exhaust dual.map) 

lemma map_dual_func2 : "map_dual id = id"
  by simp

text ‹The functor map-dual has an inverse functor as well.›

definition map_dual_inv :: "('a dual ⇒ 'b dual) => ('a => 'b)" where
  "map_dual_inv f = ∂⇧- ∘ f ∘ ∂"

lemma map_dual_inv_func1: "map_dual_inv id = id"
  by (simp add: map_dual_inv_def)

lemma map_dual_inv_func2: "map_dual_inv (f ∘ g) = map_dual_inv f ∘ map_dual_inv g"
  unfolding fun_eq_iff comp_def map_dual_inv_def by (metis dual_iff)

lemma map_dual_inv1: "map_dual ∘ map_dual_inv = id"
  unfolding fun_eq_iff map_dual_def_var map_dual_inv_def comp_def id_def
  by (metis dual_iff) 

lemma map_dual_inv2: "map_dual_inv ∘ map_dual = id"
  unfolding fun_eq_iff map_dual_def_var map_dual_inv_def comp_def id_def
  by (metis dual_iff) 

text ‹Hence dual is an isomorphism between categories.›

lemma subset_dual: "(∂ ` X = Y) ⟷ (X = ∂⇧- ` Y)"
  by (metis dual_inj image_comp image_inv_f_f inv_o_cancel dual_inv2)

lemma subset_dual1: "(X ⊆ Y) ⟷ (∂ ` X ⊆ ∂ ` Y)"
  by (simp add: dual_inj inj_image_subset_iff) 

lemma dual_ball: "(∀x ∈ X. P (∂ x)) ⟷ (∀y ∈ ∂ ` X. P y)"
  by simp

lemma dual_inv_ball: "(∀x ∈ X. P (∂⇧- x)) ⟷ (∀y ∈ ∂⇧- ` X. P y)"
  by simp

lemma dual_all: "(∀x. P (∂ x)) ⟷ (∀y. P y)"
  by (metis dual.collapse)

lemma dual_inv_all: "(∀x. P (∂⇧- x)) ⟷ (∀y. P y)"
  by (metis dual_inv_surj surj_def)

lemma dual_ex: "(∃x. P (∂ x)) ⟷ (∃y. P y)"  
  by (metis UNIV_I bex_imageD dual_surj)

lemma dual_inv_ex: "(∃x. P (∂⇧- x)) ⟷ (∃y. P y)"
  by (metis dual.sel)

lemma dual_Collect: "{∂ x |x. P (∂ x)} = {y. P y}"
  by (metis dual.exhaust)

lemma dual_inv_Collect: "{∂⇧- x |x. P (∂⇧- x)} = {y. P y}"
  by (metis dual.collapse dual.inject)

lemma fun_dual1: "(f ∘ ∂ = g) ⟷ (f = g ∘ ∂⇧-)"
  by auto

lemma fun_dual2: "(∂ ∘ f = g) ⟷ (f = ∂⇧- ∘ g)"
  by auto

lemma fun_dual3: "(f ∘ (`) ∂ = g) ⟷ (f = g ∘ (`) ∂⇧-)"
  unfolding fun_eq_iff comp_def by (metis subset_dual)

lemma fun_dual4: "(f = ∂⇧- ∘ g ∘ (`) ∂) ⟷ (∂ ∘ f ∘ (`) ∂⇧- = g)"
  by (metis fun_dual2 fun_dual3 o_assoc)

text ‹The next facts show incrementally that the dual of a complete lattice is a complete lattice.
This follows once again Wenzel.›

instantiation dual :: (ord) ord
begin  

definition less_eq_dual_def: "(≤) = rel_dual (≥)"

definition less_dual_def: "(<) = rel_dual (>)"

instance..

end

lemma less_eq_dual_def_var: "(x ≤ y) = (∂⇧- y ≤ ∂⇧- x)"
  apply (rule antisym)
  apply (simp add: dual.rel_sel less_eq_dual_def)
  by (simp add: dual.rel_sel less_eq_dual_def)

lemma less_dual_def_var: "(x < y) = (∂⇧- y < ∂⇧- x)"
  by (simp add: dual.rel_sel less_dual_def) 

instance dual :: (preorder) preorder
  apply standard
  apply (simp add: less_dual_def_var less_eq_dual_def_var less_le_not_le)
  apply (simp add: less_eq_dual_def_var)
  by (meson less_eq_dual_def_var order_trans)
 
instance dual :: (order) order
  by (standard, simp add: dual.expand less_eq_dual_def_var)

lemma dual_anti: "x ≤ y ⟹ ∂ y ≤ ∂ x" 
  by (simp add: dual_inj less_eq_dual_def the_inv_f_f)

lemma dual_anti_iff: "(x ≤ y) = (∂ y ≤ ∂ x)"
  by (simp add: dual_inj less_eq_dual_def the_inv_f_f)

text ‹map-dual does not map isotone functions to antitone ones. It simply lifts the type!›

lemma "mono f ⟹ mono (map_dual f)"
  unfolding map_dual_def_var mono_def by (metis comp_apply dual_anti less_eq_dual_def_var)

instantiation dual :: (lattice) lattice
begin

definition inf_dual_def: "x ⊓ y = ∂ (∂⇧- x ⊔ ∂⇧- y)"

definition sup_dual_def: "x ⊔ y = ∂ (∂⇧- x ⊓ ∂⇧- y)"

instance
  by (standard, simp_all add: dual_inj inf_dual_def sup_dual_def less_eq_dual_def_var the_inv_f_f)

end

instantiation dual :: (complete_lattice) complete_lattice
begin

definition Inf_dual_def: "Inf = ∂ ∘ Sup ∘ (`) ∂⇧-"

definition Sup_dual_def: "Sup = ∂ ∘ Inf ∘ (`) ∂⇧-"

definition bot_dual_def: "⊥ = ∂ ⊤"

definition top_dual_def: "⊤ = ∂ ⊥"

instance
   by (standard, simp_all add: Inf_dual_def top_dual_def Sup_dual_def bot_dual_def dual_inj le_INF_iff SUP_le_iff INF_lower SUP_upper less_eq_dual_def_var the_inv_f_f)

end

text ‹Next, directed and filtered sets, upsets, downsets, filters and ideals in posets are defined.›

context ord
begin

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}"

end

subsection ‹Examples that Do Not Dualise›

text ‹Filtered and directed sets are dual.›

text ‹Proofs could be simplified if dual was idempotent.›

lemma filtered_directed_dual: "filtered ∘ (`) ∂ = directed"
proof-
  {fix X::"'a set"
    have "(filtered ∘ (`) ∂) X = (∀Y. finite (∂⇧- ` Y) ∧ ∂⇧- ` Y ⊆ X ⟶ (∃x ∈ X.∀y ∈ (∂⇧- ` Y). ∂ x ≤ ∂ y))"
      unfolding filtered_def comp_def by (simp, metis dual_iff finite_subset_image subset_dual subset_dual1)
    also have "... = (∀Y. finite Y ∧ Y ⊆ X ⟶ (∃x ∈ X.∀y ∈ Y. y ≤ x))"
      by (metis dual_anti_iff dual_inv_surj finite_subset_image top.extremum)
    finally have "(filtered ∘ (`) ∂) X = directed X"
      using directed_def by auto}
  thus ?thesis
    unfolding fun_eq_iff by simp 
qed

lemma directed_filtered_dual: "directed ∘ (`) ∂ = filtered"
proof-
  {fix X::"'a set"
    have "(directed ∘ (`) ∂) X = (∀Y. finite (∂⇧- ` Y) ∧ ∂⇧- ` Y ⊆ X ⟶ (∃x ∈ X.∀y ∈ (∂⇧- ` Y). ∂ y ≤ ∂ x))"
      unfolding directed_def comp_def by (simp, metis dual_iff finite_subset_image subset_dual subset_dual1)
  also have "... = (∀Y. finite Y ∧ Y ⊆ X ⟶ (∃x ∈ X.∀y ∈ Y. x ≤ y))"
    unfolding dual_anti_iff[symmetric] by (metis dual_inv_surj finite_subset_image top_greatest)
  finally have "(directed ∘ (`) ∂) X = filtered X"
    using filtered_def by auto}
  thus ?thesis
    unfolding fun_eq_iff by simp
qed

text ‹This example illustrates the deficiency of the approach. In the class-based approach the second proof is trivial.›

text ‹The next example shows that this is a systematic problem.›

lemma downset_set_upset_set_dual: "(`) ∂ ∘ ⇓ = ⇑ ∘ (`) ∂"
  proof-
    {fix X::"'a set"
  have "((`) ∂ ∘ ⇓) X = {∂ y |y. ∃x ∈ X. y ≤ x}"
    by (simp add: downset_set_def setcompr_eq_image)
  also have "... = {∂ y |y. ∃x ∈ X. ∂ x ≤ ∂ y}"
    by (meson dual_anti_iff)
  also have "... = {y. ∃x ∈ ∂ ` X. x ≤ y}"
    by (metis (mono_tags, opaque_lifting) dual.exhaust image_iff)
  finally have "((`) ∂ ∘ ⇓) X = (⇑ ∘ (`) ∂) X"
    by (simp add: upset_set_def)}
  thus ?thesis
    unfolding fun_eq_iff by simp
qed

lemma upset_set_downset_set_dual: "(`) ∂ ∘ ⇑ = ⇓ ∘ (`) ∂"
  unfolding downset_set_def upset_set_def fun_eq_iff comp_def
  apply (safe, force simp: dual_anti)
  by (metis (mono_tags, lifting) dual.exhaust dual_anti_iff mem_Collect_eq rev_image_eqI)

end