section‹Modular and Distributive Lattices› (* Author: Viorel Preoteasa *) theory Modular_Distrib_Lattice imports Lattice_Prop begin text ‹ The main result of this theory is the fact that a lattice is distributive if and only if it satisfies the following property: › term "(∀ x y z . x ⊓ z = y ⊓ z ∧ x ⊔ z = y ⊔ z ⟹ x = y)" text‹ This result was proved by Bergmann in \<^cite>‹"bergmann:1929"›. The formalization presented here is based on \<^cite>‹"birkhoff:1967" and "burris:sankappanavar:1981"›. › class modular_lattice = lattice + assumes modular: "x ≤ y ⟹ x ⊔ (y ⊓ z) = y ⊓ (x ⊔ z)" context distrib_lattice begin subclass modular_lattice apply unfold_locales by (simp add: inf_sup_distrib inf_absorb2) end context lattice begin definition "d_aux a b c = (a ⊓ b) ⊔ (b ⊓ c) ⊔ (c ⊓ a)" lemma d_b_c_a: "d_aux b c a = d_aux a b c" by (metis d_aux_def sup.assoc sup_commute) lemma d_c_a_b: "d_aux c a b = d_aux a b c" by (metis d_aux_def sup.assoc sup_commute) definition "e_aux a b c = (a ⊔ b) ⊓ (b ⊔ c) ⊓ (c ⊔ a)" lemma e_b_c_a: "e_aux b c a = e_aux a b c" by (simp add: e_aux_def ac_simps) lemma e_c_a_b: "e_aux c a b = e_aux a b c" by (simp add: e_aux_def ac_simps) definition "a_aux a b c = (a ⊓ (e_aux a b c)) ⊔ (d_aux a b c)" definition "b_aux a b c = (b ⊓ (e_aux a b c)) ⊔ (d_aux a b c)" definition "c_aux a b c = (c ⊓ (e_aux a b c)) ⊔ (d_aux a b c)" lemma b_a: "b_aux a b c = a_aux b c a" by (simp add: a_aux_def b_aux_def e_b_c_a d_b_c_a) lemma c_a: "c_aux a b c = a_aux c a b" by (simp add: a_aux_def c_aux_def e_c_a_b d_c_a_b) lemma [simp]: "a_aux a b c ≤ e_aux a b c" apply (simp add: a_aux_def e_aux_def d_aux_def) apply (rule_tac y = "(a ⊔ b) ⊓ (b ⊔ c) ⊓ (c ⊔ a)" in order_trans) apply (rule inf_le2) by simp lemma [simp]: "b_aux a b c ≤ e_aux a b c" apply (unfold b_a) apply (subst e_b_c_a [THEN sym]) by simp lemma [simp]: "c_aux a b c ≤ e_aux a b c" apply (unfold c_a) apply (subst e_c_a_b [THEN sym]) by simp lemma [simp]: "d_aux a b c ≤ a_aux a b c" by (simp add: a_aux_def e_aux_def d_aux_def) lemma [simp]: "d_aux a b c ≤ b_aux a b c" apply (unfold b_a) apply (subst d_b_c_a [THEN sym]) by simp lemma [simp]: "d_aux a b c ≤ c_aux a b c" apply (unfold c_a) apply (subst d_c_a_b [THEN sym]) by simp lemma a_meet_e: "a ⊓ (e_aux a b c) = a ⊓ (b ⊔ c)" by (rule order.antisym) (simp_all add: e_aux_def le_infI2) lemma b_meet_e: "b ⊓ (e_aux a b c) = b ⊓ (c ⊔ a)" by (simp add: a_meet_e [THEN sym] e_b_c_a) lemma c_meet_e: "c ⊓ (e_aux a b c) = c ⊓ (a ⊔ b)" by (simp add: a_meet_e [THEN sym] e_c_a_b) lemma a_join_d: "a ⊔ d_aux a b c = a ⊔ (b ⊓ c)" by (rule order.antisym) (simp_all add: d_aux_def le_supI2) lemma b_join_d: "b ⊔ d_aux a b c = b ⊔ (c ⊓ a)" by (simp add: a_join_d [THEN sym] d_b_c_a) end context lattice begin definition "no_distrib a b c = (a ⊓ b ⊔ c ⊓ a < a ⊓ (b ⊔ c))" definition "incomp x y = (¬ x ≤ y ∧ ¬ y ≤ x)" definition "N5_lattice a b c = (a ⊓ c = b ⊓ c ∧ a < b ∧ a ⊔ c = b ⊔ c)" definition "M5_lattice a b c = (a ⊓ b = b ⊓ c ∧ c ⊓ a = b ⊓ c ∧ a ⊔ b = b ⊔ c ∧ c ⊔ a = b ⊔ c ∧ a ⊓ b < a ⊔ b)" lemma M5_lattice_incomp: "M5_lattice a b c ⟹ incomp a b" apply (simp add: M5_lattice_def incomp_def) apply safe apply (simp_all add: inf_absorb1 inf_absorb2 ) apply (simp_all add: sup_absorb1 sup_absorb2 ) apply (subgoal_tac "c ⊓ (b ⊔ c) = c") apply simp apply (subst sup_commute) by simp end context modular_lattice begin lemma a_meet_d: "a ⊓ (d_aux a b c) = (a ⊓ b) ⊔ (c ⊓ a)" proof - have "a ⊓ (d_aux a b c) = a ⊓ ((a ⊓ b) ⊔ (b ⊓ c) ⊔ (c ⊓ a))" by (simp add: d_aux_def) also have "... = a ⊓ (a ⊓ b ⊔ c ⊓ a ⊔ b ⊓ c)" by (simp add: sup_assoc, simp add: sup_commute) also have "... = (a ⊓ b ⊔ c ⊓ a) ⊔ (a ⊓ (b ⊓ c))" by (simp add: modular) also have "... = (a ⊓ b) ⊔ (c ⊓ a)" by (rule order.antisym, simp_all, rule_tac y = "a ⊓ b" in order_trans, simp_all) finally show ?thesis by simp qed lemma b_meet_d: "b ⊓ (d_aux a b c) = (b ⊓ c) ⊔ (a ⊓ b)" by (simp add: a_meet_d [THEN sym] d_b_c_a) lemma c_meet_d: "c ⊓ (d_aux a b c) = (c ⊓ a) ⊔ (b ⊓ c)" by (simp add: a_meet_d [THEN sym] d_c_a_b) lemma d_less_e: "no_distrib a b c ⟹ d_aux a b c < e_aux a b c" apply (subst less_le) apply(case_tac "d_aux a b c = e_aux a b c") apply simp_all apply (simp add: no_distrib_def a_meet_e [THEN sym] a_meet_d [THEN sym]) apply (rule_tac y = "a_aux a b c" in order_trans) by simp_all lemma a_meet_b_eq_d: " d_aux a b c ≤ e_aux a b c ⟹ a_aux a b c ⊓ b_aux a b c = d_aux a b c" proof - assume d_less_e: " d_aux a b c ≤ e_aux a b c" have "(a ⊓ e_aux a b c ⊔ d_aux a b c) ⊓ (b ⊓ e_aux a b c ⊔ d_aux a b c) = (b ⊓ e_aux a b c ⊔ d_aux a b c) ⊓ (d_aux a b c ⊔ a ⊓ e_aux a b c)" by (simp add: inf_commute sup_commute) also have "… = d_aux a b c ⊔ ((b ⊓ e_aux a b c ⊔ d_aux a b c) ⊓ (a ⊓ e_aux a b c))" by (simp add: modular) also have "… = d_aux a b c ⊔ (d_aux a b c ⊔ e_aux a b c ⊓ b) ⊓ (a ⊓ e_aux a b c)" by (simp add: inf_commute sup_commute) also have "… = d_aux a b c ⊔ (e_aux a b c ⊓ (d_aux a b c ⊔ b)) ⊓ (a ⊓ e_aux a b c)" by (cut_tac d_less_e, simp add: modular [THEN sym] less_le) also have "… = d_aux a b c ⊔ ((a ⊓ e_aux a b c) ⊓ (e_aux a b c ⊓ (b ⊔ d_aux a b c)))" by (simp add: inf_commute sup_commute) also have "… = d_aux a b c ⊔ (a ⊓ e_aux a b c ⊓ (b ⊔ d_aux a b c))" by (simp add: inf_assoc) also have "… = d_aux a b c ⊔ (a ⊓ e_aux a b c ⊓ (b ⊔ (c ⊓ a)))" by (simp add: b_join_d) also have "… = d_aux a b c ⊔ (a ⊓ (b ⊔ c) ⊓ (b ⊔ (c ⊓ a)))" by (simp add: a_meet_e) also have "… = d_aux a b c ⊔ (a ⊓ ((b ⊔ c) ⊓ (b ⊔ (c ⊓ a))))" by (simp add: inf_assoc) also have "… = d_aux a b c ⊔ (a ⊓ (b ⊔ ((b ⊔ c) ⊓ (c ⊓ a))))" by (simp add: modular) also have "… = d_aux a b c ⊔ (a ⊓ (b ⊔ (c ⊓ a)))" by (simp add: inf_absorb2) also have "… = d_aux a b c ⊔ (a ⊓ ((c ⊓ a) ⊔ b))" by (simp add: sup_commute inf_commute) also have "… = d_aux a b c ⊔ ((c ⊓ a) ⊔ (a ⊓ b))" by (simp add: modular) also have "… = d_aux a b c" by (rule order.antisym, simp_all add: d_aux_def) finally show ?thesis by (simp add: a_aux_def b_aux_def) qed lemma b_meet_c_eq_d: " d_aux a b c ≤ e_aux a b c ⟹ b_aux a b c ⊓ c_aux a b c = d_aux a b c" apply (subst b_a) apply (subgoal_tac "c_aux a b c = b_aux b c a") apply simp apply (subst a_meet_b_eq_d) by (simp_all add: c_aux_def b_aux_def d_b_c_a e_b_c_a) lemma c_meet_a_eq_d: "d_aux a b c ≤ e_aux a b c ⟹ c_aux a b c ⊓ a_aux a b c = d_aux a b c" apply (subst c_a) apply (subgoal_tac "a_aux a b c = b_aux c a b") apply simp apply (subst a_meet_b_eq_d) by (simp_all add: a_aux_def b_aux_def d_b_c_a e_b_c_a) lemma a_def_equiv: "d_aux a b c ≤ e_aux a b c ⟹ a_aux a b c = (a ⊔ d_aux a b c) ⊓ e_aux a b c" apply (simp add: a_aux_def) apply (subst inf_commute) apply (subst sup_commute) apply (simp add: modular) by (simp add: inf_commute sup_commute) lemma b_def_equiv: "d_aux a b c ≤ e_aux a b c ⟹ b_aux a b c = (b ⊔ d_aux a b c) ⊓ e_aux a b c" apply (cut_tac a = b and b = c and c = a in a_def_equiv) by (simp_all add: d_b_c_a e_b_c_a b_a) lemma c_def_equiv: "d_aux a b c ≤ e_aux a b c ⟹ c_aux a b c = (c ⊔ d_aux a b c) ⊓ e_aux a b c" apply (cut_tac a = c and b = a and c = b in a_def_equiv) by (simp_all add: d_c_a_b e_c_a_b c_a) lemma a_join_b_eq_e: "d_aux a b c ≤ e_aux a b c ⟹ a_aux a b c ⊔ b_aux a b c = e_aux a b c" proof - assume d_less_e: " d_aux a b c ≤ e_aux a b c" have "((a ⊔ d_aux a b c) ⊓ e_aux a b c) ⊔ ((b ⊔ d_aux a b c) ⊓ e_aux a b c) = ((b ⊔ d_aux a b c) ⊓ e_aux a b c) ⊔ (e_aux a b c ⊓ (a ⊔ d_aux a b c))" by (simp add: inf_commute sup_commute) also have "… = e_aux a b c ⊓ (((b ⊔ d_aux a b c) ⊓ e_aux a b c) ⊔ (a ⊔ d_aux a b c))" by (simp add: modular) also have "… = e_aux a b c ⊓ ((e_aux a b c ⊓ (d_aux a b c ⊔ b)) ⊔ (a ⊔ d_aux a b c))" by (simp add: inf_commute sup_commute) also have "… = e_aux a b c ⊓ ((d_aux a b c ⊔ (e_aux a b c ⊓ b)) ⊔ (a ⊔ d_aux a b c))" by (cut_tac d_less_e, simp add: modular) also have "… = e_aux a b c ⊓ ((a ⊔ d_aux a b c) ⊔ (d_aux a b c ⊔ (b ⊓ e_aux a b c)))" by (simp add: inf_commute sup_commute) also have "… = e_aux a b c ⊓ (a ⊔ d_aux a b c ⊔ (b ⊓ e_aux a b c))" by (simp add: sup_assoc) also have "… = e_aux a b c ⊓ (a ⊔ d_aux a b c ⊔ (b ⊓ (c ⊔ a)))" by (simp add: b_meet_e) also have "… = e_aux a b c ⊓ (a ⊔ (b ⊓ c) ⊔ (b ⊓ (c ⊔ a)))" by (simp add: a_join_d) also have "… = e_aux a b c ⊓ (a ⊔ ((b ⊓ c) ⊔ (b ⊓ (c ⊔ a))))" by (simp add: sup_assoc) also have "… = e_aux a b c ⊓ (a ⊔ (b ⊓ ((b ⊓ c) ⊔ (c ⊔ a))))" by (simp add: modular) also have "… = e_aux a b c ⊓ (a ⊔ (b ⊓ (c ⊔ a)))" by (simp add: sup_absorb2) also have "… = e_aux a b c ⊓ (a ⊔ ((c ⊔ a) ⊓ b))" by (simp add: sup_commute inf_commute) also have "… = e_aux a b c ⊓ ((c ⊔ a) ⊓ (a ⊔ b))" by (simp add: modular) also have "… = e_aux a b c" by (rule order.antisym, simp_all, simp_all add: e_aux_def) finally show ?thesis by (cut_tac d_less_e, simp add: a_def_equiv b_def_equiv) qed lemma b_join_c_eq_e: " d_aux a b c <= e_aux a b c ⟹ b_aux a b c ⊔ c_aux a b c = e_aux a b c" apply (subst b_a) apply (subgoal_tac "c_aux a b c = b_aux b c a") apply simp apply (subst a_join_b_eq_e) by (simp_all add: c_aux_def b_aux_def d_b_c_a e_b_c_a) lemma c_join_a_eq_e: "d_aux a b c <= e_aux a b c ⟹ c_aux a b c ⊔ a_aux a b c = e_aux a b c" apply (subst c_a) apply (subgoal_tac "a_aux a b c = b_aux c a b") apply simp apply (subst a_join_b_eq_e) by (simp_all add: a_aux_def b_aux_def d_b_c_a e_b_c_a) lemma "no_distrib a b c ⟹ incomp a b" apply (simp add: no_distrib_def incomp_def ac_simps) using order.strict_iff_not inf.absorb_iff2 inf.commute modular apply fastforce done lemma M5_modular: "no_distrib a b c ⟹ M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)" apply (frule d_less_e) by (simp add: M5_lattice_def a_meet_b_eq_d b_meet_c_eq_d c_meet_a_eq_d a_join_b_eq_e b_join_c_eq_e c_join_a_eq_e) lemma M5_modular_def: "M5_lattice a b c = (a ⊓ b = b ⊓ c ∧ c ⊓ a = b ⊓ c ∧ a ⊔ b = b ⊔ c ∧ c ⊔ a = b ⊔ c ∧ a ⊓ b < a ⊔ b)" by (simp add: M5_lattice_def) end context lattice begin lemma not_modular_N5: "(¬ class.modular_lattice inf ((≤)::'a ⇒ 'a ⇒ bool) (<) sup) = (∃ a b c::'a . N5_lattice a b c)" apply (subgoal_tac "class.lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) sup") apply (unfold N5_lattice_def class.modular_lattice_def class.modular_lattice_axioms_def) apply simp_all apply safe apply (subgoal_tac "x ⊔ y ⊓ z < y ⊓ (x ⊔ z)") apply (rule_tac x = "x ⊔ y ⊓ z" in exI) apply (rule_tac x = "y ⊓ (x ⊔ z)" in exI) apply (rule_tac x = z in exI) apply safe apply (rule order.antisym) apply simp apply (rule_tac y = "x ⊔ y ⊓ z" in order_trans) apply simp_all apply (rule_tac y = "y ⊓ z" in order_trans) apply simp_all apply (rule order.antisym) apply simp_all apply (rule_tac y = "y ⊓ (x ⊔ z)" in order_trans) apply simp_all apply (rule_tac y = "x ⊔ z" in order_trans) apply simp_all apply (rule neq_le_trans) apply simp apply simp apply (rule_tac x = a in exI) apply (rule_tac x = b in exI) apply safe apply (simp add: less_le) apply (rule_tac x = c in exI) apply simp apply (simp add: less_le) apply safe apply (subgoal_tac "a ⊔ a ⊓ c = b") apply (unfold sup_inf_absorb) [1] apply simp apply simp proof qed lemma not_distrib_N5_M5: "(¬ class.distrib_lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) (⊔)) = ((∃ a b c::'a . N5_lattice a b c) ∨ (∃ a b c::'a . M5_lattice a b c))" apply (unfold not_modular_N5 [THEN sym]) proof assume A: "¬ class.distrib_lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) (⊔)" have B: "∃ a b c:: 'a . (a ⊓ b) ⊔ (a ⊓ c) < a ⊓ (b ⊔ c)" apply (cut_tac A) apply (unfold class.distrib_lattice_def) apply safe apply simp_all proof fix x y z::'a assume A: "∀(a::'a) (b::'a) c::'a. ¬ a ⊓ b ⊔ a ⊓ c < a ⊓ (b ⊔ c)" show "x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)" apply (cut_tac A) apply (rule distrib_imp1) by (simp add: less_le) qed from B show "¬ class.modular_lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) (⊔) ∨ (∃a b c::'a. M5_lattice a b c)" proof (unfold disj_not1, safe) fix a b c::'a assume A: "a ⊓ b ⊔ a ⊓ c < a ⊓ (b ⊔ c)" assume B: "class.modular_lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) (⊔)" interpret modular: modular_lattice "(⊓)" "((≤)::'a ⇒ 'a ⇒ bool)" "(<)" "(⊔)" by (fact B) have H: "M5_lattice (a_aux a b c) (b_aux a b c) (c_aux a b c)" apply (cut_tac a = a and b = b and c = c in modular.M5_modular) apply (unfold no_distrib_def) by (simp_all add: A inf_commute) from H show "∃a b c::'a. M5_lattice a b c" by blast qed next assume A: "¬ class.modular_lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) (⊔) ∨ (∃(a::'a) (b::'a) c::'a. M5_lattice a b c)" show "¬ class.distrib_lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) (⊔)" apply (cut_tac A) apply safe apply (erule notE) apply unfold_locales apply (unfold class.distrib_lattice_def) apply (unfold class.distrib_lattice_axioms_def) apply safe apply (simp add: sup_absorb2) apply (frule M5_lattice_incomp) apply (unfold M5_lattice_def) apply (drule_tac x = a in spec) apply (drule_tac x = b in spec) apply (drule_tac x = c in spec) apply safe proof - fix a b c:: 'a assume A:"a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)" assume B: "a ⊓ b = b ⊓ c" assume D: "a ⊔ b = b ⊔ c" assume E: "c ⊔ a = b ⊔ c" assume G: "incomp a b" have H: "a ⊔ b ⊓ c = a" by (simp add: B [THEN sym] sup_absorb1) have I: "(a ⊔ b) ⊓ (a ⊔ c) = a ⊔ b" by (cut_tac E, simp add: sup_commute D) have J: "a = a ⊔ b" by (cut_tac A, simp add: H I) show False apply (cut_tac G J) apply (subgoal_tac "b ≤ a") apply (simp add: incomp_def) apply (rule_tac y = "a ⊔ b" in order_trans) apply (rule sup_ge2) by simp qed qed lemma distrib_not_N5_M5: "(class.distrib_lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) (⊔)) = ((∀ a b c::'a . ¬ N5_lattice a b c) ∧ (∀ a b c::'a . ¬ M5_lattice a b c))" apply (cut_tac not_distrib_N5_M5) by auto lemma distrib_inf_sup_eq: "(class.distrib_lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) (⊔)) = (∀ x y z::'a . x ⊓ z = y ⊓ z ∧ x ⊔ z = y ⊔ z ⟶ x = y)" apply safe proof - fix x y z:: 'a assume A: "class.distrib_lattice (⊓) ((≤) ::'a ⇒ 'a ⇒ bool) (<) (⊔)" interpret distrib: distrib_lattice "(⊓)" "(≤) :: 'a ⇒ 'a ⇒ bool" "(<)" "(⊔)" by (fact A) assume B: "x ⊓ z = y ⊓ z" assume C: "x ⊔ z = y ⊔ z" have "x = x ⊓ (x ⊔ z)" by simp also have "… = x ⊓ (y ⊔ z)" by (simp add: C) also have "… = (x ⊓ y) ⊔ (x ⊓ z)" by (simp add: distrib.inf_sup_distrib) also have "… = (y ⊓ x) ⊔ (y ⊓ z)" by (simp add: B inf_commute) also have "… = y ⊓ (x ⊔ z)" by (simp add: distrib.inf_sup_distrib) also have "… = y" by (simp add: C) finally show "x = y" . next assume A: "(∀x y z:: 'a. x ⊓ z = y ⊓ z ∧ x ⊔ z = y ⊔ z ⟶ x = y)" have B: "!! x y z :: 'a. x ⊓ z = y ⊓ z ∧ x ⊔ z = y ⊔ z ⟹ x = y" by (cut_tac A, blast) show "class.distrib_lattice (⊓) ((≤)::'a ⇒ 'a ⇒ bool) (<) (⊔)" apply (unfold distrib_not_N5_M5) apply safe apply (unfold N5_lattice_def) apply (cut_tac x = a and y = b and z = c in B) apply (simp_all) apply (unfold M5_lattice_def) apply (cut_tac x = a and y = b and z = c in B) by (simp_all add: inf_commute sup_commute) qed end class inf_sup_eq_lattice = lattice + assumes inf_sup_eq: "x ⊓ z = y ⊓ z ⟹ x ⊔ z = y ⊔ z ⟹ x = y" begin subclass distrib_lattice by (metis distrib_inf_sup_eq inf_sup_eq) end end