1.1 --- a/doc-src/ZF/ZF.tex Wed Feb 03 13:29:24 1999 +0100
1.2 +++ b/doc-src/ZF/ZF.tex Wed Feb 03 14:02:49 1999 +0100
1.3 @@ -1393,7 +1393,12 @@
1.4 list functions by primitive recursion. See theory \texttt{List}.
1.5
1.6
1.7 -\section{Simplification and classical reasoning}
1.8 +\section{Automatic Tools}
1.9 +
1.10 +{\ZF} provides the simplifier and the classical reasoner. Moreover it
1.11 +supplies a specialized tool to infer `types' of terms.
1.12 +
1.13 +\subsection{Simplification}
1.14
1.15 {\ZF} inherits simplification from {\FOL} but adopts it for set theory. The
1.16 extraction of rewrite rules takes the {\ZF} primitives into account. It can
1.17 @@ -1412,6 +1417,9 @@
1.18 Fig.\ts\ref{zf-simpdata}. See the file \texttt{ZF/simpdata.ML} for a fuller
1.19 list.
1.20
1.21 +
1.22 +\subsection{Classical Reasoning}
1.23 +
1.24 As for the classical reasoner, tactics such as \texttt{Blast_tac} and {\tt
1.25 Best_tac} refer to the default claset (\texttt{claset()}). This works for
1.26 most purposes. Named clasets include \ttindexbold{ZF_cs} (basic set theory)
1.27 @@ -1437,6 +1445,77 @@
1.28 \end{figure}
1.29
1.30
1.31 +\subsection{Type-Checking Tactics}
1.32 +\index{type-checking tactics}
1.33 +
1.34 +Isabelle/{\ZF} provides simple tactics to help automate those proofs that are
1.35 +essentially type-checking. Such proofs are built by applying rules such as
1.36 +these:
1.37 +\begin{ttbox}
1.38 +[| ?P ==> ?a : ?A; ~ ?P ==> ?b : ?A |] ==> (if ?P then ?a else ?b) : ?A
1.39 +
1.40 +[| ?m : nat; ?n : nat |] ==> ?m #+ ?n : nat
1.41 +
1.42 +?a : ?A ==> Inl(?a) : ?A + ?B
1.43 +\end{ttbox}
1.44 +In typical applications, the goal has the form $t\in\Var{A}$: in other words,
1.45 +we have a specific term~$t$ and need to infer its `type' by instantiating the
1.46 +set variable~$\Var{A}$. Neither the simplifier nor the classical reasoner
1.47 +does this job well. The if-then-else rule, and many similar ones, can make
1.48 +the classical reasoner loop. The simplifier refuses (on principle) to
1.49 +instantiate variables during rewriting, so goals such as \texttt{i\#+j :\ ?A}
1.50 +are left unsolved.
1.51 +
1.52 +The simplifier calls the type-checker to solve rewritten subgoals: this stage
1.53 +can indeed instantiate variables. If you have defined new constants and
1.54 +proved type-checking rules for them, then insert the rules using
1.55 +\texttt{AddTCs} and the rest should be automatic. In particular, the
1.56 +simplifier will use type-checking to help satisfy conditional rewrite rules.
1.57 +Call the tactic \ttindex{Typecheck_tac} to break down all subgoals using
1.58 +type-checking rules.
1.59 +
1.60 +Though the easiest way to invoke the type-checker is via the simplifier,
1.61 +specialized applications may require more detailed knowledge of
1.62 +the type-checking primitives. They are modelled on the simplifier's:
1.63 +\begin{ttdescription}
1.64 +\item[\ttindexbold{tcset}] is the type of tcsets: sets of type-checking rules.
1.65 +
1.66 +\item[\ttindexbold{addTCs}] is an infix operator to add type-checking rules to
1.67 + a tcset.
1.68 +
1.69 +\item[\ttindexbold{delTCs}] is an infix operator to remove type-checking rules
1.70 + from a tcset.
1.71 +
1.72 +\item[\ttindexbold{typecheck_tac}] is a tactic for attempting to prove all
1.73 + subgoals using the rules given in its argument, a tcset.
1.74 +\end{ttdescription}
1.75 +
1.76 +Tcsets, like simpsets, are associated with theories and are merged when
1.77 +theories are merged. There are further primitives that use the default tcset.
1.78 +\begin{ttdescription}
1.79 +\item[\ttindexbold{tcset}] is a function to return the default tcset; use the
1.80 + expression \texttt{tcset()}.
1.81 +
1.82 +\item[\ttindexbold{AddTCs}] adds type-checking rules to the default tcset.
1.83 +
1.84 +\item[\ttindexbold{DelTCs}] removes type-checking rules from the default
1.85 + tcset.
1.86 +
1.87 +\item[\ttindexbold{Typecheck_tac}] calls \texttt{typecheck_tac} using the
1.88 + default tcset.
1.89 +\end{ttdescription}
1.90 +
1.91 +To supply some type-checking rules temporarily, using \texttt{Addrules} and
1.92 +later \texttt{Delrules} is the simplest way. There is also a high-tech
1.93 +approach. Call the simplifier with a new solver expressed using
1.94 +\ttindexbold{type_solver_tac} and your temporary type-checking rules.
1.95 +\begin{ttbox}
1.96 +by (asm_simp_tac
1.97 + (simpset() setSolver type_solver_tac (tcset() addTCs prems)) 2);
1.98 +\end{ttbox}
1.99 +
1.100 +
1.101 +
1.102 \section{Datatype definitions}
1.103 \label{sec:ZF:datatype}
1.104 \index{*datatype|(}
1.105 @@ -1804,6 +1883,7 @@
1.106 \subsection{Recursive function definitions}\label{sec:ZF:recursive}
1.107 \index{recursive functions|see{recursion}}
1.108 \index{*primrec|(}
1.109 +\index{recursion!primitive|(}
1.110
1.111 Datatypes come with a uniform way of defining functions, {\bf primitive
1.112 recursion}. Such definitions rely on the recursion operator defined by the
1.113 @@ -2039,7 +2119,7 @@
1.114 Proving monotonicity...
1.115 \ttbreak
1.116 Proving the introduction rules...
1.117 -The typechecking subgoal:
1.118 +The type-checking subgoal:
1.119 0 : Fin(A)
1.120 1. 0 : Pow(A)
1.121 \ttbreak
1.122 @@ -2052,7 +2132,7 @@
1.123 $\emptyset\in\texttt{Pow}(A)$. Restoring the \texttt{type_intrs} but not the
1.124 \texttt{type_elims}, we again get an error message:
1.125 \begin{ttbox}
1.126 -The typechecking subgoal:
1.127 +The type-checking subgoal:
1.128 0 : Fin(A)
1.129 1. 0 : Pow(A)
1.130 \ttbreak
1.131 @@ -2060,7 +2140,7 @@
1.132 0 : Fin(A)
1.133 1. 0 : Pow(A)
1.134 \ttbreak
1.135 -The typechecking subgoal:
1.136 +The type-checking subgoal:
1.137 cons(a, b) : Fin(A)
1.138 1. [| a : A; b : Fin(A) |] ==> cons(a, b) : Pow(A)
1.139 \ttbreak