(*
$Id: ex.thy,v 1.3 2008/07/04 15:37:41 nipkow Exp $
Author: Stefan Berghofer, Tobias Nipkow
*)
header {* Representation of Propositional Formulae by Polynomials *}
(*<*) theory ex imports Main begin (*>*)
text {*
Let the following data type for propositional formulae be given:
*}
datatype form = T | Var nat | And form form | Xor form form
text {*
Here @{term "T"} denotes a formula that is always true, @{term "Var n"} denotes
a propositional variable, its name given by a natural number, @{term "And f1
f2"} denotes the AND combination, and @{term "Xor f1 f2"} the XOR (exclusive or)
combination of two formulae. A constructor @{term "F"} for a formula that is
always false is not necessary, since @{term "F"} can be expressed by @{term "Xor
T T"}.
{\bf Exercise 1:} Define a function
*}
(*<*)consts(*>*) evalf :: "(nat \ bool) \ form \ bool"
text {*
that evaluates a formula under a given variable assignment.
*}
text {*
Propositional formulae can be represented by so-called {\it polynomials}. A
polynomial is a list of lists of propositional variables, i.e.\ an element of
type @{typ "nat list list"}. The inner lists (the so-called {\it monomials})
are interpreted as conjunctive combination of variables, whereas the outer list
is interpreted as exclusive-or combination of the inner lists.
{\bf Exercise 2:} Define two functions
*}
(*<*)consts(*>*)
evalm :: "(nat \ bool) \ nat list \ bool"
evalp :: "(nat \ bool) \ nat list list \ bool"
text {*
for evaluation of monomials and polynomials under a given variable assignment.
In particular think about how empty lists have to be evaluated.
*}
text {*
{\bf Exercise 3:} Define a function
*}
(*<*)consts(*>*) poly :: "form \ nat list list"
text {*
that turns a formula into a polynomial. You will need an auxiliary function
*}
(*<*)consts(*>*) mulpp :: "nat list list \ nat list list \ nat list list"
text {*
to ``multiply'' two polynomials, i.e.\ to compute
\[
((v^1_1 \mathbin{\odot} \cdots \mathbin{\odot} v^1_{m_1}) \mathbin{\oplus} \cdots \mathbin{\oplus} (v^k_1 \mathbin{\odot} \cdots \mathbin{\odot} v^k_{m_k})) \mathbin{\odot}
((w^1_1 \mathbin{\odot} \cdots \mathbin{\odot} w^1_{n_1}) \mathbin{\oplus} \cdots \mathbin{\oplus} (w^l_1 \mathbin{\odot} \cdots \mathbin{\odot} w^l_{n_l}))
\]
where $\mathbin{\oplus}$ denotes ``exclusive or'', and $\mathbin{\odot}$ denotes
``and''. This is done using the usual calculation rules for addition and
multiplication.
*}
text {*
{\bf Exercise 4:} Now show correctness of your function @{term "poly"}:
*}
theorem poly_correct: "evalf e f = evalp e (poly f)"
(*<*) oops (*>*)
text {*
It is useful to prove a similar correctness theorem for @{term "mulpp"} first.
*}
(*<*) end (*>*)