--- a/doc-src/Logics/HOL.tex Wed Jan 08 15:12:44 1997 +0100
+++ b/doc-src/Logics/HOL.tex Wed Jan 08 15:17:25 1997 +0100
@@ -838,8 +838,7 @@
\section{Generic packages}
-\HOL\ instantiates most of Isabelle's generic packages;
-see {\tt HOL/ROOT.ML} for details.
+\HOL\ instantiates most of Isabelle's generic packages.
\subsection{Substitution and simplification}
@@ -847,10 +846,12 @@
tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a
subgoal and its hypotheses.
-It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
-simplification set for higher-order logic. Equality~($=$), which also
-expresses logical equivalence, may be used for rewriting. See the file {\tt
-HOL/simpdata.ML} for a complete listing of the simplification rules.
+It instantiates the simplifier. Tactics such as {\tt Asm_simp_tac} and {\tt
+Full_simp_tac} use the default simpset ({\tt!simpset}), which works for most
+purposes. A minimal simplification set for higher-order logic
+is~\ttindexbold{HOL_ss}. Equality~($=$), which also expresses logical
+equivalence, may be used for rewriting. See the file {\tt HOL/simpdata.ML}
+for a complete listing of the simplification rules.
See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
@@ -881,32 +882,14 @@
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
rule; recall Fig.\ts\ref{hol-lemmas2} above.
-The classical reasoner is set up as the structure
-{\tt Classical}. This structure is open, so {\ML} identifiers such
-as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
-\HOL\ defines the following classical rule sets:
-\begin{ttbox}
-prop_cs : claset
-HOL_cs : claset
-set_cs : claset
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{prop_cs}] contains the propositional rules, namely
-those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
-along with the rule~{\tt refl}.
-
-\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
- {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
- and~{\tt exI}, as well as rules for unique existence. Search using
- this classical set is incomplete: quantified formulae are used at most
- once.
-
-\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
- quantifiers, subsets, comprehensions, unions and intersections,
- complements, finite sets, images and ranges.
-\end{ttdescription}
-\noindent
-See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
+The classical reasoner is installed. Tactics such as {\tt Fast_tac} and {\tt
+Best_tac} use the default claset ({\tt!claset}), which works for most
+purposes. Named clasets include \ttindexbold{prop_cs}, which includes the
+propositional rules, \ttindexbold{HOL_cs}, which also includes quantifier
+rules, and \ttindexbold{set_cs}, which also includes rules for subsets,
+comprehensions, unions and intersections, etc. See the file
+{\tt HOL/cladata.ML} for lists of the classical rules, and
+\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
{Chap.\ts\ref{chap:classical}}
for more discussion of classical proof methods.
@@ -1537,9 +1520,8 @@
end
\end{ttbox}
After loading the theory (\verb$use_thy "MyList"$), we can prove
-$Cons~x~xs\neq xs$. First we build a suitable simpset for the simplifier:
+$Cons~x~xs\neq xs$.
\begin{ttbox}
-val mylist_ss = HOL_ss addsimps MyList.list.simps;
goal MyList.thy "!x. Cons x xs ~= xs";
{\out Level 0}
{\out ! x. Cons x xs ~= xs}
@@ -1555,19 +1537,20 @@
{\out ! x. Cons x list ~= list ==>}
{\out ! x. Cons x (Cons a list) ~= Cons a list}
\end{ttbox}
-The first subgoal can be proved with the simplifier and the distinctness
-axioms which are part of \verb$mylist_ss$.
+The first subgoal can be proved using the simplifier.
+Isabelle has already added the freeness properties of lists to the
+default simplification set.
\begin{ttbox}
-by (simp_tac mylist_ss 1);
+by (Simp_tac 1);
{\out Level 2}
{\out ! x. Cons x xs ~= xs}
{\out 1. !!a list.}
{\out ! x. Cons x list ~= list ==>}
{\out ! x. Cons x (Cons a list) ~= Cons a list}
\end{ttbox}
-Using the freeness axioms we can quickly prove the remaining goal.
+Similarly, we prove the remaining goal.
\begin{ttbox}
-by (asm_simp_tac mylist_ss 1);
+by (Asm_simp_tac 1);
{\out Level 3}
{\out ! x. Cons x xs ~= xs}
{\out No subgoals!}
@@ -1575,7 +1558,7 @@
Because both subgoals were proved by almost the same tactic we could have
done that in one step using
\begin{ttbox}
-by (ALLGOALS (asm_simp_tac mylist_ss));
+by (ALLGOALS Asm_simp_tac);
\end{ttbox}
@@ -1604,17 +1587,17 @@
end
\end{ttbox}
Because there are more than four constructors, the theory must be based on
-{\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although
-the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},
-it can be proved by the simplifier if \verb$arith_ss$ is used:
+{\tt Arith}. Inequality is defined via a function \verb|days_ord|.
+The expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},
+but the simplifier can prove it thanks to rewrite rules inherited from theory
+{\tt Arith}.
\begin{ttbox}
-val days_ss = arith_ss addsimps Days.days.simps;
+goal Days.thy "Mo ~= Tu";
+by (Simp_tac 1);
+\end{ttbox}
+You need not derive such inequalities explicitly: the simplifier will dispose
+of them automatically.
-goal Days.thy "Mo ~= Tu";
-by (simp_tac days_ss 1);
-\end{ttbox}
-Note that usually it is not necessary to derive these inequalities explicitly
-because the simplifier will dispose of them automatically.
\subsection{Primitive recursive functions}
\label{sec:HOL:primrec}
@@ -1688,7 +1671,7 @@
as theorems from an explicit definition of the recursive function in terms of
a recursion operator on the datatype.
-The primitive recursive function can also use infix or mixfix syntax:
+The primitive recursive function can have infix or mixfix syntax:
\begin{ttbox}
Append = MyList +
consts "@" :: ['a list,'a list] => 'a list (infixr 60)
@@ -1699,13 +1682,13 @@
\end{ttbox}
The reduction rules become part of the ML structure \verb$Append$ and can
-be used to prove theorems about the function:
+be used to prove theorems about the function. The defining equations for
+primitive recursive functions are automatically provided to the simplifier
+(via the default simpset).
\begin{ttbox}
-val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons];
-
goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";
by (MyList.list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac append_ss));
+by (ALLGOALS Asm_simp_tac);
\end{ttbox}
%Note that underdefined primitive recursive functions are allowed: