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