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 = ⊤" by (simp add: top_eq towards_sup_compl) 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" unbundle no set_product_syntax 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