# Theory Robbins_Conjecture

section ‹Robbins Conjecture›

theory Robbins_Conjecture
imports Main
begin

text ‹The document gives a formalization of the proof of the Robbins
conjecture, following A. Mann, \emph{A Complete Proof of the
Robbins Conjecture}, 2003, DOI 10.1.1.6.7838›

section ‹Axiom Systems›

text ‹The following presents several axiom systems that shall be under study.

The first axiom sets common systems that underly all of
the systems we shall be looking at.

The second system is a reformulation of Boolean algebra.  We shall
follow pages 7--8 in S. Koppelberg. \emph{General Theory of Boolean
Algebras}, Volume 1 of \emph{Handbook of Boolean Algebras}. North
Holland, 1989. Note that our formulation deviates slightly from this,
as we only provide one distribution axiom, as the dual is redundant.

The third system is Huntington's algebra and the fourth system is
Robbins' algebra.

Apart from the common system, all of these systems are demonstrated
to be equivalent to the library formulation of Boolean algebra, under
appropriate interpretation.›

subsection ‹Common Algebras›

class common_algebra = uminus +
fixes inf :: "'a ⇒ 'a ⇒ 'a" (infixl "⊓" 70)
fixes sup :: "'a ⇒ 'a ⇒ 'a" (infixl "⊔" 65)
fixes bot :: "'a" ("⊥")
fixes top :: "'a" ("⊤")
assumes sup_assoc: "x ⊔ (y ⊔ z) = (x ⊔ y) ⊔ z"
assumes sup_comm: "x ⊔ y = y ⊔ x"

context common_algebra begin

definition less_eq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50) where
"x ⊑ y = (x ⊔ y = y)"
definition less :: "'a ⇒ 'a ⇒ bool" (infix "⊏" 50) where
"x ⊏ y = (x ⊑ y ∧ ¬ y ⊑ x)"
definition minus :: "'a ⇒ 'a ⇒ 'a"  (infixl "-" 65) where
"minus x y = (x ⊓ - y)"

(* We shall need some object in order to define falsum and verum *)
definition secret_object1 :: "'a" ("ι") where
"ι = (SOME x. True)"

end

class ext_common_algebra = common_algebra +
assumes inf_eq: "x ⊓ y = -(- x ⊔ - y)"
assumes top_eq: "⊤ = ι ⊔ - ι"
assumes bot_eq: "⊥ = -(ι ⊔ - ι)"

subsection ‹Boolean Algebra›

class boolean_algebra_II =
common_algebra +
assumes inf_comm: "x ⊓ y = y ⊓ x"
assumes inf_assoc: "x ⊓ (y ⊓ z) = (x ⊓ y) ⊓ z"
assumes sup_absorb: "x ⊔ (x ⊓ y) = x"
assumes inf_absorb: "x ⊓ (x ⊔ y) = x"
assumes sup_inf_distrib1: "x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)"
assumes sup_compl: "x ⊔ - x = ⊤"
assumes inf_compl: "x ⊓ - x = ⊥"

subsection ‹Huntington's Algebra›

class huntington_algebra = ext_common_algebra +
assumes huntington: "- (-x ⊔ -y) ⊔ - (-x ⊔  y) = x"

subsection ‹Robbins' Algebra›

class robbins_algebra = ext_common_algebra +
assumes robbins: "- (- (x ⊔ y) ⊔ - (x ⊔ -y)) = x"

section ‹Equivalence›

text ‹With our axiom systems defined, we turn to providing equivalence
results between them.

We shall begin by illustrating equivalence for our formulation and
the library formulation of Boolean algebra.›

subsection ‹Boolean Algebra›

text ‹The following provides the canonical definitions for order and
relative complementation for Boolean algebras.  These are necessary
since the Boolean algebras presented in the Isabelle/HOL library have
a lot of structure, while our formulation is considerably simpler.

Since our formulation of Boolean algebras is considerably simple, it is
easy to show that the library instantiates our axioms.›

context boolean_algebra_II begin

lemma boolean_II_is_boolean:
"class.boolean_algebra minus uminus (⊓) (⊑) (⊏) (⊔) ⊥ ⊤"
apply unfold_locales
apply (metis inf_absorb inf_assoc inf_comm inf_compl
less_def less_eq_def minus_def
sup_absorb sup_assoc sup_comm
sup_compl sup_inf_distrib1
sup_absorb inf_comm)+
done

end

context boolean_algebra begin

lemma boolean_is_boolean_II:
"class.boolean_algebra_II uminus inf sup bot top"
apply unfold_locales
apply (metis sup_assoc sup_commute sup_inf_absorb sup_compl_top
inf_assoc inf_commute inf_sup_absorb inf_compl_bot
sup_inf_distrib1)+
done

end

subsection ‹Huntington Algebra›

text ‹We shall illustrate here that all Boolean algebra using our
formulation are Huntington algebras, and illustrate that every
Huntington algebra may be interpreted as a Boolean algebra.

Since the Isabelle/HOL library has good automation, it is convenient
to first show that the library instances Huntington algebras to exploit
previous results, and then use our previously derived correspondence.›

context boolean_algebra begin
lemma boolean_is_huntington:
"class.huntington_algebra uminus inf sup bot top"
apply unfold_locales
apply (metis double_compl inf_sup_distrib1 inf_top_right
compl_inf inf_commute inf_compl_bot
compl_sup sup_commute sup_compl_top
sup_compl_top sup_assoc)+
done

end

context boolean_algebra_II begin

lemma boolean_II_is_huntington:
"class.huntington_algebra uminus (⊓) (⊔) ⊥ ⊤"
proof -
interpret boolean:
boolean_algebra minus uminus "(⊓)" "(⊑)" "(⊏)" "(⊔)" ⊥ ⊤
by (fact boolean_II_is_boolean)
show ?thesis by (simp add: boolean.boolean_is_huntington)
qed

end

context huntington_algebra begin

lemma huntington_id: "x ⊔ -x = -x ⊔ -(-x)"
proof -
from huntington have
"x ⊔ -x = -(-x ⊔ -(-(-x))) ⊔ -(-x ⊔ -(-x)) ⊔
(-(-(-x) ⊔ -(-(-x))) ⊔ -(-(-x) ⊔ -(-x)))"
by simp
also from sup_comm have
"… = -(-(-x) ⊔ -(-x)) ⊔ -(-(-x) ⊔ -(-(-x))) ⊔
(-(-(-x) ⊔ -x) ⊔ -(-(-(-x)) ⊔ -x))"
by simp
also from sup_assoc have
"… = -(-(-x) ⊔ -(-x)) ⊔
(-(-(-x) ⊔ -(-(-x))) ⊔ -(-(-x) ⊔ -x)) ⊔
-(-(-(-x)) ⊔ -x)"
by simp
also from sup_comm have
"… = -(-(-x) ⊔ -(-x)) ⊔
(-(-(-x) ⊔ -x) ⊔ -(-(-x) ⊔ -(-(-x)))) ⊔
-(-(-(-x)) ⊔ -x)"
by simp
also from sup_assoc have
"… = -(-(-x) ⊔ -(-x)) ⊔ -(-(-x) ⊔ -x) ⊔
(-(-(-x) ⊔ -(-(-x))) ⊔ -(-(-(-x)) ⊔ -x))"
by simp
also from sup_comm have
"… = -(-(-x) ⊔ -(-x)) ⊔ -(-(-x) ⊔ -x) ⊔
(-(-(-(-x)) ⊔ -(-x)) ⊔ -(-(-(-x)) ⊔ -x))"
by simp
also from huntington have
"… = -x ⊔ -(-x)"
by simp
finally show ?thesis by simp
qed

lemma dbl_neg: "- (-x) = x"
apply (metis huntington huntington_id sup_comm)
done

lemma towards_sup_compl: "x ⊔ -x = y ⊔ -y"
proof -
from huntington have
"x ⊔ -x = -(-x ⊔ -(-y)) ⊔ -(-x ⊔ -y) ⊔ (-(-(-x) ⊔ -(-y)) ⊔ -(-(-x) ⊔ -y))"
by simp
also from sup_comm have
"… = -(-(-y) ⊔ -x) ⊔ -(-y ⊔ -x) ⊔ (-(-y ⊔ -(-x)) ⊔ -(-(-y) ⊔ -(-x)))"
by simp
also from sup_assoc have
"… = -(-(-y) ⊔ -x) ⊔ (-(-y ⊔ -x) ⊔ -(-y ⊔ -(-x))) ⊔ -(-(-y) ⊔ -(-x))"
by simp
also from sup_comm have
"… = -(-y ⊔ -(-x)) ⊔ -(-y ⊔ -x) ⊔ -(-(-y) ⊔ -x) ⊔ -(-(-y) ⊔ -(-x))"
by simp
also from sup_assoc have
"… = -(-y ⊔ -(-x)) ⊔ -(-y ⊔ -x) ⊔ (-(-(-y) ⊔ -x) ⊔ -(-(-y) ⊔ -(-x)))"
by simp
also from sup_comm have
"… = -(-y ⊔ -(-x)) ⊔ -(-y ⊔ -x) ⊔ (-(-(-y) ⊔ -(-x)) ⊔ -(-(-y) ⊔ -x))"
by simp
also from huntington have
"y ⊔ -y = …" by simp
finally show ?thesis by simp
qed

lemma sup_compl: "x ⊔ -x = ⊤"

lemma towards_inf_compl: "x ⊓ -x = y ⊓ -y"
by (metis dbl_neg inf_eq sup_comm sup_compl)

lemma inf_compl: "x ⊓ -x = ⊥"
by (metis dbl_neg sup_comm bot_eq towards_inf_compl inf_eq)

lemma towards_idem: "⊥ = ⊥ ⊔ ⊥"
by (metis dbl_neg huntington inf_compl inf_eq sup_assoc sup_comm sup_compl)

lemma sup_ident: "x ⊔ ⊥ = x"
by (metis dbl_neg huntington inf_compl inf_eq sup_assoc
sup_comm sup_compl towards_idem)

lemma inf_ident: "x ⊓ ⊤ = x"
by (metis dbl_neg inf_compl inf_eq sup_ident sup_comm sup_compl)

lemma sup_idem: "x ⊔ x = x"
by (metis dbl_neg huntington inf_compl inf_eq sup_ident sup_comm sup_compl)

lemma inf_idem: "x ⊓ x = x"
by (metis dbl_neg inf_eq sup_idem)

lemma sup_nil: "x ⊔ ⊤ = ⊤"
by (metis sup_idem sup_assoc sup_comm sup_compl)

lemma inf_nil: "x ⊓ ⊥ = ⊥"
by (metis dbl_neg inf_compl inf_eq sup_nil sup_comm sup_compl)

lemma sup_absorb: "x ⊔ x ⊓ y = x"
by (metis huntington inf_eq sup_idem sup_assoc sup_comm)

lemma inf_absorb: "x ⊓ (x ⊔ y) = x"
by (metis dbl_neg inf_eq sup_absorb)

lemma partition: "x ⊓ y ⊔ x ⊓ -y = x"
by (metis dbl_neg huntington inf_eq sup_comm)

lemma demorgans1: "-(x ⊓ y) = -x ⊔ -y"
by (metis dbl_neg inf_eq)

lemma demorgans2: "-(x ⊔ y) = -x ⊓ -y"
by (metis dbl_neg inf_eq)

lemma inf_comm: "x ⊓ y = y ⊓ x"
by (metis inf_eq sup_comm)

lemma inf_assoc: "x ⊓ (y ⊓ z) = x ⊓ y ⊓ z"
by (metis dbl_neg inf_eq sup_assoc)

lemma inf_sup_distrib1: "x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)"
proof -
from partition have
"x ⊓ (y ⊔ z) = x ⊓ (y ⊔ z) ⊓ y ⊔ x ⊓ (y ⊔ z) ⊓ -y" ..
also from inf_assoc have
"… = x ⊓ ((y ⊔ z) ⊓ y) ⊔ x ⊓ (y ⊔ z) ⊓ -y" by simp
also from inf_comm have
"… = x ⊓ (y ⊓ (y ⊔ z)) ⊔ x ⊓ (y ⊔ z) ⊓ -y" by simp
also from inf_absorb have
"… = (x ⊓ y) ⊔ (x ⊓ (y ⊔ z) ⊓ -y)" by simp
also from partition have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔
((x ⊓ (y ⊔ z) ⊓ -y ⊓ z) ⊔ (x ⊓ (y ⊔ z) ⊓ -y ⊓ -z))" by simp
also from inf_assoc have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔
((x ⊓ ((y ⊔ z) ⊓ (-y ⊓ z))) ⊔ (x ⊓ ((y ⊔ z) ⊓ (-y ⊓ -z))))" by simp
also from demorgans2 have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔
((x ⊓ ((y ⊔ z) ⊓ (-y ⊓ z))) ⊔ (x ⊓ ((y ⊔ z) ⊓ -(y ⊔ z))))" by simp
also from inf_compl have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔
((x ⊓ ((y ⊔ z) ⊓ (-y ⊓ z))) ⊔ (x ⊓ ⊥))" by simp
also from inf_nil have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔
((x ⊓ ((y ⊔ z) ⊓ (-y ⊓ z))) ⊔ ⊥)" by simp
also from sup_idem have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔
((x ⊓ ((y ⊔ z) ⊓ (-y ⊓ z))) ⊔ ⊥)" by simp
also from sup_ident have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔
(x ⊓ ((y ⊔ z) ⊓ (-y ⊓ z)))" by simp
also from inf_comm have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔
(x ⊓ ((-y ⊓ z) ⊓ (y ⊔ z)))" by simp
also from sup_comm have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔
(x ⊓ ((-y ⊓ z) ⊓ (z ⊔ y)))" by simp
also from inf_assoc have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ (y ⊓ z)) ⊔ (x ⊓ y ⊓ -z)) ⊔
(x ⊓ (-y ⊓ (z ⊓ (z ⊔ y))))" by simp
also from inf_absorb have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ (y ⊓ z)) ⊔ (x ⊓ y ⊓ -z)) ⊔ (x ⊓ (-y ⊓ z))"
by simp
also from inf_comm have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ (z ⊓ y)) ⊔ (x ⊓ y ⊓ -z)) ⊔ (x ⊓ (z ⊓ -y))"
by simp
also from sup_assoc have
"… = ((x ⊓ y ⊓ z) ⊔ ((x ⊓ (z ⊓ y)) ⊔ (x ⊓ y ⊓ -z))) ⊔ (x ⊓ (z ⊓ -y))"
by simp
also from sup_comm have
"… = ((x ⊓ y ⊓ z) ⊔ ((x ⊓ y ⊓ -z) ⊔ (x ⊓ (z ⊓ y)))) ⊔ (x ⊓ (z ⊓ -y))"
by simp
also from sup_assoc have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔ ((x ⊓ (z ⊓ y)) ⊔ (x ⊓ (z ⊓ -y)))"
by simp
also from inf_assoc have
"… = ((x ⊓ y ⊓ z) ⊔ (x ⊓ y ⊓ -z)) ⊔ ((x ⊓ z ⊓ y) ⊔ (x ⊓ z ⊓ -y))" by simp
also from partition have "… = (x ⊓ y) ⊔ (x ⊓ z)" by simp
finally show ?thesis by simp
qed

lemma sup_inf_distrib1:
"x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)"
proof -
from dbl_neg have
"x ⊔ (y ⊓ z) = -(-(-(-x) ⊔ (y ⊓ z)))" by simp
also from inf_eq have
"… = -(-x ⊓ (-y ⊔ -z))" by simp
also from inf_sup_distrib1 have
"… = -((-x ⊓ -y) ⊔ (-x ⊓ -z))" by simp
also from demorgans2 have
"… = -(-x ⊓ -y) ⊓ -(-x ⊓ -z)" by simp
also from demorgans1 have
"… = (-(-x) ⊔ -(-y)) ⊓ (-(-x) ⊔ -(-z))" by simp
also from dbl_neg have
"… = (x ⊔ y) ⊓ (x ⊔ z)" by simp
finally show ?thesis by simp
qed

lemma huntington_is_boolean_II:
"class.boolean_algebra_II uminus (⊓) (⊔) ⊥ ⊤"
apply unfold_locales
apply (metis inf_comm inf_assoc sup_absorb
inf_absorb sup_inf_distrib1
sup_compl inf_compl)+
done

lemma huntington_is_boolean:
"class.boolean_algebra minus uminus (⊓) (⊑) (⊏) (⊔) ⊥ ⊤"
proof -
interpret boolean_II:
boolean_algebra_II uminus "(⊓)" "(⊔)" ⊥ ⊤
by (fact huntington_is_boolean_II)
show ?thesis by (simp add: boolean_II.boolean_II_is_boolean)
qed
end

subsection ‹Robbins' Algebra›

context boolean_algebra begin
lemma boolean_is_robbins:
"class.robbins_algebra uminus inf sup bot top"
apply unfold_locales
apply (metis sup_assoc sup_commute compl_inf double_compl sup_compl_top
inf_compl_bot diff_eq sup_bot_right sup_inf_distrib1)+
done
end

context boolean_algebra_II begin
lemma boolean_II_is_robbins:
"class.robbins_algebra uminus inf sup bot top"
proof -
interpret boolean:
boolean_algebra minus uminus "(⊓)" "(⊑)" "(⊏)" "(⊔)" ⊥ ⊤
by (fact boolean_II_is_boolean)
show ?thesis by (simp add: boolean.boolean_is_robbins)
qed
end

context huntington_algebra begin
lemma huntington_is_robbins:
"class.robbins_algebra uminus inf sup bot top"
proof -
interpret boolean:
boolean_algebra minus uminus "(⊓)" "(⊑)" "(⊏)" "(⊔)" ⊥ ⊤
by (fact huntington_is_boolean)
show ?thesis by (simp add: boolean.boolean_is_robbins)
qed
end

text ‹Before diving into the proof that the Robbins algebra is Boolean,
we shall present some shorthand machinery›

context common_algebra begin

(* Iteration Machinery/Shorthand *)

primrec copyp :: "nat ⇒ 'a ⇒ 'a" (infix "⊗" 80)
where
copyp_0:   "0 ⊗ x = x"
| copyp_Suc: "(Suc k) ⊗ x = (k ⊗ x) ⊔ x"

no_notation
Product_Type.Times (infixr "×" 80)

primrec copy :: "nat ⇒ 'a ⇒ 'a" (infix "×" 85)
where
"0 × x = x"
| "(Suc k) × x = k ⊗ x"

(* Theorems for translating shorthand into syntax *)

lemma one:  "1 × x = x"
proof -
have       "1 = Suc(0)" by arith
hence      "1 × x = Suc(0) × x" by metis
also have  "… = x" by simp
finally show ?thesis by simp
qed

lemma two:  "2 × x = x ⊔ x"
proof -
have       "2 = Suc(Suc(0))" by arith
hence      "2 × x = Suc(Suc(0)) × x" by metis
also have  "… = x ⊔ x" by simp
finally show ?thesis by simp
qed

lemma three:  "3 × x = x ⊔ x ⊔ x"
proof -
have       "3 = Suc(Suc(Suc(0)))" by arith
hence      "3 × x = Suc(Suc(Suc(0))) × x" by metis
also have  "… = x ⊔ x ⊔ x" by simp
finally show ?thesis by simp
qed

lemma four:  "4 × x = x ⊔ x ⊔ x ⊔ x"
proof -
have       "4 = Suc(Suc(Suc(Suc(0))))" by arith
hence      "4 × x = Suc(Suc(Suc(Suc(0)))) × x" by metis
also have  "… = x ⊔ x ⊔ x ⊔ x" by simp
finally show ?thesis by simp
qed

lemma five:  "5 × x = x ⊔ x ⊔ x ⊔ x ⊔ x"
proof -
have       "5 = Suc(Suc(Suc(Suc(Suc(0)))))" by arith
hence      "5 × x = Suc(Suc(Suc(Suc(Suc(0))))) × x" by metis
also have  "… = x ⊔ x ⊔ x ⊔ x ⊔ x" by simp
finally show ?thesis by simp
qed

lemma six:  "6 × x = x ⊔ x ⊔ x ⊔ x ⊔ x ⊔ x"
proof -
have       "6 = Suc(Suc(Suc(Suc(Suc(Suc(0))))))" by arith
hence      "6 × x = Suc(Suc(Suc(Suc(Suc(Suc(0)))))) × x" by metis
also have  "… = x ⊔ x ⊔ x ⊔ x ⊔ x ⊔ x" by simp
finally show ?thesis by simp
qed

(* Distribution Laws *)

lemma copyp_distrib: "k ⊗ (x ⊔ y) = (k ⊗ x) ⊔ (k ⊗ y)"
proof (induct k)
case 0 show ?case by simp
case Suc thus ?case by (simp, metis sup_assoc sup_comm)
qed

corollary copy_distrib: "k × (x ⊔ y) = (k × x) ⊔ (k × y)"
by (induct k, (simp add: sup_assoc sup_comm copyp_distrib)+)

lemma copyp_arith: "(k + l + 1) ⊗ x = (k ⊗ x) ⊔ (l ⊗ x)"
proof (induct l)
case 0 have "k + 0 + 1 = Suc(k)" by arith
thus ?case by simp
case (Suc l) note ind_hyp = this
have "k + Suc(l) + 1 = Suc(k + l + 1)" by arith+
hence "(k + Suc(l) + 1) ⊗ x = (k + l + 1) ⊗ x ⊔ x" by (simp add: ind_hyp)
also from ind_hyp have
"… = (k ⊗ x) ⊔ (l ⊗ x) ⊔ x" by simp
also note sup_assoc
finally show ?case by simp
qed

lemma copy_arith:
assumes "k ≠ 0" and "l ≠ 0"
shows "(k + l) × x = (k × x) ⊔ (l × x)"
using assms
proof -
from assms have "∃ k'. Suc(k') = k"
and "∃ l'. Suc(l') = l" by arith+
from this obtain k' l' where A: "Suc(k') = k"
and B: "Suc(l') = l" by fast+
from this have A1: "k × x = k' ⊗ x"
and B1: "l × x = l' ⊗ x" by fastforce+
from A B have "k + l = Suc(k' + l' + 1)" by arith
hence "(k + l) × x = (k' + l' + 1) ⊗ x" by simp
also from copyp_arith have
"… = k' ⊗ x ⊔ l' ⊗ x" by fast
also from A1 B1 have
"… = k × x ⊔ l × x" by fastforce
finally show ?thesis by simp
qed

end

text ‹The theorem asserting all Robbins algebras are Boolean
comes in 6 movements.

First: The Winker identity is proved.

Second: Idempotence for a particular object is proved.
Note that falsum is defined in terms of this object.

Third: An identity law for falsum is derived.

Fourth: Idempotence for supremum is derived.

Fifth: The double negation law is proven

Sixth: Robbin's algebras are proven to be Huntington Algebras.›

context robbins_algebra begin

definition secret_object2 :: "'a" ("α") where
"α = -(-(ι ⊔ ι ⊔ ι) ⊔ ι)"
definition secret_object3 :: "'a" ("β") where
"β = ι ⊔ ι"
definition secret_object4 :: "'a" ("δ") where
"δ = β ⊔ (-(α ⊔ -β) ⊔ -(α ⊔ -β))"
definition secret_object5 :: "'a" ("γ") where
"γ = δ ⊔ -(δ ⊔ -δ)"
definition winker_object :: "'a" ("ρ") where
"ρ = γ ⊔ γ ⊔ γ"
definition fake_bot :: "'a" ("⊥⊥") where
"⊥⊥ = -(ρ ⊔ -ρ)"

(* Towards Winker's Identity *)

(* These lemmas are due to Alan Mann *)

lemma robbins2: "y = -(-(-x ⊔ y) ⊔ -(x ⊔ y))"
by (metis robbins sup_comm)

lemma mann0: "-(x ⊔ y) = -(-(-(x ⊔ y) ⊔ -x ⊔ y) ⊔ y)"
by (metis robbins sup_comm sup_assoc)

lemma mann1: "-(-x ⊔ y) = -(-(-(-x ⊔ y) ⊔ x ⊔ y) ⊔ y)"
by (metis robbins sup_comm sup_assoc)

lemma mann2: "y = -(-(-(-x ⊔ y) ⊔ x ⊔ y ⊔ y) ⊔ -(-x ⊔ y))"
by (metis mann1 robbins sup_comm sup_assoc)

lemma mann3: "z = -(-(-(-(-x ⊔ y) ⊔ x ⊔ y ⊔ y) ⊔ -(-x ⊔ y) ⊔ z) ⊔ -(y ⊔ z))"
proof -
let ?w = "-(-(-x ⊔ y) ⊔ x ⊔ y ⊔ y) ⊔ -(-x ⊔ y)"
from robbins[where x="z" and y="?w"] sup_comm mann2
have "z = -(-(y ⊔ z) ⊔ -(?w ⊔ z))" by metis
thus ?thesis by (metis sup_comm)
qed

lemma mann4: "-(y ⊔ z) =
-(-(-(-(-x ⊔ y) ⊔ x ⊔ y ⊔ y) ⊔ -(-x ⊔ y) ⊔ -(y ⊔ z) ⊔ z) ⊔ z)"
proof -
from robbins2[where x="-(-(-x ⊔ y) ⊔ x ⊔ y ⊔ y) ⊔ -(-x ⊔ y) ⊔ z"
and y="-(y ⊔ z)"]
mann3[where x="x" and y="y" and z="z"]
have "-(y ⊔ z) =
-(z ⊔ -(-(-(-x ⊔ y) ⊔ x ⊔ y ⊔ y) ⊔ -(-x ⊔ y) ⊔ z ⊔ -(y ⊔ z)))"
by metis
with sup_comm sup_assoc show ?thesis by metis
qed

lemma mann5: "u =
-(-(-(-(-(-x ⊔ y) ⊔ x ⊔ y ⊔ y) ⊔
-(-x ⊔ y) ⊔ - (y ⊔ z) ⊔ z) ⊔ z ⊔ u) ⊔
-(-(y ⊔ z) ⊔ u))"
using robbins2[where x="-(-(-(-x ⊔ y) ⊔ x ⊔ y ⊔ y) ⊔
-(-x ⊔ y) ⊔ -(y ⊔ z) ⊔ z) ⊔ z"
and y="u"]
mann4[where x=x and y=y and z=z]
sup_comm
by metis

lemma mann6:
"-(- 3×x ⊔ x) = -(-(-(- 3×x ⊔ x) ⊔ - 3×x) ⊔ -(-(- 3×x ⊔ x) ⊔ 5×x))"
proof -
have "3+2=(5::nat)" and "3≠(0::nat)" and "2≠(0::nat)" by arith+
with copy_arith have ♡: "3×x ⊔ 2×x = 5×x" by metis
let ?p = "-(- 3×x ⊔ x)"
{ fix q
from sup_comm have
"-(q ⊔ 5×x) = -(5×x ⊔ q)" by metis
also from ♡ mann0[where x="3×x" and y="q ⊔ 2×x"] sup_assoc sup_comm have
"… = -(-(-(3×x ⊔ (q ⊔ 2×x)) ⊔ - 3×x ⊔ (q ⊔ 2×x)) ⊔ (q ⊔ 2×x))"
by metis
also from sup_assoc have
"… = -(-(-((3×x ⊔ q) ⊔ 2×x) ⊔ - 3×x ⊔ (q ⊔ 2×x)) ⊔ (q ⊔ 2×x))" by metis
also from sup_comm have
"… = -(-(-((q ⊔ 3×x) ⊔ 2×x) ⊔ - 3×x ⊔ (q ⊔ 2×x)) ⊔ (q ⊔ 2×x))" by metis
also from sup_assoc have
"… = -(-(-(q ⊔ (3×x ⊔ 2×x)) ⊔ - 3×x ⊔ (q ⊔ 2×x)) ⊔ (q ⊔ 2×x))" by metis
also from ♡ have
"… = -(-(-(q ⊔ 5×x) ⊔ - 3×x ⊔ (q ⊔ 2×x)) ⊔ (q ⊔ 2×x))" by metis
also from sup_assoc have
"… = -(-(-(q ⊔ 5×x) ⊔ (- 3×x ⊔ q) ⊔ 2×x) ⊔ (q ⊔ 2×x))" by metis
also from sup_comm have
"… = -(-(-(q ⊔ 5×x) ⊔ (q ⊔ - 3×x) ⊔ 2×x) ⊔ (2×x ⊔ q))" by metis
also from sup_assoc have
"… = -(-(-(q ⊔ 5×x) ⊔ q ⊔ - 3×x ⊔ 2×x) ⊔ 2×x ⊔ q)" by metis
finally have
"-(q ⊔ 5×x) = -(-(-(q ⊔ 5×x) ⊔ q ⊔ - 3×x ⊔ 2×x) ⊔ 2×x ⊔ q)" by simp
} hence ♠:
"-(?p ⊔ 5×x) = -(-(-(?p ⊔ 5×x) ⊔ ?p ⊔ - 3×x ⊔ 2×x) ⊔ 2×x ⊔ ?p)"
by simp

from mann5[where x="3×x" and y="x" and z="2×x" and u="?p"]
sup_assoc three[where x=x] five[where x=x] have
"?p =
-(-(-(-(?p ⊔ 5×x) ⊔ ?p ⊔ -(x ⊔ 2×x) ⊔ 2×x) ⊔ 2×x ⊔ ?p) ⊔
-(-(x ⊔ 2×x) ⊔ ?p))" by metis
also from sup_comm have
"… =
-(-(-(-(?p ⊔ 5×x) ⊔ ?p ⊔ -(2×x ⊔ x) ⊔ 2×x) ⊔ 2×x ⊔ ?p) ⊔
-(-(2×x ⊔ x) ⊔ ?p))" by metis
also from two[where x=x] three[where x=x] have
"… =
-(-(-(-(?p ⊔ 5×x) ⊔ ?p ⊔ - 3×x ⊔ 2×x) ⊔ 2×x ⊔ ?p) ⊔
-(- 3×x ⊔ ?p))" by metis
also from ♠ have "… = -(-(?p ⊔ 5×x) ⊔ -(- 3×x ⊔ ?p))" by simp
also from sup_comm have "… = -(-(?p ⊔ 5×x) ⊔ -(?p ⊔ - 3×x))" by simp
also from sup_comm have "… = -(-(?p ⊔ - 3×x) ⊔ -(?p ⊔ 5×x))" by simp
finally show ?thesis .
qed

lemma mann7:
"- 3×x = -(-(- 3×x ⊔ x) ⊔ 5×x)"
proof -
let ?p = "-(- 3×x ⊔ x)"
let ?q = "?p ⊔ - 3×x"
let ?r = "-(?p ⊔ 5×x)"
from robbins2[where x="?q"
and y="?r"]
mann6[where x=x]
have "?r = - (?p ⊔ - (?q ⊔ ?r))" by simp
also from sup_comm have "… = - (- (?q ⊔ ?r) ⊔ ?p)" by simp
also from sup_comm have "… = - (- (?r ⊔ ?q) ⊔ ?p)" by simp
finally have ♠: "?r = - (- (?r ⊔ ?q) ⊔ ?p)" .
from mann3[where x="3×x" and y="x" and z="- 3×x"]
sup_comm have
"- 3×x = -(-(-(?p ⊔ 3×x ⊔ x ⊔ x) ⊔ ?p ⊔ - 3×x) ⊔ ?p)" by metis
also from sup_assoc have
"… = -(-(-(?p ⊔ (3×x ⊔ x ⊔ x)) ⊔ ?q) ⊔ ?p)" by metis
also from three[where x=x] five[where x=x] have
"… = -(-(?r ⊔ ?q) ⊔ ?p)" by metis
finally have "- 3×x = -(-(?r ⊔ ?q) ⊔ ?p)" by metis
with ♠ show ?thesis by simp
qed

lemma mann8:
"-(- 3×x ⊔ x) ⊔ 2×x = -(-(-(- 3×x ⊔ x) ⊔ - 3×x ⊔ 2×x) ⊔ - 3×x)"
(is "?lhs = ?rhs")
proof -
let ?p = "-(- 3×x ⊔ x)"
let ?q = "?p ⊔ 2×x"
let ?r = "3×x"
have "3+2=(5::nat)" and "3≠(0::nat)" and "2≠(0::nat)" by arith+
with copy_arith have ♡: "3×x ⊔ 2×x = 5×x" by metis
from robbins2[where x="?r" and y="?q"] and sup_assoc
have "?q = -(-(- 3×x ⊔ ?q) ⊔ -(3×x ⊔ ?p ⊔ 2×x))" by metis
also from sup_comm have
"… = -(-(?q ⊔ - 3×x) ⊔ -(?p ⊔ 3×x ⊔ 2×x))" by metis
also from ♡ sup_assoc have
"… = -(-(?q ⊔ - 3×x) ⊔ -(?p ⊔ 5×x))" by metis
also from mann7[where x=x] have
"… = -(-(?q ⊔ - 3×x) ⊔ - 3×x)" by metis
also from sup_assoc have
"… = -(-(?p ⊔ (2×x  ⊔ - 3×x)) ⊔ - 3×x)" by metis
also from sup_comm have
"… = -(-(?p ⊔ (- 3×x  ⊔ 2×x)) ⊔ - 3×x)" by metis
also from sup_assoc have
"… = ?rhs" by metis
finally show ?thesis by simp
qed

lemma mann9: "x = -(-(- 3×x ⊔ x) ⊔ - 3×x )"
proof -
let ?p = "-(- 3×x ⊔ x)"
let ?q = "?p ⊔ 4×x"
have "4+1=(5::nat)" and "1≠(0::nat)" and "4≠(0::nat)" by arith+
with copy_arith one have ♡: "4×x ⊔ x = 5×x" by metis
with sup_assoc robbins2[where y=x and x="?q"]
have "x = -(-(-?q ⊔ x) ⊔ -(?p ⊔ 5×x))" by metis
with mann7 have "x = -(-(-?q ⊔ x) ⊔ - 3×x)" by metis
moreover
have "3+1=(4::nat)" and "1≠(0::nat)" and "3≠(0::nat)" by arith+
with copy_arith one have ♠: "3×x ⊔ x = 4×x" by metis
with mann1[where x="3×x" and y="x"] sup_assoc have
"-(-?q ⊔ x) = ?p" by metis
ultimately show ?thesis by simp
qed

lemma mann10: "y = -(-(-(- 3×x ⊔ x) ⊔ - 3×x ⊔ y) ⊔ -(x ⊔ y))"
using robbins2[where x="-(- 3×x ⊔ x) ⊔ - 3×x" and y=y]
mann9[where x=x]
sup_comm
by metis

theorem mann: "2×x = -(- 3×x ⊔ x) ⊔ 2×x"
using mann10[where x=x and y="2×x"]
mann8[where x=x]
two[where x=x] three[where x=x] sup_comm
by metis

corollary winkerr: "α ⊔ β = β"
using mann secret_object2_def secret_object3_def two three
by metis

corollary winker: "β ⊔ α = β"
by (metis winkerr sup_comm)

corollary multi_winkerp: "β ⊔ k ⊗ α = β"
by (induct k, (simp add: winker sup_comm sup_assoc)+)

corollary multi_winker: "β ⊔ k × α = β"
by (induct k, (simp add: multi_winkerp winker sup_comm sup_assoc)+)

(* Towards Idempotence *)

lemma less_eq_introp:
"-(x ⊔ -(y ⊔ z)) = -(x ⊔ y ⊔ -z) ⟹ y ⊑ x"
by (metis robbins sup_assoc less_eq_def
sup_comm[where x=x and y=y])

corollary less_eq_intro:
"-(x ⊔ -(y ⊔ z)) = -(x ⊔ y ⊔ -z) ⟹ x ⊔ y = x"
by (metis less_eq_introp less_eq_def sup_comm)

lemma eq_intro:
"-(x ⊔ -(y ⊔ z)) = -(y ⊔ -(x ⊔ z)) ⟹ x = y"
by (metis robbins sup_assoc sup_comm)

lemma copyp0:
assumes "-(x ⊔ -y) = z"
shows "-(x ⊔ -(y ⊔ k ⊗ (x ⊔ z))) = z"
using assms
proof (induct k)
case 0 show ?case
by (simp, metis assms robbins sup_assoc sup_comm)
case Suc note ind_hyp = this
show ?case
by (simp, metis ind_hyp robbins sup_assoc sup_comm)
qed

lemma copyp1:
assumes "-(-(x ⊔ -y) ⊔ -y) = x"
shows "-(y ⊔ k ⊗ (x ⊔ -(x ⊔ -y))) = -y"
using assms
proof -
let ?z = "-(x ⊔ - y)"
let ?ky = "y ⊔ k ⊗ (x ⊔ ?z)"
have "-(x ⊔ -?ky) = ?z" by (simp add: copyp0)
hence "-(-?ky ⊔ -(-y ⊔ ?z)) = ?z" by (metis assms sup_comm)
also have "-(?z ⊔ -?ky) = x" by (metis assms copyp0 sup_comm)
hence "?z = -(-y ⊔ -(-?ky ⊔ ?z))" by (metis sup_comm)
finally show ?thesis by (metis eq_intro)
qed

corollary copyp2:
assumes "-(x ⊔ y) = -y"
shows "-(y ⊔ k ⊗ (x ⊔ -(x ⊔ -y))) = -y"
by (metis assms robbins sup_comm copyp1)

lemma two_threep:
assumes "-(2 × x ⊔ y) = -y"
and "-(3 × x ⊔ y) = -y"
shows "2 × x ⊔ y = 3 × x ⊔ y"
using assms
proof -
from assms two three have
A: "-(x ⊔ x ⊔ y) = -y" and
B: "-(x ⊔ x ⊔ x ⊔ y) = -y"  by simp+
with sup_assoc
copyp2[where x="x" and y="x ⊔ x ⊔ y" and k="0"]
have "-(x ⊔ x ⊔ y ⊔ x ⊔ -(x ⊔ -y)) = -y" by simp
moreover
from sup_comm sup_assoc A B
copyp2[where x="x ⊔ x" and y="y" and k="0"]
have "-(y ⊔ x ⊔ x ⊔ -(x ⊔ x ⊔ -y)) = -y" by fastforce
with sup_comm sup_assoc
have "-(x ⊔ x ⊔ y ⊔ -(x ⊔ (x ⊔ -y))) = -y" by metis
ultimately have
"-(x ⊔ x ⊔ y ⊔ -(x ⊔ (x ⊔ -y))) = -(x ⊔ x ⊔ y ⊔ x ⊔ -(x ⊔ -y))" by simp
with less_eq_intro have "x ⊔ x ⊔ y = x ⊔ x ⊔ y ⊔ x" by metis
with sup_comm sup_assoc two three show ?thesis by metis
qed

lemma two_three:
assumes "-(x ⊔ y) = -y ∨ -(-(x ⊔ -y) ⊔ -y) = x"
shows "y ⊔ 2 × (x ⊔ -(x ⊔ -y)) = y ⊔ 3 × (x ⊔ -(x ⊔ -y))"
(is "y ⊔ ?z2 = y ⊔ ?z3")
using assms
proof
assume "-(x ⊔ y) = -y"
with copyp2[where k="Suc(0)"]
copyp2[where k="Suc(Suc(0))"]
two three
have "-(y ⊔ ?z2) = -y" and "-(y ⊔ ?z3) = -y" by simp+
with two_threep sup_comm show ?thesis by metis
next
assume "-(-(x ⊔ -y) ⊔ -y) = x"
with copyp1[where k="Suc(0)"]
copyp1[where k="Suc(Suc(0))"]
two three
have "-(y ⊔ ?z2) = -y" and "-(y ⊔ ?z3) = -y" by simp+
with two_threep sup_comm show ?thesis by metis
qed

lemma sup_idem: "ρ ⊔ ρ = ρ"
proof -
from winkerr two
copyp2[where x="α" and y="β" and k="Suc(0)"] have
"-β = -(β ⊔ 2 × (α ⊔ -(α ⊔ -β)))" by simp
also from copy_distrib sup_assoc have
"… = -(β ⊔ 2 × α ⊔ 2 × (-(α ⊔ -β)))" by simp
also from sup_assoc secret_object4_def two
multi_winker[where k="2"] have
"… = -δ" by metis
finally have "-β = -δ" by simp
with secret_object4_def sup_assoc three have
"δ ⊔ -(α ⊔ -δ) = β ⊔ 3 × (-(α ⊔ -β))" by simp
also from copy_distrib[where k="3"]
multi_winker[where k="3"]
sup_assoc have
"… = β ⊔ 3 × (α ⊔ -(α ⊔ -β))" by metis
also from winker sup_comm two_three[where x="α" and y="β"] have
"… = β ⊔ 2 × (α ⊔ -(α ⊔ -β))" by fastforce
also from copy_distrib[where k="2"]
multi_winker[where k="2"]
sup_assoc two secret_object4_def have
"… = δ" by metis
finally have ♡: "δ ⊔ -(α ⊔ -δ) = δ" by simp
from secret_object4_def winkerr sup_assoc have
"α ⊔ δ = δ" by metis
hence "δ ⊔ α = δ" by (metis sup_comm)
hence "-(-(δ ⊔ -δ) ⊔ -δ) = -(-(δ ⊔ (α ⊔ -δ)) ⊔ -δ)" by (metis sup_assoc)
also from ♡ have
"… = -(-(δ ⊔ (α ⊔ -δ)) ⊔ -(δ ⊔ -(α ⊔ -δ)))" by metis
also from robbins have
"… = δ" by metis
finally have "-(-(δ ⊔ -δ) ⊔ -δ) = δ" by simp
with two_three[where x="δ" and y="δ"]
secret_object5_def sup_comm
have "3 × γ ⊔ δ = 2 × γ ⊔ δ" by fastforce
with secret_object5_def sup_assoc sup_comm have
"3 × γ ⊔ γ = 2 × γ ⊔ γ" by fastforce
with two three four five six have
"6 × γ = 3 × γ" by simp
moreover have "3 + 3 = (6::nat)" and "3 ≠ (0::nat)" by arith+
moreover note copy_arith[where k="3" and l="3" and x="γ"]
winker_object_def three
ultimately show ?thesis by simp
qed

(* Idempotence implies the identity law *)

lemma sup_ident: "x ⊔ ⊥⊥ = x"
proof -
have I: "ρ = -(-ρ ⊔ ⊥⊥)"
by (metis fake_bot_def inf_eq robbins sup_comm sup_idem)

{ fix x have "x = -(-(x ⊔ -ρ ⊔ ⊥⊥) ⊔ -(x ⊔ ρ))"
by (metis I robbins sup_assoc) }
note II = this

have III: "-ρ = -(-(ρ ⊔ -ρ ⊔ -ρ) ⊔ ρ)"
by (metis robbins[where x="-ρ" and y="ρ ⊔ -ρ"]
I sup_comm fake_bot_def)
hence "ρ = -(-(ρ ⊔ -ρ ⊔ -ρ) ⊔ -ρ)"
by (metis robbins[where x="ρ" and y="ρ ⊔ -ρ ⊔ -ρ"]
sup_comm[where x="ρ" and y="-(ρ ⊔ -ρ ⊔ -ρ)"]
sup_assoc sup_idem)
hence "-(ρ ⊔ -ρ ⊔ -ρ) = ⊥⊥"
by (metis robbins[where x="-(ρ ⊔ -ρ ⊔ -ρ)" and y="ρ"]
III sup_comm fake_bot_def)
hence "-ρ = -(ρ ⊔ ⊥⊥)"
by (metis III sup_comm)
hence "ρ = -(-(ρ ⊔ ⊥⊥) ⊔ -(ρ ⊔ ⊥⊥ ⊔ -ρ))"
by (metis II sup_idem sup_comm sup_assoc)
moreover have "ρ ⊔ ⊥⊥ = -(-(ρ ⊔ ⊥⊥) ⊔ -(ρ ⊔ ⊥⊥ ⊔ -ρ))"
by (metis robbins[where x="ρ ⊔ ⊥⊥" and y="ρ"]
sup_comm[where y="ρ"]
sup_assoc sup_idem)
ultimately have "ρ = ρ ⊔ ⊥⊥" by auto
hence "x ⊔ ⊥⊥ = -(-(x ⊔ ρ) ⊔ -(x ⊔ ⊥⊥ ⊔ -ρ))"
by (metis robbins[where x="x ⊔ ⊥⊥" and y=ρ]
sup_comm[where x="⊥⊥" and y=ρ]
sup_assoc)
thus ?thesis by (metis sup_assoc sup_comm II)
qed

(* The identity law implies double negation *)

lemma dbl_neg: "- (-x) = x"
proof -
{ fix x have "⊥⊥ = -(-x ⊔ -(-x))"
by (metis robbins sup_comm sup_ident)
} note I = this

{ fix x have "-x = -(-(-x ⊔ -(-(-x))))"
by (metis I robbins sup_comm sup_ident)
} note II = this

{ fix x have "-(-(-x)) = -(-(-x ⊔ -(-(-x))))"
by (metis I II robbins sup_assoc sup_comm sup_ident)
} note III = this

show ?thesis by (metis II III robbins)
qed

(* Double negation implies Huntington's axiom, hence Boolean*)

theorem robbins_is_huntington:
"class.huntington_algebra uminus (⊓) (⊔) ⊥ ⊤"
apply unfold_locales
apply (metis dbl_neg robbins sup_comm)
done

theorem robbins_is_boolean_II:
"class.boolean_algebra_II uminus (⊓) (⊔) ⊥ ⊤"
proof -
interpret huntington:
huntington_algebra uminus "(⊓)" "(⊔)" ⊥ ⊤
by (fact robbins_is_huntington)
show ?thesis by (simp add: huntington.huntington_is_boolean_II)
qed

theorem robbins_is_boolean:
"class.boolean_algebra minus uminus (⊓) (⊑) (⊏) (⊔) ⊥ ⊤"
proof -
interpret huntington:
huntington_algebra uminus "(⊓)" "(⊔)" ⊥ ⊤
by (fact robbins_is_huntington)
show ?thesis by (simp add: huntington.huntington_is_boolean)
qed

end

no_notation secret_object1 ("ι")
and secret_object2 ("α")
and secret_object3 ("β")
and secret_object4 ("δ")
and secret_object5 ("γ")
and winker_object ("ρ")
and less_eq  (infix "⊑" 50)
and less (infix "⊏" 50)
and inf (infixl "⊓" 70)
and sup (infixl "⊔" 65)
and top ("⊤")
and bot ("⊥")
and copyp (infix "⊗" 80)
and copy (infix "×" 85)

notation
Product_Type.Times  (infixr "×" 80)

end