* algebra/boolean.spad.pamphlet (PropositionalFormulaFunctions1): New.

	(PropositionalFormulaFunctions2): Likewise.

1 files changed, 80 insertions, 1 deletions

diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index 15071693..9be8f2a3 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -246,6 +246,81 @@ PropositionalFormula(T: SetCategory): Public == Private where
 
 @
 
+<<package PROPFUN1 PropositionalFormulaFunctions1>>=
+)abbrev package PROPFUN1 PropositionalFormulaFunctions1
+++ Author: Gabriel Dos Reis
+++ Date Created: April 03, 2010
+++ Date Last Modified: April 03, 2010
+++ Description:
+++   This package collects unary functions operating on propositional
+++   formulae.
+PropositionalFormulaFunctions1(T): Public == Private where
+  T: SetCategory
+  Public == Type with
+    dual: PropositionalFormula T -> PropositionalFormula T
+      ++ \spad{dual f} returns the dual of the proposition \spad{f}.
+    terms: PropositionalFormula T -> Set T
+      ++ \spad{terms f} ++ returns the set of terms appearing in
+      ++ the formula \spad{f}.
+  Private == add
+    macro F == PropositionalFormula T
+    inline Pair(F,F)
+    dual f ==
+      f = true$F => false$F
+      f = false$F => true$F
+      isTerm f case T => f
+      (f1 := isNot f) case F => not dual f1
+      (f2 := isAnd f) case Pair(F,F) =>
+         disjunction(dual first f2, dual second f2)
+      (f2 := isOr f) case Pair(F,F) =>
+         conjunction(dual first f2, dual second f2)
+      error "formula contains `equiv' or `implies'"
+    terms f ==
+      (t := isTerm f) case T => { t }
+      (f1 := isNot f) case F => terms f1
+      (f2 := isAnd f) case Pair(F,F) =>
+         union(terms first f2, terms second f2)
+      (f2 := isOr f) case Pair(F,F) =>
+         union(terms first f2, terms second f2)
+      empty()$Set(T)
+@
+
+<<package PROPFUN2 PropositionalFormulaFunctions2>>=
+)abbrev package PROPFUN2 PropositionalFormulaFunctions2
+++ Author: Gabriel Dos Reis
+++ Date Created: April 03, 2010
+++ Date Last Modified: April 03, 2010
+++ Description:
+++   This package collects binary functions operating on propositional
+++   formulae.
+PropositionalFormulaFunctions2(S,T): Public == Private where
+  S: SetCategory
+  T: SetCategory
+  Public == Type with
+    map: (S -> T, PropositionalFormula S) -> PropositionalFormula T
+      ++ \spad{map(f,x)} returns a propositional formula where
+      ++ all terms in \spad{x} have been replaced by the result
+      ++ of applying the function \spad{f} to them.
+  Private == add
+    macro FS == PropositionalFormula S
+    macro FT == PropositionalFormula T
+    map(f,x) ==
+      x = true$FS => true$FT
+      x = false$FS => false$FT
+      (t := isTerm x) case S => f(t)::FT
+      (f1 := isNot x) case FS => not map(f,f1)
+      (f2 := isAnd x) case Pair(FS,FS) =>
+         conjunction(map(f,first f2), map(f,second f2))
+      (f2 := isOr x) case Pair(FS,FS) =>
+         disjunction(map(f,first f2), map(f,second f2))
+      (f2 := isImplies x) case Pair(FS,FS) =>
+         implies(map(f,first f2), map(f,second f2))
+      (f2 := isEquiv x) case Pair(FS,FS) =>
+         equiv(map(f,first f2), map(f,second f2))
+      error "invalid propositional formula"
+
+@
+
 \section{domain REF Reference}
 <<domain REF Reference>>=
 )abbrev domain REF Reference
@@ -532,7 +607,7 @@ KleeneTrivalentLogic(): Public == Private where
 <<license>>=
 --Copyright (c) 1991-2002, The Numerical Algorithms Group Ltd.
 --All rights reserved.
---Copyright (C) 2007-2009, Gabriel Dos Reis.
+--Copyright (C) 2007-2010, Gabriel Dos Reis.
 --All rights reserved.
 --
 --Redistribution and use in source and binary forms, with or without
@@ -571,8 +646,12 @@ KleeneTrivalentLogic(): Public == Private where
 <<domain BOOLEAN Boolean>>
 <<domain IBITS IndexedBits>>
 <<domain BITS Bits>>
+
 <<category PROPLOG PropositionalLogic>>
 <<domain PROPFRML PropositionalFormula>>
+<<package PROPFUN1 PropositionalFormulaFunctions1>>
+<<package PROPFUN2 PropositionalFormulaFunctions2>>
+
 <<domain KTVLOGIC KleeneTrivalentLogic>>
 
 @