6.7.12 Implementation of lemmas

Prev Up Next Page 98 of 800 Search internet

Now take a look at the extract of multzero and go to the list of definition of 3.2l. The definitions read:

lgcdef lgcname of 3.2l as "3.2l" enddef
This is the name definition generated by ""N.
lgcdef lgccharge of 3.2l as "0" enddef
This is the charge definition generated by ""C.
Define tex show of 3.2l as " \mathbf{3.2l}" end define
This is what makes 3.2l a bold assumption.
define statement of 3.2l as PA infer f.allfunc \ x . [[0 * x] = 0] end define
PA lemma 3.2l : all x : 0 * x = 0 end lemma macro expands into two definition. This is one of the two definitions and it is the one which indicates what the lemma states. For an explanation of f.allfunc see the section on representation of object quantifiers.
define unitac of 3.2l as \ u . unitac-lemma ( u ) end define
This is the other of the two definitions Lemma 3.2l macro expands into. The definition indicates that 3.2l behaves as a lemma during unitac expansion. The behavior of lemmas is slightly different from e.g. rules and have to be treated slightly differently. As an example, Lemma 3.2l has form PA infer all x : 0 * x = 0 so the unification tactic has to do meta modus ponens to get rid of the PA premise.
define proof of 3.2l as \ p . \ c . taceval1 ( quote PA end quote , ... , c )
This is what the proof of 3.2l macro expands into. It is the macro expander which installs the tactic evaluator taceval1 in the proof. During proof checking, the proof checker calls seqeval* ( x , c ) where c is the cache of the page and x comes from the codex of the page. For each proof in x, seqeval* ( x , c ) calls eval ( x , true , c ) to get the value of the proof and then applies the value to the proof p and the cache c, leading to evaluation of the tactic evaluator taceval1. Then seqeval* ( x , c ) calls seqeval ( q , c ) on the return value q from tactic evaluation to see what the proof proves.

statement, unitac, and proof aspects are defined thus on the check page:

   eager message define statement as "statement/kg" end define
   eager message define proof as "proof/kg" end define
   eager message define unitac as "unitac/kg" end define

As an example, define unitac of 3.2l as \ u . unitac-lemma ( u ) end define defines the !"unitac/kg" aspect of 3.2l. The statement/kg, proof/kg, and unitac/kg aspects are non-reserved because they contain a slash each. In general, an aspect is reserved if it contains reserved characters only. The reserved characters are the small letters a to z of the English alphabet plus the space character. An aspect is non-reserved if it contains at least one non-reserved character such as a capital letter, a digit, or some other character. By convention, reserved aspects are reserved for future extensions of Logiweb. Since the Logiweb proof checker is not hard-coded into Logiweb, it does not use reserved aspects.

Prev Up Next Page 98 of 800 Search logiweb.eu

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