Page 311 of 800
| 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 
.
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 
and cache 
. For proofs defined by
PA proof of 3.2l : ...
the proof is ignored but the cache 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:
Thus, proofs stated within 
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.
| Page 311 of 800 | Search logiweb.eu |