HOL Exercise 9: Conversions and Arithmetic

Before beginning these exercises load the numLib library to define the type num of natural numbers in HOL.

Conversions

A common class of inference rules in HOL are called conversions. Conversions have the type term -> thm, which is usually abbreviated to conv. All conversions take a term t and return a theorem of the form |- t = t'. For example, BETA_CONV implements the following rule:

-------------------------- BETA_CONV (Term `(\v. t[v]) x`)
 |- (\v. t[v]) x = t[x/v]

Try evaluating the following ML expression.

BETA_CONV (Term `(\v. 1 + v) 0`);

Since conversions prove equalities, they are useful in both forwards and backwards proofs. The function CONV_RULE changes a conversion into an inference rule. For example, CONV_RULE BETA_CONV implements the following inference rule:

 |- (\v. t[v]) x
----------------- (CONV_RULE BETA_CONV)
    |- t[x/v]

Use CONV_TAC and BETA_CONV to solve the following trivial goal:

(\v. v) T

Lookup _CONV using the LAL online help system to find a list of all the conversions available in HOL, and read the documentation on a few of them to figure out what they do. For example, check out LEFT_IMP_EXISTS_CONV.

Conversionals

Term `(\v. v 1) (\w.w + 0)`

You could also have used (REPEATC BETA_CONV) to do the same job.

By far the most useful conversionals are the depth conversionals. These a functions that take a conversion and a term and then traverse the term applying the conversion to its subterms. Consider the following term:

1 + (\v. v + 1) 0

The HOL Reduce Library

Proving some trivial arithmetic properties in HOL can be a real pain. However, HOL also provides various libraries that provide extra functionality for tackling particular kinds of problems. Two of these, the reduce and arith libraries are particularly helpful with arithmetic. Load reduceLib now.

The reduce library defines a a conversion, reduceLib.RED_CONV that will evaluate and arithmetic or boolean expression. For example, try reduceLib.RED_CONV on Term `2 EXP 8`.

The library defines several other functions in terms of RED_CONV:

• REDUCE_CONV = DEPTH_CONV RED_CONV
• REDUCE_RULE = CONV_RULE REDUCE_CONV
• REDUCE_TAC = CONV_TAC REDUCE_CONV

An Adder Fragment

Lets now work though the definition and verification of a simple circuit that adds two 1-bit binary inputs and produces a 1-bit binary output. A simple adder with no carry. First we need to define a function to give a numeric interpretation to the value of a wire. Using the conditional expression notation (a => b | c) define a function BVAL that takes a wire (a boolean) and returns 1 if the wire is high (true) and 0 if the wire is low (false).

Next, use BVAL to define a predicate ADD_FRAG a b c which is true when c is the sum of a and b, mod two. Be careful with your brackets here. The mod operator is written as infix MOD in HOL.

Give an implementation for ADD_FRAG using the gates you have already proved correct, and then prove your implementation of ADD_FRAG correct. The proof should be an easy application of rewriting, reduction (using REDUCE_TAC), and brute force boolean case-analysis.