diff options
Diffstat (limited to 'src/algebra/boolean.spad.pamphlet')
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet index 032655ee..15071693 100644 --- a/src/algebra/boolean.spad.pamphlet +++ b/src/algebra/boolean.spad.pamphlet @@ -76,6 +76,14 @@ PropositionalFormula(T: SetCategory): Public == Private where ++ \spad{v case Pair(%,%)} holds if the formula \spad{f} ++ is an equivalence formula. + conjunction: (%,%) -> % + ++ \spad{conjunction(p,q)} returns a formula denoting the + ++ conjunction of \spad{p} and \spad{q}. + + disjunction: (%,%) -> % + ++ \spad{disjunction(p,q)} returns a formula denoting the + ++ disjunction of \spad{p} and \spad{q}. + Private == add Rep == Union(T, Kernel %) import Kernel % @@ -85,7 +93,7 @@ PropositionalFormula(T: SetCategory): Public == Private where -- Local names for proposition logical operators macro NOT == '%not macro AND == '%and - macro OR == '%OR + macro OR == '%or macro IMP == '%implies macro EQV == '%equiv @@ -102,12 +110,16 @@ PropositionalFormula(T: SetCategory): Public == Private where not p == per kernel(operator(NOT, 1::Arity), [p], 1 + level p) - p and q == + conjunction(p,q) == per kernel(operator(AND, 2), [p, q], 1 + max(level p, level q)) - p or q == + p and q == conjunction(p,q) + + disjunction(p,q) == per kernel(operator(OR, 2), [p, q], 1 + max(level p, level q)) + p or q == disjunction(p,q) + implies(p,q) == per kernel(operator(IMP, 2), [p, q], 1 + max(level p, level q)) |