6.7.12 Implementation of lemmas

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 a bold assumption.

define statement of 3.2l as PA infer f.allfunc \ x . [[0 * x] = 0] end define

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 so the unification tactic has to do meta modus ponens to get rid of the 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 where is the cache of the page and comes from the codex of the page. For each proof in , calls to get the value of the proof and then applies the value to the proof and the cache , leading to evaluation of the tactic evaluator taceval1. Then calls on the return value 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, defines the aspect of . 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.

Page 98 of 800

Search logiweb.eu