Theory LatticeProperties.Modular_Distrib_Lattice
section‹Modular and Distributive Lattices›
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