Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	Safe-Inferred
Language	Haskell2010

OAlg.Data.Boolean.Proposition

Contents

Tautologies
- Not
- And
- Or
Impl
Eqvl
Lazy

Description

propositions on boolean structures which must always be true, i.e. tautologies. They serve also to describe the semantic of the boolean operators.

Synopsis

prpBool :: Statement
prpBoolTautologies :: Statement
prpTautologies :: Boolean b => (b -> Statement) -> X b -> X [b] -> Statement
prpNotNot :: Boolean b => b -> b
prpAndAssoc :: Boolean b => b -> b -> b -> b
prpAndOr :: Boolean b => b -> b -> b -> b
prpAndTrue :: Boolean b => b -> b
prpAnd0 :: Boolean b => b
prpAnds :: Boolean b => b -> [b] -> b
prpOrAssoc :: Boolean b => b -> b -> b -> b
prpOrAnd :: Boolean b => b -> b -> b -> b
prpOr0 :: Boolean b => b
prpOrs :: Boolean b => b -> [b] -> b
prpImplRefl :: Boolean b => b -> b
prpImplFalseEverything :: Boolean b => b -> b
prpImplCurry :: Boolean b => b -> b -> b -> b
prpImplTransitive :: Boolean b => b -> b -> b -> b
prpEqvlAnd :: Boolean b => b -> b -> b
prpLazy :: Boolean b => (b -> Statement) -> Statement
prpLazyAnd :: Boolean b => b
prpLazyOr :: Boolean b => b
prpLazyImpl :: Boolean b => b

Documentation

prpBool :: Statement Source #

validity of the Boolean structure of Bool.

prpBoolTautologies :: Statement Source #

tautologies for Bool.

Tautologies

prpTautologies :: Boolean b => (b -> Statement) -> X b -> X [b] -> Statement Source #

tautologies on boolean structures.

Not

prpNotNot :: Boolean b => b -> b Source #

for all p holds: not (not p) <~> p.

And

prpAndAssoc :: Boolean b => b -> b -> b -> b Source #

for all a, b and c holds: (a && b) && c <~> a && (b && c).

prpAndOr :: Boolean b => b -> b -> b -> b Source #

for all a, b and c holds: (a && b) || c <~> (a || c) && (b || c).

prpAndTrue :: Boolean b => b -> b Source #

for all p holds: true && p <~> p.

prpAnd0 :: Boolean b => b Source #

and [] <~> true.

prpAnds :: Boolean b => b -> [b] -> b Source #

for all a and as holds: and (a:as) <~> a && and as.

Or

prpOrAssoc :: Boolean b => b -> b -> b -> b Source #

for all a, b and c holds: (a || b) || c <~> a || (b || c).

prpOrAnd :: Boolean b => b -> b -> b -> b Source #

for all a, b and c holds: (a || b) && c <~> (a && c) || (b && c).

prpOr0 :: Boolean b => b Source #

or [] <~> false.

prpOrs :: Boolean b => b -> [b] -> b Source #

for all a and as holds: or (a:as) <~> a || or as.

Impl

prpImplRefl :: Boolean b => b -> b Source #

for all p holds: p ~> p.

prpImplFalseEverything :: Boolean b => b -> b Source #

for all p holds: false ~> (p <~> true).

i.e. a false premisis implies everithing.

prpImplCurry :: Boolean b => b -> b -> b -> b Source #

for all a, b and c holds: ((a && b) ~> c) <~> (a ~> b ~> c).

prpImplTransitive :: Boolean b => b -> b -> b -> b Source #

for all a, b and c holds: (a ~> b) && (b ~> c) ~> (a ~> c).

Eqvl

prpEqvlAnd :: Boolean b => b -> b -> b Source #

for all a and b holds: (a <~> b) <~> ((a ~> b) && (b ~> a)).

Lazy

prpLazy :: Boolean b => (b -> Statement) -> Statement Source #

laziness of and, or and (~>).

prpLazyAnd :: Boolean b => b Source #

lazy evaluation of &&, i.e. false && undefined <~> false.

Note (undefined && false) evaluates to an exception!

prpLazyOr :: Boolean b => b Source #

lazy evaluationof ||, i.e. true || undefined.

prpLazyImpl :: Boolean b => b Source #

lazy evaluation of ~>, i.e. false :=> undefined.