Exercise 6: Proving the CMOS NOT Gate

To start these exercises you first need to get back to the state you were in at the end of Exercise 5. At this point we had developed a little theory of the primitive CMOS circuit components, given a specification of a not gate, and proposed a CMOS implementation for it. We would now like to prove that implementation correct.

Setting the Goal

Goal directed proofs in HOL are managed as a stack of goals that remain to be solved to complete the proof. A new interactive goal-directed proof of some property P is started by creating a new goal stack with the single outstanding goal P. This is done by evaluating the ML expression `g `P''. For example, enter the following text at the HOL prompt to start the proof of correctness for the CMOS not gate:

g `!a b. NOT_IMP a b ==> NOT a b`;

Expanding Tactics and Backing Up

You progress a goal-directed proof in HOL by expanding a tactic on the goal you are trying to prove. This will either solve the goal, or give you a new set of (hopefully simpler) goals to prove. The old goal is popped off the stack of outstanding goals, and any new goals are pushed on. To expand the tactic tactic on the current goal, simply evaluate the expression `e tactic'.

The goal you are trying to prove has the general form of !x. P[x]. A proof of P[x] that makes no assumptions about the value of the variable x can always be generalised to a proof of !x. P[x]. Therefore, we can reduce a goal of the form !x. P[x] to one of the form P[x], which is done using the tactic GEN_TAC. Expand GEN_TAC on the current goal by evaluating the expression `e GEN_TAC'.

After expanding GEN_TAC the goal still has the form !x. P[x], because the original goal was quantified twice! So, apply the tactic again. When this is done the goal no longer has the form of a universal quantification, so if you try expanding the tactic GEN_TAC a third time it will fail. Try it out.

If you decide that the last tactic expansion you performed wasn't such a good idea after all, you can back up one step in the proof by evaluating the ML expression `b ()'. Try this now to undo the last generalisation tactic you expanded, then redo it again because it actually is a good idea at this stage in the proof.

A Little Rewriting

By now you should have reduced the proof to the following single outstanding goal:

NOT_IMP a b ==> NOT a b

In Exercise 5 we bound the definitions of NOT and NOT_IMP in the ML identifiers NOT_DEF and NOT_IMP_DEF respectively. Evaluate the expressions NOT_DEF and NOT_IMP_DEF now so that you can see what they look like. Notice that they are equations, instances of the left-hand sides of which feature prominently in our current goal. We can rewrite the current goal with these definitions as follows:

e (REWRITE_TAC [NOT_IMP_DEF,NOT_DEF]);

By now you should be faced with the following goal:

(?x y. PWR x /\ GND y /\ PTRAN a x b /\ NTRAN a y b) ==> (b = ~a)

Use REWRITE_TAC to replace instances of PWR, GND, PTRAN and NTRAN in the goal with their definitions.

Bringing Out the Big Guns

We have now eliminated all the definitions to obtain the goal

(?x y. x /\ ~y /\ (~a ==> (x = b)) /\ (a ==> (y = b))) ==> (b = ~a)

The theorem that results from a proof can be retrieved by evaluating `top_thm ()'. Bind this theorem to the ML identifier NOT_IMP_THM for later use.

Of course, you'll also have to learn to do proofs without the Meson library so you will know what to do when it can't solve your goal for you. We'll start building those skills in Exercise 7.