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
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

Data P Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> P -> c P # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c P # toConstr :: P -> Constr # dataTypeOf :: P -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c P) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c P) # gmapT :: (forall b. Data b => b -> b) -> P -> P # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> P -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> P -> r # gmapQ :: (forall d. Data d => d -> u) -> P -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> P -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> P -> m P # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> P -> m P # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> P -> m P #
Read P Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods readsPrec :: Int -> ReadS P # readList :: ReadS [P] # readPrec :: ReadPrec P # readListPrec :: ReadPrec [P] #
Show P Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods showsPrec :: Int -> P -> ShowS # show :: P -> String # showList :: [P] -> ShowS #
SymVal P Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV P) Source # literal :: P -> SBV P Source # fromCV :: CV -> P Source # isConcretely :: SBV P -> (P -> Bool) -> Bool 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 # 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 # isUserSort :: P -> Bool Source # isChar :: P -> Bool Source # isString :: P -> Bool Source # isList :: P -> Bool Source # isSet :: P -> Bool Source # isTuple :: P -> Bool Source # isMaybe :: P -> Bool Source # isEither :: P -> Bool Source # showType :: P -> String Source #
SatModel P Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods parseCVs :: [CV] -> Maybe (P, [CV]) Source # cvtModel :: (P -> Maybe b) -> Maybe (P, [CV]) -> Maybe (b, [CV]) Source #

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.