header {* Assessed Exercise I: \\ Verifying a Tautology Checker*}
(*<*)theory Taut_ex imports Main
begin
(*>*)
text{*This exercise reproduces an example first done by Boyer and Moore \cite{bm79}
during the 1970s. It concerns a topology checker for propositional logic
with only one connective, namely if-then-else.
\[ @{text"\ ::= FALSE | TRUE | VAR n | IF \ THEN \1 ELSE \2"}\]
This one connective can represent all the familiar Boolean operators, such as conjunction.
We declare a datatype @{text ifexpr} of propositional formulas, using
natural numbers for the names of propositional variables.
*}
datatype ifexpr =
FALSE
| TRUE
| VAR nat
| IF ifexpr ifexpr ifexpr
(*<*) consts eval :: "[nat set, ifexpr] => bool"
norm :: "ifexpr \ ifexpr"
normalised :: "ifexpr \ bool"
(*>*)
text{*\begin{task}A propositional formula is evaluated with
respect to an environment mapping all propositional
variables to either true or false.
A set of the ``true'' variables is one simple representation of an environment.
Define a function @{text "eval :: [nat set, ifexpr] => bool"} to evaluate
propositional formulas according to the obvious semantics of the
conditional operator.\marks{5}\end{task}
*}
text{*The tautology checker requires if-expressions to be transformed
into normal form, where @{term IF} does not appear within the condition of an if-expression.
Normal form can be reached by repeatedly replacing
\begin{quote} @{term "IF (IF p p1 p2) q r"} \qquad by \qquad
@{term "IF p (IF p1 q r) (IF p2 q r)"}
\end{quote}
until this replacement is no longer possible.
Proving termination of a function to normalise an if-expression requires
first defining the following function, which provides an upper bound on the recursive calls.
*}
fun normrank :: "ifexpr \ nat"
where
"normrank (IF p q r) =
normrank p + normrank p * normrank q + normrank p * normrank r"
| "normrank p = 1"
text{*\begin{task}
Write a function @{text "norm :: ifexpr \ ifexpr"} to transform if-expressions into normal form.
Because the proof of termination involves @{term normrank},
it is necessary to use @{text function} rather than @{text fun}.
See section 4.1 of ``Defining Recursive Functions in Isabelle/HOL'' for details.
The termination proof requires a very simple lemma about
@{term normrank}, as well as some algebraic reasoning.\marks{7}
\end{task}
*}
text{*
\begin{task}
Prove the following theorem, which states that normalisation
preserves the meaning of a formula.\marks{3}
\end{task}
*}
lemma norm_is_sound: "eval env (norm p) = eval env p"
(*<*) oops (*>*)
text{*
\begin{task}
Define a predicate @{text "normalised :: ifexpr \ bool"}
that returns true if and only if the given formula is in normal form.
Then prove the following result, which states that the normalisation function
indeed converts formulas into normal form.\marks{5}
\end{task}
*}
lemma normalised_norm: "normalised (norm p)"
(*<*) oops (*>*)
text{*
The tautology checker is defined as follows. The if-expression is assumed to be
normalised, so its condition can only be some variable @{term n}.
The sets @{term ts} and @{term fs} are assumed to be disjoint.
*}
fun (sequential) taut :: "[nat set, nat set, ifexpr] => bool"
where
"taut ts fs FALSE = False"
| "taut ts fs TRUE = True"
| "taut ts fs (VAR n) = (n \ ts)"
| "taut ts fs (IF (VAR n) q r) =
(if n \ ts then taut ts fs q
else if n \ fs then taut ts fs r
else taut (insert n ts) fs q \ taut ts (insert n fs) r)"
| "taut ts fs p = False" --{*default case (overlapping patterns)*}
text{*
The main tautology checker begins with empty sets of true and false variables.
*}
definition tautology
where "tautology p \ taut {} {} (norm p)"
text{*
\begin{task}
Prove the following theorem, which states that any formula @{term p}
accepted by the tautology checker evaluates to true.
Hint: this will require a lemma to be proved by induction, describing the behaviour of
@{term "taut ts fs p"}, assuming @{term "normalised p"};
you will need to find the right relationships among
@{term env}, @{term ts} and @{term fs}.\marks{13}
\end{task}
*}
theorem tautology_sound: "tautology p \ eval env p"
(*<*) oops (*>*)
text{*
\begin{task}
Prove the following completeness theorem: any normalised formula @{term p}
such that @{term "eval env p"} evaluates to true for all @{term"env"} will be
accepted by the tautology checker.
Hint: as in the previous task.\marks{17}
\end{task}
*}
theorem tautology_complete: "(\env. eval env p) \ tautology p"
(*<*) oops (*>*)
text{*\checkmarks*}
(*<*)
end
(*>*)