public class Theorem extends Assrt
Theorem is distinguished from Axiom by having a... proof, as well as an OptFrame (Optional Frame).
A Metamath "proof" is simply an array of Stmt labels, which in mmj equates to
Stmt[]
. The proof is in RPN, Reverse Polish Notation format and when
fed into the Proof Verifier engine recreates the Theorem's Formula -- that's
all a "proof" is, assuming it follows the "rules". See Metamath.pdf and
mmj.verify.VerifyProofs.java for more info.
The proof need not be complete, and may consist of nothing but a "?" step in
the source file -- which is stored as a null
proof step in mmj.
Non-missing Proof steps must refer to "active" Hyp's or Assrt's with Stmt.seq
< Theorem.seq. Verification of a proof is not performed within Theorem --
that is handled by mmj.verify.VerifyProofs (in theory, Proof Verification
could be performed at this time, but since most proofs are static and the
Proof Verification process is very CPU intensive, normal Metamath practice is
to verify proofs only when the user requests it.)
An OptFrame consists of those Hyp's and DjVars that are "in scope" but are not present in the the MandFrame (Mandatory Frame). Together the OptFrame and MandFrame comprise what Metamath.pdf terms the "Extended Frame".
(As a side note, the "validity" of a proof has nothing to do with the Theorem being reference-able by subsequent Theorems' proofs. Nor does Metamath formally require that every LogHyp in scope be referenced within a Theorem's proof. A warning message could be presented for the latter situation, but has not yet been coded.)
logHypArray, mandFrame, NBR_LOG_HYP_SEQ, varHypArray
DESC_NBR_PROOF_REFS, exprParseTree, LABEL, logHypsL1HiLoKey, logHypsMaxDepth, nbrProofRefs
chapterNbr, description, isTempObject, SECTION_AND_MOBJ_NBR, sectionMObjNbr, sectionNbr, seq, SEQ
Constructor and Description |
---|
Theorem(int seq,
java.util.List<ScopeDef> scopeDefList,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl,
java.lang.String labelS,
int column,
java.lang.String typS,
java.util.List<java.lang.String> symList,
java.util.List<java.lang.String> proofList,
BlockList proofBlockList,
ProofCompression proofCompression,
Messages messages)
Construct Theorem using the entire enchilada from mmj.mmio.SrcStmt.java
including compressed proof blocks.
|
Theorem(int seq,
java.util.List<ScopeDef> scopeDefList,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl,
java.lang.String labelS,
int column,
java.lang.String typS,
java.util.List<java.lang.String> symList,
java.util.List<java.lang.String> proofList,
Messages messages)
Construct Theorem using the entire enchilada from mmj.mmio.SrcStmt.java,
plus a few condiments.
|
Modifier and Type | Method and Description |
---|---|
ParseTree.RPNStep[] |
editProofListDefAndActive(java.util.Map<java.lang.String,Stmt> stmtTbl,
java.util.List<java.lang.String> proofList)
Validates each proof step for a proof being loaded into mmj.
|
int |
getColumn()
Get the starting column for the theorem.
|
ScopeFrame |
getOptFrame()
Get the Theorem's OptFrame.
|
ParseTree.RPNStep[] |
getProof()
Return Theorem's proof.
|
boolean |
isProofStepInExtendedFrame(Stmt proofStep)
Checks to see whether or not a proof step is contained in the Theorem's
Extended Frame.
|
void |
loadMandAndOptDjVarsUpdateLists(java.util.Map<java.lang.String,Sym> symTbl,
java.util.List<java.util.List<java.lang.String>> inputDjVarsStmtList,
java.util.List<DjVars> mandDjVarsUpdateList,
java.util.List<DjVars> optDjVarsUpdateList)
Utility routine for Theorem Loader to split an input list of Distinct
Variable statement symbol lists into Mandatory and Optional DjVars lists.
|
void |
mergeDjVars(java.util.List<DjVars> mandDjVarsUpdateList,
java.util.List<DjVars> optDjVarsUpdateList)
Merge existing Mandatory and Optional DjVars into the existing Mandatory
and Optional Frame data.
|
void |
proofUpdates(ParseTree.RPNStep[] newProof,
DjVars[] newDjVarsArray,
DjVars[] newOptDjVarsArray)
Applies updates made to proof related data.
|
int |
renderParsedSubExpr(java.lang.StringBuilder sb,
int maxDepth,
int maxLength,
ParseNode[] child)
Throws an IllegalArgumentException because a ParseTree for a parsed
sub-expression should contain only VarHyp and Syntax Axiom nodes.
|
void |
replaceDjVars(java.util.List<DjVars> mandDjVarsUpdateList,
java.util.List<DjVars> optDjVarsUpdateList)
Replace existing Mandatory and Optional DjVars.
|
ParseTree.RPNStep[] |
setProof(java.util.Map<java.lang.String,Stmt> stmtTbl,
java.util.List<java.lang.String> proofList)
Set Theorem's proof.
|
accumHypInList, getLogHypArray, getLogHypArrayLength, getLogHypsL1HiLoKey, getLogHypsMaxDepth, getMandFrame, getMandHypArrayLength, getMandVarHypArray, getReversePermutationForSortedHyp, getSortedLogHypArray, isActive, isExcluded, loadLogHypArray, setExcluded, setLogHypArray, setMandFrame, setMandVarHypArray, sortListIntoArray
equals, getExprParseTree, getExprRPN, getFormula, getLabel, getNbrProofRefs, getTyp, hashCode, incrementNbrProofRefs, initNbrProofRefs, resetLogHypsL1HiLoKey, resetLogHypsMaxDepth, setExprParseTree, setExprRPN, setLogHypsL1HiLoKey, setLogHypsMaxDepth, setTyp, toJSONString, toString
getChapterNbr, getDescription, getDescriptionForSearch, getIsTempObject, getOrigSectionNbr, getSectionMObjNbr, getSectionNbr, getSeq, setChapterNbr, setDescription, setIsTempObject, setSectionMObjNbr, setSectionNbr
public Theorem(int seq, java.util.List<ScopeDef> scopeDefList, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl, java.lang.String labelS, int column, java.lang.String typS, java.util.List<java.lang.String> symList, java.util.List<java.lang.String> proofList, Messages messages) throws LangException
seq
- MObj.seq sequence numberscopeDefList
- Scope info in effect at the timesymTbl
- Symbol Table (Map)stmtTbl
- Statement Table (Map)labelS
- Theorem label Stringcolumn
- Starting columntypS
- Theorem Formula Type Code StringsymList
- Theorem Expression Sym String ListproofList
- Theorem Proof Stmt String List.messages
- for error reportingLangException
- if an error occurrededitProofListDefAndActive(Map stmtTbl, List
proofList)
public Theorem(int seq, java.util.List<ScopeDef> scopeDefList, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl, java.lang.String labelS, int column, java.lang.String typS, java.util.List<java.lang.String> symList, java.util.List<java.lang.String> proofList, BlockList proofBlockList, ProofCompression proofCompression, Messages messages) throws LangException
seq
- MObj.seq sequence numberscopeDefList
- Scope info in effect at the timesymTbl
- Symbol Table (Map)stmtTbl
- Statement Table (Map)labelS
- Theorem label Stringcolumn
- Starting columntypS
- Theorem Formula Type Code StringsymList
- Theorem Expression Sym String ListproofList
- Theorem Proof Stmt String List.proofBlockList
- list containing one or more blocks of compressed
proof symbols.proofCompression
- instance of ProofCompression.java used to
decompress proof.messages
- for error reportingLangException
- if there was a decompression erroreditProofListDefAndActive(Map stmtTbl, List
proofList)
public ParseTree.RPNStep[] getProof()
public ParseTree.RPNStep[] setProof(java.util.Map<java.lang.String,Stmt> stmtTbl, java.util.List<java.lang.String> proofList) throws LangException
stmtTbl
- Statement Table (Map)proofList
- Theorem Proof Stmt String List.LangException
- if an error occurrededitProofListDefAndActive(Map stmtTbl, List
proofList)
public ScopeFrame getOptFrame()
public int getColumn()
public ParseTree.RPNStep[] editProofListDefAndActive(java.util.Map<java.lang.String,Stmt> stmtTbl, java.util.List<java.lang.String> proofList) throws LangException
stmtTbl
-- except for
missing steps denoted by "?", which are converted to "null".
stmtTbl
- Map of statements already loaded.proofList
- Theorem's proof steps, the labels (Strings) of existing
Stmt's (or "?" for missing step(s)).LangException
- (see mmj.lang.LangConstants.java
)public boolean isProofStepInExtendedFrame(Stmt proofStep)
First checks to see if the proof step is in the MandFrame's hypArray. If not it checks the OptFrame's hypArray
proofStep
- a Statement reference.public int renderParsedSubExpr(java.lang.StringBuilder sb, int maxDepth, int maxLength, ParseNode[] child)
renderParsedSubExpr
in class Stmt
sb
- StringBuilder already initialized for appending characters.maxDepth
- maximum depth of Notation Syntax axioms in sub-tree to be
printed. Set to Integer.MAX_VALUE to turn off depth checking.maxLength
- maximum length of output sub-expression. Set to
Integer.MAX_VALUE to turn off depth checking.child
- array of ParseNode, corresponding to VarHyp nodes to be
substituted into the Stmt.java.lang.IllegalArgumentException
- alwayspublic void proofUpdates(ParseTree.RPNStep[] newProof, DjVars[] newDjVarsArray, DjVars[] newOptDjVarsArray)
newProof
- previous proof.newDjVarsArray
- previous Mandatory DjVarsnewOptDjVarsArray
- previous Optional DjVarspublic void loadMandAndOptDjVarsUpdateLists(java.util.Map<java.lang.String,Sym> symTbl, java.util.List<java.util.List<java.lang.String>> inputDjVarsStmtList, java.util.List<DjVars> mandDjVarsUpdateList, java.util.List<DjVars> optDjVarsUpdateList) throws LangException
Will throw LangException if both variables not contained in Mandatory or Optional Frame hyp arrays!
symTbl
- Symbol Table from Logical System.inputDjVarsStmtList
- List of lists where the inner list is symList
from SrcStmt.mandDjVarsUpdateList
- empty list upon input to contain the
Mandatory DjVars generated from the inputDjVarsStmtList.optDjVarsUpdateList
- empty list upon input to contain the Optional
DjVars generated from the inputDjVarsStmtList.LangException
- if validation error.public void replaceDjVars(java.util.List<DjVars> mandDjVarsUpdateList, java.util.List<DjVars> optDjVarsUpdateList)
mandDjVarsUpdateList
- List of DjVars object to be stored.optDjVarsUpdateList
- List of DjVars object to be stored.public void mergeDjVars(java.util.List<DjVars> mandDjVarsUpdateList, java.util.List<DjVars> optDjVarsUpdateList)
mandDjVarsUpdateList
- List of DjVars object to be stored.optDjVarsUpdateList
- List of DjVars object to be stored.