--- a/doc-src/Logics/FOL.tex Wed Jan 08 15:12:44 1997 +0100
+++ b/doc-src/Logics/FOL.tex Wed Jan 08 15:17:25 1997 +0100
@@ -193,18 +193,20 @@
\section{Generic packages}
-\FOL{} instantiates most of Isabelle's generic packages;
-see {\tt FOL/ROOT.ML} for details.
+\FOL{} instantiates most of Isabelle's generic packages.
\begin{itemize}
\item
Because it includes a general substitution rule, \FOL{} instantiates the
tactic \ttindex{hyp_subst_tac}, which substitutes for an equality
throughout a subgoal and its hypotheses.
+(See {\tt FOL/ROOT.ML} for details.)
\item
-It instantiates the simplifier. \ttindexbold{IFOL_ss} is the simplification
-set for intuitionistic first-order logic, while \ttindexbold{FOL_ss} is the
-simplification set for classical logic. Both equality ($=$) and the
-biconditional ($\bimp$) may be used for rewriting. See the file
+It instantiates the simplifier. Both equality ($=$) and the biconditional
+($\bimp$) may be used for rewriting. Tactics such as {\tt Asm_simp_tac} and
+{\tt Full_simp_tac} use the default simpset ({\tt!simpset}), which works for
+most purposes. Named simplification sets include \ttindexbold{IFOL_ss},
+for intuitionistic first-order logic, and \ttindexbold{FOL_ss},
+for classical logic. See the file
{\tt FOL/simpdata.ML} for a complete listing of the simplification
rules%
\iflabelundefined{sec:setting-up-simp}{}%
@@ -329,30 +331,11 @@
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
rule (see Fig.\ts\ref{fol-cla-derived}).
-The classical reasoner is set up for \FOL, as the
-structure~{\tt Cla}. This structure is open, so \ML{} identifiers
-such as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
-Single-step proofs can be performed, using \ttindex{swap_res_tac} to deal
-with negated assumptions.\index{assumptions!negated}
-
-{\FOL} defines the following classical rule sets:
-\begin{ttbox}
-prop_cs : claset
-FOL_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{FOL_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 is incomplete since quantified
-formulae are used at most once.
-\end{ttdescription}
-\noindent
-See the file {\tt FOL/FOL.ML} for derivations of the
+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, and \ttindexbold{FOL_cs}, which also includes quantifier
+rules. See the file {\tt FOL/cladata.ML} for lists of the
classical rules, and
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
{Chap.\ts\ref{chap:classical}}
@@ -621,7 +604,7 @@
{\out Level 0}
{\out EX y. ALL x. P(y) --> P(x)}
{\out 1. EX y. ALL x. P(y) --> P(x)}
-by (deepen_tac FOL_cs 0 1);
+by (Deepen_tac 0 1);
{\out Depth = 0}
{\out Depth = 2}
{\out Level 1}
@@ -682,9 +665,10 @@
{\out 1. P & Q | ~ P & R}
\end{ttbox}
The premises (bound to the {\ML} variable {\tt prems}) are passed as
-introduction rules to \ttindex{fast_tac}:
+introduction rules to \ttindex{fast_tac}. Remember that {\tt!claset} refers
+to the default classical set.
\begin{ttbox}
-by (fast_tac (FOL_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
{\out Level 1}
{\out if(P,Q,R)}
{\out No subgoals!}
@@ -712,7 +696,7 @@
{\out S}
{\out 1. P & Q | ~ P & R ==> S}
\ttbreak
-by (fast_tac (FOL_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
{\out Level 2}
{\out S}
{\out No subgoals!}
@@ -723,7 +707,7 @@
{\S\ref{definitions}}, there are other
ways of treating definitions when deriving a rule. We can start the
proof using {\tt goal}, which does not expand definitions, instead of
-{\tt goalw}. We can use \ttindex{rewrite_goals_tac}
+{\tt goalw}. We can use \ttindex{rew_tac}
to expand definitions in the subgoals --- perhaps after calling
\ttindex{cut_facts_tac} to insert the rule's premises. We can use
\ttindex{rewrite_rule}, which is a meta-inference rule, to expand
@@ -797,17 +781,21 @@
{\out 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
\end{ttbox}
Where do we stand? The first subgoal holds by assumption; the second and
-third, by contradiction. This is getting tedious. Let us revert to the
-initial proof state and let \ttindex{fast_tac} solve it. The classical
-rule set {\tt if_cs} contains the rules of~{\FOL} plus the derived rules
+third, by contradiction. This is getting tedious. We could use the classical
+reasoner, but first let us extend the default claset with the derived rules
for~$if$.
\begin{ttbox}
+AddSIs [ifI];
+AddSEs [ifE];
+\end{ttbox}
+Now we can revert to the
+initial proof state and let \ttindex{fast_tac} solve it.
+\begin{ttbox}
choplev 0;
{\out Level 0}
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
{\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
-val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
-by (fast_tac if_cs 1);
+by (Fast_tac 1);
{\out Level 1}
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
{\out No subgoals!}
@@ -819,7 +807,7 @@
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
\ttbreak
-by (fast_tac if_cs 1);
+by (Fast_tac 1);
{\out Level 1}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
{\out No subgoals!}
@@ -838,13 +826,15 @@
\end{ttbox}
This time, simply unfold using the definition of $if$:
\begin{ttbox}
-by (rewrite_goals_tac [if_def]);
+by (rewtac if_def);
{\out Level 1}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
{\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
{\out P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}
\end{ttbox}
-We are left with a subgoal in pure first-order logic:
+We are left with a subgoal in pure first-order logic, which is why the
+classical reasoner can prove it given {\tt FOL_cs} alone. (We could, of
+course, have used {\tt Fast_tac}.)
\begin{ttbox}
by (fast_tac FOL_cs 1);
{\out Level 2}
@@ -853,8 +843,9 @@
\end{ttbox}
Expanding definitions reduces the extended logic to the base logic. This
approach has its merits --- especially if the prover for the base logic is
-good --- but can be slow. In these examples, proofs using {\tt if_cs} (the
-derived rules) run about six times faster than proofs using {\tt FOL_cs}.
+good --- but can be slow. In these examples, proofs using the default
+claset (which includes the derived rules) run about six times faster
+than proofs using {\tt FOL_cs}.
Expanding definitions also complicates error diagnosis. Suppose we are having
difficulties in proving some goal. If by expanding definitions we have
@@ -867,13 +858,13 @@
{\out Level 0}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
-by (fast_tac FOL_cs 1);
+by (Fast_tac 1);
{\out by: tactic failed}
\end{ttbox}
This failure message is uninformative, but we can get a closer look at the
situation by applying \ttindex{step_tac}.
\begin{ttbox}
-by (REPEAT (step_tac if_cs 1));
+by (REPEAT (Step_tac 1));
{\out Level 1}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
{\out 1. [| A; ~ P; R; ~ P; R |] ==> B}
@@ -893,7 +884,7 @@
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
\ttbreak
-by (rewrite_goals_tac [if_def]);
+by (rewtac if_def);
{\out Level 1}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
{\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
--- 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:
--- a/doc-src/Logics/ZF.tex Wed Jan 08 15:12:44 1997 +0100
+++ b/doc-src/Logics/ZF.tex Wed Jan 08 15:17:25 1997 +0100
@@ -19,11 +19,13 @@
Thus, we may even regard set theory as a computational logic, loosely
inspired by Martin-L\"of's Type Theory.
-Because {\ZF} is an extension of {\FOL}, it provides the same packages,
-namely {\tt hyp_subst_tac}, the simplifier, and the classical reasoner.
-The main simplification set is called {\tt ZF_ss}. Several
-classical rule sets are defined, including {\tt lemmas_cs},
-{\tt upair_cs} and~{\tt ZF_cs}.
+Because {\ZF} is an extension of {\FOL}, it provides the same packages, namely
+{\tt hyp_subst_tac}, the simplifier, and the classical reasoner. The default
+simpset and claset are usually satisfactory. Named simpsets include
+\ttindexbold{ZF_ss} (basic set theory rules) and \ttindexbold{rank_ss} (for
+proving termination of well-founded recursion). Named clasets sets include
+\ttindexbold{ZF_cs} (basic set theory) and \ttindexbold{le_cs} (useful for
+reasoning about the relations $<$ and $\le$).
{\tt ZF} has a flexible package for handling inductive definitions,
such as inference systems, and datatype definitions, such as lists and
@@ -1503,11 +1505,11 @@
f(x)=g(x)$. Given $a\in\{x\in A.P(x)\}$ it extracts rewrite rules from
$a\in A$ and~$P(a)$. It can also break down $a\in A\int B$ and $a\in A-B$.
-The simplification set \ttindexbold{ZF_ss} contains congruence rules for
+The default simplification set contains congruence rules for
all the binding operators of {\ZF}\@. It contains all the conversion
rules, such as {\tt fst} and {\tt snd}, as well as the rewrites
-shown in Fig.\ts\ref{zf-simpdata}.
-
+shown in Fig.\ts\ref{zf-simpdata}. See the file
+{\tt ZF/simpdata.ML} for a fuller list.
\begin{figure}
\begin{eqnarray*}
@@ -1521,7 +1523,7 @@
(\forall x \in \emptyset. P(x)) & \bimp & \top\\
(\forall x \in A. \top) & \bimp & \top
\end{eqnarray*}
-\caption{Rewrite rules for set theory} \label{zf-simpdata}
+\caption{Some rewrite rules for set theory} \label{zf-simpdata}
\end{figure}
@@ -1598,7 +1600,7 @@
We enter the goal and make the first step, which breaks the equation into
two inclusions by extensionality:\index{*equalityI theorem}
\begin{ttbox}
-goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
+goal thy "Pow(A Int B) = Pow(A) Int Pow(B)";
{\out Level 0}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out 1. Pow(A Int B) = Pow(A) Int Pow(B)}
@@ -1687,7 +1689,7 @@
\end{ttbox}
\medskip
We could have performed this proof in one step by applying
-\ttindex{fast_tac} with the classical rule set \ttindex{ZF_cs}. Let us
+\ttindex{Fast_tac}. Let us
go back to the start:
\begin{ttbox}
choplev 0;
@@ -1695,11 +1697,11 @@
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out 1. Pow(A Int B) = Pow(A) Int Pow(B)}
\end{ttbox}
-We must add \tdx{equalityI} to {\tt ZF_cs} as an introduction rule.
-Extensionality is not used by default because many equalities can be proved
+We must add \tdx{equalityI} as an introduction rule.
+Extensionality is not used by default: many equalities can be proved
by rewriting.
\begin{ttbox}
-by (fast_tac (ZF_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
{\out Level 1}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out No subgoals!}
@@ -1713,7 +1715,7 @@
${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$. To begin, we
tackle the inclusion using \tdx{subsetI}:
\begin{ttbox}
-val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
+val [prem] = goal thy "C<=D ==> Union(C) <= Union(D)";
{\out Level 0}
{\out Union(C) <= Union(D)}
{\out 1. Union(C) <= Union(D)}
@@ -1763,10 +1765,10 @@
{\out Union(C) <= Union(D)}
{\out No subgoals!}
\end{ttbox}
-Again, \ttindex{fast_tac} with \ttindex{ZF_cs} can do this proof in one
+Again, \ttindex{fast_tac} can prove the theorem in one
step, provided we somehow supply it with~{\tt prem}. We can either add
this premise to the assumptions using \ttindex{cut_facts_tac}, or add
-\hbox{\tt prem RS subsetD} to \ttindex{ZF_cs} as an introduction rule.
+\hbox{\tt prem RS subsetD} to the claset as an introduction rule.
The file {\tt ZF/equalities.ML} has many similar proofs. Reasoning about
general intersection can be difficult because of its anomalous behaviour on
@@ -1790,7 +1792,7 @@
functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then
$(f\un g)`a = f`a$:
\begin{ttbox}
-val prems = goal ZF.thy
+val prems = goal thy
"[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ttback
\ttback (f Un g)`a = f`a";
{\out Level 0}