# Theory Modular_Distrib_Lattice

Up to index of Isabelle/HOL/LatticeProperties

theory Modular_Distrib_Lattice
imports Lattice_Prop
`header{* Modular and Distributive Lattices *}(*    Author: Viorel Preoteasa*)theory Modular_Distrib_Latticeimports Lattice_Propbegintext {*The main result of this theory is the fact that a lattice is distributiveif and only if it satisfies the following property:*}term "(∀ x y z . x \<sqinter> z = y \<sqinter> z ∧ x \<squnion> z = y \<squnion> z ==> x = y)"text{*This result was proved by Bergmann in \cite{bergmann:1929}. The formalizationpresented here is based on \cite{birkhoff:1967,burris:sankappanavar:1981}.*}class modular_lattice = lattice +  assumes modular: "x ≤ y ==>  x \<squnion> (y \<sqinter> z) = y \<sqinter> (x \<squnion> z)"context distrib_lattice beginsubclass modular_lattice  apply unfold_locales  by (simp add: inf_sup_distrib inf_absorb2)endcontext lattice begindefinition  "d_aux a b c = (a \<sqinter> b) \<squnion> (b \<sqinter> c) \<squnion> (c \<sqinter> 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 \<squnion> b) \<sqinter> (b \<squnion> c) \<sqinter> (c \<squnion> a)"lemma e_b_c_a: "e_aux b c a = e_aux a b c"  apply (simp add: e_aux_def)  apply (rule antisym)  by (simp_all add: sup_commute)lemma e_c_a_b: "e_aux c a b = e_aux a b c"  apply (simp add: e_aux_def)  apply (rule antisym)  by (simp_all add: sup_commute)definition  "a_aux a b c = (a \<sqinter> (e_aux a b c)) \<squnion> (d_aux a b c)"definition  "b_aux a b c = (b \<sqinter> (e_aux a b c)) \<squnion> (d_aux a b c)"definition  "c_aux a b c = (c \<sqinter> (e_aux a b c)) \<squnion> (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 \<squnion> b) \<sqinter> (b \<squnion> c) \<sqinter> (c \<squnion> a)" in order_trans)  apply (rule inf_le2)  by simplemma [simp]: "b_aux a b c ≤ e_aux a b c"  apply (unfold b_a)  apply (subst e_b_c_a [THEN sym])  by simplemma [simp]: "c_aux a b c ≤ e_aux a b c"  apply (unfold c_a)  apply (subst e_c_a_b [THEN sym])  by simplemma [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 simplemma [simp]: "d_aux a b c ≤ c_aux a b c"  apply (unfold c_a)  apply (subst d_c_a_b [THEN sym])  by simplemma a_meet_e: "a \<sqinter> (e_aux a b c) = a \<sqinter> (b \<squnion> c)"  apply (simp add: e_aux_def)  apply (rule antisym)  apply simp_all  apply (rule_tac y = "(a \<squnion> b) \<sqinter> (b \<squnion> c) \<sqinter> (c \<squnion> a)" in order_trans)  apply (rule inf_le2)  by simp  lemma b_meet_e: "b \<sqinter> (e_aux a b c) = b \<sqinter> (c \<squnion> a)"  by (simp add: a_meet_e [THEN sym] e_b_c_a)lemma c_meet_e: "c \<sqinter> (e_aux a b c) = c \<sqinter> (a \<squnion> b)"  by (simp add: a_meet_e [THEN sym] e_c_a_b)lemma a_join_d: "a \<squnion> d_aux a b c = a \<squnion> (b \<sqinter> c)"  apply (simp add: d_aux_def)  apply (rule antisym)  apply simp_all  apply (rule_tac y = "a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a" in order_trans)  by simp_alllemma b_join_d: "b \<squnion> d_aux a b c = b \<squnion> (c \<sqinter> a)"  by (simp add: a_join_d [THEN sym] d_b_c_a)endcontext lattice begindefinition  "no_distrib a b c = (a \<sqinter> b \<squnion> c \<sqinter> a < a \<sqinter> (b \<squnion> c))"definition  "incomp x y = (¬ x ≤ y ∧ ¬ y ≤ x)"definition   "N5_lattice a b c = (a \<sqinter> c = b \<sqinter> c ∧ a < b ∧ a \<squnion> c = b \<squnion> c)"definition   "M5_lattice a b c = (a \<sqinter> b = b \<sqinter> c ∧ c \<sqinter> a = b \<sqinter> c ∧ a \<squnion> b = b \<squnion> c ∧ c \<squnion> a = b \<squnion> c ∧ a \<sqinter> b < a \<squnion> 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 \<sqinter> (b \<squnion> c) = c")  apply simp  apply (subst sup_commute)  by simpendcontext modular_lattice beginlemma a_meet_d: "a \<sqinter> (d_aux a b c) = (a \<sqinter> b) \<squnion> (c \<sqinter> a)"  proof -    have "a \<sqinter> (d_aux a b c) = a \<sqinter> ((a \<sqinter> b) \<squnion> (b \<sqinter> c) \<squnion> (c \<sqinter> a))" by (simp add: d_aux_def)    also have "... = a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c)" by (simp add: sup_assoc, simp add: sup_commute)    also have "... = (a \<sqinter> b \<squnion> c \<sqinter> a) \<squnion> (a \<sqinter> (b \<sqinter> c))" by (simp add: modular)    also have "... = (a \<sqinter> b) \<squnion> (c \<sqinter> a)" by (rule antisym, simp_all, rule_tac y = "a \<sqinter> b" in order_trans, simp_all)    finally show ?thesis by simp  qed  lemma b_meet_d: "b \<sqinter> (d_aux a b c) = (b \<sqinter> c) \<squnion> (a \<sqinter> b)"  by (simp add: a_meet_d [THEN sym] d_b_c_a)lemma c_meet_d: "c \<sqinter> (d_aux a b c) = (c \<sqinter> a) \<squnion> (b \<sqinter> 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_alllemma a_meet_b_eq_d: " d_aux a b c ≤ e_aux a b c ==> a_aux a b c \<sqinter> 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 \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) = (b \<sqinter> e_aux a b c \<squnion>  d_aux a b c) \<sqinter> (d_aux a b c \<squnion> a \<sqinter> e_aux a b c)"      by (simp add: inf_commute sup_commute)    also have "… = d_aux a b c \<squnion> ((b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (a \<sqinter> e_aux a b c))"       by (simp add: modular)    also have "… = d_aux a b c \<squnion> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b) \<sqinter> (a \<sqinter> e_aux a b c)"       by (simp add: inf_commute sup_commute)    also have "… = d_aux a b c \<squnion> (e_aux a b c \<sqinter> (d_aux a b c \<squnion> b)) \<sqinter> (a \<sqinter> 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 \<squnion> ((a \<sqinter> e_aux a b c) \<sqinter> (e_aux a b c \<sqinter> (b \<squnion> d_aux a b c)))"       by (simp add: inf_commute sup_commute)    also have "… = d_aux a b c \<squnion> (a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> d_aux a b c))" by (simp add: inf_assoc)    also have "… = d_aux a b c \<squnion> (a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> (c \<sqinter> a)))" by (simp add: b_join_d)    also have "… = d_aux a b c \<squnion> (a \<sqinter> (b \<squnion> c) \<sqinter> (b \<squnion> (c \<sqinter> a)))" by (simp add: a_meet_e)    also have "… = d_aux a b c \<squnion> (a \<sqinter> ((b \<squnion> c) \<sqinter> (b \<squnion> (c \<sqinter> a))))" by (simp add: inf_assoc)    also have "… = d_aux a b c \<squnion> (a \<sqinter> (b \<squnion> ((b \<squnion> c) \<sqinter> (c \<sqinter> a))))" by (simp add: modular)    also have "… = d_aux a b c \<squnion> (a \<sqinter> (b \<squnion> (c \<sqinter> a)))" by (simp add: inf_absorb2)    also have "… = d_aux a b c \<squnion> (a \<sqinter> ((c \<sqinter> a) \<squnion> b))" by (simp add: sup_commute inf_commute)    also have "… = d_aux a b c \<squnion> ((c \<sqinter> a) \<squnion> (a \<sqinter> b))" by (simp add: modular)    also have "… = d_aux a b c"      by (rule antisym, simp_all add: d_aux_def)    finally show ?thesis by (simp add: a_aux_def b_aux_def)  qedlemma b_meet_c_eq_d: " d_aux a b c ≤ e_aux a b c ==> b_aux a b c \<sqinter> 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 \<sqinter> 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 \<squnion> d_aux a b c) \<sqinter> 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 \<squnion> d_aux a b c) \<sqinter> 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 \<squnion> d_aux a b c) \<sqinter> 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 \<squnion> 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 \<squnion> d_aux a b c) \<sqinter> e_aux a b c) \<squnion> ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c) = ((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c) \<squnion> (e_aux a b c \<sqinter> (a \<squnion> d_aux a b c))"      by (simp add: inf_commute sup_commute)    also have "… = e_aux a b c \<sqinter> (((b \<squnion> d_aux a b c) \<sqinter> e_aux a b c) \<squnion> (a \<squnion> d_aux a b c))"       by (simp add: modular)    also have "… = e_aux a b c \<sqinter> ((e_aux a b c \<sqinter> (d_aux a b c \<squnion> b)) \<squnion> (a \<squnion> d_aux a b c))"       by (simp add: inf_commute sup_commute)    also have "… = e_aux a b c \<sqinter> ((d_aux a b c \<squnion> (e_aux a b c \<sqinter> b)) \<squnion> (a \<squnion> d_aux a b c))"       by (cut_tac d_less_e, simp add: modular)    also have "… = e_aux a b c \<sqinter> ((a \<squnion> d_aux a b c) \<squnion> (d_aux a b c \<squnion> (b \<sqinter> e_aux a b c)))"       by (simp add: inf_commute sup_commute)    also have "… = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (b \<sqinter> e_aux a b c))" by (simp add: sup_assoc)    also have "… = e_aux a b c \<sqinter> (a \<squnion> d_aux a b c \<squnion> (b \<sqinter> (c \<squnion> a)))" by (simp add: b_meet_e)    also have "… = e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> c) \<squnion> (b \<sqinter> (c \<squnion> a)))" by (simp add: a_join_d)    also have "… = e_aux a b c \<sqinter> (a \<squnion> ((b \<sqinter> c) \<squnion> (b \<sqinter> (c \<squnion> a))))" by (simp add: sup_assoc)    also have "… = e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> ((b \<sqinter> c) \<squnion> (c \<squnion> a))))" by (simp add: modular)    also have "… = e_aux a b c \<sqinter> (a \<squnion> (b \<sqinter> (c \<squnion> a)))" by (simp add: sup_absorb2)     also have "… = e_aux a b c \<sqinter> (a \<squnion> ((c \<squnion> a) \<sqinter> b))" by (simp add: sup_commute inf_commute)    also have "… = e_aux a b c \<sqinter> ((c \<squnion> a) \<sqinter> (a \<squnion> b))" by (simp add: modular)    also have "… = e_aux a b c"      by (rule 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)  qedlemma b_join_c_eq_e: " d_aux a b c <= e_aux a b c ==> b_aux a b c \<squnion> 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 \<squnion> 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)  apply safe  apply (simp add: inf_absorb1)   apply (subgoal_tac "a \<squnion> c \<sqinter> a = a ∧ a \<sqinter> (b \<squnion> c) = a")  apply simp  apply safe  apply (rule antisym)  apply simp  apply simp  apply (rule antisym)  apply simp_all  apply (rule_tac y = b in order_trans)  apply simp_all  apply (simp add: inf_absorb2)   apply (unfold modular [THEN sym])  by (simp add: inf_commute)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 \<sqinter> b = b \<sqinter> c ∧ c \<sqinter> a = b \<sqinter> c ∧ a \<squnion> b = b \<squnion> c ∧ c \<squnion> a = b \<squnion> c ∧ a \<sqinter> b < a \<squnion> b)"  by (simp add: M5_lattice_def)endcontext lattice beginlemma not_modular_N5: "(¬ class.modular_lattice inf ((op ≤)::'a => 'a => bool) op < sup) =   (∃ a b c::'a . N5_lattice a b c)"  apply (subgoal_tac "class.lattice op \<sqinter> ((op ≤)::'a => 'a => bool) op < sup")  apply (unfold N5_lattice_def class.modular_lattice_def class.modular_lattice_axioms_def)  apply simp_all  apply safe  apply (subgoal_tac "x \<squnion> y \<sqinter> z < y \<sqinter> (x \<squnion> z)")  apply (rule_tac x = "x \<squnion> y \<sqinter> z" in exI)  apply (rule_tac x = "y \<sqinter> (x \<squnion> z)" in exI)  apply (rule_tac x = z in exI)  apply safe  apply (rule antisym)  apply simp  apply (rule_tac y = "x \<squnion> y \<sqinter> z" in order_trans)  apply simp_all  apply (rule_tac y = "y \<sqinter> z" in order_trans)  apply simp_all  apply (rule antisym)  apply simp_all  apply (rule_tac y = "y \<sqinter> (x \<squnion> z)" in order_trans)  apply simp_all  apply (rule_tac y = "x \<squnion> 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 \<squnion> a \<sqinter> c = b")  apply (unfold sup_inf_absorb) [1]  apply simp  apply simp  proof qedlemma not_distrib_N5_M5: "(¬ class.distrib_lattice op \<sqinter> ((op ≤)::'a => 'a => bool) op < op \<squnion>) =   ((∃ 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 op \<sqinter> ((op ≤)::'a => 'a => bool) op < op \<squnion>"    have B: "∃ a b c:: 'a . (a \<sqinter> b) \<squnion> (a \<sqinter> c) < a \<sqinter> (b \<squnion> 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 \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)"        show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"          apply (cut_tac A)          apply (rule distrib_imp1)          by (simp add: less_le)      qed    from B show "¬ class.modular_lattice op \<sqinter> ((op ≤)::'a => 'a => bool) op < op \<squnion> ∨ (∃a b c::'a. M5_lattice a b c)"      proof (unfold disj_not1, safe)        fix a b c::'a        assume A: "a \<sqinter> b \<squnion> a \<sqinter> c < a \<sqinter> (b \<squnion> c)"        assume B: "class.modular_lattice op \<sqinter> ((op ≤)::'a => 'a => bool) op < op \<squnion>"        interpret modular: modular_lattice "op \<sqinter>" "((op ≤)::'a => 'a => bool)" "op <" "op \<squnion>"          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 op \<sqinter> ((op ≤)::'a => 'a => bool) op < op \<squnion> ∨ (∃(a::'a) (b::'a) c::'a. M5_lattice a b c)"     show "¬ class.distrib_lattice op \<sqinter> ((op ≤)::'a => 'a => bool) op < op \<squnion>"       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 \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)"         assume B: "a \<sqinter> b = b \<sqinter> c"         assume D: "a \<squnion> b = b \<squnion> c"         assume E: "c \<squnion> a = b \<squnion> c"         assume G: "incomp a b"         have H: "a \<squnion> b \<sqinter> c = a" by (simp add: B [THEN sym] sup_absorb1)         have I: "(a \<squnion> b) \<sqinter> (a \<squnion> c) = a \<squnion> b" by (cut_tac E, simp add: sup_commute D)         have J: "a = a \<squnion> 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 \<squnion> b" in order_trans)           apply (rule sup_ge2)           by simp       qed     qed lemma distrib_not_N5_M5: "(class.distrib_lattice op \<sqinter> ((op ≤)::'a => 'a => bool) op < op \<squnion>) =   ((∀ 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 autolemma distrib_inf_sup_eq:  "(class.distrib_lattice op \<sqinter> ((op ≤)::'a => 'a => bool) op < op \<squnion>) =     (∀ x y z::'a . x \<sqinter> z = y \<sqinter> z ∧ x \<squnion> z = y \<squnion> z --> x = y)"  apply safe  proof -    fix x y z:: 'a    assume A: "class.distrib_lattice op \<sqinter> (op ≤ ::'a => 'a => bool) op < op \<squnion>"    interpret distrib: distrib_lattice "op \<sqinter>" "op ≤ :: 'a => 'a => bool" "op <" "op \<squnion>"      by (fact A)    assume B: "x \<sqinter> z = y \<sqinter> z"    assume C: "x \<squnion> z = y \<squnion> z"    have "x = x \<sqinter> (x \<squnion> z)" by simp    also have "… = x \<sqinter> (y \<squnion> z)" by (simp add: C)    also have "… = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by (simp add: distrib.inf_sup_distrib)    also have "… = (y \<sqinter> x) \<squnion> (y \<sqinter> z)" by (simp add: B inf_commute)    also have "… = y \<sqinter> (x \<squnion> 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 \<sqinter> z = y \<sqinter> z ∧ x \<squnion> z = y \<squnion> z --> x = y)"    have B: "!! x y z :: 'a. x \<sqinter> z = y \<sqinter> z ∧ x \<squnion> z = y \<squnion> z ==> x = y"      by (cut_tac A, blast)    show "class.distrib_lattice op \<sqinter> ((op ≤)::'a => 'a => bool) op < op \<squnion>"      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) qedendclass inf_sup_eq_lattice = lattice +  assumes inf_sup_eq: "x \<sqinter> z = y \<sqinter> z ==> x \<squnion> z = y \<squnion> z ==> x = y"beginsubclass distrib_lattice  by (metis distrib_inf_sup_eq inf_sup_eq)endend`