Theory Distributive

theory Distributive
imports Main
section{*\label{sec_Distributive}Complete Distributive Lattice*}

theory Distributive imports Main
begin
  
notation
    bot ("⊥") and
    top ("⊤") and
    inf (infixl "⊓" 70)
    and sup (infixl "⊔" 65)

context complete_lattice
begin
lemma Sup_Inf_le: "Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈ Y)}) ≤ Inf (Sup ` A)"
  by (rule SUP_least, clarify, rule INF_greatest, simp add: INF_lower2 Sup_upper)
end 

class complete_distributive_lattice = complete_lattice +
  assumes Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈ Y)})"
begin
  
lemma Inf_Sup: "Inf (Sup ` A) = Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈ Y)})"
  by (rule antisym, rule Inf_Sup_le, rule Sup_Inf_le)

lemma Sup_Inf: "Sup (Inf ` A) = Inf (Sup ` {f ` A | f . (∀ Y ∈ A . f Y ∈ Y)})"
proof (rule antisym)
  show "SUPREMUM A Inf ≤ INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Sup"
    apply (rule Sup_least, rule INF_greatest)
    using Inf_lower2 Sup_upper by auto
next
  show "INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Sup ≤ SUPREMUM A Inf"
  proof (simp add:  Inf_Sup, rule_tac SUP_least, simp, safe)
    fix f
    assume "∀Y. (∃f. Y = f ` A ∧ (∀Y∈A. f Y ∈ Y)) ⟶ f Y ∈ Y"
    from this have B: "⋀ F . (∀ Y ∈ A . F Y ∈ Y) ⟹ ∃ Z ∈ A . f (F ` A) = F Z"
      by auto
    show "INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} f ≤ SUPREMUM A Inf"
    proof (cases "∃ Z ∈ A . INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} f ≤ Inf Z")
      case True
      from this obtain Z where [simp]: "Z ∈ A" and A: "INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} f ≤ Inf Z"
        by blast
      have B: "... ≤ SUPREMUM A Inf"
        by (simp add: SUP_upper)
      from A and B show ?thesis
        by (drule_tac order_trans, simp_all)
    next
      case False
      from this have X: "⋀ Z . Z ∈ A ⟹ ∃ x . x ∈ Z ∧ ¬ INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} f ≤ x"
        using Inf_greatest by blast
  
      define F where "F = (λ Z . SOME x . x ∈ Z ∧ ¬ INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} f ≤ x)"
      have C: "⋀ Y . Y ∈ A ⟹ F Y ∈ Y"
        using X by (simp add: F_def, rule someI2_ex, auto)
                 
      have E: "⋀ Y . Y ∈ A ⟹ ¬ INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} f ≤ F Y"
        using X by (simp add: F_def, rule someI2_ex, auto)
  
      from C and B obtain  Z where D: "Z ∈ A " and Y: "f (F ` A) = F Z"
        by blast

      from E and D have W: "¬ INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} f ≤ F Z"
        by simp

      from C have "INFIMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} f ≤ f (F ` A)"
        by (rule_tac INF_lower, blast)
            
      from this and W and Y show ?thesis
        by simp
    qed
  qed
qed
  
lemma dual_complete_distributive_lattice:
  "class.complete_distributive_lattice Sup Inf sup (op ≥) (op >) inf ⊤ ⊥"
  apply (rule class.complete_distributive_lattice.intro)
   apply (fact dual_complete_lattice)
  by (simp add: class.complete_distributive_lattice_axioms_def Sup_Inf)
  
lemma sup_Inf: "a ⊔ Inf B = (INF b:B. a ⊔ b)"
proof (rule antisym)
  show "a ⊔ Inf B ≤ (INF b:B. a ⊔ b)"
    using Inf_lower sup.mono by (rule_tac INF_greatest, fastforce)
next
  have "(INF b:B. a ⊔ b) ≤ INFIMUM {{f {a}, f B} |f. f {a} = a ∧ f B ∈ B} Sup"
    by (rule INF_greatest, auto simp add: INF_lower)
  also have "... = a ⊔ Inf B"
    by (cut_tac A = "{{a}, B}" in Sup_Inf, simp)
  finally show "(INF b:B. a ⊔ b) ≤ a ⊔ Inf B"
    by simp
qed
  
lemma inf_Sup: "a ⊓ Sup B = (SUP b:B. a ⊓ b)"
proof (rule antisym)
  show " (SUP b:B. a ⊓ b) ≤ a ⊓ Sup B"
    by (metis SUP_least Sup_upper inf.orderI inf_idem inf_mono)
next
  have "a ⊓ Sup B = SUPREMUM {{f {a}, f B} |f. f {a} = a ∧ f B ∈ B} Inf"
    by (cut_tac A = "{{a}, B}" in Inf_Sup, simp)

  also have "... ≤ (SUP b:B. a ⊓ b)"
    by (rule SUP_least, auto simp add: SUP_upper)
      
  finally show "a ⊓ Sup B ≤ (SUP b:B. a ⊓ b)"
    by simp
qed
  
subclass complete_distrib_lattice
  by (standard, rule sup_Inf, rule inf_Sup)

  
end
  
instantiation bool :: complete_distributive_lattice
begin
instance proof
  fix A :: "(bool set) set"
  show "INFIMUM A Sup ≤ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf"
    by (clarsimp, fastforce)
      
qed
end

instantiation "set" :: (type) complete_distributive_lattice
begin
instance proof (standard, clarsimp)
  fix A :: "(('a set) set) set"
  fix x::'a
  define F where "F = (λ Y . (SOME X . (Y ∈ A ∧ X ∈ Y ∧ x ∈ X)))"
  assume A: "∀xa∈A. ∃X∈xa. x ∈ X"
    
  have B: " (∀xa ∈ F ` A. x ∈ xa)"
    by (safe, metis (no_types, lifting) A F_def someI_ex)
    
  have "(∃f. F ` A  = f ` A ∧ (∀Y∈A. f Y ∈ Y))"
    by (rule_tac x = "F" in exI, metis (no_types, lifting) A F_def someI_ex)
      
  from B and this show "∃xa. (∃f. xa = f ` A ∧ (∀Y∈A. f Y ∈ Y)) ∧ (∀xa∈xa. x ∈ xa)"
    by auto
qed
end
  
context complete_distributive_lattice
begin
       
lemma INF_SUP: "(INF y. SUP x. ((P x y)::'a)) = (SUP x. INF y. P (x y) y)"
proof (rule antisym)
  show "(SUP x. INF y. P (x y) y) ≤ (INF y. SUP x. P x y)"
    by (meson UNIV_I image_eqI INF_lower2 Sup_upper INF_greatest SUP_least)
next
  have "(INF y. SUP x. ((P x y))) ≤ Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A ≤ ?B")
  proof (rule_tac INF_greatest, clarsimp)
    fix y
    have "?A ≤ (SUP x. P x y)"
      by (rule INF_lower, simp)
    also have "... ≤ Sup {uu. ∃x. uu = P x y}"
      by (simp add: full_SetCompr_eq)
    finally show "?A ≤ Sup {uu. ∃x. uu = P x y}"
      by simp
  qed
 
  also have "... ≤  (SUP x. INF y. P (x y) y)"
  proof (subst  Inf_Sup, rule_tac SUP_least, clarsimp)
    fix f
    assume A: "∀Y. (∃y. Y = {uu. ∃x. uu = P x y}) ⟶ f Y ∈ Y"
      
    have "(INF x:{uu. ∃y. uu = {uu. ∃x. uu = P x y}}. f x) ≤  (INF y. P ((λ y. SOME x . f ({P x y | x. True}) = P x y) y) y)"
    proof (rule INF_greatest, clarsimp)
      fix y
        have "(INF x:{uu. ∃y. uu = {uu. ∃x. uu = P x y}}. f x) ≤ f {uu. ∃x. uu = P x y}"
          by (rule_tac INF_lower, blast)
        also have "... ≤ P (SOME x. f {uu . ∃x. uu = P x y} = P x y) y"
          using A by (rule_tac someI2_ex, auto)
        finally show "(INF x:{uu. ∃y. uu = {uu. ∃x. uu = P x y}}. f x) ≤ P (SOME x. f {uu . ∃x. uu = P x y} = P x y) y"
          by simp
      qed
      also have "... ≤ (SUP x. INF y. P (x y) y)"
        by (rule SUP_upper, simp)
      finally show "(INF x:{uu. ∃y. uu = {uu. ∃x. uu = P x y}}. f x) ≤ (SUP x. INF y. P (x y) y)"
        by simp
    qed
    
  finally show "(INF y. SUP x. P x y) ≤ (SUP x. INF y. P (x y) y)"
    by simp
qed

end
  

instantiation "fun" :: (type, complete_distributive_lattice) complete_distributive_lattice
begin
          
instance proof (standard, simp add: le_fun_def, clarify)
  fix A::"('a ⇒ 'b) set set" 
  fix x
  have "⋀ X . X ∈ A ⟹  (INF xa:A. SUP f:xa. f x) ≤  (SUP f:X. f x)"
    by (rule_tac INF_lower, simp)
  also have "⋀ X . X ∈ A ⟹ (SUP f:X. f x) ≤ Sup {f x |f. f ∈ X}"
    by (metis (mono_tags, lifting) SUP_least Sup_upper mem_Collect_eq)
  finally have "(INF xa:A. SUP f:xa. f x) ≤ Inf (Sup ` { {f x | f . f ∈ X} | X . X ∈ A})"
    by (rule_tac INF_greatest, blast)
  also have "... ≤ (SUP xa:{f ` A |f. ∀Y∈A. f Y ∈ Y}. INF f:xa. f x)"
  proof (unfold Inf_Sup, rule SUP_least, clarsimp)
    fix f
    assume A: "∀Y. (∃X. Y = {f x |f. f ∈ X} ∧ X ∈ A) ⟶ f Y ∈ Y"
    from this have [simp]: "⋀ xa . xa ∈ A ⟹  (SOME g. g ∈ xa ∧ g x = f {h x |h. h ∈ xa}) x = f {h x |h. h ∈ xa}"
      apply (rule_tac Q = "λ F . F x = f {h x |h. h ∈ xa}" in  someI2_ex)
      by (drule_tac x = "{g x | g . g ∈ xa}" in spec, auto)
    from A have [simp]: "⋀ Y .  Y ∈ A ⟹ (SOME g. g ∈ Y ∧ g x = f {h x |h. h ∈ Y}) ∈ Y"
      apply (rule_tac Q = "λ F . F ∈ Y" in  someI2_ex)
      by (drule_tac x = "{g x | g . g ∈ Y}" in spec, auto)
        
    have "(INF x:{{f x |f. f ∈ X} |X. X ∈ A}. f x) ≤ (INF g:((λ Y . SOME g . g ∈ Y ∧ g x = f({h x | h . h ∈ Y})) `A). g x)"
      by (rule INF_greatest, clarsimp, rule INF_lower, blast)
    also have "... ≤ (SUP xa:{f ` A |f. ∀Y∈A. f Y ∈ Y}. INF f:xa. f x)"
      by (rule SUP_upper, clarsimp, rule_tac x = "((λ Y . SOME g . g ∈ Y ∧ g x = f({h x | h . h ∈ Y})))" in exI, simp)
        
    finally show "(INF x:{{f x |f. f ∈ X} |X. X ∈ A}. f x) ≤ (SUP xa:{f ` A |f. ∀Y∈A. f Y ∈ Y}. INF f:xa. f x)"
      by simp
  qed
  finally show "(INF xa:A. SUP f:xa. f x) ≤ (SUP xa:{f ` A |f. ∀Y∈A. f Y ∈ Y}. INF f:xa. f x)"
    by simp
qed
  
end
  
context complete_linorder
begin
  
subclass complete_distributive_lattice
proof (standard, rule ccontr)
  fix A
  assume "¬ INFIMUM A Sup ≤ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf"
  from this have C: "INFIMUM A Sup > SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf"
    using local.not_le by blast
  show "False"
    proof (cases "∃ z . INFIMUM A Sup > z ∧ z > SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf")
      case True
      from this obtain z where A: "z < INFIMUM A Sup" and X: "SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf < z"
        by blast
          
      from A have "⋀ Y . Y ∈ A ⟹ z < Sup Y"
        by (meson local.less_INF_D)
    
      from this have B: "⋀ Y . Y ∈ A ⟹ ∃ k ∈Y . z < k"
        using local.less_Sup_iff by blast
          
      define F where "F = (λ Y . SOME k . k ∈ Y ∧ z < k)"
        
      have D: "⋀ Y . Y ∈ A ⟹ z < F Y"
        by (metis (no_types, lifting) F_def B  someI_ex)
    
      have E: "⋀ Y . Y ∈ A ⟹ F Y ∈ Y"
        apply (simp add: F_def)
        by (metis (mono_tags, lifting) B someI_ex)
    
      have "z ≤ Inf (F ` A)"
        by (simp add: D local.INF_greatest local.order.strict_implies_order)
    
      also have "... ≤ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf"
        apply (rule SUP_upper, safe)
        using E by blast
      finally have "z ≤ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf"
        by simp
          
      from X and this show ?thesis
        using local.not_less by blast
    next
      case False
      from this have A: "⋀ z . INFIMUM A Sup ≤ z ∨ z ≤ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf"
        using local.le_less_linear by blast
          
      from C have "⋀ Y . Y ∈ A ⟹ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf < Sup Y"
        by (meson local.less_INF_D)
    
      from this have B: "⋀ Y . Y ∈ A ⟹ ∃ k ∈Y . SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf < k"
        using local.less_Sup_iff by blast
          
      define F where "F = (λ Y . SOME k . k ∈ Y ∧ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf < k)"
        
      have D: "⋀ Y . Y ∈ A ⟹ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf < F Y"
        by (metis (no_types, lifting) F_def B  someI_ex)
    
      have E: "⋀ Y . Y ∈ A ⟹ F Y ∈ Y"
        apply (simp add: F_def)
        by (metis (mono_tags, lifting) B someI_ex)
          
      have "⋀ Y . Y ∈ A ⟹ INFIMUM A Sup ≤ F Y"
        using D False local.leI by blast
         
      from this have "INFIMUM A Sup ≤ Inf (F ` A)"
        by (simp add: local.INF_greatest)
          
      also have "Inf (F ` A) ≤ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf"
        apply (rule SUP_upper, safe)
        using E by blast
          
      finally have "INFIMUM A Sup ≤ SUPREMUM {f ` A |f. ∀Y∈A. f Y ∈ Y} Inf"
        by simp
        
      from C and this show ?thesis
        using local.not_less by blast
    qed
  qed
  
end

 
end