How to derive distributivity from Boolean algebra laws

Let $(L,\le,\bot,\top)$ be a bounded lattice and $\neg: L \rightarrow L$ be a map that satisfies the following laws:

1. $a \wedge b = \bot \Leftrightarrow a \le \neg b$
2. $\neg\neg a =a$

I'd like to show distributivity, namely, $a\wedge(b\vee c) = (a \wedge b) \vee (a \wedge c)$ and $a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c)$.

I've already shown the following laws:

1. $a \wedge \neg a = \bot$, $a \vee \neg a = \top$
2. The de Morgan's laws: $\neg (a \wedge b) = \neg a \vee \neg b$ and $\neg (a \vee b) = \neg a \wedge \neg b$

I've also shown the distributive inequalities that hold for all lattices, and that the two forms of distributivity are equivalent. How should I use these laws to show what I'd like to?

-
I wanted to say that any Heyting algebra is automatically distributive, but I'm having trouble showing that $(\lnot a \lor b)$ defines a Heyting implication precisely because we don't have the distributive law... –  Zhen Lin Aug 26 '12 at 15:17
@ZhenLin Yes, this should be fairly complicated. When I peeped at my peer's answer, it was somewhat lengthy. –  Pteromys Aug 26 '12 at 15:37
I figured it out... turns out having double negation elimination around is very handy. –  Zhen Lin Aug 26 '12 at 15:52

First, let's recall the notion of a Heyting implication $\to$: it is a binary operation on a lattice such that $$a \le (b \to c) \text{ if and only if } (a \land b) \le c$$ A lattice equipped with a Heyting implication $\to$ is automatically distributive. Indeed, $a \land (b \lor c) \le d$ if and only if $(b \lor c) \le (a \to d)$, so if and only if $b \le (a \to d)$ and $c \le (a \to d)$, so if and only if $a \land b \le d$ and $a \land c \le d$. Hence, $a \land (b \lor c) \le (a \land b) \lor (a \land c)$ and $(a \land b) \lor (a \land c) \le a \land (b \lor c)$.

Now, a lattice equipped with a boolean negation automatically has a Heyting implication: take $(a \to b) = \lnot (b \land \lnot c)$, as usual. This works, because $a \land b \le c = \lnot \lnot c$ implies $a \land b \land \lnot c = \bot$, so $a \le \lnot (b \land \lnot c)$; why $a \le \lnot (b \land \lnot c)$ implies $a \land b \land \lnot c = \bot$, so $a \land b \le \lnot \lnot c = c$.

-