1520 |
1520 |
1521 Constructors satisfy {\em freeness} properties. Constructions are distinct, |
1521 Constructors satisfy {\em freeness} properties. Constructions are distinct, |
1522 for example $\texttt{Nil}\not=\texttt{Cons}(a,l)$, and they are injective, for |
1522 for example $\texttt{Nil}\not=\texttt{Cons}(a,l)$, and they are injective, for |
1523 example $\texttt{Cons}(a,l)=\texttt{Cons}(a',l') \bimp a=a' \conj l=l'$. |
1523 example $\texttt{Cons}(a,l)=\texttt{Cons}(a',l') \bimp a=a' \conj l=l'$. |
1524 Because the number of freeness is quadratic in the number of constructors, the |
1524 Because the number of freeness is quadratic in the number of constructors, the |
1525 datatype package does not prove them, but instead provides several means of |
1525 datatype package does not prove them. Instead, it ensures that simplification |
1526 proving them dynamically. For the \texttt{list} datatype, freeness reasoning |
1526 will prove them dynamically: when the simplifier encounters a formula |
1527 can be done in two ways: by simplifying with the theorems |
1527 asserting the equality of two datatype constructors, it performs freeness |
1528 \texttt{list.free_iffs} or by invoking the classical reasoner with |
1528 reasoning. |
1529 \texttt{list.free_SEs} as safe elimination rules. Occasionally this exposes |
1529 |
1530 the underlying representation of some constructor, which can be rectified |
1530 Freeness reasoning can also be done using the classical reasoner, but it is |
1531 using the command \hbox{\tt fold_tac list.con_defs}. |
1531 more complicated. You have to add some safe elimination rules rules to the |
|
1532 claset. For the \texttt{list} datatype, they are called |
|
1533 \texttt{list.free_SEs}. Occasionally this exposes the underlying |
|
1534 representation of some constructor, which can be rectified using the command |
|
1535 \hbox{\tt fold_tac list.con_defs}. |
|
1536 |
1532 |
1537 |
1533 \subsubsection{Structural induction} |
1538 \subsubsection{Structural induction} |
1534 |
1539 |
1535 The datatype package also provides structural induction rules. For datatypes |
1540 The datatype package also provides structural induction rules. For datatypes |
1536 without mutual or nested recursion, the rule has the form exemplified by |
1541 without mutual or nested recursion, the rule has the form exemplified by |
1629 contained in the set, a coinduction rule gives a way of constructing new |
1634 contained in the set, a coinduction rule gives a way of constructing new |
1630 values of the set. |
1635 values of the set. |
1631 |
1636 |
1632 Most of the theorems about datatypes become part of the default simpset. You |
1637 Most of the theorems about datatypes become part of the default simpset. You |
1633 never need to see them again because the simplifier applies them |
1638 never need to see them again because the simplifier applies them |
1634 automatically. Add freeness properties (\texttt{free_iffs}) to the simpset |
1639 automatically. Induction or exhaustion are usually invoked by hand, |
1635 when you want them. Induction or exhaustion are usually invoked by hand, |
|
1636 usually via these special-purpose tactics: |
1640 usually via these special-purpose tactics: |
1637 \begin{ttdescription} |
1641 \begin{ttdescription} |
1638 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] applies structural |
1642 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] applies structural |
1639 induction on variable $x$ to subgoal $i$, provided the type of $x$ is a |
1643 induction on variable $x$ to subgoal $i$, provided the type of $x$ is a |
1640 datatype. The induction variable should not occur among other assumptions |
1644 datatype. The induction variable should not occur among other assumptions |
1716 {\out 2. !!a t1 t2.} |
1720 {\out 2. !!a t1 t2.} |
1717 {\out [| a : A; t1 : bt(A); ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);} |
1721 {\out [| a : A; t1 : bt(A); ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);} |
1718 {\out ALL x r. Br(x, t2, r) ~= t2 |]} |
1722 {\out ALL x r. Br(x, t2, r) ~= t2 |]} |
1719 {\out ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)} |
1723 {\out ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)} |
1720 \end{ttbox} |
1724 \end{ttbox} |
1721 Both subgoals are proved using the simplifier. Tactic |
1725 Both subgoals are proved using \texttt{Auto_tac}, which performs the necessary |
1722 \texttt{asm_full_simp_tac} is used, rewriting the assumptions. |
1726 freeness reasoning. |
1723 This is because simplification using the freeness properties can unfold the |
1727 \begin{ttbox} |
1724 definition of constructor~\texttt{Br}, so we arrange that all occurrences are |
1728 by Auto_tac; |
1725 unfolded. |
|
1726 \begin{ttbox} |
|
1727 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs))); |
|
1728 {\out Level 2} |
1729 {\out Level 2} |
1729 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l} |
1730 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l} |
1730 {\out No subgoals!} |
1731 {\out No subgoals!} |
1731 \end{ttbox} |
1732 \end{ttbox} |
1732 To remove the quantifiers from the induction formula, we save the theorem using |
1733 To remove the quantifiers from the induction formula, we save the theorem using |
1790 rather than assumed, full processing of this definition takes under 15 seconds |
1791 rather than assumed, full processing of this definition takes under 15 seconds |
1791 (on a 300 MHz Pentium). The constructors have a balanced representation, |
1792 (on a 300 MHz Pentium). The constructors have a balanced representation, |
1792 essentially binary notation, so freeness properties can be proved fast. |
1793 essentially binary notation, so freeness properties can be proved fast. |
1793 \begin{ttbox} |
1794 \begin{ttbox} |
1794 Goal "C00 ~= C01"; |
1795 Goal "C00 ~= C01"; |
1795 by (simp_tac (simpset() addsimps enum.free_iffs) 1); |
1796 by (Simp_tac 1); |
1796 \end{ttbox} |
1797 \end{ttbox} |
1797 You need not derive such inequalities explicitly. The simplifier will dispose |
1798 You need not derive such inequalities explicitly. The simplifier will dispose |
1798 of them automatically, given the theorem list \texttt{free_iffs}. |
1799 of them automatically. |
1799 |
1800 |
1800 \index{*datatype|)} |
1801 \index{*datatype|)} |
1801 |
1802 |
1802 |
1803 |
1803 \subsection{Recursive function definitions}\label{sec:ZF:recursive} |
1804 \subsection{Recursive function definitions}\label{sec:ZF:recursive} |