sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c P Source #

toConstr :: P -> Constr Source #

dataTypeOf :: P -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c P) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c P) Source #

gmapT :: (forall b. Data b => b -> b) -> P -> P Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> P -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> P -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> P -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> P -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> P -> m P Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> P -> m P Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> P -> m P Source #

Read P Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods readsPrec :: Int -> ReadS P Source # readList :: ReadS [P] Source # readPrec :: ReadPrec P Source # readListPrec :: ReadPrec [P] Source #
Show P Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Drinker Methods showsPrec :: Int -> P -> ShowS Source # show :: P -> String Source # showList :: [P] -> ShowS Source #
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.