author paulson Tue Jan 19 12:56:27 1999 +0100 (1999-01-19) changeset 6143 1eb364a68c54 parent 6142 c0c93b9434ef child 6144 7d38744313c8
freeness reasoning: T.free_iffs
 doc-src/ZF/ZF.tex file | annotate | diff | revisions
     1.1 --- a/doc-src/ZF/ZF.tex	Tue Jan 19 11:46:18 1999 +0100
1.2 +++ b/doc-src/ZF/ZF.tex	Tue Jan 19 12:56:27 1999 +0100
1.3 @@ -1522,13 +1522,18 @@
1.4  for example $\texttt{Nil}\not=\texttt{Cons}(a,l)$, and they are injective, for
1.5  example $\texttt{Cons}(a,l)=\texttt{Cons}(a',l') \bimp a=a' \conj l=l'$.
1.6  Because the number of freeness is quadratic in the number of constructors, the
1.7 -datatype package does not prove them, but instead provides several means of
1.8 -proving them dynamically.  For the \texttt{list} datatype, freeness reasoning
1.9 -can be done in two ways: by simplifying with the theorems
1.10 -\texttt{list.free_iffs} or by invoking the classical reasoner with
1.11 -\texttt{list.free_SEs} as safe elimination rules.  Occasionally this exposes
1.12 -the underlying representation of some constructor, which can be rectified
1.13 -using the command \hbox{\tt fold_tac list.con_defs}.
1.14 +datatype package does not prove them.  Instead, it ensures that simplification
1.15 +will prove them dynamically: when the simplifier encounters a formula
1.16 +asserting the equality of two datatype constructors, it performs freeness
1.17 +reasoning.
1.18 +
1.19 +Freeness reasoning can also be done using the classical reasoner, but it is
1.20 +more complicated.  You have to add some safe elimination rules rules to the
1.21 +claset.  For the \texttt{list} datatype, they are called
1.22 +\texttt{list.free_SEs}.  Occasionally this exposes the underlying
1.23 +representation of some constructor, which can be rectified using the command
1.24 +\hbox{\tt fold_tac list.con_defs}.
1.25 +
1.26
1.27  \subsubsection{Structural induction}
1.28
1.29 @@ -1631,8 +1636,7 @@
1.30
1.31  Most of the theorems about datatypes become part of the default simpset.  You
1.32  never need to see them again because the simplifier applies them
1.33 -automatically.  Add freeness properties (\texttt{free_iffs}) to the simpset
1.34 -when you want them.  Induction or exhaustion are usually invoked by hand,
1.35 +automatically.  Induction or exhaustion are usually invoked by hand,
1.36  usually via these special-purpose tactics:
1.37  \begin{ttdescription}
1.38  \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] applies structural
1.39 @@ -1718,13 +1722,10 @@
1.40  {\out           ALL x r. Br(x, t2, r) ~= t2 |]}
1.41  {\out        ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)}
1.42  \end{ttbox}
1.43 -Both subgoals are proved using the simplifier.  Tactic
1.44 -\texttt{asm_full_simp_tac} is used, rewriting the assumptions.
1.45 -This is because simplification using the freeness properties can unfold the
1.46 -definition of constructor~\texttt{Br}, so we arrange that all occurrences are
1.47 -unfolded.
1.48 +Both subgoals are proved using \texttt{Auto_tac}, which performs the necessary
1.49 +freeness reasoning.
1.50  \begin{ttbox}
1.51 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs)));
1.52 +by Auto_tac;
1.53  {\out Level 2}
1.54  {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
1.55  {\out No subgoals!}
1.56 @@ -1792,10 +1793,10 @@
1.57  essentially binary notation, so freeness properties can be proved fast.
1.58  \begin{ttbox}
1.59  Goal "C00 ~= C01";
1.60 -by (simp_tac (simpset() addsimps enum.free_iffs) 1);
1.61 +by (Simp_tac 1);
1.62  \end{ttbox}
1.63  You need not derive such inequalities explicitly.  The simplifier will dispose
1.64 -of them automatically, given the theorem list \texttt{free_iffs}.
1.65 +of them automatically.
1.66
1.67  \index{*datatype|)}
1.68