8.3.2 Proof level tactics

Prev Up Next Page 311 of 800 Search internet

The proof on the previous page has form

   PA proof of 3.2l : ...

Before such a proof is verified, it is macro expanded and tactic expanded. To see the macro expanded version of the proof of 3.2l, go to the multzero page, click on 'extract', and scroll down to the proof definition of 3.2l.

The right hand side of the proof definition of 3.2l reads

   \ p . \ c . taceval1 ( quote PA end quote , quote ... end quote , c )

where the ellipsis ... is the macro expanded version of the body of the proof.

The proof is tactic expanded by evaluating the right hand side of the proof definition and applying the result to the proof p and cache c. For proofs defined by

   PA proof of 3.2l : ...

the proof p is ignored but the cache c is passed to taceval1. The taceval1 function gets access to the proof through its second argument which contains the macro expanded version of the proof.

You cannot see the tactic expanded version anywhere. As soon as the tactic expanded version has been generated, it is passed on to the verifier for verification and is then discarded.

What the taceval1 function does is governed by the following definition on the Peano page:

tactic define PA as \ u . tactic-FOL ( u ) end define

Thus, proofs stated within PA are tactic expanded in a way suited for first order logic.

In general, the construct

   T proof of L : P

constructs a proof which is tactic expanded as specified by the tactic of the theory T. Usually, such a tactic will start by assuming T so that all axioms and inference rules of T become available.

Prev Up Next Page 311 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05