Theory LatticeProperties.Modular_Distrib_Lattice

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