Booléens

TYPE boolean
  INHERIT equality{boolean}
  IMPORT Partial_ordering FROM partial_order{boolean}
    -- Generated by {true, false}.

  MESSAGE true REPLY(b: boolean)

  MESSAGE false REPLY(b: boolean)
    WHERE true ~= false

  MESSAGE "~"(b1: boolean) REPLY(b2: boolean)
    WHERE ~true = false, ~false = true, ~! = !

  MESSAGE and(b1 b2: boolean) REPLY(b3: boolean)
    WHERE ALL(b: boolean :: and(b, true) = b = and(true, b)),
      ALL(b: boolean :: and(b, false) = false = and(false, b)),
      ALL(b: boolean :: and(b, !) = ! = and(!, b))

  MESSAGE or(b1 b2: boolean) REPLY(b3: boolean)
    WHERE ALL(b: boolean :: or(b, true) = true = or(true, b)),
      ALL(b: boolean :: or(b, false) = b = or(false, b)),
      ALL(b: boolean :: or(b, !) = ! = or(!, b))

  MESSAGE implies(b1 b2: boolean) REPLY(b3: boolean)
    WHERE b3 = or(~b1, b2), Partial_ordering(implies),
      ALL(b: boolean :: implies(b, !) = ! = implies(!, b))

  MESSAGE "<=>"(b1 b2: boolean) REPLY(b3: boolean)
    WHERE b3 = ((b1 => b2) & (b2 => b1)),
      ALL(b: boolean :: (b <=> !) = ! = (! <=> b))

  CONCEPT "&"(b1 b2: boolean) VALUE(b3: boolean)
    -- "and" extended to undefined values, not strict.
    WHERE ALL(b: boolean :: (b & true) = b = (true & b)),
      ALL(b: boolean :: (b & false) = false = (false & b)),
      (! & true) = ! = (true & !),
      (! & false) = false = (false & !),
      (! & !) = !

  CONCEPT "|"(b1 b2: boolean) VALUE(b3: boolean)
    -- "or" extended to undefined values, not strict.
    WHERE ALL(b: boolean :: (b | true) = true = (true | b)),
      ALL(b: boolean :: (b | false) = b = (false | b)),
      (! | true) = true = (true | !),
      (! | false) = ! = (false | !),
      (! | !) = !

  CONCEPT "=>"(b1 b2: boolean) VALUE(b3: boolean)
    -- "implies" extended to undefined values, not strict.
    WHERE b3 = (~b1 | b2), Partial_ordering("=>")
END