347 ; |
347 ; |
348 attributes: '[' (nameref args * ',') ']' |
348 attributes: '[' (nameref args * ',') ']' |
349 ; |
349 ; |
350 \end{rail} |
350 \end{rail} |
351 |
351 |
352 Theorem specifications come in several flavors: \railnonterm{axmdecl} and |
352 Theorem specifications come in several flavors: \railnonterm{axmdecl} |
353 \railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal |
353 and \railnonterm{thmdecl} usually refer to axioms, assumptions or |
354 statements, while \railnonterm{thmdef} collects lists of existing theorems. |
354 results of goal statements, while \railnonterm{thmdef} collects lists |
355 Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs}, |
355 of existing theorems. Existing theorems are given by |
356 the former requires an actual singleton result. There are three forms of |
356 \railnonterm{thmref} and \railnonterm{thmrefs}, the former requires an |
357 theorem references: (1) named facts $a$, (2) selections from named facts $a(i, |
357 actual singleton result. There are three forms of theorem references: |
358 j - k)$, or (3) literal fact propositions using $altstring$ syntax |
358 (1) named facts $a$, (2) selections from named facts $a(i, j - k)$, or |
|
359 (3) literal fact propositions using $altstring$ syntax |
359 $\backquote\phi\backquote$, (see also method $fact$ in |
360 $\backquote\phi\backquote$, (see also method $fact$ in |
360 \S\ref{sec:pure-meth-att}). |
361 \S\ref{sec:pure-meth-att}). |
361 |
362 |
362 Any kind of theorem specification may include lists of attributes both on the |
363 Any kind of theorem specification may include lists of attributes both |
363 left and right hand sides; attributes are applied to any immediately preceding |
364 on the left and right hand sides; attributes are applied to any |
364 fact. If names are omitted, the theorems are not stored within the theorem |
365 immediately preceding fact. If names are omitted, the theorems are |
365 database of the theory or proof context, but any given attributes are applied |
366 not stored within the theorem database of the theory or proof context, |
366 nonetheless. |
367 but any given attributes are applied nonetheless. |
|
368 |
|
369 An attribute declaration with an extra pair of brackets --- such as |
|
370 ``$[[simproc~a]]$'' --- abbreviates a theorem reference that involves |
|
371 an internal dummy fact, which will be ignored later on. So only the |
|
372 effect of the attribute on the background context will persist. This |
|
373 form of in-place declarations is particularly useful with commands |
|
374 like $\DECLARE$ and $\USINGNAME$. |
367 |
375 |
368 \indexouternonterm{axmdecl}\indexouternonterm{thmdecl} |
376 \indexouternonterm{axmdecl}\indexouternonterm{thmdecl} |
369 \indexouternonterm{thmdef}\indexouternonterm{thmref} |
377 \indexouternonterm{thmdef}\indexouternonterm{thmref} |
370 \indexouternonterm{thmrefs}\indexouternonterm{selection} |
378 \indexouternonterm{thmrefs}\indexouternonterm{selection} |
371 \begin{rail} |
379 \begin{rail} |