Theory 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 ⟹ --y ≤ --x"
  by (metis inf_absorb inf_demorgan sub_less_eq_def)

lemma less_eq_inf:
  "-x ≤ -y ⟷ -x ⊓ -y = -x"
  by (metis inf_absorb inf_commutative sub_less_eq_def upper_bound_right sup_absorb)

lemma inf_complement_left_antitone:
  "-x ≤ -y ⟹ -(-y ⊓ -z) ≤ -(-x ⊓ -z)"
  by (simp add: sub_complement_antitone inf_demorgan sub_sup_left_isotone)

lemma sub_inf_left_isotone:
  "-x ≤ -y ⟹ -x ⊓ -z ≤ -y ⊓ -z"
  using sub_complement_antitone inf_closed inf_complement_left_antitone by fastforce

lemma sub_inf_right_isotone:
  "-x ≤ -y ⟹ -z ⊓ -x ≤ -z ⊓ -y"
  by (simp add: inf_commutative sub_inf_left_isotone)

lemma inf_isotone:
  assumes "-p ≤ -q"
      and "-r ≤ -s"
    shows "-p ⊓ -r ≤ -q ⊓ -s"
proof -
  have "∀w x y z. (-w ≤ -x ⊓ -y ∨ ¬ -w ≤ -x ⊓ -z) ∨ ¬ -z ≤ -y"
    by (metis (no_types) inf_closed sub_inf_right_isotone transitive)
  thus ?thesis
    by (metis (no_types) assms inf_closed sub_inf_left_isotone)
qed

lemma least_upper_bound:
  "-x ≤ -z ∧ -y ≤ -z ⟷ -x ⊔ -y ≤ -z"
  by (metis sub_sup_closed transitive upper_bound_right sup_idempotent sup_isotone upper_bound_left)

lemma lower_bound_left:
  "-x ⊓ -y ≤ -x"
  by (metis sub_inf_def upper_bound_right sup_absorb)

lemma lower_bound_right:
  "-x ⊓ -y ≤ -y"
  using inf_commutative lower_bound_left by fastforce

lemma greatest_lower_bound:
  "-x ≤ -y ∧ -x ≤ -z ⟷ -x ≤ -y ⊓ -z"
  by (metis inf_closed sub_inf_left_isotone less_eq_inf transitive lower_bound_left lower_bound_right)

lemma less_eq_sup_top:
  "-x ≤ -y ⟷ --x ⊔ -y = top"
  by (metis complement_1 inf_commutative inf_complement_intro sub_inf_left_zero less_eq_inf sub_complement sup_complement_intro top_def)

lemma less_eq_inf_bot:
  "-x ≤ -y ⟷ -x ⊓ --y = bot"
  by (metis complement_bot complement_top double_negation inf_demorgan less_eq_sup_top sub_inf_def)

lemma shunting:
  "-x ⊓ -y ≤ -z ⟷ -y ≤ --x ⊔ -z"
proof (cases "--x ⊔ (-z ⊔ --y) = top")
  case True
  have "∀v w. -v ≤ -w ∨ -w ⊔ --v ≠ top"
    using less_eq_sup_top sub_commutative by blast
  thus ?thesis
    by (metis True sub_associative sub_commutative sub_inf_def sub_sup_closed)
next
  case False
  hence "--x ⊔ (-z ⊔ --y) ≠ top ∧ ¬ -y ≤ -z ⊔ --x"
    by (metis (no_types) less_eq_sup_top sub_associative sub_commutative sub_sup_closed)
  thus ?thesis
    using less_eq_sup_top sub_associative sub_commutative sub_inf_def sub_sup_closed by auto
qed

lemma shunting_right:
  "-x ⊓ -y ≤ -z ⟷ -x ≤ -z ⊔ --y"
  by (metis inf_commutative sub_commutative shunting)

lemma sup_less_eq_cases:
  assumes "-z ≤ -x ⊔ -y"
      and "-z ≤ --x ⊔ -y"
    shows "-z ≤ -y"
proof -
  have "-z ≤ (-x ⊔ -y) ⊓ (--x ⊔ -y)"
    by (metis assms greatest_lower_bound sub_sup_closed)
  also have "... = -y"
    by (metis inf_cases sub_commutative)
  finally show ?thesis
    .
qed

lemma sup_less_eq_cases_2:
  "-x ⊔ -y ≤ -x ⊔ -z ⟹ --x ⊔ -y ≤ --x ⊔ -z ⟹ -y ≤ -z"
  by (metis least_upper_bound sup_less_eq_cases sub_sup_closed)

lemma sup_less_eq_cases_3:
  "-y ⊔ -x ≤ -z ⊔ -x ⟹ -y ⊔ --x ≤ -z ⊔ --x ⟹ -y ≤ -z"
  by (simp add: sup_less_eq_cases_2 sub_commutative)

lemma inf_less_eq_cases:
  "-x ⊓ -y ≤ -z ⟹ --x ⊓ -y ≤ -z ⟹ -y ≤ -z"
  by (simp add: shunting sup_less_eq_cases)

lemma inf_less_eq_cases_2:
  "-x ⊓ -y ≤ -x ⊓ -z ⟹ --x ⊓ -y ≤ --x ⊓ -z ⟹ -y ≤ -z"
  by (metis greatest_lower_bound inf_closed inf_less_eq_cases)

lemma inf_less_eq_cases_3:
  "-y ⊓ -x ≤ -z ⊓ -x ⟹ -y ⊓ --x ≤ -z ⊓ --x ⟹ -y ≤ -z"
  by (simp add: inf_commutative inf_less_eq_cases_2)

lemma inf_eq_cases:
  "-x ⊓ -y = -x ⊓ -z ⟹ --x ⊓ -y = --x ⊓ -z ⟹ -y = -z"
  by (metis inf_commutative sup_cases)

lemma inf_eq_cases_2:
  "-y ⊓ -x = -z ⊓ -x ⟹ -y ⊓ --x = -z ⊓ --x ⟹ -y = -z"
  using inf_commutative inf_eq_cases by auto

lemma wnf_lemma_1:
  "((-x ⊔ -y) ⊓ (--x ⊔ -z)) ⊔ -x = -x ⊔ -y"
proof -
  have "∀u v w. (-u ⊓ (-v ⊔ --w)) ⊔ -w = -u ⊔ -w"
    by (metis inf_right_zero sub_associative sub_sup_closed sup_complement sup_idempotent sup_right_dist_inf)
  thus ?thesis
    by (metis (no_types) sub_associative sub_commutative sub_sup_closed sup_idempotent)
qed

lemma wnf_lemma_2:
  "((-x ⊔ -y) ⊓ (-z ⊔ --y)) ⊔ -y = -x ⊔ -y"
  using sub_commutative wnf_lemma_1 by fastforce

lemma wnf_lemma_3:
  "((-x ⊔ -z) ⊓ (--x ⊔ -y)) ⊔ --x = --x ⊔ -y"
  by (metis case_duality case_duality_2 double_negation sub_commutative wnf_lemma_2)

lemma wnf_lemma_4:
  "((-z ⊔ -y) ⊓ (-x ⊔ --y)) ⊔ --y = -x ⊔ --y"
  using sub_commutative wnf_lemma_3 by auto

end

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': "∃z . -x ⊔ -y = -z"
begin

subclass subset_boolean_algebra
proof
  show "⋀x y z. - x ⊔ (- y ⊔ - z) = - x ⊔ - y ⊔ - z"
    by (simp add: sub_associative')
  show "⋀x y. - x ⊔ - y = - y ⊔ - x"
    by (simp add: sub_commutative')
  show "⋀x y. - x = - (- - x ⊔ - y) ⊔ - (- - x ⊔ - - y)"
    by (simp add: sub_complement')
  show "⋀x y. - x ⊔ - y = - - (- x ⊔ - y)"
  proof -
    fix x y
    have "∀x y. -y ⊔ (-(--y ⊔ -x) ⊔ -(---x ⊔ -y)) = -y ⊔ --x"
      by (metis (no_types) sub_associative' sub_commutative' sub_complement')
    hence "∀x. ---x = -x"
      by (metis (no_types) sub_commutative' sub_complement')
    thus "-x ⊔ -y = --(-x ⊔ -y)"
      by (metis sub_sup_closed')
  qed
qed

end

text ‹
We introduce a type for the range of complement and show that it is an instance of ‹boolean_algebra›.
›

typedef (overloaded) 'a boolean_subset = "{ x::'a::uminus . ∃y . x = -y }"
  by auto

lemma simp_boolean_subset[simp]:
  "∃y . Rep_boolean_subset x = -y"
  using Rep_boolean_subset by simp

setup_lifting type_definition_boolean_subset

text ‹Theorem 8.1›

instantiation boolean_subset :: (subset_boolean_algebra) huntington
begin

lift_definition sup_boolean_subset :: "'a boolean_subset ⇒ 'a boolean_subset ⇒ 'a boolean_subset" is sup
  using sub_sup_closed by auto

lift_definition uminus_boolean_subset :: "'a boolean_subset ⇒ 'a boolean_subset" is uminus
  by auto

instance
proof
  show "⋀x y z::'a boolean_subset. x ⊔ (y ⊔ z) = x ⊔ y ⊔ z"
    apply transfer
    using sub_associative by blast
  show "⋀x y::'a boolean_subset. x ⊔ y = y ⊔ x"
    apply transfer
    using sub_commutative by blast
  show "⋀x y::'a boolean_subset. x = - (- x ⊔ y) ⊔ - (- x ⊔ - y)"
    apply transfer
    using sub_complement by blast
qed

end

text ‹Theorem 8.2›

instantiation boolean_subset :: (subset_boolean_algebra_extended) huntington_extended
begin

lift_definition inf_boolean_subset :: "'a boolean_subset ⇒ 'a boolean_subset ⇒ 'a boolean_subset" is inf
  using inf_closed by auto

lift_definition minus_boolean_subset :: "'a boolean_subset ⇒ 'a boolean_subset ⇒ 'a boolean_subset" is minus
  using sub_minus_def by auto

lift_definition bot_boolean_subset :: "'a boolean_subset" is bot
  by (metis complement_top)

lift_definition top_boolean_subset :: "'a boolean_subset" is top
  by (metis complement_bot)

lift_definition less_eq_boolean_subset :: "'a boolean_subset ⇒ 'a boolean_subset ⇒ bool" is less_eq .

lift_definition less_boolean_subset :: "'a boolean_subset ⇒ 'a boolean_subset ⇒ bool" is less .

instance
proof
  show 1: "top = (THE x. ∀y::'a boolean_subset. x = y ⊔ - y)"
  proof (rule the_equality[symmetric])
    show "∀y::'a boolean_subset. top = y ⊔ - y"
      apply transfer
      by auto
    show "⋀x::'a boolean_subset. ∀y. x = y ⊔ - y ⟹ x = top"
      apply transfer
      by force
  qed
  have "(bot::'a boolean_subset) = - top"
    apply transfer
    by simp
  thus "bot = - (THE x. ∀y::'a boolean_subset. x = y ⊔ - y)"
    using 1 by simp
  show "⋀x y::'a boolean_subset. x ⊓ y = - (- x ⊔ - y)"
    apply transfer
    using sub_inf_def by blast
  show "⋀x y::'a boolean_subset. x - y = - (- x ⊔ y)"
    apply transfer
    using sub_minus_def by blast
  show "⋀x y::'a boolean_subset. (x ≤ y) = (x ⊔ y = y)"
    apply transfer
    using sub_less_eq_def by blast
  show "⋀x y::'a boolean_subset. (x < y) = (x ⊔ y = y ∧ y ⊔ x ≠ x)"
    apply transfer
    using sub_less_def by blast
qed

end

section ‹Subset Boolean algebras with Additional Structure›

text ‹
We now discuss axioms that make the range of a unary operation a Boolean algebra, but add further properties that are common to the intended models.
In the intended models, the unary operation can be a complement, a pseudocomplement or the antidomain operation.
For simplicity, we mostly call the unary operation `complement'.

We first look at structures based only on join and complement, and then add axioms for the remaining operations of Boolean algebras.
In the intended models, the operation that is meet on the range of the complement can be a meet in the whole algebra or composition.
›

subsection ‹Axioms Derived from the New Axiomatisation›

text ‹
The axioms of the first algebra are based on ‹boolean_algebra_3›.
›

text ‹Definition 9›

class subset_boolean_algebra_1 = sup + uminus +
  assumes sba1_associative: "x ⊔ (y ⊔ z) = (x ⊔ y) ⊔ z"
  assumes sba1_commutative: "x ⊔ y = y ⊔ x"
  assumes sba1_idempotent[simp]: "x ⊔ x = x"
  assumes sba1_double_complement[simp]: "---x = -x"
  assumes sba1_bot_unique: "-(x ⊔ -x) = -(y ⊔ -y)"
  assumes sba1_export: "-x ⊔ -(-x ⊔ y) = -x ⊔ -y"
begin

text ‹Theorem 11.1›

subclass subset_boolean_algebra
proof
  show "⋀x y z. - x ⊔ (- y ⊔ - z) = - x ⊔ - y ⊔ - z"
    by (simp add: sba1_associative)
  show "⋀x y. - x ⊔ - y = - y ⊔ - x"
    by (simp add: sba1_commutative)
  show "⋀x y. - x = - (- - x ⊔ - y) ⊔ - (- - x ⊔ - - y)"
    by (smt sba1_bot_unique sba1_commutative sba1_double_complement sba1_export sba1_idempotent)
  thus "⋀x y. - x ⊔ - y = - - (- x ⊔ - y)"
    by (metis sba1_double_complement sba1_export)
qed

definition "sba1_bot ≡ THE x . ∀z . x = -(z ⊔ -z)"

lemma sba1_bot:
  "sba1_bot = -(z ⊔ -z)"
  using sba1_bot_def sba1_bot_unique by auto

end

text ‹Boolean algebra operations based on join and complement›

text ‹Definition 10›

class subset_extended_1 = sup + inf + minus + uminus + bot + top + ord +
  assumes ba_bot: "bot = (THE x . ∀z . x = -(z ⊔ -z))"
  assumes ba_top: "top = -(THE x . ∀z . x = -(z ⊔ -z))"
  assumes ba_inf: "-x ⊓ -y = -(--x ⊔ --y)"
  assumes ba_minus: "-x - -y = -(--x ⊔ -y)"
  assumes ba_less_eq: "x ≤ y ⟷ x ⊔ y = y"
  assumes ba_less: "x < y ⟷ x ⊔ y = y ∧ ¬ (y ⊔ x = x)"

class subset_extended_2 = subset_extended_1 +
  assumes ba_bot_unique: "-(x ⊔ -x) = -(y ⊔ -y)"
begin

lemma ba_bot_def:
  "bot = -(z ⊔ -z)"
  using ba_bot ba_bot_unique by auto

lemma ba_top_def:
  "top = --(z ⊔ -z)"
  using ba_bot_def ba_top by simp

end

text ‹Subset forms Boolean Algebra, extended by Boolean algebra operations›

class subset_boolean_algebra_1_extended = subset_boolean_algebra_1 + subset_extended_1
begin

subclass subset_extended_2
proof
  show "⋀x y. - (x ⊔ - x) = - (y ⊔ - y)"
    by (simp add: sba1_bot_unique)
qed

subclass semilattice_sup
proof
  show "⋀x y. (x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    by (simp add: ba_less ba_less_eq)
  show "⋀x. x ≤ x"
    by (simp add: ba_less_eq)
  show "⋀x y z. x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
    by (metis sba1_associative ba_less_eq)
  show "⋀x y. x ≤ y ⟹ y ≤ x ⟹ x = y"
    by (simp add: sba1_commutative ba_less_eq)
  show "⋀x y. x ≤ x ⊔ y"
    by (simp add: sba1_associative ba_less_eq)
  thus "⋀y x. y ≤ x ⊔ y"
    by (simp add: sba1_commutative)
  show "⋀y x z. y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x"
    by (metis sba1_associative ba_less_eq)
qed

text ‹Theorem 11.2›

subclass subset_boolean_algebra_extended
proof
  show "top = (THE x. ∀y. x = - y ⊔ - - y)"
    by (smt ba_bot ba_bot_def ba_top sub_sup_closed the_equality)
  thus "bot = - (THE x. ∀y. x = - y ⊔ - - y)"
    using ba_bot_def ba_top_def by force
  show "⋀x y. - x ⊓ - y = - (- - x ⊔ - - y)"
    by (simp add: ba_inf)
  show "⋀x y. - x - - y = - (- - x ⊔ - y)"
    by (simp add: ba_minus)
  show "⋀x y. (- x ≤ - y) = (- x ⊔ - y = - y)"
    using le_iff_sup by auto
  show "⋀x y. (- x < - y) = (- x ⊔ - y = - y ∧ - y ⊔ - x ≠ - x)"
    by (simp add: ba_less)
qed

end

subsection ‹Stronger Assumptions based on Join and Complement›

text ‹
We add further axioms covering properties common to the antidomain and (pseudo)complement instances.
›

text ‹Definition 12›

class subset_boolean_algebra_2 = sup + uminus +
  assumes sba2_associative: "x ⊔ (y ⊔ z) = (x ⊔ y) ⊔ z"
  assumes sba2_commutative: "x ⊔ y = y ⊔ x"
  assumes sba2_idempotent[simp]: "x ⊔ x = x"
  assumes sba2_bot_unit: "x ⊔ -(y ⊔ -y) = x"
  assumes sba2_sub_sup_demorgan: "-(x ⊔ y) = -(--x ⊔ --y)"
  assumes sba2_export: "-x ⊔ -(-x ⊔ y) = -x ⊔ -y"
begin

text ‹Theorem 13.1›

subclass subset_boolean_algebra_1
proof
  show "⋀x y z. x ⊔ (y ⊔ z) = x ⊔ y ⊔ z"
    by (simp add: sba2_associative)
  show "⋀x y. x ⊔ y = y ⊔ x"
    by (simp add: sba2_commutative)
  show "⋀x. x ⊔ x = x"
    by simp
  show "⋀x. - - - x = - x"
    by (metis sba2_idempotent sba2_sub_sup_demorgan)
  show "⋀x y. - (x ⊔ - x) = - (y ⊔ - y)"
    by (metis sba2_bot_unit sba2_commutative)
  show "⋀x y. - x ⊔ - (- x ⊔ y) = - x ⊔ - y"
    by (simp add: sba2_export)
qed

text ‹Theorem 13.2›

lemma double_complement_dist_sup:
  "--(x ⊔ y) = --x ⊔ --y"
  by (metis sba2_commutative sba2_export sba2_idempotent sba2_sub_sup_demorgan)

lemma maddux_3_3[simp]:
  "-(x ⊔ y) ⊔ -(x ⊔ -y) = -x"
  by (metis double_complement_dist_sup sba1_double_complement sba2_commutative sub_complement)

lemma huntington_3_pp[simp]:
  "-(-x ⊔ -y) ⊔ -(-x ⊔ y) = --x"
  using sba2_commutative maddux_3_3 by fastforce

end

class subset_boolean_algebra_2_extended = subset_boolean_algebra_2 + subset_extended_1
begin

subclass subset_boolean_algebra_1_extended ..

subclass bounded_semilattice_sup_bot
proof
  show "⋀x. bot ≤ x"
    using sba2_bot_unit ba_bot_def sup_right_divisibility by auto
qed

text ‹Theorem 13.3›

lemma complement_antitone:
  "x ≤ y ⟹ -y ≤ -x"
  by (metis le_iff_sup maddux_3_3 sba2_export sup_monoid.add_commute)

lemma double_complement_isotone:
  "x ≤ y ⟹ --x ≤ --y"
  by (simp add: complement_antitone)

lemma sup_demorgan:
  "-(x ⊔ y) = -x ⊓ -y"
  using sba2_sub_sup_demorgan ba_inf by auto

end

subsection ‹Axioms for Meet›

text ‹
We add further axioms of ‹inf› covering properties common to the antidomain and pseudocomplement instances.
We omit the left distributivity rule and the right zero rule as they do not hold in some models.
In particular, the operation ‹inf› does not have to be commutative.
›

text ‹Definition 14›

class subset_boolean_algebra_3_extended = subset_boolean_algebra_2_extended +
  assumes sba3_inf_associative: "x ⊓ (y ⊓ z) = (x ⊓ y) ⊓ z"
  assumes sba3_inf_right_dist_sup: "(x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z)"
  assumes sba3_inf_complement_bot: "-x ⊓ x = bot"
  assumes sba3_inf_left_unit[simp]: "top ⊓ x = x"
  assumes sba3_complement_inf_double_complement: "-(x ⊓ --y) = -(x ⊓ y)"
begin

text ‹Theorem 15›

lemma inf_left_zero:
  "bot ⊓ x = bot"
  by (metis inf_right_unit sba3_inf_associative sba3_inf_complement_bot)

lemma inf_double_complement_export:
  "--(--x ⊓ y) = --x ⊓ --y"
  by (metis inf_closed sba3_complement_inf_double_complement)

lemma inf_left_isotone:
  "x ≤ y ⟹ x ⊓ z ≤ y ⊓ z"
  using sba3_inf_right_dist_sup sup_right_divisibility by auto

lemma inf_complement_export:
  "--(-x ⊓ y) = -x ⊓ --y"
  by (metis inf_double_complement_export sba1_double_complement)

lemma double_complement_above:
  "--x ⊓ x = x"
  by (metis sup_monoid.add_0_right complement_bot inf_demorgan sba1_double_complement sba3_inf_complement_bot sba3_inf_right_dist_sup sba3_inf_left_unit)

lemma "x ≤ y ⟹ z ⊓ x ≤ z ⊓ y" nitpick [expect=genuine] oops
lemma "x ⊓ top = x" nitpick [expect=genuine] oops
lemma "x ⊓ y = y ⊓ x" nitpick [expect=genuine] oops

end

subsection ‹Stronger Assumptions for Meet›

text ‹
The following axioms also hold in both models, but follow from the axioms of ‹subset_boolean_algebra_5_operations›.
›

text ‹Definition 16›

class subset_boolean_algebra_4_extended = subset_boolean_algebra_3_extended +
  assumes sba4_inf_right_unit[simp]: "x ⊓ top = x"
  assumes inf_right_isotone: "x ≤ y ⟹ z ⊓ x ≤ z ⊓ y"
begin

lemma "x ⊔ top = top" nitpick [expect=genuine] oops
lemma "x ⊓ bot = bot" nitpick [expect=genuine] oops
lemma "x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)" nitpick [expect=genuine] oops
lemma "(x ⊓ y = bot) = (x ≤ - y)" nitpick [expect=genuine] oops

end

section ‹Boolean Algebras in Stone Algebras›

text ‹
We specialise ‹inf› to meet and complement to pseudocomplement.
This puts Stone algebras into the picture; for these it is well known that regular elements form a Boolean subalgebra \<^cite>‹"Graetzer1971"›.
›

text ‹Definition 17›

class subset_boolean_algebra_5_extended = subset_boolean_algebra_3_extended +
  assumes sba5_inf_commutative: "x ⊓ y = y ⊓ x"
  assumes sba5_inf_absorb: "x ⊓ (x ⊔ y) = x"
begin

subclass distrib_lattice_bot
proof
  show "⋀x y. x ⊓ y ≤ x"
    by (metis sba5_inf_commutative sba3_inf_right_dist_sup sba5_inf_absorb sup_right_divisibility)
  show "⋀x y. x ⊓ y ≤ y"
    by (metis inf_left_isotone sba5_inf_absorb sba5_inf_commutative sup_ge2)
  show "⋀x y z. x ≤ y ⟹ x ≤ z ⟹ x ≤ y ⊓ z"
    by (metis inf_left_isotone sba5_inf_absorb sup.orderE sup_monoid.add_commute)
  show "⋀x y z. x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z) "
    by (metis sba3_inf_right_dist_sup sba5_inf_absorb sba5_inf_commutative sup_assoc)
qed

lemma inf_demorgan_2:
  "-(x ⊓ y) = -x ⊔ -y"
  using sba3_complement_inf_double_complement sba5_inf_commutative sub_sup_closed sub_sup_demorgan by auto

lemma inf_export:
  "x ⊓ -(x ⊓ y) = x ⊓ -y"
  using inf_demorgan_2 sba3_inf_complement_bot sba3_inf_right_dist_sup sba5_inf_commutative by auto

lemma complement_inf[simp]:
  "x ⊓ -x = bot"
  using sba3_inf_complement_bot sba5_inf_commutative by auto

text ‹Theorem 18.2›

subclass stone_algebra
proof
  show "⋀x. x ≤ top"
    by (simp add: inf.absorb_iff2)
  show "⋀x y. (x ⊓ y = bot) = (x ≤ - y)"
    by (metis (full_types) complement_bot complement_inf inf.cobounded1 inf.order_iff inf_export sba3_complement_inf_double_complement sba3_inf_left_unit)
  show "⋀x. - x ⊔ - - x = top"
    by simp
qed

text ‹Theorem 18.1›

subclass subset_boolean_algebra_4_extended
proof
  show "⋀x. x ⊓ top = x"
    by simp
  show "⋀x y z. x ≤ y ⟹ z ⊓ x ≤ z ⊓ y"
    using inf.sup_right_isotone by blast
qed

end

context stone_algebra_extended
begin

text ‹Theorem 18.3›

subclass subset_boolean_algebra_5_extended
proof
  show "⋀x y z. x ⊔ (y ⊔ z) = x ⊔ y ⊔ z"
    using sup_assoc by auto
  show "⋀x y. x ⊔ y = y ⊔ x"
    by (simp add: sup_commute)
  show "⋀x. x ⊔ x = x"
    by simp
  show "⋀x y. x ⊔ - (y ⊔ - y) = x"
    by simp
  show "⋀x y. - (x ⊔ y) = - (- - x ⊔ - - y)"
    by auto
  show "⋀x y. - x ⊔ - (- x ⊔ y) = - x ⊔ - y"
    by (metis maddux_3_21_pp p_dist_sup regular_closed_p)
  show "bot = (THE x. ∀z. x = - (z ⊔ - z))"
    by simp
  thus "top = - (THE x. ∀z. x = - (z ⊔ - z))"
    using p_bot by blast
  show "⋀x y. - x ⊓ - y = - (- - x ⊔ - - y)"
    by simp
  show "⋀x y. - x - - y = - (- - x ⊔ - y)"
    by auto
  show "⋀x y. (x ≤ y) = (x ⊔ y = y)"
    by (simp add: le_iff_sup)
  thus "⋀x y. (x < y) = (x ⊔ y = y ∧ y ⊔ x ≠ x)"
    by (simp add: less_le_not_le)
  show "⋀x y z. x ⊓ (y ⊓ z) = x ⊓ y ⊓ z"
    by (simp add: inf.sup_monoid.add_assoc)
  show "⋀x y z. (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z"
    by (simp add: inf_sup_distrib2)
  show "⋀x. - x ⊓ x = bot"
    by simp
  show "⋀x. top ⊓ x = x"
    by simp
  show "⋀x y. - (x ⊓ - - y) = - (x ⊓ y)"
    by simp
  show "⋀x y. x ⊓ y = y ⊓ x"
    by (simp add: inf_commute)
  show "⋀x y. x ⊓ (x ⊔ y) = x"
    by simp
qed

end

section ‹Domain Semirings›

text ‹
The following development of tests in IL-semirings, prepredomain semirings, predomain semirings and domain semirings is mostly based on \<^cite>‹"MoellerDesharnais2019"›; see also \<^cite>‹"DesharnaisMoeller2014"›.
See \<^cite>‹"DesharnaisMoellerStruth2006b"› for domain axioms in idempotent semirings.
See \<^cite>‹"DesharnaisJipsenStruth2009" and "JacksonStokes2004"› for domain axioms in semigroups and monoids.
Some variants have been implemented in \<^cite>‹"GomesGuttmannHoefnerStruthWeber2016"›.
›

subsection ‹Idempotent Left Semirings›

text ‹Definition 19›

class il_semiring = sup + inf + bot + top + ord +
  assumes il_associative: "x ⊔ (y ⊔ z) = (x ⊔ y) ⊔ z"
  assumes il_commutative: "x ⊔ y = y ⊔ x"
  assumes il_idempotent[simp]: "x ⊔ x = x"
  assumes il_bot_unit: "x ⊔ bot = x"
  assumes il_inf_associative: "x ⊓ (y ⊓ z) = (x ⊓ y) ⊓ z"
  assumes il_inf_right_dist_sup: "(x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z)"
  assumes il_inf_left_unit[simp]: "top ⊓ x = x"
  assumes il_inf_right_unit[simp]: "x ⊓ top = x"
  assumes il_sub_inf_left_zero[simp]: "bot ⊓ x = bot"
  assumes il_sub_inf_right_isotone: "x ≤ y ⟹ z ⊓ x ≤ z ⊓ y"
  assumes il_less_eq: "x ≤ y ⟷ x ⊔ y = y"
  assumes il_less_def: "x < y ⟷ x ≤ y ∧ ¬(y ≤ x)"
begin

lemma il_unit_bot: "bot ⊔ x = x"
  using il_bot_unit il_commutative by fastforce

subclass order
proof
  show "⋀x y. (x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    by (simp add: il_less_def)
  show "⋀x. x ≤ x"
    by (simp add: il_less_eq)
  show "⋀x y z. x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
    by (metis il_associative il_less_eq)
  show "⋀x y. x ≤ y ⟹ y ≤ x ⟹ x = y"
    by (simp add: il_commutative il_less_eq)
qed

lemma il_sub_inf_right_isotone_var:
  "(x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z)"
  by (smt il_associative il_commutative il_idempotent il_less_eq il_sub_inf_right_isotone)

lemma il_sub_inf_left_isotone:
  "x ≤ y ⟹ x ⊓ z ≤ y ⊓ z"
  by (metis il_inf_right_dist_sup il_less_eq)

lemma il_sub_inf_left_isotone_var:
  "(y ⊓ x) ⊔ (z ⊓ x) ≤ (y ⊔ z) ⊓ x"
  by (simp add: il_inf_right_dist_sup)

lemma sup_left_isotone:
  "x ≤ y ⟹ x ⊔ z ≤ y ⊔ z"
  by (smt il_associative il_commutative il_idempotent il_less_eq)

lemma sup_right_isotone:
  "x ≤ y ⟹ z ⊔ x ≤ z ⊔ y"
  by (simp add: il_commutative sup_left_isotone)

lemma bot_least:
  "bot ≤ x"
  by (simp add: il_less_eq il_unit_bot)

lemma less_eq_bot:
  "x ≤ bot ⟷ x = bot"
  by (simp add: il_bot_unit il_less_eq)

abbreviation are_complementary :: "'a ⇒ 'a ⇒ bool"
  where "are_complementary x y ≡ x ⊔ y = top ∧ x ⊓ y = bot ∧ y ⊓ x = bot"

abbreviation test :: "'a ⇒ bool"
  where "test x ≡ ∃y . are_complementary x y"

definition tests :: "'a set"
  where "tests = { x . test x }"

lemma bot_test:
  "test bot"
  by (simp add: il_unit_bot)

lemma top_test:
  "test top"
  by (simp add: il_bot_unit)

lemma test_sub_identity:
  "test x ⟹ x ≤ top"
  using il_associative il_less_eq by auto

lemma neg_unique:
  "are_complementary x y ⟹ are_complementary x z ⟹ y = z"
  by (metis order.antisym il_inf_left_unit il_inf_right_dist_sup il_inf_right_unit il_sub_inf_right_isotone_var)

definition neg :: "'a ⇒ 'a" (‹!›)
  where "!x ≡ THE y . are_complementary x y"

lemma neg_char:
  assumes "test x"
    shows "are_complementary x (!x)"
proof (unfold neg_def)
  from assms obtain y where 1: "are_complementary x y"
    by auto
  show "are_complementary x (THE y. are_complementary x y)"
  proof (rule theI)
    show "are_complementary x y"
      using 1 by simp
    show "⋀z. are_complementary x z ⟹ z = y"
      using 1 neg_unique by blast
  qed
qed

lemma are_complementary_symmetric:
  "are_complementary x y ⟷ are_complementary y x"
  using il_commutative by auto

lemma neg_test:
  "test x ⟹ test (!x)"
  using are_complementary_symmetric neg_char by blast

lemma are_complementary_test:
  "test x ⟹ are_complementary x y ⟹ test y"
  using il_commutative by auto

lemma neg_involutive:
  "test x ⟹ !(!x) = x"
  using are_complementary_symmetric neg_char neg_unique by blast

lemma test_inf_left_below:
  "test x ⟹ x ⊓ y ≤ y"
  by (metis il_associative il_idempotent il_inf_left_unit il_inf_right_dist_sup il_less_eq)

lemma test_inf_right_below:
  "test x ⟹ y ⊓ x ≤ y"
  by (metis il_inf_right_unit il_sub_inf_right_isotone test_sub_identity)

lemma neg_bot:
  "!bot = top"
  using il_unit_bot neg_char by fastforce

lemma neg_top:
  "!top = bot"
  using bot_test neg_bot neg_involutive by fastforce

lemma test_inf_idempotent:
  "test x ⟹ x ⊓ x = x"
  by (metis il_bot_unit il_inf_left_unit il_inf_right_dist_sup)

lemma test_inf_semicommutative:
  assumes "test x"
      and "test y"
  shows "x ⊓ y ≤ y ⊓ x"
proof -
  have "x ⊓ y = (y ⊓ x ⊓ y) ⊔ (!y ⊓ x ⊓ y)"
    by (metis assms(2) il_inf_left_unit il_inf_right_dist_sup neg_char)
  also have "... ≤ (y ⊓ x ⊓ y) ⊔ (!y ⊓ y)"
  proof -
    obtain z where "are_complementary y z"
      using assms(2) by blast
    hence "y ⊓ (x ⊓ y) ⊔ !y ⊓ (x ⊓ y) ≤ y ⊓ (x ⊓ y)"
      by (metis assms(1) calculation il_sub_inf_left_isotone il_bot_unit il_idempotent il_inf_associative il_less_eq neg_char test_inf_right_below)
    thus ?thesis
      by (simp add: il_associative il_inf_associative il_less_eq)
  qed
  also have "... ≤ (y ⊓ x) ⊔ (!y ⊓ y)"
    by (metis assms(2) il_bot_unit il_inf_right_unit il_sub_inf_right_isotone neg_char test_sub_identity)
  also have "... = y ⊓ x"
    by (simp add: assms(2) il_bot_unit neg_char)
  finally show ?thesis
    .
qed

lemma test_inf_commutative:
  "test x ⟹ test y ⟹ x ⊓ y = y ⊓ x"
  by (simp add: order.antisym test_inf_semicommutative)

lemma test_inf_bot:
  "test x ⟹ x ⊓ bot = bot"
  using il_inf_associative test_inf_idempotent by fastforce

lemma test_absorb_1:
  "test x ⟹ test y ⟹ x ⊔ (x ⊓ y) = x"
  using il_commutative il_less_eq test_inf_right_below by auto

lemma test_absorb_2:
  "test x ⟹ test y ⟹ x ⊔ (y ⊓ x) = x"
  by (metis test_absorb_1 test_inf_commutative)

lemma test_absorb_3:
  "test x ⟹ test y ⟹ x ⊓ (x ⊔ y) = x"
  apply (rule order.antisym)
  apply (metis il_associative il_inf_right_unit il_less_eq il_sub_inf_right_isotone test_sub_identity)
  by (metis il_sub_inf_right_isotone_var test_absorb_1 test_inf_idempotent)

lemma test_absorb_4:
  "test x ⟹ test y ⟹ (x ⊔ y) ⊓ x = x"
  by (smt il_inf_right_dist_sup test_inf_idempotent il_commutative il_less_eq test_inf_left_below)

lemma test_import_1:
  assumes "test x"
      and "test y"
    shows "x ⊔ (!x ⊓ y) = x ⊔ y"
proof -
  have "x ⊔ (!x ⊓ y) = x ⊔ ((y ⊔ !y) ⊓ x) ⊔ (!x ⊓ y)"
    by (simp add: assms(2) neg_char)
  also have "... = x ⊔ (!y ⊓ x) ⊔ (x ⊓ y) ⊔ (!x ⊓ y)"
    by (smt assms il_associative il_commutative il_inf_right_dist_sup test_inf_commutative)
  also have "... = x ⊔ ((x ⊔ !x) ⊓ y)"
    by (smt calculation il_associative il_commutative il_idempotent il_inf_right_dist_sup)
  also have "... = x ⊔ y"
    by (simp add: assms(1) neg_char)
  finally show ?thesis
    .
qed

lemma test_import_2:
  assumes "test x"
      and "test y"
    shows "x ⊔ (y ⊓ !x) = x ⊔ y"
proof -
  obtain z where 1: "are_complementary y z"
    using assms(2) by blast
  obtain w where 2: "are_complementary x w"
    using assms(1) by auto
  hence "x ⊓ !x = bot"
    using neg_char by blast
  hence "!x ⊓ y = y ⊓ !x"
    using 1 2 by (metis il_commutative neg_char test_inf_commutative)
  thus ?thesis
    using 1 2 by (metis test_import_1)
qed

lemma test_import_3:
  assumes "test x"
    shows "(!x ⊔ y) ⊓ x = y ⊓ x"
  by (simp add: assms(1) il_inf_right_dist_sup il_unit_bot neg_char)

lemma test_import_4:
  assumes "test x"
      and "test y"
    shows "(!x ⊔ y) ⊓ x = x ⊓ y"
  by (metis assms test_import_3 test_inf_commutative)

lemma test_inf:
  "test x ⟹ test y ⟹ test z ⟹ z ≤ x ⊓ y ⟷ z ≤ x ∧ z ≤ y"
  apply (rule iffI)
  using dual_order.trans test_inf_left_below test_inf_right_below apply blast
  by (smt il_less_eq il_sub_inf_right_isotone test_absorb_4)

lemma test_shunting:
  assumes "test x"
      and "test y"
    shows "x ⊓ y ≤ z ⟷ x ≤ !y ⊔ z"
proof
  assume 1: "x ⊓ y ≤ z"
  have "x = (!y ⊓ x) ⊔ (y ⊓ x)"
    by (metis assms(2) il_commutative il_inf_left_unit il_inf_right_dist_sup neg_char)
  also have "... ≤ !y ⊔ (y ⊓ x)"
    by (simp add: assms(1) sup_left_isotone test_inf_right_below)
  also have "... ≤ !y ⊔ z"
    using 1 by (simp add: assms sup_right_isotone test_inf_commutative)
  finally show "x ≤ !y ⊔ z"
    .
next
  assume "x ≤ !y ⊔ z"
  hence "x ⊓ y ≤ (!y ⊔ z) ⊓ y"
    using il_sub_inf_left_isotone by blast
  also have "... = z ⊓ y"
    by (simp add: assms(2) test_import_3)
  also have "... ≤ z"
    by (simp add: assms(2) test_inf_right_below)
  finally show "x ⊓ y ≤ z"
    .
qed

lemma test_shunting_bot:
  assumes "test x"
      and "test y"
    shows "x ≤ y ⟷ x ⊓ !y ≤ bot"
  by (simp add: assms il_bot_unit neg_involutive neg_test test_shunting)

lemma test_shunting_bot_eq:
  assumes "test x"
      and "test y"
    shows "x ≤ y ⟷ x ⊓ !y = bot"
  by (simp add: assms test_shunting_bot less_eq_bot)

lemma neg_antitone:
  assumes "test x"
      and "test y"
      and "x ≤ y"
    shows "!y ≤ !x"
proof -
  have 1: "x ⊓ !y = bot"
    using assms test_shunting_bot_eq by blast
  have 2: "x ⊔ !x = top"
    by (simp add: assms(1) neg_char)
  have "are_complementary y (!y)"
    by (simp add: assms(2) neg_char)
  thus ?thesis
    using 1 2 by (metis il_unit_bot il_commutative il_inf_left_unit il_inf_right_dist_sup il_inf_right_unit il_sub_inf_right_isotone test_sub_identity)
qed

lemma test_sup_neg_1:
  assumes "test x"
      and "test y"
    shows "(x ⊔ y) ⊔ (!x ⊓ !y) = top"
proof -
  have "x ⊔ !x = top"
    by (simp add: assms(1) neg_char)
  hence "x ⊔ (y ⊔ !x) = top"
    by (metis assms(2) il_associative il_commutative il_idempotent)
  hence "x ⊔ (y ⊔ !x ⊓ !y) = top"
    by (simp add: assms neg_test test_import_2)
  thus ?thesis
    by (simp add: il_associative)
qed

lemma test_sup_neg_2:
  assumes "test x"
      and "test y"
    shows "(x ⊔ y) ⊓ (!x ⊓ !y) = bot"
proof -
  have 1: "are_complementary y (!y)"
    by (simp add: assms(2) neg_char)
  obtain z where 2: "are_complementary x z"
    using assms(1) by auto
  hence "!x = z"
    using neg_char neg_unique by blast
  thus ?thesis
    using 1 2 by (metis are_complementary_symmetric il_inf_associative neg_involutive test_import_3 test_inf_bot test_inf_commutative)
qed

lemma de_morgan_1:
  assumes "test x"
      and "test y"
      and "test (x ⊓ y)"
    shows "!(x ⊓ y) = !x ⊔ !y"
proof (rule order.antisym)
  have 1: "test (!(x ⊓ y))"
    by (simp add: assms neg_test)
  have "x ≤ (x ⊓ y) ⊔ !y"
    by (metis (full_types) assms il_commutative neg_char test_shunting test_shunting_bot_eq)
  hence "x ⊓ !(x ⊓ y) ≤ !y"
    using 1 by (simp add: assms(1,3) neg_involutive test_shunting)
  hence "!(x ⊓ y) ⊓ x ≤ !y"
    using 1 by (metis assms(1) test_inf_commutative)
  thus "!(x ⊓ y) ≤ !x ⊔ !y"
    using 1 assms(1) test_shunting by blast
  have 2: "!x ≤ !(x ⊓ y)"
    by (simp add: assms neg_antitone test_inf_right_below)
  have "!y ≤ !(x ⊓ y)"
    by (simp add: assms neg_antitone test_inf_left_below)
  thus "!x ⊔ !y ≤ !(x ⊓ y)"
    using 2 by (metis il_associative il_less_eq)
qed

lemma de_morgan_2:
  assumes "test x"
      and "test y"
      and "test (x ⊔ y)"
    shows "!(x ⊔ y) = !x ⊓ !y"
proof (rule order.antisym)
  have 1: "!(x ⊔ y) ≤ !x"
    by (metis assms il_inf_left_unit il_sub_inf_left_isotone neg_antitone test_absorb_3 test_sub_identity)
  have "!(x ⊔ y) ≤ !y"
    by (metis assms il_commutative il_inf_left_unit il_sub_inf_left_isotone neg_antitone test_absorb_3 test_sub_identity)
  thus "!(x ⊔ y) ≤ !x ⊓ !y"
    using 1 by (simp add: assms neg_test test_inf)
  have "top ≤ x ⊔ y ⊔ !(x ⊔ y)"
    by (simp add: assms(3) neg_char)
  hence "top ⊓ !x ≤ y ⊔ !(x ⊔ y)"
    by (smt assms(1) assms(3) il_commutative il_inf_right_dist_sup il_inf_right_unit il_sub_inf_right_isotone il_unit_bot neg_char test_sub_identity)
  thus "!x ⊓ !y ≤ !(x ⊔ y)"
    by (simp add: assms(1) assms(2) neg_involutive neg_test test_shunting)
qed

lemma test_inf_closed_sup_complement:
  assumes "test x"
      and "test y"
      and "∀u v . test u ∧ test v ⟶ test (u ⊓ v)"
    shows "!x ⊓ !y ⊓ (x ⊔ y) = bot"
proof -
  have 1: "!(!x ⊓ !y) = x ⊔ y"
    by (simp add: assms de_morgan_1 neg_involutive neg_test)
  have "test (!(!x ⊓ !y))"
    by (metis assms neg_test)
  thus ?thesis
    using 1 by (metis assms(1,2) de_morgan_2 neg_char)
qed

lemma test_sup_complement_sup_closed:
  assumes "test x"
      and "test y"
      and "∀u v . test u ∧ test v ⟶ !u ⊓ !v ⊓ (u ⊔ v) = bot"
    shows "test (x ⊔ y)"
  by (meson assms test_sup_neg_1 test_sup_neg_2)

lemma test_inf_closed_sup_closed:
  assumes "test x"
      and "test y"
      and "∀u v . test u ∧ test v ⟶ test (u ⊓ v)"
    shows "test (x ⊔ y)"
  using assms test_inf_closed_sup_complement test_sup_complement_sup_closed by simp

end

subsection ‹Prepredomain Semirings›

class dom =
  fixes d :: "'a ⇒ 'a"

class ppd_semiring = il_semiring + dom +
  assumes d_closed: "test (d x)"
  assumes d1: "x ≤ d x ⊓ x"
begin

lemma d_sub_identity:
  "d x ≤ top"
  using d_closed test_sub_identity by blast

lemma d1_eq:
  "x = d x ⊓ x"
proof -
  have "x = (d x ⊔ top) ⊓ x"
    using d_sub_identity il_less_eq by auto
  thus ?thesis
    using d1 il_commutative il_inf_right_dist_sup il_less_eq by force
qed

lemma d_increasing_sub_identity:
  "x ≤ top ⟹ x ≤ d x"
  by (metis d1_eq il_inf_right_unit il_sub_inf_right_isotone)

lemma d_top:
  "d top = top"
  by (simp add: d_increasing_sub_identity d_sub_identity dual_order.antisym)

lemma d_bot_only:
  "d x = bot ⟹ x = bot"
  by (metis d1_eq il_sub_inf_left_zero)

lemma d_strict: "d bot ≤ bot" nitpick [expect=genuine] oops
lemma d_isotone_var: "d x ≤ d (x ⊔ y)" nitpick [expect=genuine] oops
lemma d_fully_strict: "d x = bot ⟷ x = bot" nitpick [expect=genuine] oops
lemma test_d_fixpoint: "test x ⟹ d x = x" nitpick [expect=genuine] oops

end

subsection ‹Predomain Semirings›

class pd_semiring = ppd_semiring +
  assumes d2: "test p ⟹ d (p ⊓ x) ≤ p"
begin

lemma d_strict:
  "d bot ≤ bot"
  using bot_test d2 by fastforce

lemma d_strict_eq:
  "d bot = bot"
  using d_strict il_bot_unit il_less_eq by auto

lemma test_d_fixpoint:
  "test x ⟹ d x = x"
  by (metis order.antisym d1_eq d2 test_inf_idempotent test_inf_right_below)

lemma d_surjective:
  "test x ⟹ ∃y . d y = x"
  using test_d_fixpoint by blast

lemma test_d_fixpoint_iff:
  "test x ⟷ d x = x"
  by (metis d_closed test_d_fixpoint)

lemma d_surjective_iff:
  "test x ⟷ (∃y . d y = x)"
  using d_surjective d_closed by blast

lemma tests_d_range:
  "tests = range d"
  using tests_def image_def d_surjective_iff by auto

lemma llp:
  assumes "test y"
    shows "d x ≤ y ⟷ x ≤ y ⊓ x"
  by (metis assms d1_eq d2 order.eq_iff il_sub_inf_left_isotone test_inf_left_below)

lemma gla:
  assumes "test y"
    shows "y ≤ !(d x) ⟷ y ⊓ x ≤ bot"
proof -
  obtain ad where 1: "∀x. are_complementary (d x) (ad x)"
    using d_closed by moura
  hence 2: "∀x y. d (d y ⊓ x) ≤ d y"
    using d2 by blast
  have 3: "∀x. ad x ⊓ x = bot"
    using 1 by (metis d1_eq il_inf_associative il_sub_inf_left_zero)
  have 4: "∀x y. d y ⊓ x ⊔ ad y ⊓ x = top ⊓ x"
    using 1 by (metis il_inf_right_dist_sup)
  have 5: "∀x y z. z ⊓ y ≤ x ⊓ y ∨ (z ⊔ x) ⊓ y ≠ x ⊓ y"
    by (simp add: il_inf_right_dist_sup il_less_eq)
  have 6: "∀x. !(d x) = ad x"
    using 1 neg_char neg_unique by blast
  have 7: "∀x. top ⊓ x = x"
    by auto
  hence "∀x. y ⊓ x ⊔ !y ⊓ x = x"
    by (metis assms il_inf_right_dist_sup neg_char)
  thus ?thesis
    using 1 2 3 4 5 6 7 by (metis assms d1_eq il_commutative il_less_eq test_d_fixpoint)
qed

lemma gla_var:
  "test y ⟹ y ⊓ d x ≤ bot ⟷ y ⊓ x ≤ bot"
  using gla d_closed il_bot_unit test_shunting by auto

lemma llp_var:
  assumes "test y"
    shows "y ≤ !(d x) ⟷ x ≤ !y ⊓ x"
  apply (rule iffI)
  apply (metis (no_types, opaque_lifting) assms gla Least_equality il_inf_left_unit il_inf_right_dist_sup il_less_eq il_unit_bot order.refl neg_char)
  by (metis assms gla gla_var llp il_commutative il_sub_inf_right_isotone neg_char)

lemma d_idempotent:
  "d (d x) = d x"
  using d_closed test_d_fixpoint_iff by auto

lemma d_neg:
  "test x ⟹ d (!x) = !x"
  using il_commutative neg_char test_d_fixpoint_iff by fastforce

lemma d_fully_strict:
  "d x = bot ⟷ x = bot"
  using d_strict_eq d_bot_only by blast

lemma d_ad_comp:
  "!(d x) ⊓ x = bot"
proof -
  have "∀x. !(d x) ⊓ d x = bot"
    by (simp add: d_closed neg_char)
  thus ?thesis
    by (metis d1_eq il_inf_associative il_sub_inf_left_zero)
qed

lemma d_isotone:
  assumes "x ≤ y"
    shows "d x ≤ d y"
proof -
  obtain ad where 1: "∀x. are_complementary (d x) (ad x)"
    using d_closed by moura
  hence "ad y ⊓ x ≤ bot"
    by (metis assms d1_eq il_inf_associative il_sub_inf_left_zero il_sub_inf_right_isotone)
  thus ?thesis
    using 1 by (metis d2 il_bot_unit il_inf_left_unit il_inf_right_dist_sup il_less_eq)
qed

lemma d_isotone_var:
  "d x ≤ d (x ⊔ y)"
  using d_isotone il_associative il_less_eq by auto

lemma d3_conv:
  "d (x ⊓ y) ≤ d (x ⊓ d y)"
  by (metis (mono_tags, opaque_lifting) d1_eq d2 d_closed il_inf_associative)

lemma d_test_inf_idempotent:
  "d x ⊓ d x = d x"
  by (metis d_idempotent d1_eq)

lemma d_test_inf_closed:
  assumes "test x"
      and "test y"
    shows "d (x ⊓ y) = x ⊓ y"
proof (rule order.antisym)
  have "d (x ⊓ y) = d (x ⊓ y) ⊓ d (x ⊓ y)"
    by (simp add: d_test_inf_idempotent)
  also have "... ≤ x ⊓ d (x ⊓ y)"
    by (simp add: assms(1) d2 il_sub_inf_left_isotone)
  also have "... ≤ x ⊓ y"
    by (metis assms d_isotone il_sub_inf_right_isotone test_inf_left_below test_d_fixpoint)
  finally show "d (x ⊓ y) ≤ x ⊓ y"
    .
  show "x ⊓ y ≤ d (x ⊓ y)"
    using assms d_increasing_sub_identity dual_order.trans test_inf_left_below test_sub_identity by blast
qed

lemma test_inf_closed:
  "test x ⟹ test y ⟹ test (x ⊓ y)"
  using d_test_inf_closed test_d_fixpoint_iff by simp

lemma test_sup_closed:
  "test x ⟹ test y ⟹ test (x ⊔ y)"
  using test_inf_closed test_inf_closed_sup_closed by simp

lemma d_export:
  assumes "test x"
    shows "d (x ⊓ y) = x ⊓ d y"
proof (rule order.antisym)
  have 1: "d (x ⊓ y) ≤ x"
    by (simp add: assms d2)
  have "d (x ⊓ y) ≤ d y"
    by (metis assms d_isotone_var il_inf_left_unit il_inf_right_dist_sup)
  thus "d (x ⊓ y) ≤ x ⊓ d y"
    using 1 by (metis assms d_idempotent llp dual_order.trans il_sub_inf_right_isotone)
  have "y = (!x ⊓ y) ⊔ (x ⊓ y)"
    by (metis assms il_commutative il_inf_left_unit il_inf_right_dist_sup neg_char)
  also have "... = (!x ⊓ y) ⊔ (d (x ⊓ y) ⊓ x ⊓ y)"
    by (metis d1_eq il_inf_associative)
  also have "... = (!x ⊓ y) ⊔ (d (x ⊓ y) ⊓ y)"
    using 1 by (smt calculation d1_eq il_associative il_commutative il_inf_associative il_inf_right_dist_sup il_less_eq il_sub_inf_right_isotone_var)
  also have "... = (!x ⊔ d (x ⊓ y)) ⊓ y"
    by (simp add: il_inf_right_dist_sup)
  finally have "y ≤ (!x ⊔ d (x ⊓ y)) ⊓ y"
    by simp
  hence "d y ≤ !x ⊔ d (x ⊓ y)"
    using assms llp test_sup_closed neg_test d_closed by simp
  hence "d y ⊓ x ≤ d (x ⊓ y)"
    by (simp add: assms d_closed test_shunting)
  thus "x ⊓ d y ≤ d (x ⊓ y)"
    by (metis assms d_closed test_inf_commutative)
qed

lemma test_inf_left_dist_sup:
  assumes "test x"
      and "test y"
      and "test z"
    shows "x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)"
proof -
  have "x ⊓ (y ⊔ z) = (y ⊔ z) ⊓ x"
    using assms test_sup_closed test_inf_commutative by smt
  also have "... = (y ⊓ x) ⊔ (z ⊓ x)"
    using il_inf_right_dist_sup by simp
  also have "... = (x ⊓ y) ⊔ (x ⊓ z)"
    using assms test_sup_closed test_inf_commutative by smt
  finally show ?thesis
    .
qed

lemma "!x ⊔ !y = !(!(!x ⊔ !y))" nitpick [expect=genuine] oops
lemma "d x = !(!x)" nitpick [expect=genuine] oops

sublocale subset_boolean_algebra where uminus = "λ x . !(d x)"
proof
  show "⋀x y z. !(d x) ⊔ (!(d y) ⊔ !(d z)) = !(d x) ⊔ !(d y) ⊔ !(d z)"
    using il_associative by blast
  show "⋀x y. !(d x) ⊔ !(d y) = !(d y) ⊔ !(d x)"
    by (simp add: il_commutative)
  show "⋀x y. !(d x) ⊔ !(d y) = !(d (!(d (!(d x) ⊔ !(d y)))))"
  proof -
    fix x y
    have "test (!(d x)) ∧ test (!(d y))"
      by (simp add: d_closed neg_test)
    hence "test (!(d x) ⊔ !(d y))"
      by (simp add: test_sup_closed)
    thus "!(d x) ⊔ !(d y) = !(d (!(d (!(d x) ⊔ !(d y)))))"
      by (simp add: d_neg neg_involutive test_d_fixpoint)
  qed
  show "⋀x y. !(d x) = !(d (!(d (!(d x))) ⊔ !(d y))) ⊔ !(d (!(d (!(d x))) ⊔ !(d (!(d y)))))"
  proof -
    fix x y
    have "!(d (!(d (!(d x))) ⊔ !(d y))) ⊔ !(d (!(d (!(d x))) ⊔ !(d (!(d y))))) = !(d x ⊔ !(d y)) ⊔ !(d x ⊔ d y)"
      using d_closed neg_test test_sup_closed neg_involutive test_d_fixpoint by auto
    also have "... = (!(d x) ⊓ d y) ⊔ (!(d x) ⊓ !(d y))"
      using d_closed neg_test test_sup_closed neg_involutive de_morgan_2 by auto
    also have "... = !(d x) ⊓ (d y ⊔ !(d y))"
      using d_closed neg_test test_inf_left_dist_sup by auto
    also have "... = !(d x) ⊓ top"
      by (simp add: neg_char d_closed)
    finally show "!(d x) = !(d (!(d (!(d x))) ⊔ !(d y))) ⊔ !(d (!(d (!(d x))) ⊔ !(d (!(d y)))))"
      by simp
  qed
qed

lemma d_dist_sup:
  "d (x ⊔ y) = d x ⊔ d y"
proof (rule order.antisym)
  have "x ≤ d x ⊓ x"
    by (simp add: d1)
  also have "... ≤ (d x ⊔ d y) ⊓ (x ⊔ y)"
    using il_associative il_inf_right_dist_sup il_less_eq il_sub_inf_right_isotone by auto
  finally have 1: "x ≤ (d x ⊔ d y) ⊓ (x ⊔ y)"
    .
  have "y ≤ d y ⊓ y"
    by (simp add: d1)
  also have "... ≤ (d y ⊔ d x) ⊓ (y ⊔ x)"
    using il_associative il_idempotent il_inf_right_dist_sup il_less_eq il_sub_inf_right_isotone by simp
  finally have "y ≤ (d x ⊔ d y) ⊓ (x ⊔ y)"
    using il_commutative by auto
  hence "x ⊔ y ≤ (d x ⊔ d y) ⊓ (x ⊔ y)"
    using 1 by (metis il_associative il_less_eq)
  thus "d (x ⊔ y) ≤ d x ⊔ d y"
    using llp test_sup_closed neg_test d_closed by simp
  show "d x ⊔ d y ≤ d (x ⊔ y)"
    using d_isotone_var il_associative il_commutative il_less_eq by fastforce
qed

end

class pd_semiring_extended = pd_semiring + uminus +
  assumes uminus_def: "-x = !(d x)"
begin

subclass subset_boolean_algebra
  by (metis subset_boolean_algebra_axioms uminus_def ext)

end

subsection ‹Domain Semirings›

class d_semiring = pd_semiring +
  assumes d3: "d (x ⊓ d y) ≤ d (x ⊓ y)"
begin

lemma d3_eq: "d (x ⊓ d y) = d (x ⊓ y)"
  by (simp add: order.antisym d3 d3_conv)

end

text ‹
Axioms (d1), (d2) and (d3) are independent in IL-semirings.
›

context il_semiring
begin

context
  fixes d :: "'a ⇒ 'a"
  assumes d_closed: "test (d x)"
begin

context
  assumes d1: "x ≤ d x ⊓ x"
  assumes d2: "test p ⟹ d (p ⊓ x) ≤ p"
begin

lemma d3: "d (x ⊓ d y) ≤ d (x ⊓ y)" nitpick [expect=genuine] oops

end

context
  assumes d1: "x ≤ d x ⊓ x"
  assumes d3: "d (x ⊓ d y) ≤ d (x ⊓ y)"
begin

lemma d2: "test p ⟹ d (p ⊓ x) ≤ p" nitpick [expect=genuine] oops

end

context
  assumes d2: "test p ⟹ d (p ⊓ x) ≤ p"
  assumes d3: "d (x ⊓ d y) ≤ d (x ⊓ y)"
begin

lemma d1: "x ≤ d x ⊓ x" nitpick [expect=genuine] oops

end

end

end

class d_semiring_var = ppd_semiring +
  assumes d3_var: "d (x ⊓ d y) ≤ d (x ⊓ y)"
  assumes d_strict_eq_var: "d bot = bot"
begin

lemma d2_var:
  assumes "test p"
    shows "d (p ⊓ x) ≤ p"
proof -
  have "!p ⊓ p ⊓ x = bot"
    by (simp add: assms neg_char)
  hence "d (!p ⊓ p ⊓ x) = bot"
    by (simp add: d_strict_eq_var)
  hence "d (!p ⊓ d (p ⊓ x)) = bot"
    by (metis d3_var il_inf_associative less_eq_bot)
  hence "!p ⊓ d (p ⊓ x) = bot"
    using d_bot_only by blast
  thus ?thesis
    by (metis (no_types, opaque_lifting) assms d_sub_identity il_bot_unit il_inf_left_unit il_inf_right_dist_sup il_inf_right_unit il_sub_inf_right_isotone neg_char)
qed

subclass d_semiring
proof
  show "⋀p x. test p ⟹ d (p ⊓ x) ≤ p"
    by (simp add: d2_var)
  show "⋀x y. d (x ⊓ d y) ≤ d (x ⊓ y)"
    by (simp add: d3_var)
qed

end

section ‹Antidomain Semirings›

text ‹
We now develop prepreantidomain semirings, preantidomain semirings and antidomain semirings.
See \<^cite>‹"DesharnaisStruth2008b" and "DesharnaisStruth2008a" and "DesharnaisStruth2011"› for related work on internal axioms for antidomain.
›

subsection ‹Prepreantidomain Semirings›

text ‹Definition 20›

class ppa_semiring = il_semiring + uminus +
  assumes a_inf_complement_bot: "-x ⊓ x = bot"
  assumes a_stone[simp]: "-x ⊔ --x = top"
begin

text ‹Theorem 21›

lemma l1:
  "-top = bot"
  by (metis a_inf_complement_bot il_inf_right_unit)

lemma l2:
  "-bot = top"
  by (metis l1 a_stone il_unit_bot)

lemma l3:
  "-x ≤ -y ⟹ -x ⊓ y = bot"
  by (metis a_inf_complement_bot il_bot_unit il_inf_right_dist_sup il_less_eq)

lemma l5:
  "--x ≤ --y ⟹ -y ≤ -x"
  by (metis (mono_tags, opaque_lifting) l3 a_stone bot_least il_bot_unit il_inf_left_unit il_inf_right_dist_sup il_inf_right_unit il_sub_inf_right_isotone sup_right_isotone)

lemma l4:
  "---x = -x"
  by (metis l5 a_inf_complement_bot a_stone order.antisym bot_least il_inf_left_unit il_inf_right_dist_sup il_inf_right_unit il_sub_inf_right_isotone il_unit_bot)

lemma l6:
  "-x ⊓ --x = bot"
  by (metis l3 l5 a_inf_complement_bot a_stone il_inf_left_unit il_inf_right_dist_sup il_inf_right_unit il_less_eq il_sub_inf_right_isotone il_unit_bot)

lemma l7:
  "-x ⊓ -y = -y ⊓ -x"
  using l6 a_inf_complement_bot a_stone test_inf_commutative by blast

lemma l8:
  "x ≤ --x ⊓ x"
  by (metis a_inf_complement_bot a_stone il_idempotent il_inf_left_unit il_inf_right_dist_sup il_less_eq il_unit_bot)

sublocale ppa_ppd: ppd_semiring where d = "λx . --x"
proof
  show "⋀x. test (- - x)"
    using l4 l6 by force
  show "⋀x. x ≤ - - x ⊓ x"
    by (simp add: l8)
qed

(*
The following statements have counterexamples, but they take a while to find.

lemma "- x = - (- - x ⊔ - y) ⊔ - (- - x ⊔ - - y)" nitpick [card=8, expect=genuine] oops
lemma "- x ⊔ - y = - - (- x ⊔ - y)" nitpick [card=8, expect=genuine] oops
*)

end

subsection ‹Preantidomain Semirings›

text ‹Definition 22›

class pa_semiring = ppa_semiring +
  assumes pad2: "--x ≤ -(-x ⊓ y)"
begin

text ‹Theorem 23›

lemma l10:
  "-x ⊓ y = bot ⟹ -x ≤ -y"
  by (metis a_stone il_inf_left_unit il_inf_right_dist_sup il_unit_bot l4 pad2)

lemma l10_iff:
  "-x ⊓ y = bot ⟷ -x ≤ -y"
  using l10 l3 by blast

lemma l13:
  "--(--x ⊓ y) ≤ --x"
  by (metis l4 l5 pad2)

lemma l14:
  "-(x ⊓ --y) ≤ -(x ⊓ y)"
  by (metis il_inf_associative l4 pad2 ppa_ppd.d1_eq)

lemma l9:
  "x ≤ y ⟹ -y ≤ -x"
  by (metis l10 a_inf_complement_bot il_commutative il_less_eq il_sub_inf_right_isotone il_unit_bot)

lemma l11:
  "- x ⊔ - y = - (- - x ⊓ - - y)"
proof -
  have 1: "⋀x y . x ≤ y ⟷ x ⊔ y = y"
    by (simp add: il_less_eq)
  have 4: "⋀x y . ¬(x ≤ y) ∨ x ⊔ y = y"
    using 1 by metis
  have 5: "⋀x y z . (x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z)"
    by (simp add: il_sub_inf_right_isotone_var)
  have 6: "⋀x y . - - x ≤ - (- x ⊓ y)"
    by (simp add: pad2)
  have 7: "⋀x y z . x ⊔ (y ⊔ z) = (x ⊔ y) ⊔ z"
    by (simp add: il_associative)
  have 8: "⋀x y z . (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)"
    using 7 by metis
  have 9: "⋀x y . x ⊔ y = y ⊔ x"
    by (simp add: il_commutative)
  have 10: "⋀x . x ⊔ bot = x"
    by (simp add: il_bot_unit)
  have 11: "⋀x . x ⊔ x = x"
    by simp
  have 12: "⋀x y z . x ⊓ (y ⊓ z) = (x ⊓ y) ⊓ z"
    by (simp add: il_inf_associative)
  have 13: "⋀x y z . (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)"
    using 12 by metis
  have 14: "⋀x . top ⊓ x = x"
    by simp
  have 15: "⋀x . x ⊓ top = x"
    by simp
  have 16: "⋀x y z . (x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z)"
    by (simp add: il_inf_right_dist_sup)
  have 17: "⋀x y z . (x ⊓ y) ⊔ (z ⊓ y) = (x ⊔ z) ⊓ y"
    using 16 by metis
  have 18: "⋀x . bot ⊓ x = bot"
    by simp
  have 19: "⋀x . - x ⊔ - - x = top"
    by simp
  have 20: "⋀x . - x ⊓ x = bot"
    by (simp add: a_inf_complement_bot)
  have 23: "⋀x y z . ((x ⊓ y) ⊔ (x ⊓ z)) ⊔ (x ⊓ (y ⊔ z)) = x ⊓ (y ⊔ z)"
    using 4 5 by metis
  have 24: "⋀x y z . (x ⊓ (y ⊔ z)) ⊔ ((x ⊓ y) ⊔ (x ⊓ z)) = x ⊓ (y ⊔ z)"
    using 9 23 by metis
  have 25: "⋀x y . - - x ⊔ - (- x ⊓ y) = - (- x ⊓ y)"
    using 4 6 by metis
  have 26: "⋀x y z . x ⊔ (y ⊔ z) = y ⊔ (x ⊔ z)"
    using 8 9 by metis
  have 27: "⋀x y z . (x ⊓ y) ⊔ ((x ⊓ z) ⊔ (x ⊓ (y ⊔ z))) = x ⊓ (y ⊔ z)"
    using 9 24 26 by metis
  have 30: "⋀x . bot ⊔ x = x"
    using 9 10 by metis
  have 31: "⋀x y . x ⊔ (x ⊔ y) = x ⊔ y"
    using 8 11 by metis
  have 34: "⋀u x y z . ((x ⊔ y) ⊓ z) ⊔ u = (x ⊓ z) ⊔ ((y ⊓ z) ⊔ u)"
    using 8 17 by metis
  have 35: "⋀u x y z . (x ⊓ (y ⊓ z)) ⊔ (u ⊓ z) = ((x ⊓ y) ⊔ u) ⊓ z"
    using 13 17 by metis
  have 36: "⋀u x y z . (x ⊓ y) ⊔ (z ⊓ (u ⊓ y)) = (x ⊔ (z ⊓ u)) ⊓ y"
    using 13 17 by metis
  have 39: "⋀x y . - x ⊔ (- - x ⊔ y) = top ⊔ y"
    using 8 19 by metis
  have 41: "⋀x y . - x ⊓ (x ⊓ y) = bot"
    using 13 18 20 by metis
  have 42: "- top = bot"
    using 15 20 by metis
  have 43: "⋀x y . (- x ⊔ y) ⊓ x = y ⊓ x"
    using 17 20 30 by metis
  have 44: "⋀x y . (x ⊔ - y) ⊓ y = x ⊓ y"
    using 9 17 20 30 by metis
  have 46: "⋀x . - bot ⊔ - - x = - bot"
    using 9 20 25 by metis
  have 50: "- bot = top"
    using 19 30 42 by metis
  have 51: "⋀x . top ⊔ - - x = top"
    using 46 50 by metis
  have 63: "⋀x y . x ⊔ ((x ⊓ - y) ⊔ (x ⊓ - - y)) = x"
    using 9 15 19 26 27 by metis
  have 66: "⋀x y . (- (x ⊔ y) ⊓ x) ⊔ (- (x ⊔ y) ⊓ y) = bot"
    using 9 20 27 30 by metis
  have 67: "⋀x y z . (x ⊓ - - y) ⊔ (x ⊓ - (- y ⊓ z)) = x ⊓ - (- y ⊓ z)"
    using 11 25 27 by metis
  have 70: "⋀x y . x ⊔ (x ⊓ - - y) = x"
    using 9 15 27 31 51 by metis
  have 82: "⋀x . top ⊔ - x = top"
    using 9 19 31 by metis
  have 89: "⋀x y . x ⊔ (- y ⊓ x) = x"
    using 14 17 82 by metis
  have 102: "⋀x y z . x ⊔ (y ⊔ (x ⊓ - - z)) = y ⊔ x"
    using 26 70 by metis
  have 104: "⋀x y . x ⊔ (x ⊓ - y) = x"
    using 9 63 102 by metis
  have 112: "⋀x y z . (- x ⊓ y) ⊔ ((- - x ⊓ y) ⊔ z) = y ⊔ z"
    using 14 19 34 by metis
  have 117: "⋀x y z . x ⊔ ((x ⊓ - y) ⊔ z) = x ⊔ z"
    using 8 104 by metis
  have 120: "⋀x y z . x ⊔ (y ⊔ (x ⊓ - z)) = y ⊔ x"
    using 26 104 by metis
  have 124: "⋀x . - - x ⊓ x = x"
    using 14 19 43 by metis
  have 128: "⋀x y . - - x ⊓ (x ⊓ y) = x ⊓ y"
    using 13 124 by metis
  have 131: "⋀x . - x ⊔ - - - x = - x"
    using 9 25 124 by metis
  have 133: "⋀x . - - - x = - x"
    using 9 104 124 131 by metis
  have 135: "⋀x y . - x ⊔ - (- - x ⊓ y) = - (- - x ⊓ y)"
    using 25 133 by metis
  have 137: "⋀x y . (- x ⊔ y) ⊓ - - x = y ⊓ - - x"
    using 43 133 by metis
  have 145: "⋀x y z . ((- (x ⊓ y) ⊓ x) ⊔ z) ⊓ y = z ⊓ y"
    using 20 30 35 by metis
  have 183: "⋀x y z . (x ⊔ (- - (y ⊓ z) ⊓ y)) ⊓ z = (x ⊔ y) ⊓ z"
    using 17 36 124 by metis
  have 289: "⋀x y . - x ⊔ - (- x ⊓ y) = top"
    using 25 39 82 by metis
  have 316: "⋀x y . - (- x ⊓ y) ⊓ x = x"
    using 14 43 289 by metis
  have 317: "⋀x y z . - (- x ⊓ y) ⊓ (x ⊓ z) = x ⊓ z"
    using 13 316 by metis
  have 320: "⋀x y . - x ⊔ - - (- x ⊓ y) = - x"
    using 9 25 316 by metis
  have 321: "⋀x y . - - (- x ⊓ y) ⊓ x = bot"
    using 41 316 by metis
  have 374: "⋀x y . - x ⊔ - (x ⊓ y) = - (x ⊓ y)"
    using 25 128 133 by metis
  have 388: "⋀x y . - (x ⊓ y) ⊓ - x = - x"
    using 128 316 by metis
  have 389: "⋀x y . - - (x ⊓ y) ⊓ - x = bot"
    using 128 321 by metis
  have 405: "⋀x y z . - (x ⊓ y) ⊓ (- x ⊓ z) = - x ⊓ z"
    using 13 388 by metis
  have 406: "⋀x y z . - (x ⊓ (y ⊓ z)) ⊓ - (x ⊓ y) = - (x ⊓ y)"
    using 13 388 by metis
  have 420: "⋀x y . - x ⊓ - - (- x ⊓ y) = - - (- x ⊓ y)"
    using 316 388 by metis
  have 422: "⋀x y z . - - (x ⊓ y) ⊓ (- x ⊓ z) = bot"
    using 13 18 389 by metis
  have 758: "⋀x y z . x ⊔ (x ⊓ (- y ⊓ - z)) = x"
    using 13 104 117 by metis
  have 1092: "⋀x y . - (x ⊔ y) ⊓ x = bot"
    using 9 30 31 66 by metis
  have 1130: "⋀x y z . (- (x ⊔ y) ⊔ z) ⊓ x = z ⊓ x"
    using 17 30 1092 by metis
  have 1156: "⋀x y . - - x ⊓ - (- x ⊓ y) = - - x"
    using 67 104 124 133 by metis
  have 2098: "⋀x y . - - (x ⊔ y) ⊓ x = x"
    using 14 19 1130 by metis
  have 2125: "⋀x y . - - (x ⊔ y) ⊓ y = y"
    using 9 2098 by metis
  have 2138: "⋀x y . - x ⊔ - - (x ⊔ y) = top"
    using 9 289 2098 by metis
  have 2139: "⋀x y . - x ⊓ - (x ⊔ y) = - (x ⊔ y)"
    using 316 2098 by metis
  have 2192: "⋀x y . - - x ⊓ (- y ⊓ x) = - y ⊓ x"
    using 89 2125 by metis
  have 2202: "⋀x y . - x ⊔ - - (y ⊔ x) = top"
    using 9 289 2125 by metis
  have 2344: "⋀x y . - (- x ⊓ y) ⊔ - - y = top"
    using 89 2202 by metis
  have 2547: "⋀x y z . - x ⊔ ((- - x ⊓ - y) ⊔ z) = - x ⊔ (- y ⊔ z)"
    using 112 117 by metis
  have 3023: "⋀x y . - x ⊔ - (- y ⊓ - x) = top"
    using 9 133 2344 by metis
  have 3134: "⋀x y . - (- x ⊓ - y) ⊓ y = y"
    using 14 43 3023 by metis
  have 3135: "⋀x y . - x ⊓ (- y ⊓ - x) = - y ⊓ - x"
    using 14 44 3023 by metis
  have 3962: "⋀x y . - - (x ⊔ y) ⊓ - - x = - - x"
    using 14 137 2138 by metis
  have 5496: "⋀x y z . - - (x ⊓ y) ⊓ - (x ⊔ z) = bot"
    using 422 2139 by metis
  have 9414: "⋀x y . - - (- x ⊓ y) ⊓ y = - x ⊓ y"
    using 9 104 183 320 by metis
  have 9520: "⋀x y z . - - (- x ⊓ y) ⊓ - - (x ⊓ z) = bot"
    using 374 5496 by metis
  have 11070: "⋀x y z . - (- - x ⊓ y) ⊔ (- x ⊓ - z) = - (- - x ⊓ y)"
    using 317 758 by metis
  have 12371: "⋀x y . - x ⊓ - (- - x ⊓ y) = - x"
    using 133 1156 by metis
  have 12377: "⋀x y . - x ⊓ - (x ⊓ y) = - x"
    using 128 133 1156 by metis
  have 12384: "⋀x y . - (x ⊔ y) ⊓ - y = - (x ⊔ y)"
    using 133 1156 2125 by metis
  have 12394: "⋀x y . - - (- x ⊓ - y) = - x ⊓ - y"
    using 1156 3134 9414 by metis
  have 12640: "⋀x y . - x ⊓ - (- y ⊓ x) = - x"
    using 89 12384 by metis
  have 24648: "⋀x y . (- x ⊓ - y) ⊔ - (- x ⊓ - y) = top"
    using 19 12394 by metis
  have 28270: "⋀x y z . - - (x ⊓ y) ⊔ - (- x ⊓ z) = - (- x ⊓ z)"
    using 374 405 by metis
  have 28339: "⋀x y . - (- - (x ⊓ y) ⊓ x) = - (x ⊓ y)"
    using 124 406 12371 by metis
  have 28423: "⋀x y . - (- x ⊓ - y) = - (- y ⊓ - x)"
    using 13 3135 12394 28339 by metis
  have 28487: "⋀x y . - x ⊓ - y = - y ⊓ - x"
    using 2098 3962 12394 28423 by metis
  have 52423: "⋀x y . - (- x ⊓ - (- x ⊓ y)) ⊓ y = y"
    using 14 145 24648 28487 by metis
  have 52522: "⋀x y . - x ⊓ - (- x ⊓ y) = - x ⊓ - y"
    using 13 12377 12394 12640 28487 52423 by metis
  have 61103: "⋀x y z . - (- - x ⊓ y) ⊔ z = - x ⊔ (- y ⊔ z)"
    using 112 2547 12371 52522 by metis
  have 61158: "⋀x y . - - (- x ⊓ y) = - x ⊓ - - y"
    using 420 52522 by metis
  have 61231: "⋀x y z . - x ⊓ (- - y ⊓ - (x ⊓ z)) = - x ⊓ - - y"
    using 13 15 50 133 9520 52522 61158 by metis
  have 61313: "⋀x y . - x ⊔ - y = - (- - y ⊓ x)"
    using 120 11070 61103 by metis
  have 61393: "⋀x y . - (- x ⊓ - - y) = - (- x ⊓ y)"
    using 13 28270 61158 61231 61313 by metis
  have 61422: "⋀x y . - (- - x ⊓ y) = - (- - y ⊓ x)"
    using 13 135 2192 61158 61313 by metis
  show ?thesis
    using 61313 61393 61422 by metis
qed

lemma l12:
  "- x ⊓ - y = - (x ⊔ y)"
proof -
  have 1: "⋀x y . x ≤ y ⟷ x ⊔ y = y"
    by (simp add: il_less_eq)
  have 4: "⋀x y . ¬(x ≤ y) ∨ x ⊔ y = y"
    using 1 by metis
  have 5: "⋀x y z . (x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z)"
    by (simp add: il_sub_inf_right_isotone_var)
  have 6: "⋀x y . - - x ≤ - (- x ⊓ y)"
    by (simp add: pad2)
  have 7: "⋀x y z . x ⊔ (y ⊔ z) = (x ⊔ y) ⊔ z"
    by (simp add: il_associative)
  have 8: "⋀x y z . (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)"
    using 7 by metis
  have 9: "⋀x y . x ⊔ y = y ⊔ x"
    by (simp add: il_commutative)
  have 10: "⋀x . x ⊔ bot = x"
    by (simp add: il_bot_unit)
  have 11: "⋀x . x ⊔ x = x"
    by simp
  have 12: "⋀x y z . x ⊓ (y ⊓ z) = (x ⊓ y) ⊓ z"
    by (simp add: il_inf_associative)
  have 13: "⋀x y z . (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)"
    using 12 by metis
  have 14: "⋀x . top ⊓ x = x"
    by simp
  have 15: "⋀x . x ⊓ top = x"
    by simp
  have 16: "⋀x y z . (x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z)"
    by (simp add: il_inf_right_dist_sup)
  have 17: "⋀x y z . (x ⊓ y) ⊔ (z ⊓ y) = (x ⊔ z) ⊓ y"
    using 16 by metis
  have 18: "⋀x . bot ⊓ x = bot"
    by simp
  have 19: "⋀x . - x ⊔ - - x = top"
    by simp
  have 20: "⋀x . - x ⊓ x = bot"
    by (simp add: a_inf_complement_bot)
  have 22: "⋀x y z . ((x ⊓ y) ⊔ (x ⊓ z)) ⊔ (x ⊓ (y ⊔ z)) = x ⊓ (y ⊔ z)"
    using 4 5 by metis
  have 23: "⋀x y z . (x ⊓ (y ⊔ z)) ⊔ ((x ⊓ y) ⊔ (x ⊓ z)) = x ⊓ (y ⊔ z)"
    using 9 22 by metis
  have 24: "⋀x y . - - x ⊔ - (- x ⊓ y) = - (- x ⊓ y)"
    using 4 6 by metis
  have 25: "⋀x y z . x ⊔ (y ⊔ z) = y ⊔ (x ⊔ z)"
    using 8 9 by metis
  have 26: "⋀x y z . (x ⊓ y) ⊔ ((x ⊓ z) ⊔ (x ⊓ (y ⊔ z))) = x ⊓ (y ⊔ z)"
    using 9 23 25 by metis
  have 29: "⋀x . bot ⊔ x = x"
    using 9 10 by metis
  have 30: "⋀x y . x ⊔ (x ⊔ y) = x ⊔ y"
    using 8 11 by metis
  have 32: "⋀x y . x ⊔ (y ⊔ x) = y ⊔ x"
    using 8 9 11 by metis
  have 33: "⋀u x y z . ((x ⊔ y) ⊓ z) ⊔ u = (x ⊓ z) ⊔ ((y ⊓ z) ⊔ u)"
    using 8 17 by metis
  have 34: "⋀u x y z . (x ⊓ (y ⊓ z)) ⊔ (u ⊓ z) = ((x ⊓ y) ⊔ u) ⊓ z"
    using 13 17 by metis
  have 35: "⋀u x y z . (x ⊓ y) ⊔ (z ⊓ (u ⊓ y)) = (x ⊔ (z ⊓ u)) ⊓ y"
    using 13 17 by metis
  have 36: "⋀x y . (top ⊔ x) ⊓ y = y ⊔ (x ⊓ y)"
    using 14 17 by metis
  have 37: "⋀x y . (x ⊔ top) ⊓ y = y ⊔ (x ⊓ y)"
    using 9 14 17 by metis
  have 38: "⋀x y . - x ⊔ (- - x ⊔ y) = top ⊔ y"
    using 8 19 by metis
  have 40: "⋀x y . - x ⊓ (x ⊓ y) = bot"
    using 13 18 20 by metis
  have 41: "- top = bot"
    using 15 20 by metis
  have 42: "⋀x y . (- x ⊔ y) ⊓ x = y ⊓ x"
    using 17 20 29 by metis
  have 43: "⋀x y . (x ⊔ - y) ⊓ y = x ⊓ y"
    using 9 17 20 29 by metis
  have 45: "⋀x . - bot ⊔ - - x = - bot"
    using 9 20 24 by metis
  have 46: "⋀u x y z . (x ⊓ y) ⊔ (z ⊔ (u ⊓ y)) = z ⊔ ((x ⊔ u) ⊓ y)"
    using 17 25 by metis
  have 47: "⋀x y . - x ⊔ (y ⊔ - - x) = y ⊔ top"
    using 19 25 by metis
  have 49: "- bot = top"
    using 19 29 41 by metis
  have 50: "⋀x . top ⊔ - - x = top"
    using 45 49 by metis
  have 54: "⋀u x y z . (x ⊓ y) ⊔ ((x ⊓ z) ⊔ ((x ⊓ (y ⊔ z)) ⊔ u)) = (x ⊓ (y ⊔ z)) ⊔ u"
    using 8 26 by metis
  have 58: "⋀u x y z . (x ⊓ (y ⊓ z)) ⊔ ((x ⊓ (y ⊓ u)) ⊔ (x ⊓ (y ⊓ (z ⊔ u)))) = x ⊓ (y ⊓ (z ⊔ u))"
    using 13 26 by metis
  have 60: "⋀x y . x ⊔ ((x ⊓ y) ⊔ (x ⊓ (y ⊔ top))) = x ⊓ (y ⊔ top)"
    using 15 25 26 by metis
  have 62: "⋀x y . x ⊔ ((x ⊓ - y) ⊔ (x ⊓ - - y)) = x"
    using 9 15 19 25 26 by metis
  have 65: "⋀x y . (- (x ⊔ y) ⊓ x) ⊔ (- (x ⊔ y) ⊓ y) = bot"
    using 9 20 26 29 by metis
  have 66: "⋀x y z . (x ⊓ - - y) ⊔ (x ⊓ - (- y ⊓ z)) = x ⊓ - (- y ⊓ z)"
    using 11 24 26 by metis
  have 69: "⋀x y . x ⊔ (x ⊓ - - y) = x"
    using 9 15 26 30 50 by metis
  have 81: "⋀x . top ⊔ - x = top"
    using 9 19 30 by metis
  have 82: "⋀x y z . (x ⊓ y) ⊔ (x ⊓ (y ⊔ z)) = x ⊓ (y ⊔ z)"
    using 11 26 30 by metis
  have 83: "⋀x y . x ⊔ (x ⊓ (y ⊔ top)) = x ⊓ (y ⊔ top)"
    using 60 82 by metis
  have 88: "⋀x y . x ⊔ (- y ⊓ x) = x"
    using 14 17 81 by metis
  have 89: "⋀x y . top ⊔ (x ⊔ - y) = x ⊔ top"
    using 25 81 by metis
  have 91: "⋀x y z . x ⊔ (y ⊔ (z ⊔ x)) = y ⊔ (z ⊔ x)"
    using 8 32 by metis
  have 94: "⋀x y z . x ⊔ (y ⊔ (- z ⊓ x)) = y ⊔ x"
    using 25 88 by metis
  have 101: "⋀x y z . x ⊔ (y ⊔ (x ⊓ - - z)) = y ⊔ x"
    using 25 69 by metis
  have 102: "⋀x . x ⊔ (x ⊓ bot) = x"
    using 41 49 69 by metis
  have 103: "⋀x y . x ⊔ (x ⊓ - y) = x"
    using 9 62 101 by metis
  have 109: "⋀x y . x ⊔ (y ⊔ (x ⊓ bot)) = y ⊔ x"
    using 25 102 by metis
  have 111: "⋀x y z . (- x ⊓ y) ⊔ ((- - x ⊓ y) ⊔ z) = y ⊔ z"
    using 14 19 33 by metis
  have 116: "⋀x y z . x ⊔ ((x ⊓ - y) ⊔ z) = x ⊔ z"
    using 8 103 by metis
  have 119: "⋀x y z . x ⊔ (y ⊔ (x ⊓ - z)) = y ⊔ x"
    using 25 103 by metis
  have 123: "⋀x . - - x ⊓ x = x"
    using 14 19 42 by metis
  have 127: "⋀x y . - - x ⊓ (x ⊓ y) = x ⊓ y"
    using 13 123 by metis
  have 130: "⋀x . - x ⊔ - - - x = - x"
    using 9 24 123 by metis
  have 132: "⋀x . - - - x = - x"
    using 9 103 123 130 by metis
  have 134: "⋀x y . - x ⊔ - (- - x ⊓ y) = - (- - x ⊓ y)"
    using 24 132 by metis
  have 136: "⋀x y . (- x ⊔ y) ⊓ - - x = y ⊓ - - x"
    using 42 132 by metis
  have 138: "⋀x . - x ⊓ - x = - x"
    using 123 132 by metis
  have 144: "⋀x y z . ((- (x ⊓ y) ⊓ x) ⊔ z) ⊓ y = z ⊓ y"
    using 20 29 34 by metis
  have 157: "⋀x y . (- x ⊔ y) ⊓ - x = (top ⊔ y) ⊓ - x"
    using 17 36 138 by metis
  have 182: "⋀x y z . (x ⊔ (- - (y ⊓ z) ⊓ y)) ⊓ z = (x ⊔ y) ⊓ z"
    using 17 35 123 by metis
  have 288: "⋀x y . - x ⊔ - (- x ⊓ y) = top"
    using 24 38 81 by metis
  have 315: "⋀x y . - (- x ⊓ y) ⊓ x = x"
    using 14 42 288 by metis
  have 316: "⋀x y z . - (- x ⊓ y) ⊓ (x ⊓ z) = x ⊓ z"
    using 13 315 by metis
  have 319: "⋀x y . - x ⊔ - - (- x ⊓ y) = - x"
    using 9 24 315 by metis
  have 320: "⋀x y . - - (- x ⊓ y) ⊓ x = bot"
    using 40 315 by metis
  have 373: "⋀x y . - x ⊔ - (x ⊓ y) = - (x ⊓ y)"
    using 24 127 132 by metis
  have 387: "⋀x y . - (x ⊓ y) ⊓ - x = - x"
    using 127 315 by metis
  have 388: "⋀x y . - - (x ⊓ y) ⊓ - x = bot"
    using 127 320 by metis
  have 404: "⋀x y z . - (x ⊓ y) ⊓ (- x ⊓ z) = - x ⊓ z"
    using 13 387 by metis
  have 405: "⋀x y z . - (x ⊓ (y ⊓ z)) ⊓ - (x ⊓ y) = - (x ⊓ y)"
    using 13 387 by metis
  have 419: "⋀x y . - x ⊓ - - (- x ⊓ y) = - - (- x ⊓ y)"
    using 315 387 by metis
  have 420: "⋀x y . - - x ⊓ - - (x ⊓ y) = - - (x ⊓ y)"
    using 387 by metis
  have 421: "⋀x y z . - - (x ⊓ y) ⊓ (- x ⊓ z) = bot"
    using 13 18 388 by metis
  have 536: "⋀x y . (x ⊔ - - y) ⊓ y = (x ⊔ top) ⊓ y"
    using 42 47 by metis
  have 662: "⋀u x y z . (x ⊓ y) ⊔ ((x ⊓ (z ⊔ y)) ⊔ u) = (x ⊓ (z ⊔ y)) ⊔ u"
    using 9 32 54 by metis
  have 705: "⋀u x y z . (x ⊓ (y ⊔ z)) ⊔ ((x ⊓ (y ⊔ (z ⊓ bot))) ⊔ u) = (x ⊓ (y ⊔ z)) ⊔ u"
    using 25 54 109 662 by metis
  have 755: "⋀x y z . (x ⊓ - y) ⊔ (z ⊔ x) = z ⊔ x"
    using 32 91 116 by metis
  have 757: "⋀x y z . x ⊔ (x ⊓ (- y ⊓ - z)) = x"
    using 13 103 116 by metis
  have 930: "⋀x y z . (- (x ⊓ (y ⊔ z)) ⊓ (x ⊓ y)) ⊔ (- (x ⊓ (y ⊔ z)) ⊓ (x ⊓ z)) = bot"
    using 9 20 29 58 by metis
  have 1091: "⋀x y . - (x ⊔ y) ⊓ x = bot"
    using 9 29 30 65 by metis
  have 1092: "⋀x y . - (x ⊔ y) ⊓ y = bot"
    using 29 30 65 1091 by metis
  have 1113: "⋀u x y z . - (x ⊔ ((y ⊔ z) ⊓ u)) ⊓ (x ⊔ (z ⊓ u)) = bot"
    using 29 46 65 1091 by metis
  have 1117: "⋀x y z . - (x ⊔ y) ⊓ (x ⊔ (- z ⊓ y)) = bot"
    using 29 65 94 1092 by metis
  have 1128: "⋀x y z . - (x ⊔ (y ⊔ z)) ⊓ (x ⊔ y) = bot"
    using 8 1091 by metis
  have 1129: "⋀x y z . (- (x ⊔ y) ⊔ z) ⊓ x = z ⊓ x"
    using 17 29 1091 by metis
  have 1155: "⋀x y . - - x ⊓ - (- x ⊓ y) = - - x"
    using 66 103 123 132 by metis
  have 1578: "⋀x y z . - (x ⊓ (y ⊔ z)) ⊓ (x ⊓ y) = bot"
    using 82 1091 by metis
  have 1594: "⋀x y z . - (x ⊓ (y ⊔ z)) ⊓ (x ⊓ z) = bot"
    using 29 930 1578 by metis
  have 2094: "⋀x y z . - (x ⊔ (y ⊓ (z ⊔ top))) ⊓ (x ⊔ y) = bot"
    using 83 1128 by metis
  have 2097: "⋀x y . - - (x ⊔ y) ⊓ x = x"
    using 14 19 1129 by metis
  have 2124: "⋀x y . - - (x ⊔ y) ⊓ y = y"
    using 9 2097 by metis
  have 2135: "⋀x y . - - ((top ⊔ x) ⊓ y) ⊓ y = y"
    using 36 2097 by metis
  have 2136: "⋀x y . - - ((x ⊔ top) ⊓ y) ⊓ y = y"
    using 37 2097 by metis
  have 2137: "⋀x y . - x ⊔ - - (x ⊔ y) = top"
    using 9 288 2097 by metis
  have 2138: "⋀x y . - x ⊓ - (x ⊔ y) = - (x ⊔ y)"
    using 315 2097 by metis
  have 2151: "⋀x y . - x ⊔ - (x ⊔ y) = - x"
    using 9 132 373 2097 by metis
  have 2191: "⋀x y . - - x ⊓ (- y ⊓ x) = - y ⊓ x"
    using 88 2124 by metis
  have 2201: "⋀x y . - x ⊔ - - (y ⊔ x) = top"
    using 9 288 2124 by metis
  have 2202: "⋀x y . - x ⊓ - (y ⊔ x) = - (y ⊔ x)"
    using 315 2124 by metis
  have 2320: "⋀x y . - (x ⊓ (y ⊔ top)) = - x"
    using 83 373 2151 by metis
  have 2343: "⋀x y . - (- x ⊓ y) ⊔ - - y = top"
    using 88 2201 by metis
  have 2546: "⋀x y z . - x ⊔ ((- - x ⊓ - y) ⊔ z) = - x ⊔ (- y ⊔ z)"
    using 111 116 by metis
  have 2706: "⋀x y z . - x ⊔ (y ⊔ - - ((top ⊔ z) ⊓ - x)) = y ⊔ - - ((top ⊔ z) ⊓ - x)"
    using 755 2135 by metis
  have 2810: "⋀x y . - x ⊓ - ((y ⊔ top) ⊓ x) = - ((y ⊔ top) ⊓ x)"
    using 315 2136 by metis
  have 3022: "⋀x y . - x ⊔ - (- y ⊓ - x) = top"
    using 9 132 2343 by metis
  have 3133: "⋀x y . - (- x ⊓ - y) ⊓ y = y"
    using 14 42 3022 by metis
  have 3134: "⋀x y . - x ⊓ (- y ⊓ - x) = - y ⊓ - x"
    using 14 43 3022 by metis
  have 3961: "⋀x y . - - (x ⊔ y) ⊓ - - x = - - x"
    using 14 136 2137 by metis
  have 4644: "⋀x y z . - (x ⊓ - y) ⊓ (x ⊓ - (y ⊔ z)) = bot"
    using 1594 2151 by metis
  have 5495: "⋀x y z . - - (x ⊓ y) ⊓ - (x ⊔ z) = bot"
    using 421 2138 by metis
  have 9413: "⋀x y . - - (- x ⊓ y) ⊓ y = - x ⊓ y"
    using 9 103 182 319 by metis
  have 9519: "⋀x y z . - - (- x ⊓ y) ⊓ - - (x ⊓ z) = bot"
    using 373 5495 by metis
  have 11069: "⋀x y z . - (- - x ⊓ y) ⊔ (- x ⊓ - z) = - (- - x ⊓ y)"
    using 316 757 by metis
  have 12370: "⋀x y . - x ⊓ - (- - x ⊓ y) = - x"
    using 132 1155 by metis
  have 12376: "⋀x y . - x ⊓ - (x ⊓ y) = - x"
    using 127 132 1155 by metis
  have 12383: "⋀x y . - (x ⊔ y) ⊓ - y = - (x ⊔ y)"
    using 132 1155 2124 by metis
  have 12393: "⋀x y . - - (- x ⊓ - y) = - x ⊓ - y"
    using 1155 3133 9413 by metis
  have 12407: "⋀x y . - - x ⊓ - - (x ⊔ y) = - - x"
    using 1155 2138 by metis
  have 12639: "⋀x y . - x ⊓ - (- y ⊓ x) = - x"
    using 88 12383 by metis
  have 24647: "⋀x y . (- x ⊓ - y) ⊔ - (- x ⊓ - y) = top"
    using 19 12393 by metis
  have 28269: "⋀x y z . - - (x ⊓ y) ⊔ - (- x ⊓ z) = - (- x ⊓ z)"
    using 373 404 by metis
  have 28338: "⋀x y . - (- - (x ⊓ y) ⊓ x) = - (x ⊓ y)"
    using 123 405 12370 by metis
  have 28422: "⋀x y . - (- x ⊓ - y) = - (- y ⊓ - x)"
    using 13 3134 12393 28338 by metis
  have 28485: "⋀x y . - x ⊓ - y = - y ⊓ - x"
    using 2097 3961 12393 28422 by metis
  have 30411: "⋀x y . - x ⊓ (x ⊔ (x ⊓ y)) = bot"
    using 9 82 2094 2320 by metis
  have 30469: "⋀x . - x ⊓ (x ⊔ - - x) = bot"
    using 9 123 132 30411 by metis
  have 37513: "⋀x y . - (- x ⊓ - y) ⊓ - (y ⊔ x) = bot"
    using 2202 4644 by metis
  have 52421: "⋀x y . - (- x ⊓ - (- x ⊓ y)) ⊓ y = y"
    using 14 144 24647 28485 by metis
  have 52520: "⋀x y . - x ⊓ - (- x ⊓ y) = - x ⊓ - y"
    using 13 12376 12393 12639 28485 52421 by metis
  have 52533: "⋀x y z . - - (x ⊔ (y ⊓ (z ⊔ top))) ⊓ (x ⊔ y) = x ⊔ y"
    using 15 49 2094 52421 by metis
  have 61101: "⋀x y z . - (- - x ⊓ y) ⊔ z = - x ⊔ (- y ⊔ z)"
    using 111 2546 12370 52520 by metis
  have 61156: "⋀x y . - - (- x ⊓ y) = - x ⊓ - - y"
    using 419 52520 by metis
  have 61162: "⋀x y . - (x ⊔ (x ⊓ y)) = - x"
    using 15 49 2138 30411 52520 by metis
  have 61163: "⋀x . - (x ⊔ - - x) = - x"
    using 15 49 2138 30469 52520 by metis
  have 61229: "⋀x y z . - x ⊓ (- - y ⊓ - (x ⊓ z)) = - x ⊓ - - y"
    using 13 15 49 132 9519 52520 61156 by metis
  have 61311: "⋀x y . - x ⊔ - y = - (- - y ⊓ x)"
    using 119 11069 61101 by metis
  have 61391: "⋀x y . - (- x ⊓ - - y) = - (- x ⊓ y)"
    using 13 28269 61156 61229 61311 by metis
  have 61420: "⋀x y . - (- - x ⊓ y) = - (- - y ⊓ x)"
    using 13 134 2191 61156 61311 by metis
  have 61454: "⋀x y . - (x ⊔ - (- y ⊓ - x)) = - y ⊓ - x"
    using 9 132 3133 61156 61162 by metis
  have 61648: "⋀x y . - x ⊓ (x ⊔ (- y ⊓ - - x)) = bot"
    using 1117 61163 by metis
  have 62434: "⋀x y . - (- - x ⊓ y) ⊓ x = - y ⊓ x"
    using 43 61311 by metis
  have 63947: "⋀x y . - (- x ⊓ y) ⊓ - (- y ⊔ x) = bot"
    using 37513 61391 by metis
  have 64227: "⋀x y . - (x ⊔ (- y ⊓ - - x)) = - x"
    using 15 49 2138 52520 61648 by metis
  have 64239: "⋀x y . - (x ⊔ (- - x ⊔ y)) = - (x ⊔ y)"
    using 9 25 12407 64227 by metis
  have 64241: "⋀x y . - (x ⊔ (- - x ⊓ - y)) = - x"
    using 28485 64227 by metis
  have 64260: "⋀x y . - (x ⊔ - - (x ⊓ y)) = - x"
    using 420 64241 by metis
  have 64271: "⋀x y . - (- x ⊔ (y ⊔ - - (y ⊓ x))) = - (- x ⊔ y)"
    using 9 25 42 64260 by metis
  have 64281: "⋀x y . - (- x ⊔ y) = - (y ⊔ - - ((top ⊔ y) ⊓ - x))"
    using 9 25 157 2706 64260 by metis
  have 64282: "⋀x y . - (x ⊔ - - ((x ⊔ top) ⊓ y)) = - (x ⊔ - - y)"
    using 9 25 132 536 2810 28485 61311 64260 by metis
  have 65110: "⋀x y . - ((- x ⊓ y) ⊔ (- y ⊔ x)) = bot"
    using 9 14 49 37513 63947 by metis
  have 65231: "⋀x y . - (x ⊔ ((- x ⊓ y) ⊔ - y)) = bot"
    using 9 25 65110 by metis
  have 65585: "⋀x y . - (x ⊔ - y) = - - y ⊓ - x"
    using 61311 61454 64239 by metis
  have 65615: "⋀x y . - x ⊓ - ((x ⊔ top) ⊓ y) = - y ⊓ - x"
    using 132 28485 64282 65585 by metis
  have 65616: "⋀x y . - (- x ⊔ y) = - y ⊓ - ((top ⊔ y) ⊓ - x)"
    using 132 28485 64281 65585 by metis
  have 65791: "⋀x y . - x ⊓ - ((top ⊔ x) ⊓ - y) = - - y ⊓ - x"
    using 89 132 12376 28485 64271 65585 65615 65616 by metis
  have 65933: "⋀x y . - (- x ⊔ y) = - - x ⊓ - y"
    using 65616 65791 by metis
  have 66082: "⋀x y z . - (x ⊔ (y ⊔ - z)) = - - z ⊓ - (x ⊔ y)"
    using 8 65585 by metis
  have 66204: "⋀x y . - - x ⊓ - (y ⊔ (- y ⊓ x)) = bot"
    using 65231 66082 by metis
  have 66281: "⋀x y z . - (x ⊔ (- y ⊔ z)) = - - y ⊓ - (x ⊔ z)"
    using 25 65933 by metis
  have 67527: "⋀x y . - - (x ⊔ (- x ⊓ y)) ⊓ y = y"
    using 14 49 62434 66204 by metis
  have 67762: "⋀x y . - (- - x ⊓ (y ⊔ (- y ⊓ x))) = - x"
    using 61420 67527 by metis
  have 68018: "⋀x y z . - (x ⊔ y) ⊓ (x ⊔ (y ⊓ (z ⊔ top))) = bot"
    using 8 83 1113 2320 by metis
  have 71989: "⋀x y z . - (x ⊔ (y ⊓ (z ⊔ top))) = - (x ⊔ y)"
    using 9 29 52533 67762 68018 by metis
  have 71997: "⋀x y z . - ((x ⊓ (y ⊔ top)) ⊔ z) = - (x ⊔ z)"
    using 17 2320 71989 by metis
  have 72090: "⋀x y z . - (x ⊔ ((x ⊓ y) ⊔ z)) = - (x ⊔ z)"
    using 10 14 705 71997 by metis
  have 72139: "⋀x y . - (x ⊔ y) = - x ⊓ - y"
    using 25 123 132 2138 65933 66281 72090 by metis
  show ?thesis
    using 72139 by metis
qed

lemma l15:
  "--(x ⊔ y) = --x ⊔ --y"
  by (simp add: l11 l12 l4)

lemma l13_var:
  "- - (- x ⊓ y) = - x ⊓ - - y"
proof -
  have 1: "⋀x y . x ≤ y ⟷ x ⊔ y = y"
    by (simp add: il_less_eq)
  have 4: "⋀x y . ¬(x ≤ y) ∨ x ⊔ y = y"
    using 1 by metis
  have 5: "⋀x y z . (x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z)"
    by (simp add: il_sub_inf_right_isotone_var)
  have 6: "⋀x y . - - x ≤ - (- x ⊓ y)"
    by (simp add: pad2)
  have 7: "⋀x y z . x ⊔ (y ⊔ z) = (x ⊔ y) ⊔ z"
    by (simp add: il_associative)
  have 8: "⋀x y z . (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)"
    using 7 by metis
  have 9: "⋀x y . x ⊔ y = y ⊔ x"
    by (simp add: il_commutative)
  have 10: "⋀x . x ⊔ bot = x"
    by (simp add: il_bot_unit)
  have 11: "⋀x . x ⊔ x = x"
    by simp
  have 12: "⋀x y z . x ⊓ (y ⊓ z) = (x ⊓ y) ⊓ z"
    by (simp add: il_inf_associative)
  have 13: "⋀x y z . (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)"
    using 12 by metis
  have 14: "⋀x . top ⊓ x = x"
    by simp
  have 15: "⋀x . x ⊓ top = x"
    by simp
  have 16: "⋀x y z . (x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z)"
    by (simp add: il_inf_right_dist_sup)
  have 17: "⋀x y z . (x ⊓ y) ⊔ (z ⊓ y) = (x ⊔ z) ⊓ y"
    using 16 by metis
  have 19: "⋀x . - x ⊔ - - x = top"
    by simp
  have 20: "⋀x . - x ⊓ x = bot"
    by (simp add: a_inf_complement_bot)
  have 22: "⋀x y z . ((x ⊓ y) ⊔ (x ⊓ z)) ⊔ (x ⊓ (y ⊔ z)) = x ⊓ (y ⊔ z)"
    using 4 5 by metis
  have 23: "⋀x y z . (x ⊓ (y ⊔ z)) ⊔ ((x ⊓ y) ⊔ (x ⊓ z)) = x ⊓ (y ⊔ z)"
    using 9 22 by metis
  have 24: "⋀x y . - - x ⊔ - (- x ⊓ y) = - (- x ⊓ y)"
    using 4 6 by metis
  have 25: "⋀x y z . x ⊔ (y ⊔ z) = y ⊔ (x ⊔ z)"
    using 8 9 by metis
  have 26: "⋀x y z . (x ⊓ y) ⊔ ((x ⊓ z) ⊔ (x ⊓ (y ⊔ z))) = x ⊓ (y ⊔ z)"
    using 9 23 25 by metis
  have 29: "⋀x . bot ⊔ x = x"
    using 9 10 by metis
  have 30: "⋀x y . x ⊔ (x ⊔ y) = x ⊔ y"
    using 8 11 by metis
  have 34: "⋀u x y z . (x ⊓ (y ⊓ z)) ⊔ (u ⊓ z) = ((x ⊓ y) ⊔ u) ⊓ z"
    using 13 17 by metis
  have 35: "⋀u x y z . (x ⊓ y) ⊔ (z ⊓ (u ⊓ y)) = (x ⊔ (z ⊓ u)) ⊓ y"
    using 13 17 by metis
  have 38: "⋀x y . - x ⊔ (- - x ⊔ y) = top ⊔ y"
    using 8 19 by metis
  have 41: "- top = bot"
    using 15 20 by metis
  have 42: "⋀x y . (- x ⊔ y) ⊓ x = y ⊓ x"
    using 17 20 29 by metis
  have 43: "⋀x y . (x ⊔ - y) ⊓ y = x ⊓ y"
    using 9 17 20 29 by metis
  have 45: "⋀x . - bot ⊔ - - x = - bot"
    using 9 20 24 by metis
  have 49: "- bot = top"
    using 19 29 41 by metis
  have 50: "⋀x . top ⊔ - - x = top"
    using 45 49 by metis
  have 62: "⋀x y . x ⊔ ((x ⊓ - y) ⊔ (x ⊓ - - y)) = x"
    using 9 15 19 25 26 by metis
  have 65: "⋀x y . (- (x ⊔ y) ⊓ x) ⊔ (- (x ⊔ y) ⊓ y) = bot"
    using 9 20 26 29 by metis
  have 66: "⋀x y z . (x ⊓ - - y) ⊔ (x ⊓ - (- y ⊓ z)) = x ⊓ - (- y ⊓ z)"
    using 11 24 26 by metis
  have 69: "⋀x y . x ⊔ (x ⊓ - - y) = x"
    using 9 15 26 30 50 by metis
  have 81: "⋀x . top ⊔ - x = top"
    using 9 19 30 by metis
  have 88: "⋀x y . x ⊔ (- y ⊓ x) = x"
    using 14 17 81 by metis
  have 101: "⋀x y z . x ⊔ (y ⊔ (x ⊓ - - z)) = y ⊔ x"
    using 25 69 by metis
  have 103: "⋀x y . x ⊔ (x ⊓ - y) = x"
    using 9 62 101 by metis
  have 123: "⋀x . - - x ⊓ x = x"
    using 14 19 42 by metis
  have 127: "⋀x y . - - x ⊓ (x ⊓ y) = x ⊓ y"
    using 13 123 by metis
  have 130: "⋀x . - x ⊔ - - - x = - x"
    using 9 24 123 by metis
  have 132: "⋀x . - - - x = - x"
    using 9 103 123 130 by metis
  have 136: "⋀x y . (- x ⊔ y) ⊓ - - x = y ⊓ - - x"
    using 42 132 by metis
  have 144: "⋀x y z . ((- (x ⊓ y) ⊓ x) ⊔ z) ⊓ y = z ⊓ y"
    using 20 29 34 by metis
  have 182: "⋀x y z . (x ⊔ (- - (y ⊓ z) ⊓ y)) ⊓ z = (x ⊔ y) ⊓ z"
    using 17 35 123 by metis
  have 288: "⋀x y . - x ⊔ - (- x ⊓ y) = top"
    using 24 38 81 by metis
  have 315: "⋀x y . - (- x ⊓ y) ⊓ x = x"
    using 14 42 288 by metis
  have 319: "⋀x y . - x ⊔ - - (- x ⊓ y) = - x"
    using 9 24 315 by metis
  have 387: "⋀x y . - (x ⊓ y) ⊓ - x = - x"
    using 127 315 by metis
  have 405: "⋀x y z . - (x ⊓ (y ⊓ z)) ⊓ - (x ⊓ y) = - (x ⊓ y)"
    using 13 387 by metis
  have 419: "⋀x y . - x ⊓ - - (- x ⊓ y) = - - (- x ⊓ y)"
    using 315 387 by metis
  have 1091: "⋀x y . - (x ⊔ y) ⊓ x = bot"
    using 9 29 30 65 by metis
  have 1129: "⋀x y z . (- (x ⊔ y) ⊔ z) ⊓ x = z ⊓ x"
    using 17 29 1091 by metis
  have 1155: "⋀x y . - - x ⊓ - (- x ⊓ y) = - - x"
    using 66 103 123 132 by metis
  have 2097: "⋀x y . - - (x ⊔ y) ⊓ x = x"
    using 14 19 1129 by metis
  have 2124: "⋀x y . - - (x ⊔ y) ⊓ y = y"
    using 9 2097 by metis
  have 2137: "⋀x y . - x ⊔ - - (x ⊔ y) = top"
    using 9 288 2097 by metis
  have 2201: "⋀x y . - x ⊔ - - (y ⊔ x) = top"
    using 9 288 2124 by metis
  have 2343: "⋀x y . - (- x ⊓ y) ⊔ - - y = top"
    using 88 2201 by metis
  have 3022: "⋀x y . - x ⊔ - (- y ⊓ - x) = top"
    using 9 132 2343 by metis
  have 3133: "⋀x y . - (- x ⊓ - y) ⊓ y = y"
    using 14 42 3022 by metis
  have 3134: "⋀x y . - x ⊓ (- y ⊓ - x) = - y ⊓ - x"
    using 14 43 3022 by metis
  have 3961: "⋀x y . - - (x ⊔ y) ⊓ - - x = - - x"
    using 14 136 2137 by metis
  have 9413: "⋀x y . - - (- x ⊓ y) ⊓ y = - x ⊓ y"
    using 9 103 182 319 by metis
  have 12370: "⋀x y . - x ⊓ - (- - x ⊓ y) = - x"
    using 132 1155 by metis
  have 12376: "⋀x y . - x ⊓ - (x ⊓ y) = - x"
    using 127 132 1155 by metis
  have 12383: "⋀x y . - (x ⊔ y) ⊓ - y = - (x ⊔ y)"
    using 132 1155 2124 by metis
  have 12393: "⋀x y . - - (- x ⊓ - y) = - x ⊓ - y"
    using 1155 3133 9413 by metis
  have 12639: "⋀x y . - x ⊓ - (- y ⊓ x) = - x"
    using 88 12383 by metis
  have 24647: "⋀x y . (- x ⊓ - y) ⊔ - (- x ⊓ - y) = top"
    using 19 12393 by metis
  have 28338: "⋀x y . - (- - (x ⊓ y) ⊓ x) = - (x ⊓ y)"
    using 123 405 12370 by metis
  have 28422: "⋀x y . - (- x ⊓ - y) = - (- y ⊓ - x)"
    using 13 3134 12393 28338 by metis
  have 28485: "⋀x y . - x ⊓ - y = - y ⊓ - x"
    using 2097 3961 12393 28422 by metis
  have 52421: "⋀x y . - (- x ⊓ - (- x ⊓ y)) ⊓ y = y"
    using 14 144 24647 28485 by metis
  have 52520: "⋀x y . - x ⊓ - (- x ⊓ y) = - x ⊓ - y"
    using 13 12376 12393 12639 28485 52421 by metis
  have 61156: "⋀x y . - - (- x ⊓ y) = - x ⊓ - - y"
    using 419 52520 by metis
  show ?thesis
    using 61156 by metis
qed

text ‹Theorem 25.1›

subclass subset_boolean_algebra_2
proof
  show "⋀x y z. x ⊔ (y ⊔ z) = x ⊔ y ⊔ z"
    by (simp add: il_associative)
  show "⋀x y. x ⊔ y = y ⊔ x"
    by (simp add: il_commutative)
  show "⋀x. x ⊔ x = x"
    by simp
  show "⋀x y. x ⊔ - (y ⊔ - y) = x"
    using il_bot_unit l12 l6 by auto
  show "⋀x y. - (x ⊔ y) = - (- - x ⊔ - - y)"
    by (metis l15 l4)
  show "⋀x y. - x ⊔ - (- x ⊔ y) = - x ⊔ - y"
    by (smt l11 l15 il_inf_right_dist_sup il_unit_bot l6 l7)
qed

lemma aa_test:
  "p = --p ⟹ test p"
  by (metis ppa_ppd.d_closed)

lemma test_aa_increasing:
  "test p ⟹ p ≤ --p"
  by (simp add: ppa_ppd.d_increasing_sub_identity test_sub_identity)

lemma "test p ⟹ - - (p ⊓ x) ≤ p" nitpick [expect=genuine] oops
lemma "test p ⟹ --p ≤ p" nitpick [expect=genuine] oops

end

class pa_algebra = pa_semiring + minus +
  assumes pa_minus_def: "-x - -y = -(--x ⊔ -y)"
begin

subclass subset_boolean_algebra_2_extended
proof
  show "bot = (THE x. ∀z. x = - (z ⊔ - z))"
    using l12 l6 by auto
  thus "top = - (THE x. ∀z. x = - (z ⊔ - z))"
    using l2 by blast
  show "⋀x y. - x ⊓ - y = - (- - x ⊔ - - y)"
    by (metis l12 l4)
  show "⋀x y. - x - - y = - (- - x ⊔ - y)"
    by (simp add: pa_minus_def)
  show "⋀x y. (x ≤ y) = (x ⊔ y = y)"
    by (simp add: il_less_eq)
  show "⋀x y. (x < y) = (x ⊔ y = y ∧ y ⊔ x ≠ x)"
    by (simp add: il_less_eq less_le_not_le)
qed

lemma "⋀x y. - (x ⊓ - - y) = - (x ⊓ y)" nitpick [expect=genuine] oops

end

subsection ‹Antidomain Semirings›

text ‹Definition 24›

class a_semiring = ppa_semiring +
  assumes ad3: "-(x ⊓ y) ≤ -(x ⊓ --y)"
begin

lemma l16:
  "- - x ≤ - (- x ⊓ y)"
proof -
  have 1: "⋀x y . x ≤ y ⟷ x ⊔ y = y"
    by (simp add: il_less_eq)
  have 3: "⋀x y z . x ⊔ (y ⊔ z) = (x ⊔ y) ⊔ z"
    by (simp add: il_associative)
  have 4: "⋀x y z . (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)"
    using 3 by metis
  have 5: "⋀x y . x ⊔ y = y ⊔ x"
    by (simp add: il_commutative)
  have 6: "⋀x . x ⊔ bot = x"
    by (simp add: il_bot_unit)
  have 7: "⋀x . x ⊔ x = x"
    by simp
  have 8: "⋀x y . ¬(x ≤ y) ∨ x ⊔ y = y"
    using 1 by metis
  have 9: "⋀x y . x ≤ y ∨ x ⊔ y ≠ y"
    using 1 by metis
  have 10: "⋀x y z . x ⊓ (y ⊓ z) = (x ⊓ y) ⊓ z"
    by (simp add: il_inf_associative)
  have 11: "⋀x y z . (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)"
    using 10 by metis
  have 12: "⋀x . top ⊓ x = x"
    by simp
  have 13: "⋀x . x ⊓ top = x"
    by simp
  have 14: "⋀x y z . (x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z)"
    by (simp add: il_sub_inf_right_isotone_var)
  have 15: "⋀x y z . (x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z)"
    by (simp add: il_inf_right_dist_sup)
  have 16: "⋀x y z . (x ⊓ y) ⊔ (z ⊓ y) = (x ⊔ z) ⊓ y"
    using 15 by metis
  have 17: "⋀x . bot ⊓ x = bot"
    by simp
  have 18: "⋀x . - x ⊔ - - x = top"
    by simp
  have 19: "⋀x . - x ⊓ x = bot"
    by (simp add: a_inf_complement_bot)
  have 20: "⋀x y . - (x ⊓ y) ≤ - (x ⊓ - - y)"
    by (simp add: ad3)
  have 22: "⋀x y z . x ⊔ (y ⊔ z) = y ⊔ (x ⊔ z)"
    using 4 5 by metis
  have 25: "⋀x . bot ⊔ x = x"
    using 5 6 by metis
  have 26: "⋀x y . x ⊔ (x ⊔ y) = x ⊔ y"
    using 4 7 by metis
  have 33: "⋀x y z . (x ⊓ y) ⊔ ((x ⊓ z) ⊔ (x ⊓ (y ⊔ z))) = x ⊓ (y ⊔ z)"
    using 5 8 14 22 by metis
  have 47: "⋀x y . - x ⊔ (- - x ⊔ y) = top ⊔ y"
    using 4 18 by metis
  have 48: "⋀x y . - - x ⊔ (y ⊔ - x) = y ⊔ top"
    using 4 5 18 by metis
  have 51: "⋀x y . - x ⊓ (x ⊓ y) = bot"
    using 11 17 19 by metis
  have 52: "- top = bot"
    using 13 19 by metis
  have 56: "⋀x y . (- x ⊔ y) ⊓ x = y ⊓ x"
    using 16 19 25 by metis
  have 57: "⋀x y . (x ⊔ - y) ⊓ y = x ⊓ y"
    using 5 16 19 25 by metis
  have 58: "⋀x y . - (x ⊓ y) ⊔ - (x ⊓ - - y) = - (x ⊓ - - y)"
    using 8 20 by metis
  have 60: "⋀x . - x ≤ - - - x"
    using 12 20 by metis
  have 69: "- bot = top"
    using 18 25 52 by metis
  have 74: "⋀x y . x ≤ x ⊔ y"
    using 9 26 by metis
  have 78: "⋀x . top ⊔ - x = top"
    using 5 18 26 by metis
  have 80: "⋀x y . x ≤ y ⊔ x"
    using 5 74 by metis
  have 86: "⋀x y z . x ⊔ y ≤ x ⊔ (z ⊔ y)"
    using 22 80 by metis
  have 95: "⋀x . - x ⊔ - - - x = - - - x"
    using 8 60 by metis
  have 143: "⋀x y . x ⊔ (x ⊓ - y) = x"
    using 5 13 26 33 78 by metis
  have 370: "⋀x y z . x ⊔ (y ⊓ - z) ≤ x ⊔ y"
    using 86 143 by metis
  have 907: "⋀x . - x ⊓ - x = - x"
    using 12 18 57 by metis
  have 928: "⋀x y . - x ⊓ (- x ⊓ y) = - x ⊓ y"
    using 11 907 by metis
  have 966: "⋀x y . - (- x ⊓ - - (x ⊓ y)) = top"
    using 51 58 69 78 by metis
  have 1535: "⋀x . - x ⊔ - - - - x = top"
    using 47 78 95 by metis
  have 1630: "⋀x y z . (x ⊔ y) ⊓ - z ≤ (x ⊓ - z) ⊔ y"
    using 16 370 by metis
  have 2422: "⋀x . - x ⊓ - - - x = - - - x"
    using 12 57 1535 by metis
  have 6567: "⋀x y . - x ⊓ - - (x ⊓ y) = bot"
    using 12 19 966 by metis
  have 18123: "⋀x . - - - x = - x"
    using 95 143 2422 by metis
  have 26264: "⋀x y . - x ≤ (- y ⊓ - x) ⊔ - - y"
    using 12 18 1630 by metis
  have 26279: "⋀x y . - - (x ⊓ y) ≤ - - x"
    using 25 6567 26264 by metis
  have 26307: "⋀x y . - - (- x ⊓ y) ≤ - x"
    using 928 18123 26279 by metis
  have 26339: "⋀x y . - x ⊔ - - (- x ⊓ y) = - x"
    using 5 8 26307 by metis
  have 26564: "⋀x y . - x ⊔ - (- x ⊓ y) = top"
    using 5 48 78 18123 26339 by metis
  have 26682: "⋀x y . - (- x ⊓ y) ⊓ x = x"
    using 12 56 26564 by metis
  have 26864: "⋀x y . - - x ≤ - (- x ⊓ y)"
    using 18123 26279 26682 by metis
  show ?thesis
    using 26864 by metis
qed

text ‹Theorem 25.2›

subclass pa_semiring
proof
  show "⋀x y. - - x ≤ - (- x ⊓ y)"
    by (rule l16)
qed

lemma l17:
  "-(x ⊓ y) = -(x ⊓ --y)"
  by (simp add: ad3 order.antisym l14)

lemma a_complement_inf_double_complement:
  "-(x ⊓ --y) = -(x ⊓ y)"
  using l17 by auto

sublocale a_d: d_semiring_var where d = "λx . --x"
proof
  show "⋀x y. - - (x ⊓ - - y) ≤ - - (x ⊓ y)"
    using l17 by auto
  show "- - bot = bot"
    by (simp add: l1 l2)
qed

lemma "test p ⟹ - - (p ⊓ x) ≤ p"
  by (fact a_d.d2)

end

class a_algebra = a_semiring + minus +
  assumes a_minus_def: "-x - -y = -(--x ⊔ -y)"
begin

subclass pa_algebra
proof
  show "⋀x y. - x - - y = - (- - x ⊔ - y)"
    by (simp add: a_minus_def)
qed

text ‹Theorem 25.4›

subclass subset_boolean_algebra_4_extended
proof
  show "⋀x y z. x ⊓ (y ⊓ z) = x ⊓ y ⊓ z"
    by (simp add: il_inf_associative)
  show "⋀x y z. (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z"
    by (simp add: il_inf_right_dist_sup)
  show "⋀x. - x ⊓ x = bot"
    by (simp add: a_inf_complement_bot)
  show "⋀x. top ⊓ x = x"
    by simp
  show "⋀x y. - (x ⊓ - - y) = - (x ⊓ y)"
    using l17 by auto
  show "⋀x. x ⊓ top = x"
    by simp
  show "⋀x y z. x ≤ y ⟹ z ⊓ x ≤ z ⊓ y"
    by (simp add: il_sub_inf_right_isotone)
qed

end

context subset_boolean_algebra_4_extended
begin

subclass il_semiring
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. x ⊔ x = x"
    by simp
  show "⋀x. x ⊔ bot = x"
    by simp
  show "⋀x y z. x ⊓ (y ⊓ z) = x ⊓ y ⊓ z"
    by (simp add: sba3_inf_associative)
  show "⋀x y z. (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z"
    by (simp add: sba3_inf_right_dist_sup)
  show "⋀x. top ⊓ x = x"
    by simp
  show "⋀x. x ⊓ top = x"
    by simp
  show "⋀x. bot ⊓ x = bot"
    by (simp add: inf_left_zero)
  show "⋀x y z. x ≤ y ⟹ z ⊓ x ≤ z ⊓ y"
    by (simp add: inf_right_isotone)
  show "⋀x y. (x ≤ y) = (x ⊔ y = y)"
    by (simp add: le_iff_sup)
  show "⋀x y. (x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    by (simp add: less_le_not_le)
qed

subclass a_semiring
proof
  show "⋀x. - x ⊓ x = bot"
    by (simp add: sba3_inf_complement_bot)
  show "⋀x. - x ⊔ - - x = top"
    by simp
  show "⋀x y. - (x ⊓ y) ≤ - (x ⊓ - - y)"
    by (simp add: sba3_complement_inf_double_complement)
qed

sublocale sba4_a: a_algebra
proof
  show "⋀x y. - x - - y = - (- - x ⊔ - y)"
    by (simp add: sub_minus_def)
qed

end

context stone_algebra
begin

text ‹Theorem 25.3›

subclass il_semiring
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. x ⊔ x = x"
    by simp
  show "⋀x. x ⊔ bot = x"
    by simp
  show "⋀x y z. x ⊓ (y ⊓ z) = x ⊓ y ⊓ z"
    by (simp add: inf.sup_monoid.add_assoc)
  show "⋀x y z. (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z"
    by (simp add: inf_sup_distrib2)
  show "⋀x. top ⊓ x = x"
    by simp
  show "⋀x. x ⊓ top = x"
    by simp
  show "⋀x. bot ⊓ x = bot"
    by simp
  show "⋀x y z. x ≤ y ⟹ z ⊓ x ≤ z ⊓ y"
    using inf.sup_right_isotone by blast
  show "⋀x y. (x ≤ y) = (x ⊔ y = y)"
    by (simp add: le_iff_sup)
  show "⋀x y. (x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    by (simp add: less_le_not_le)
qed

subclass a_semiring
proof
  show "⋀x. - x ⊓ x = bot"
    by simp
  show "⋀x. - x ⊔ - - x = top"
    by simp
  show "⋀x y. - (x ⊓ y) ≤ - (x ⊓ - - y)"
    by simp
qed

end

end