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 = ⊤"
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