2534 |
2534 |
2535 Behind the scenes, Isabelle's built-in packages and theories rely on the |
2535 Behind the scenes, Isabelle's built-in packages and theories rely on the |
2536 following attributes to affect Nitpick's behavior: |
2536 following attributes to affect Nitpick's behavior: |
2537 |
2537 |
2538 \begin{enum} |
2538 \begin{enum} |
2539 \flushitem{\textit{nitpick\_def}} |
2539 \flushitem{\textit{nitpick\_unfold}} |
2540 |
2540 |
2541 \nopagebreak |
2541 \nopagebreak |
2542 This attribute specifies an alternative definition of a constant. The |
2542 This attribute specifies an equation that Nitpick should use to expand a |
2543 alternative definition should be logically equivalent to the constant's actual |
2543 constant. The equation should be logically equivalent to the constant's actual |
2544 axiomatic definition and should be of the form |
2544 definition and should be of the form |
2545 |
2545 |
2546 \qquad $c~{?}x_1~\ldots~{?}x_n \,=\, t$, |
2546 \qquad $c~{?}x_1~\ldots~{?}x_n \,=\, t$, |
2547 |
2547 |
2548 or |
2548 or |
2549 |
2549 |
2550 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$, |
2550 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$, |
2551 |
2551 |
2552 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in |
2552 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in |
2553 $t$. |
2553 $t$. Each occurrence of $c$ in the problem is expanded to $\lambda x_1\,\ldots |
|
2554 x_n.\; t$. |
2554 |
2555 |
2555 \flushitem{\textit{nitpick\_simp}} |
2556 \flushitem{\textit{nitpick\_simp}} |
2556 |
2557 |
2557 \nopagebreak |
2558 \nopagebreak |
2558 This attribute specifies the equations that constitute the specification of a |
2559 This attribute specifies the equations that constitute the specification of a |
2601 \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the |
2602 \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the |
2602 \textit{nitpick\_choice\_spec} set associated with the constant is not empty, it |
2603 \textit{nitpick\_choice\_spec} set associated with the constant is not empty, it |
2603 uses these theorems as the specification of the constant. |
2604 uses these theorems as the specification of the constant. |
2604 |
2605 |
2605 \item[4.] Otherwise, it looks up the definition of the constant. If the |
2606 \item[4.] Otherwise, it looks up the definition of the constant. If the |
2606 \textit{nitpick\_def} set associated with the constant is not empty, it uses the |
2607 \textit{nitpick\_unfold} set associated with the constant is not empty, it uses |
2607 latest rule added to the set as the definition of the constant; otherwise it |
2608 the latest rule added to the set as the definition of the constant; otherwise it |
2608 uses the actual definition axiom. |
2609 uses the actual definition axiom. |
2609 |
2610 |
2610 \begin{enum} |
2611 \begin{enum} |
2611 \item[1.] If the definition is of the form |
2612 \item[1.] If the definition is of the form |
2612 |
2613 |
2639 By default, Nitpick uses the \textit{lfp}-based definition in conjunction with |
2640 By default, Nitpick uses the \textit{lfp}-based definition in conjunction with |
2640 the introduction rules. To override this, you can specify an alternative |
2641 the introduction rules. To override this, you can specify an alternative |
2641 definition as follows: |
2642 definition as follows: |
2642 |
2643 |
2643 \prew |
2644 \prew |
2644 \textbf{lemma} $\mathit{odd\_alt\_def}$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$'' |
2645 \textbf{lemma} $\mathit{odd\_alt\_unfold}$ [\textit{nitpick\_unfold}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$'' |
2645 \postw |
2646 \postw |
2646 |
2647 |
2647 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2 |
2648 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2 |
2648 = 1$. Alternatively, you can specify an equational specification of the constant: |
2649 = 1$. Alternatively, you can specify an equational specification of the constant: |
2649 |
2650 |
2689 view on top of an existing constant $c$. The easiest way to achieve this is to |
2690 view on top of an existing constant $c$. The easiest way to achieve this is to |
2690 define a new constant $c'$ (co)inductively. Then prove that $c$ equals $c'$ |
2691 define a new constant $c'$ (co)inductively. Then prove that $c$ equals $c'$ |
2691 and let Nitpick know about it: |
2692 and let Nitpick know about it: |
2692 |
2693 |
2693 \prew |
2694 \prew |
2694 \textbf{lemma} \textit{c\_alt\_def} [\textit{nitpick\_def}]:\kern.4em ``$c \equiv c'$\kern2pt '' |
2695 \textbf{lemma} \textit{c\_alt\_unfold} [\textit{nitpick\_unfold}]:\kern.4em ``$c \equiv c'$\kern2pt '' |
2695 \postw |
2696 \postw |
2696 |
2697 |
2697 This ensures that Nitpick will substitute $c'$ for $c$ and use the (co)inductive |
2698 This ensures that Nitpick will substitute $c'$ for $c$ and use the (co)inductive |
2698 definition. |
2699 definition. |
2699 |
2700 |