Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Puzzles.Drinker

Description

SBV proof of the drinker paradox: http://en.wikipedia.org/wiki/Drinker_paradox

Let P be the non-empty set of people in a bar. The theorem says if there is somebody drinking in the bar, then everybody is drinking in the bar. The general formulation is:

    ∃x : P. D(x) -> ∀y : P. D(y)

Synopsis

data P
cv2P :: String -> [CV] -> P
_undefiner_P :: a
type SP = SBV P
d :: SP -> SBool
drinker :: IO ThmResult

Documentation

data P Source #

Declare a carrier data-type in Haskell named P, representing all the people in a bar.

Instances

Instances details

Arbitrary P Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods arbitrary :: Gen P # shrink :: P -> [P] #
SymVal P Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV P) Source # mkSymValInit :: State -> SBV P -> IO () Source # literal :: P -> SBV P Source # fromCV :: CV -> P Source # isConcretely :: SBV P -> (P -> Bool) -> Bool Source # minMaxBound :: Maybe (P, P) Source # free :: MonadSymbolic m => String -> m (SBV P) Source # free_ :: MonadSymbolic m => m (SBV P) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV P] Source # symbolic :: MonadSymbolic m => String -> m (SBV P) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV P] Source # unliteral :: SBV P -> Maybe P Source # unlitCV :: SBV P -> Maybe (Kind, CVal) Source # isConcrete :: SBV P -> Bool Source # isSymbolic :: SBV P -> Bool Source #
HasKind P Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods kindOf :: P -> Kind Source # hasSign :: P -> Bool Source # intSizeOf :: P -> Int Source # isBoolean :: P -> Bool Source # isBounded :: P -> Bool Source # isReal :: P -> Bool Source # isFloat :: P -> Bool Source # isDouble :: P -> Bool Source # isRational :: P -> Bool Source # isFP :: P -> Bool Source # isUnbounded :: P -> Bool Source # isADT :: P -> Bool Source # isChar :: P -> Bool Source # isString :: P -> Bool Source # isList :: P -> Bool Source # isSet :: P -> Bool Source # isTuple :: P -> Bool Source # isArray :: P -> Bool Source # isRoundingMode :: P -> Bool Source # isUninterpreted :: P -> Bool Source # showType :: P -> String Source #

cv2P :: String -> [CV] -> P Source #

Conversion from SMT values to P values.

_undefiner_P :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SP = SBV P Source #

Symbolic version of the type P.

d :: SP -> SBool Source #

Declare the uninterpret function d, standing for drinking. For each person, this function assigns whether they are drinking; but is otherwise completely uninterpreted. (i.e., our theorem will be true for all such functions.)

drinker :: IO ThmResult Source #

Formulate the drinkers paradox, if some one is drinking, then everyone is!

>>> drinker
Q.E.D.