Exercise 8: Return to CMOS

Proving the NOT Gate by Hand

Using the experience you gained in completing Exercise 7, verify the CMOS Not-Gate described in Exercise 6 again; this time without using the Meson library.

Hint: In addition to the tactics explored in Exercise 7, I found the tactic ASM_CASES_TAC useful for this proof.

Writing your First Tactic

We need bigger guns, bigger f#*king guns!
Rutger Hauer's sidekick in `Split Second'

Having completed your proof of the gate, you should now go on to use the tactic building functions (tacticals) REPEAT and THEN to join together the tactics you used to prove the NOT gate into one big tactic that can prove the goal in one step. Bind your tactic to the ML identifier NOT_IMP_TAC.

Note: TAC₁ THEN TAC₂ applies TAC₁ to a goal, and then TAC₂ to all the subgoals that produces.

The function prove: term * tactic -> thm takes a term and a tactic that proves it, and then returns the corresponding theorem. Now that you have defined NOT_IMP_TAC, you should be able to evaluate the following code:

val NOT_IMP_THM = 
    prove(Term `!x y. NOT_IMP x y ==> NOT x y`,
          NOT_IMP_TAC);

Another Proof of the NOT Gate

When you first proved the Not gate, you probably made use of the tactic ASM_CASES_TAC that I recommended to you. Try doing the proof again, but this time use a different tactic to do the boolean case analysis, namely BOOL_CASES_TAC.

Hint: BOOL_CASES_TAC effects only the variables in the conclusion of a goal, so use it before you do too much STRIP_TACing.

A Tactic of General Use

For the proof of the NOT gate, and presumably for similar proofs, it might be nice to have a tactic that would attack a goal of the form `!x:bool. P[x]' by doing a boolean case analysis on `x' to yield two subgoals: `P[T]' and `P[F]'. This tactic, lets call it GEN_BOOL_CASES_TAC, would be essentially the same as GEN_TAC THEN (BOOL_CASES_TAC (Term `x:bool`)), but would be more flexible because it would take the name of the bound variable out of the goal, rather than requiring it to be `x'.

Write the tactic GEN_BOOL_CASES_TAC.

Hint: The tactic you want to write is essentially the same as GEN_TAC THEN (BOOL_CASES_TAC (Term `x:bool`)), except you want to apply BOOL_CASES_TAC to the bound variable of the goal rather than to `x'.

Hint: We can, of course, write the tactic GEN_TAC THEN (BOOL_CASES_TAC (Term `x:bool`)) equivalently as follows:

(fn (asms,cncl) =>
  (GEN_TAC THEN (BOOL_CASES_TAC (Term `x:bool`)))
  (asms,cncl)):tactic;  

Hint: The function dest_forall will destruct a universal quantifier so that you can extract the bound variable.

Prove the CMOS NAND Gate

Extend the work you did in Exercise 5 now by defining predicates in HOL that describe the required behaviour of a NAND gate, and the CMOS implementation of a NAND gate. Now, prove your NAND gate implementation correct. You will probably want to use GEN_BOOL_CASES_TAC in your proof. Bind the theorem stating the correctness of the NAND gate to an ML value called NAND_IMP_THM. You can retrieve this theorem after completing an interactive proof by calling top_thm ().

A General Basic CMOS Tactic

By examining your proofs of the CMOS NOT gate and CMOS NAND gate, you should be able to come up with a general scheme for a tactic that would prove both goals. You should be able to isolate the differences down to the point where the only difference is that the tactic required to prove the NOT gate rewrites with the theorems NOT_DEF and NOT_IMP_DEF, where the tactic to prove the NAND gate rewrites with NAND_DEF and NAND_IMP_DEF.

Implement a general function BASIC_CMOS_TAC: thm list -> tactic that will take a list of theorems, and which can then be used to prove the correctness of both the CMOS NOT implementation and the CMOS NAND implementation.

Prove the CMOS NOR Gate

Define predicates in HOL that describe the required behaviour of a NOR gate, and the CMOS implementation of a NOR gate. Now, prove your NOR gate implementation correct. The tactic BASIC_CMOS_TAC should do the job in one hit if you give it the right theorems. If it doesn't, then generalise it further so that it will (and check that the new version can still prove the NOT gate and NAND gate in one hit as well). Bind the theorem stating the correctness of the NOR gate to the ML value NOR_IMP_THM.

A Slightly Higher Level of Design

The NOT, NOR and NAND gates are the basic gates of CMOS technology. Other, more elaborate, logic circuits are designed using these gates as primitives. We would now like to design other circuits in terms of NOT, NAND and NOR gates, but still prove the implementation of these more abstract designs correct right down to their implementation in CMOS transistors. For example, consider the following implementation of an AND gate:

val AND_IMP_DEF = 
    new_definition(
      "AND_IMP_DEF",
      (Term `AND_IMP a b c =
             ?x. (NAND_IMP a b x) /\ (NOT_IMP x c)`));

Note that the description is in terms of NAND_IMP and NOT_IMP, not just NAND and NOT. In this way we are able to abstractly describe the implementation of an AND gate in terms of CMOS transistors.

Define HOL predicates that describe the desired behaviour of AND, OR and XOR gates, and other predicates that abstractly describe basic CMOS implementations of these gates.

Proofs About Higher Level Designs

The work we have done to construct a set of primitive CMOS gates not only makes our designs more abstract, but also our proofs. By using the theorems we proved about the correctness of the basic CMOS gates we can avoid reasoning at the level of transistors, and we can also avoid using boolean case analysis in our proofs.

As a first step to writing a general tactic for proving simple designs using the CMOS basic gates, define the list BASIC_CMOS_DEFS as follows:

val BASIC_CMOS_DEFS = [NOT_DEF,NAND_DEF,NOR_DEF];

Now, begin the proof of correctness of the AND gate, and use the following tactic as your opening gambit:

(REWRITE_TAC [AND_IMP_DEF,AND_DEF]) THEN 
(REPEAT STRIP_TAC)

``c = a /\ b``
____________________________
    ``NAND_IMP a b x``
    ``NOT_IMP x c``

Use backup (b ()) to undo this proof step and get back to the goal above. Lets think about a more general solution in the form of a tactic that would augment every assumption about an implementation with one about the corresponding specification. That is, something that would add, in one step, the assumptions NAND a b x and NOT x c to this goal and do the analogous thing for other goals. You should be able to achieve this effect using the function MAP_EVERY and the list BASIC_CMOS_IMPS.

The next step of the approach can be accomplished by doing the same thing with the list BASIC_CMOS_DEFS. It should be easy to finish the proof now.

Another CMOS Tactic

Collect together the steps you used to prove the AND gate correct into a single tactic. The only thing that should be specific to the AND gate about this tactic is the fact that we began by rewriting with AND_IMP_DEF and AND_DEF. Factor this out of your tactic by turning it into a function that takes a list of theorems to rewrite with, and call the resulting tactic ABS_CMOS_TAC.

Proving the OR and XOR gate

Use ABS_CMOS_TAC to prove the correctness of your designs for OR and XOR gates in one hit. If it doesn't work, then you may need to generalise your tactic.