Theory Subset_Boolean_Algebras.Subset_Boolean_Algebras

(* Title:      Subset Boolean Algebras
   Authors:    Walter Guttmann, Bernhard Möller
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

theory Subset_Boolean_Algebras

imports Stone_Algebras.P_Algebras

begin

section ‹Boolean Algebras›

text ‹
We show that Isabelle/HOL's boolean_algebra› class is equivalent to Huntington's axioms cite"Huntington1933".
See cite"WamplerDoty2016" for related results.
›

subsection ‹Huntington's Axioms›

text ‹Definition 1›

class huntington = sup + uminus +
  assumes associative: "x  (y  z) = (x  y)  z"
  assumes commutative: "x  y = y  x"
  assumes huntington: "x = -(-x  y)  -(-x  -y)"
begin

lemma top_unique:
  "x  -x = y  -y"
proof -
  have "x  -x = y  -(--y  -x)  -(--y  --x)"
    by (smt associative commutative huntington)
  thus ?thesis
    by (metis associative huntington)
qed

end

subsection ‹Equivalence to boolean_algebra› Class›

text ‹Definition 2›

class extended = sup + inf + minus + uminus + bot + top + ord +
  assumes top_def: "top = (THE x . y . x = y  -y)" (* define without imposing uniqueness *)
  assumes bot_def: "bot = -(THE x . y . x = y  -y)"
  assumes inf_def: "x  y = -(-x  -y)"
  assumes minus_def: "x - y = -(-x  y)"
  assumes less_eq_def: "x  y  x  y = y"
  assumes less_def: "x < y  x  y = y  ¬ (y  x = x)"

class huntington_extended = huntington + extended
begin

lemma top_char:
  "top = x  -x"
  using top_def top_unique by auto

lemma bot_char:
  "bot = -top"
  by (simp add: bot_def top_def)

subclass boolean_algebra
proof
  show 1: "x y. (x < y) = (x  y  ¬ y  x)"
    by (simp add: less_def less_eq_def)
  show 2: "x. x  x"
  proof -
    fix x
    have "x  top = top  --x"
      by (metis (full_types) associative top_char)
    thus "x  x"
      by (metis (no_types) associative huntington less_eq_def top_char)
  qed
  show 3: "x y z. x  y  y  z  x  z"
    by (metis associative less_eq_def)
  show 4: "x y. x  y  y  x  x = y"
    by (simp add: commutative less_eq_def)
  show 5: "x y. x  y  x"
    using 2 by (metis associative huntington inf_def less_eq_def)
  show 6: "x y. x  y  y"
    using 5 commutative inf_def by fastforce
  show 8: "x y. x  x  y"
    using 2 associative less_eq_def by auto
  show 9: "y x. y  x  y"
    using 8 commutative by fastforce
  show 10: "y x z. y  x  z  x  y  z  x"
    by (metis associative less_eq_def)
  show 11: "x. bot  x"
    using 8 by (metis bot_char huntington top_char)
  show 12: "x. x  top"
    using 6 11 by (metis huntington bot_def inf_def less_eq_def top_def)
  show 13: "x y z. x  y  z = (x  y)  (x  z)"
  proof -
    have 2: "x y z . x  (y  z) = (x  y)  z"
      by (simp add: associative)
    have 3: "x y z . (x  y)  z = x  (y  z)"
      using 2 by metis
    have 4: "x y . x  y = y  x"
      by (simp add: commutative)
    have 5: "x y . x = - (- x  y)  - (- x  - y)"
      by (simp add: huntington)
    have 6: "x y . - (- x  y)  - (- x  - y) = x"
      using 5 by metis
    have 7: "x y . x  y = - (- x  - y)"
      by (simp add: inf_def)
    have 10: "x y z . x  (y  z) = y  (x  z)"
      using 3 4 by metis
    have 11: "x y z . - (- x  y)  (- (- x  - y)  z) = x  z"
      using 3 6 by metis
    have 12: "x y . - (x  - y)  - (- y  - x) = y"
      using 4 6 by metis
    have 13: "x y . - (- x  y)  - (- y  - x) = x"
      using 4 6 by metis
    have 14: "x y . - x  - (- (- x  y)  - - (- x  - y)) = - x  y"
      using 6 by metis
    have 18: "x y z . - (x  - y)  (- (- y  - x)  z) = y  z"
      using 3 12 by metis
    have 20: "x y . - (- x  - y)  - (y  - x) = x"
      using 4 12 by metis
    have 21: "x y . - (x  - y)  - (- x  - y) = y"
      using 4 12 by metis
    have 22: "x y . - x  - (- (y  - x)  - - (- x  - y)) = y  - x"
      using 6 12 by metis
    have 23: "x y . - x  - (- x  (- y  - (y  - x))) = y  - x"
      using 3 4 6 12 by metis
    have 24: "x y . - x  - (- (- x  - y)  - - (- x  y)) = - x  - y"
      using 6 12 by metis
    have 28: "x y . - (- x  - y)  - (- y  x) = y"
      using 4 13 by metis
    have 30: "x y . - x  - (- y  (- x  - (- x  y))) = - x  y"
      using 3 4 6 13 by metis
    have 32: "x y z . - (- x  y)  (z  - (- y  - x)) = z  x"
      using 10 13 by metis
    have 37: "x y z . - (- x  - y)  (- (y  - x)  z) = x  z"
      using 3 20 by metis
    have 39: "x y z . - (- x  - y)  (z  - (y  - x)) = z  x"
      using 10 20 by metis
    have 40: "x y z . - (x  - y)  (- (- x  - y)  z) = y  z"
      using 3 21 by metis
    have 43: "x y . - x  - (- y  (- x  - (y  - x))) = y  - x"
      using 3 4 6 21 by metis
    have 47: "x y z . - (x  y)  - (- (- x  z)  - (- (- x  - z)  y)) = - x  z"
      using 6 11 by metis
    have 55: "x y . x  - (- y  - - x) = y  - (- x  y)"
      using 4 11 12 by metis
    have 58: "x y . x  - (- - y  - x) = x  - (- x  y)"
      using 4 11 13 by metis
    have 63: "x y . x  - (- - x  - y) = y  - (- x  y)"
      using 4 11 21 by metis
    have 71: "x y . x  - (- y  x) = y  - (- x  y)"
      using 4 11 28 by metis
    have 75: "x y . x  - (- y  x) = y  - (y  - x)"
      using 4 71 by metis
    have 78: "x y . - x  (y  - (- x  (y  - - (- x  - y)))) = - x  - (- x  - y)"
      using 3 4 6 71 by metis
    have 86: "x y . - (- x  - (- y  x))  - (y  - (- x  y)) = - y  x"
      using 4 20 71 by metis
    have 172: "x y . - x  - (- x  - y) = y  - (- - x  y)"
      using 14 75 by metis
    have 201: "x y . x  - (- y  - - x) = y  - (y  - x)"
      using 4 55 by metis
    have 236: "x y . x  - (- - y  - x) = x  - (y  - x)"
      using 4 58 by metis
    have 266: "x y . - x  - (- (- x  - (y  - - x))  - - (- x  - - (- - x  y))) = - x  - (- - x  y)"
      using 14 58 236 by metis
    have 678: "x y z . - (- x  - (- y  x))  (- (y  - (- x  y))  z) = - y  (x  z)"
      using 3 4 37 71 by smt
    have 745: "x y z . - (- x  - (- y  x))  (z  - (y  - (- x  y))) = z  (- y  x)"
      using 4 39 71 by metis
    have 800: "x y . - - x  (- y  (- (y  - - x)  - (- x  (- - x  (- y  - (y  - - x)))))) = x  - (y  - - x)"
      using 3 23 63 by metis
    have 944: "x y . x  - (x  - - (- (- x  - y)  - - (- x  y))) = - (- x  - y)  - (- (- x  - y)  - - (- x  y))"
      using 4 24 71 by metis
    have 948: "x y . - x  - (- (y  - (y  - - x))  - - (- x  (- y  - x))) = - x  - (- y  - x)"
      using 24 75 by metis
    have 950: "x y . - x  - (- (y  - (- - x  y))  - - (- x  (- x  - y))) = - x  - (- x  - y)"
      using 24 75 by metis
    have 961: "x y . - x  - (- (y  - (- - x  y))  - - (- x  (- - - x  - y))) = y  - (- - x  y)"
      using 24 63 by metis
    have 966: "x y . - x  - (- (y  - (y  - - x))  - - (- x  (- y  - - - x))) = y  - (y  - - x)"
      using 24 201 by metis
    have 969: "x y . - x  - (- (- x  - (y  - - x))  - - (- x  (- - y  - - x))) = - x  - (y  - - x)"
      using 24 236 by metis
    have 1096: "x y z . - x  (- (- x  - y)  z) = y  (- (- - x  y)  z)"
      using 3 172 by metis
    have 1098: "x y z . - x  (y  - (- x  - z)) = y  (z  - (- - x  z))"
      using 10 172 by metis
    have 1105: "x y . x  - x = y  - y"
      using 4 10 12 32 172 by metis
    have 1109: "x y z . x  (- x  y) = z  (- z  y)"
      using 3 1105 by metis
    have 1110: "x y z . x  - x = y  (z  - (y  z))"
      using 3 1105 by metis
    have 1114: "x y . - (- x  - - x) = - (y  - y)"
      using 7 1105 by metis
    have 1115: "x y z . x  (y  - y) = z  (x  - z)"
      using 10 1105 by metis
    have 1117: "x y . - (x  - - x)  - (y  - y) = - x"
      using 4 13 1105 by metis
    have 1121: "x y . - (x  - x)  - (y  - - y) = - y"
      using 4 28 1105 by metis
    have 1122: "x . - - x = x"
      using 4 28 1105 1117 by metis
    have 1134: "x y z . - (x  - y)  (z  - z) = y  (- y  - x)"
      using 18 1105 1122 by metis
    have 1140: "x . - x  - (x  (x  - x)) = - x  - x"
      using 4 22 1105 1122 1134 by metis
    have 1143: "x y . x  (- x  y) = y  (x  - y)"
      using 37 1105 1122 1134 by metis
    have 1155: "x y . - (x  - x)  - (y  y) = - y"
      using 1121 1122 by metis
    have 1156: "x y . - (x  x)  - (y  - y) = - x"
      using 1117 1122 by metis
    have 1157: "x y . - (x  - x) = - (y  - y)"
      using 4 1114 1122 by metis
    have 1167: "x y z . - x  (y  - (- x  - z)) = y  (z  - (x  z))"
      using 1098 1122 by metis
    have 1169: "x y z . - x  (- (- x  - y)  z) = y  (- (x  y)  z)"
      using 1096 1122 by metis
    have 1227: "x y . - x  - (- x  (y  (x  - (- x  - (y  x))))) = - x  - (y  x)"
      using 3 4 969 1122 by smt
    have 1230: "x y . - x  - (- x  (- y  (- x  - (y  - (y  x))))) = y  - (y  x)"
      using 3 4 966 1122 by smt
    have 1234: "x y . - x  - (- x  (- x  (- y  - (y  - (x  y))))) = y  - (x  y)"
      using 3 4 961 1122 by metis
    have 1239: "x y . - x  - (- x  - y) = y  - (x  y)"
      using 3 4 950 1122 1234 by metis
    have 1240: "x y . - x  - (- y  - x) = y  - (y  x)"
      using 3 4 948 1122 1230 by metis
    have 1244: "x y . x  - (x  (y  (y  - (x  y)))) = - (- x  - y)  - (y  (y  - (x  y)))"
      using 3 4 944 1122 1167 by metis
    have 1275: "x y . x  (- y  (- (y  x)  - (x  (- x  (- y  - (y  x)))))) = x  - (y  x)"
      using 10 800 1122 by metis
    have 1346: "x y . - x  - (x  (y  (y  (x  - (x  (y  x)))))) = - x  - (x  y)"
      using 3 4 10 266 1122 1167 by smt
    have 1377: "x y . - x  (y  - (- x  (y  (- x  - y)))) = y  - (x  y)"
      using 78 1122 1239 by metis
    have 1394: "x y . - (- x  - y)  - (y  (y  (- x  - (x  y)))) = x"
      using 3 4 10 20 30 1122 1239 by smt
    have 1427: "x y . - (- x  - y)  - (y  - (x  (x  - (x  y)))) = x  (x  - (x  y))"
      using 3 4 30 40 1240 by smt
    have 1436: "x . - x  - (x  (x  (- x  - x))) = - x  (- x  - (x  - x))"
      using 3 4 30 1140 1239 by smt
    have 1437: "x y . - (x  y)  - (x  - y) = - x"
      using 6 1122 by metis
    have 1438: "x y . - (x  y)  - (y  - x) = - y"
      using 12 1122 by metis
    have 1439: "x y . - (x  y)  - (- y  x) = - x"
      using 13 1122 by metis
    have 1440: "x y . - (x  - y)  - (y  x) = - x"
      using 20 1122 by metis
    have 1441: "x y . - (x  y)  - (- x  y) = - y"
      using 21 1122 by metis
    have 1568: "x y . x  (- y  - x) = y  (- y  x)"
      using 10 1122 1143 by metis
    have 1598: "x . - x  - (x  (x  (x  - x))) = - x  (- x  - (x  - x))"
      using 4 1436 1568 by metis
    have 1599: "x y . - x  (y  - (x  (- x  (- x  y)))) = y  - (x  y)"
      using 10 1377 1568 by smt
    have 1617: "x . x  (- x  (- x  - (x  - x))) = x  - x"
      using 3 4 10 71 1122 1155 1568 1598 by metis
    have 1632: "x y z . - (x  - x)  - (- y  (- (z  - z)  - (y  - (x  - x)))) = y  - (x  - x)"
      using 43 1157 by metis
    have 1633: "x y z . - (x  - x)  - (- y  (- (x  - x)  - (y  - (z  - z)))) = y  - (x  - x)"
      using 43 1157 by metis
    have 1636: "x y . x  - (y  (- y  - (x  x))) = x  x"
      using 43 1109 1122 by metis
    have 1645: "x y . x  - x = y  (y  - y)"
      using 3 1110 1156 by metis
    have 1648: "x y z . - (x  (y  (- y  - x)))  - (z  - z) = - (y  - y)"
      using 3 1115 1156 by metis
    have 1657: "x y z . x  - x = y  (z  - z)"
      using 1105 1645 by metis
    have 1664: "x y z . x  - x = y  (z  - y)"
      using 1115 1645 by metis
    have 1672: "x y z . x  - x = y  (- y  z)"
      using 3 4 1657 by metis
    have 1697: "x y z . - x  (y  x) = z  - z"
      using 1122 1664 by metis
    have 1733: "x y z . - (x  y)  - (- (z  - z)  - (- (- x  - x)  y)) = x  - x"
      using 4 47 1105 1122 by metis
    have 1791: "x y z . x  - (y  (- y  z)) = x  - (x  - x)"
      using 4 71 1122 1672 by metis
    have 1818: "x y z . x  - (- y  (z  y)) = x  - (x  - x)"
      using 4 71 1122 1697 by metis
    have 1861: "x y z . - (x  - x)  - (y  - (z  - z)) = - y"
      using 1437 1657 by metis
    have 1867: "x y z . - (x  - x)  - (- y  - (z  y)) = y"
      using 1122 1437 1697 by metis
    have 1868: "x y . x  - (y  - y) = x"
      using 1122 1155 1633 1861 by metis
    have 1869: "x y z . - (x  - x)  - (- y  (- (z  - z)  - y)) = y"
      using 1632 1868 by metis
    have 1870: "x y . - (x  - x)  - y = - y"
      using 1861 1868 by metis
    have 1872: "x y z . x  - (- y  (z  y)) = x"
      using 1818 1868 by metis
    have 1875: "x y z . x  - (y  (- y  z)) = x"
      using 1791 1868 by metis
    have 1883: "x y . - (x  (y  (- y  - x))) = - (y  - y)"
      using 1648 1868 by metis
    have 1885: "x . x  (x  - x) = x  - x"
      using 4 1568 1617 1868 by metis
    have 1886: "x . - x  - x = - x"
      using 1598 1868 1885 by metis
    have 1890: "x . - (x  x) = - x"
      using 1156 1868 by metis
    have 1892: "x y . - (x  - x)  y = y"
      using 1122 1869 1870 1886 by metis
    have 1893: "x y . - (- x  - (y  x)) = x"
      using 1867 1892 by metis
    have 1902: "x y . x  (y  - (x  y)) = x  - x"
      using 3 4 1122 1733 1886 1892 by metis
    have 1908: "x . x  x = x"
      using 1636 1875 1890 by metis
    have 1910: "x y . x  - (y  x) = - y  x"
      using 1599 1875 by metis
    have 1921: "x y . x  (- y  - (y  x)) = - y  x"
      using 1275 1875 1910 by metis
    have 1951: "x y . - x  - (y  x) = - x"
      using 1227 1872 1893 1908 by metis
    have 1954: "x y z . x  (y  - (x  z)) = y  (- z  x)"
      using 745 1122 1910 1951 by metis
    have 1956: "x y z . x  (- (x  y)  z) = - y  (x  z)"
      using 678 1122 1910 1951 by metis
    have 1959: "x y . x  - (x  y) = - y  x"
      using 86 1122 1910 1951 by metis
    have 1972: "x y . x  (- x  y) = x  - x"
      using 1902 1910 by metis
    have 2000: "x y . - (- x  - y)  - (y  (- x  y)) = x  - (y  (- x  y))"
      using 4 1244 1910 1959 by metis
    have 2054: "x y . x  - (y  (- x  y)) = x"
      using 1394 1921 2000 by metis
    have 2057: "x y . - (x  (y  - y)) = - (y  - y)"
      using 1883 1972 by metis
    have 2061: "x y . x  (- y  x) = x  - y"
      using 4 1122 1427 1910 1959 2054 by metis
    have 2090: "x y z . x  (- (y  x)  z) = x  (- y  z)"
      using 1122 1169 1956 by metis
    have 2100: "x y . - x  - (x  y) = - x"
      using 4 1346 1868 1885 1910 1959 1972 2057 by metis
    have 2144: "x y . x  - (y  - x) = x"
      using 1122 1440 2000 2061 by metis
    have 2199: "x y . x  (x  y) = x  y"
      using 3 1908 by metis
    have 2208: "x y z . x  (- (y  - x)  z) = x  z"
      using 3 2144 by metis
    have 2349: "x y z . - (x  y)  - (x  (y  z)) = - (x  y)"
      using 3 2100 by metis
    have 2432: "x y z . - (x  (y  z))  - (y  (z  - x)) = - (y  z)"
      using 3 1438 by metis
    have 2530: "x y z . - (- (x  y)  z) = - (y  (- x  z))  - (- y  z)"
      using 4 1122 1439 2090 2208 by smt
    have 3364: "x y z . - (- x  y)  (z  - (x  y)) = z  - y"
      using 3 4 1122 1441 1910 1954 2199 by metis
    have 5763: "x y z . - (x  y)  - (- x  (y  z)) = - (x  y)  - (y  z)"
      using 4 2349 3364 by metis
    have 6113: "x y z . - (x  (y  z))  - (z  - x) = - (y  z)  - (z  - x)"
      using 4 2432 3364 5763 by metis
    show "x y z. x  y  z = (x  y)  (x  z)"
    proof -
      fix x y z
      have "- (y  z  x) = - (- (- y  z)  - (- y  - z)  x)  - (x  - - z)"
        using 1437 2530 6113 by (smt commutative inf_def)
      thus "x  y  z = (x  y)  (x  z)"
        using 12 1122 by (metis commutative inf_def)
    qed
  qed
  show 14: "x. x  - x = bot"
  proof -
    fix x
    have "(bot  x)  (bot  -x) = bot"
      using huntington bot_def inf_def by auto
    thus "x  -x = bot"
      using 11 less_eq_def by force
  qed
  show 15: "x. x  - x = top"
    using 5 14 by (metis (no_types, lifting) huntington bot_def less_eq_def top_def)
  show 16: "x y. x - y = x  - y"
    using 15 by (metis commutative huntington inf_def minus_def)
  show 7: "x y z. x  y  x  z  x  y  z"
    by (simp add: 13 less_eq_def)
qed

end

context boolean_algebra
begin

sublocale ba_he: huntington_extended
proof
  show "x y z. x  (y  z) = x  y  z"
    by (simp add: sup_assoc)
  show "x y. x  y = y  x"
    by (simp add: sup_commute)
  show "x y. x = - (- x  y)  - (- x  - y)"
    by simp
  show "top = (THE x. y. x = y  - y)"
    by auto
  show "bot = - (THE x. y. x = y  - y)"
    by auto
  show "x y. x  y = - (- x  - y)"
    by simp
  show "x y. x - y = - (- x  y)"
    by (simp add: diff_eq)
  show "x y. (x  y) = (x  y = y)"
    by (simp add: le_iff_sup)
  show "x y. (x < y) = (x  y = y  y  x  x)"
    using sup.strict_order_iff sup_commute by auto
qed

end

subsection ‹Stone Algebras›

text ‹
We relate Stone algebras to Boolean algebras.
›

class stone_algebra_extended = stone_algebra + minus +
  assumes stone_minus_def[simp]: "x - y = x  -y"

class regular_stone_algebra = stone_algebra_extended +
  assumes double_complement[simp]: "--x = x"
begin

subclass boolean_algebra
proof
  show "x. x  - x = bot"
    by simp
  show "x. x  - x = top"
    using regular_dense_top by fastforce
  show "x y. x - y = x  - y"
    by simp
qed

end

context boolean_algebra
begin

sublocale ba_rsa: regular_stone_algebra
proof
  show "x y. x - y = x  - y"
    by (simp add: diff_eq)
  show "x. - - x = x"
    by simp
qed

end

section ‹Alternative Axiomatisations of Boolean Algebras›

text ‹
We consider four axiomatisations of Boolean algebras based only on join and complement.
The first three are from the literature and the fourth, a version using equational axioms, is new.
The motivation for Byrne's and the new axiomatisation is that the axioms are easier to understand than Huntington's third axiom.
We also include Meredith's axiomatisation.
›

subsection ‹Lee Byrne's Formulation A›

text ‹
The following axiomatisation is from cite‹Formulation A› in "Byrne1946"; see also cite"Frink1941".
›

text ‹Theorem 3›

class boolean_algebra_1 = sup + uminus +
  assumes ba1_associative: "x  (y  z) = (x  y)  z"
  assumes ba1_commutative: "x  y = y  x"
  assumes ba1_complement: "x  -y = z  -z  x  y = x"
begin

subclass huntington
proof
  show 1: "x y z. x  (y  z) = x  y  z"
    by (simp add: ba1_associative)
  show "x y. x  y = y  x"
    by (simp add: ba1_commutative)
  show "x y. x = - (- x  y)  - (- x  - y)"
  proof -
    have 2: "x y. y  (y  x) = y  x"
      using 1 by (metis ba1_complement)
    hence "x. --x = x"
      by (smt ba1_associative ba1_commutative ba1_complement)
    hence "x y. y  -(y  -x) = y  x"
      by (smt ba1_associative ba1_commutative ba1_complement)
    thus "x y. x = -(-x  y)  -(-x  - y)"
      using 2 by (smt ba1_commutative ba1_complement)
  qed
qed

end

context huntington
begin

sublocale h_ba1: boolean_algebra_1
proof
  show "x y z. x  (y  z) = x  y  z"
    by (simp add: associative)
  show "x y. x  y = y  x"
    by (simp add: commutative)
  show "x y z. (x  - y = z  - z) = (x  y = x)"
  proof
    fix x y z
    have 1: "x y z. -(-x  y)  (-(-x  -y)  z) = x  z"
      using associative huntington by force
    have 2: "x y. -(x  -y)  -(-y  -x) = y"
      by (metis commutative huntington)
    show "x  - y = z  - z  x  y = x"
      by (metis 1 2 associative commutative top_unique)
    show "x  y = x  x  - y = z  - z"
      by (metis associative huntington commutative top_unique)
  qed
qed

end

subsection ‹Lee Byrne's Formulation B›

text ‹
The following axiomatisation is from cite‹Formulation B› in "Byrne1946".
›

text ‹Theorem 4›

class boolean_algebra_2 = sup + uminus +
  assumes ba2_associative_commutative: "(x  y)  z = (y  z)  x"
  assumes ba2_complement: "x  -y = z  -z  x  y = x"
begin

subclass boolean_algebra_1
proof
  show "x y z. x  (y  z) = x  y  z"
    by (smt ba2_associative_commutative ba2_complement)
  show "x y. x  y = y  x"
    by (metis ba2_associative_commutative ba2_complement)
  show "x y z. (x  - y = z  - z) = (x  y = x)"
    by (simp add: ba2_complement)
qed

end

context boolean_algebra_1
begin

sublocale ba1_ba2: boolean_algebra_2
proof
  show "x y z. x  y  z = y  z  x"
    using ba1_associative commutative by force
  show "x y z. (x  - y = z  - z) = (x  y = x)"
    by (simp add: ba1_complement)
qed

end

subsection ‹Meredith's Equational Axioms›

text ‹
The following axiomatisation is from cite‹page 221 (1) \{A,N\}› in "MeredithPrior1968".
›

class boolean_algebra_mp = sup + uminus +
  assumes ba_mp_1: "-(-x  y)  x = x"
  assumes ba_mp_2: "-(-x  y)  (z  y) = y  (z  x)"
begin

subclass huntington
proof
  show "x y z. x  (y  z) = x  y  z"
    by (metis ba_mp_1 ba_mp_2)
  show "x y. x  y = y  x"
    by (metis ba_mp_1 ba_mp_2)
  show "x y. x = - (- x  y)  - (- x  - y)"
    by (metis ba_mp_1 ba_mp_2)
qed

end

context huntington
begin

sublocale mp_h: boolean_algebra_mp
proof
  show 1: "x y. - (- x  y)  x = x"
    by (metis h_ba1.ba1_associative h_ba1.ba1_complement huntington)
  show "x y z. - (- x  y)  (z  y) = y  (z  x)"
  proof -
    fix x y z
    have "y = -(-x  -y)  y"
      using 1 h_ba1.ba1_commutative by auto
    thus "-(-x  y)  (z  y) = y  (z  x)"
      by (metis h_ba1.ba1_associative h_ba1.ba1_commutative huntington)
  qed
qed

end

subsection ‹An Equational Axiomatisation based on Semilattices›

text ‹
The following version is an equational axiomatisation based on semilattices.
We add the double complement rule and that top› is unique.
The final axiom ba3_export› encodes the logical statement $P \vee Q = P \vee (\neg P \wedge Q)$.
Its dual appears in cite"BalbesHorn1970".
›

text ‹Theorem 5›

class boolean_algebra_3 = sup + uminus +
  assumes ba3_associative: "x  (y  z) = (x  y)  z"
  assumes ba3_commutative: "x  y = y  x"
  assumes ba3_idempotent[simp]: "x  x = x"
  assumes ba3_double_complement[simp]: "--x = x"
  assumes ba3_top_unique: "x  -x = y  -y"
  assumes ba3_export: "x  -(x  y) = x  -y"
begin

subclass huntington
proof
  show "x y z. x  (y  z) = x  y  z"
    by (simp add: ba3_associative)
  show "x y. x  y = y  x"
    by (simp add: ba3_commutative)
  show "x y. x = - (- x  y)  - (- x  - y)"
    by (metis ba3_commutative ba3_double_complement ba3_export ba3_idempotent ba3_top_unique)
qed

end

context huntington
begin

sublocale h_ba3: boolean_algebra_3
proof
  show "x y z. x  (y  z) = x  y  z"
    by (simp add: h_ba1.ba1_associative)
  show "x y. x  y = y  x"
    by (simp add: h_ba1.ba1_commutative)
  show 3: "x. x  x = x"
    using h_ba1.ba1_complement by blast
  show 4: "x. - - x = x"
    by (metis h_ba1.ba1_commutative huntington top_unique)
  show "x y. x  - x = y  - y"
    by (simp add: top_unique)
  show "x y. x  - (x  y) = x  - y"
    using 3 4 by (smt h_ba1.ba1_ba2.ba2_associative_commutative h_ba1.ba1_complement)
qed

end

section ‹Subset Boolean Algebras›

text ‹
We apply Huntington's axioms to the range of a unary operation, which serves as complement on the range.
This gives a Boolean algebra structure on the range without imposing any further constraints on the set.
The obtained structure is used as a reference in the subsequent development and to inherit the results proved here.
This is taken from cite"Guttmann2012c" and "GuttmannStruthWeber2011b" and follows the development of Boolean algebras in cite"Maddux1996".
›

text ‹Definition 6›

class subset_boolean_algebra = sup + uminus +
  assumes sub_associative: "-x  (-y  -z) = (-x  -y)  -z"
  assumes sub_commutative: "-x  -y = -y  -x"
  assumes sub_complement: "-x = -(--x  -y)  -(--x  --y)"
  assumes sub_sup_closed: "-x  -y = --(-x  -y)"
begin

text ‹uniqueness of top›, resulting in the lemma top_def› to replace the assumption sub_top_def›

lemma top_unique:
  "-x  --x = -y  --y"
  by (metis sub_associative sub_commutative sub_complement)

text ‹consequences for join and complement›

lemma double_negation[simp]:
  "---x = -x"
  by (metis sub_complement sub_sup_closed)

lemma complement_1:
  "--x = -(-x  -y)  -(-x  --y)"
  by (metis double_negation sub_complement)

lemma sup_right_zero_var:
  "-x  (-y  --y) = -z  --z"
  by (smt complement_1 sub_associative sub_sup_closed top_unique)

lemma sup_right_unit_idempotent:
  "-x  -x = -x  -(-y  --y)"
  by (metis complement_1 double_negation sub_sup_closed sup_right_zero_var)

lemma sup_idempotent[simp]:
  "-x  -x = -x"
  by (smt complement_1 double_negation sub_associative sup_right_unit_idempotent)

lemma complement_2:
  "-x = -(-(-x  -y)  -(-x  --y))"
  using complement_1 by auto

lemma sup_eq_cases:
  "-x  -y = -x  -z  --x  -y = --x  -z  -y = -z"
  by (metis complement_2 sub_commutative)

lemma sup_eq_cases_2:
  "-y  -x = -z  -x  -y  --x = -z  --x  -y = -z"
  using sub_commutative sup_eq_cases by auto

end

text ‹Definition 7›

class subset_extended = sup + inf + minus + uminus + bot + top + ord +
  assumes sub_top_def: "top = (THE x . y . x = -y  --y)" (* define without imposing uniqueness *)
  assumes sub_bot_def: "bot = -(THE x . y . x = -y  --y)"
  assumes sub_inf_def: "-x  -y = -(--x  --y)"
  assumes sub_minus_def: "-x - -y = -(--x  -y)"
  assumes sub_less_eq_def: "-x  -y  -x  -y = -y"
  assumes sub_less_def: "-x < -y  -x  -y = -y  ¬ (-y  -x = -x)"

class subset_boolean_algebra_extended = subset_boolean_algebra + subset_extended
begin

lemma top_def:
  "top = -x  --x"
  using sub_top_def top_unique by blast

text ‹consequences for meet›

lemma inf_closed:
  "-x  -y = --(-x  -y)"
  by (simp add: sub_inf_def)

lemma inf_associative:
  "-x  (-y  -z) = (-x  -y)  -z"
  using sub_associative sub_inf_def sub_sup_closed by auto

lemma inf_commutative:
  "-x  -y = -y  -x"
  by (simp add: sub_commutative sub_inf_def)

lemma inf_idempotent[simp]:
  "-x  -x = -x"
  by (simp add: sub_inf_def)

lemma inf_absorb[simp]:
  "(-x  -y)  -x = -x"
  by (metis complement_1 sup_idempotent sub_inf_def sub_associative sub_sup_closed)

lemma sup_absorb[simp]:
  "-x  (-x  -y) = -x"
  by (metis sub_associative sub_complement sub_inf_def sup_idempotent)

lemma inf_demorgan:
  "-(-x  -y) = --x  --y"
  using sub_inf_def sub_sup_closed by auto

lemma sub_sup_demorgan:
  "-(-x  -y) = --x  --y"
  by (simp add: sub_inf_def)

lemma sup_cases:
  "-x = (-x  -y)  (-x  --y)"
  by (metis inf_closed inf_demorgan sub_complement)

lemma inf_cases:
  "-x = (-x  -y)  (-x  --y)"
  by (metis complement_2 sub_sup_closed sub_sup_demorgan)

lemma inf_complement_intro:
  "(-x  -y)  --x = -y  --x"
proof -
  have "(-x  -y)  --x = (-x  -y)  (--x  -y)  --x"
    by (metis inf_absorb inf_associative sub_sup_closed)
  also have "... = -y  --x"
    by (metis inf_cases sub_commutative)
  finally show ?thesis
    .
qed

lemma sup_complement_intro:
  "-x  -y = -x  (--x  -y)"
  by (metis inf_absorb inf_commutative inf_complement_intro sub_sup_closed sup_cases)

lemma inf_left_dist_sup:
  "-x  (-y  -z) = (-x  -y)  (-x  -z)"
proof -
  have "-x  (-y  -z) = (-x  (-y  -z)  -y)  (-x  (-y  -z)  --y)"
    by (metis sub_inf_def sub_sup_closed sup_cases)
  also have "... = (-x  -y)  (-x  -z  --y)"
    by (metis inf_absorb inf_associative inf_complement_intro sub_sup_closed)
  also have "... = (-x  -y)  ((-x  -y  -z)  (-x  -z  --y))"
    using sub_associative sub_inf_def sup_absorb by auto
  also have "... = (-x  -y)  ((-x  -z  -y)  (-x  -z  --y))"
    by (metis inf_associative inf_commutative)
  also have "... = (-x  -y)  (-x  -z)"
    by (metis sub_inf_def sup_cases)
  finally show ?thesis
    .
qed

lemma sup_left_dist_inf:
  "-x  (-y  -z) = (-x  -y)  (-x  -z)"
proof -
  have "-x  (-y  -z) = -(--x  (--y  --z))"
    by (metis sub_inf_def sub_sup_closed sub_sup_demorgan)
  also have "... = (-x  -y)  (-x  -z)"
    by (metis inf_left_dist_sup sub_sup_closed sub_sup_demorgan)
  finally show ?thesis
    .
qed

lemma sup_right_dist_inf:
  "(-y  -z)  -x = (-y  -x)  (-z  -x)"
  using sub_commutative sub_inf_def sup_left_dist_inf by auto

lemma inf_right_dist_sup:
  "(-y  -z)  -x = (-y  -x)  (-z  -x)"
  by (metis inf_commutative inf_left_dist_sup sub_sup_closed)

lemma case_duality:
  "(--x  -y)  (-x  -z) = (-x  -y)  (--x  -z)"
proof -
  have 1: "-(--x  --y)  ----x = --x  -y"
    using inf_commutative inf_complement_intro sub_sup_closed sub_sup_demorgan by auto
  have 2: "-(----x  -(--x  -z)) = -----x  ---z"
    by (metis (no_types) double_negation sup_complement_intro sub_sup_demorgan)
  have 3: "-(--x  --y)  -x = -x"
    using inf_commutative inf_left_dist_sup sub_sup_closed sub_sup_demorgan by auto
  hence "-(--x  --y) = -x  -y"
    using sub_sup_closed sub_sup_demorgan by auto
  thus ?thesis
    by (metis double_negation 1 2 3 inf_associative inf_left_dist_sup sup_complement_intro)
qed

lemma case_duality_2:
  "(-x  -y)  (--x  -z) = (-x  -z)  (--x  -y)"
  using case_duality sub_commutative sub_inf_def by auto

lemma complement_cases:
  "((-v  -w)  (--v  -x))  -((-v  -y)  (--v  -z)) = (-v  -w  --y)  (--v  -x  --z)"
proof -
  have 1: "(--v  -w) = --(--v  -w)  (-v  -x) = --(-v  -x)  (--v  --y) = --(--v  --y)  (-v  --z) = --(-v  --z)"
    using sub_inf_def sub_sup_closed by auto
  have 2: "(-v  (-x  --z)) = --(-v  (-x  --z))"
    using sub_inf_def sub_sup_closed by auto
  have "((-v  -w)  (--v  -x))  -((-v  -y)  (--v  -z)) = ((-v  -w)  (--v  -x))  (-(-v  -y)  -(--v  -z))"
    using sub_inf_def by auto
  also have "... = ((-v  -w)  (--v  -x))  ((--v  --y)  (-v  --z))"
    using inf_demorgan by auto
  also have "... = (--v  -w)  (-v  -x)  ((--v  --y)  (-v  --z))"
    by (metis case_duality double_negation)
  also have "... = (--v  -w)  ((-v  -x)  ((--v  --y)  (-v  --z)))"
    by (metis 1 inf_associative sub_inf_def)
  also have "... = (--v  -w)  ((-v  -x)  (--v  --y)  (-v  --z))"
    by (metis 1 inf_associative)
  also have "... = (--v  -w)  ((--v  --y)  (-v  -x)  (-v  --z))"
    by (metis 1 inf_commutative)
  also have "... = (--v  -w)  ((--v  --y)  ((-v  -x)  (-v  --z)))"
    by (metis 1 inf_associative)
  also have "... = (--v  -w)  ((--v  --y)  (-v  (-x  --z)))"
    by (simp add: sup_left_dist_inf)
  also have "... = (--v  -w)  (--v  --y)  (-v  (-x  --z))"
    using 1 2 by (metis inf_associative)
  also have "... = (--v  (-w  --y))  (-v  (-x  --z))"
    by (simp add: sup_left_dist_inf)
  also have "... = (-v  (-w  --y))  (--v  (-x  --z))"
    by (metis case_duality complement_1 complement_2 sub_inf_def)
  also have "... = (-v  -w  --y)  (--v  -x  --z)"
    by (simp add: inf_associative)
  finally show ?thesis
    .
qed

lemma inf_cases_2: "--x = -(-x  -y)  -(-x  --y)"
  using sub_inf_def sup_cases by auto

text ‹consequences for top› and bot›

lemma sup_complement[simp]:
  "-x  --x = top"
  using top_def by auto

lemma inf_complement[simp]:
  "-x  --x = bot"
  by (metis sub_bot_def sub_inf_def sub_top_def top_def)

lemma complement_bot[simp]:
  "-bot = top"
  using inf_complement inf_demorgan sup_complement by fastforce

lemma complement_top[simp]:
  "-top = bot"
  using sub_bot_def sub_top_def by blast

lemma sup_right_zero[simp]:
  "-x  top = top"
  using sup_right_zero_var by auto

lemma sup_left_zero[simp]:
  "top  -x = top"
  by (metis complement_bot sub_commutative sup_right_zero)

lemma inf_right_unit[simp]:
  "-x  bot = bot"
  by (metis complement_bot complement_top double_negation sub_sup_demorgan sup_right_zero)

lemma inf_left_unit[simp]:
  "bot  -x = bot"
  by (metis complement_top inf_commutative inf_right_unit)

lemma sup_right_unit[simp]:
  "-x  bot = -x"
  using sup_right_unit_idempotent by auto

lemma sup_left_unit[simp]:
  "bot  -x = -x"
  by (metis complement_top sub_commutative sup_right_unit)

lemma inf_right_zero[simp]:
  "-x  top = -x"
  by (metis inf_left_dist_sup sup_cases top_def)

lemma sub_inf_left_zero[simp]:
  "top  -x = -x"
  using inf_absorb top_def by fastforce

lemma bot_double_complement[simp]:
  "--bot = bot"
  by simp

lemma top_double_complement[simp]:
  "--top = top"
  by simp

text ‹consequences for the order›

lemma reflexive:
  "-x  -x"
  by (simp add: sub_less_eq_def)

lemma transitive:
  "-x  -y  -y  -z  -x  -z"
  by (metis sub_associative sub_less_eq_def)

lemma antisymmetric:
  "-x  -y  -y  -x  -x = -y"
  by (simp add: sub_commutative sub_less_eq_def)

lemma sub_bot_least:
  "bot  -x"
  using sup_left_unit complement_top sub_less_eq_def by blast

lemma top_greatest:
  "-x  top"
  using complement_bot sub_less_eq_def sup_right_zero by blast

lemma upper_bound_left:
  "-x  -x  -y"
  by (metis sub_associative sub_less_eq_def sub_sup_closed sup_idempotent)

lemma upper_bound_right:
  "-y  -x  -y"
  using sub_commutative upper_bound_left by fastforce

lemma sub_sup_left_isotone:
  assumes "-x  -y"
    shows "-x  -z  -y  -z"
proof -
  have "-x  -y = -y"
    by (meson assms sub_less_eq_def)
  thus ?thesis
    by (metis (full_types) sub_associative sub_commutative sub_sup_closed upper_bound_left)
qed

lemma sub_sup_right_isotone:
  "-x  -y  -z  -x  -z  -y"
  by (simp add: sub_commutative sub_sup_left_isotone)

lemma sup_isotone:
  assumes "-p  -q"
      and "-r  -s"
    shows "-p  -r  -q  -s"
proof -
  have "x y. ¬ -x  -y  -r  -x  -y  -s"
    by (metis (full_types) assms(2) sub_sup_closed sub_sup_right_isotone transitive)
  thus ?thesis
    by (metis (no_types) assms(1) sub_sup_closed sub_sup_left_isotone)
qed

lemma sub_complement_antitone:
  "-x  -y  -