--- a/NEWS Fri Feb 23 16:31:18 2001 +0100
+++ b/NEWS Fri Feb 23 16:31:21 2001 +0100
@@ -1,6 +1,8 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
+
* HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL
* HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
--- a/doc-src/Ref/classical.tex Fri Feb 23 16:31:18 2001 +0100
+++ b/doc-src/Ref/classical.tex Fri Feb 23 16:31:21 2001 +0100
@@ -126,7 +126,7 @@
We can easily handle reasoning on the left.
As discussed in
-\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}},
+\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{{\S}\ref{destruct}},
elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
achieves a similar effect as the corresponding sequent rules. For the
other connectives, we use sequent-style elimination rules instead of
@@ -311,7 +311,7 @@
be applied using elim-resolution. Elimination rules are applied using
elim-resolution. In a classical set, rules are sorted by the number of new
subgoals they will yield; rules that generate the fewest subgoals will be
-tried first (see \S\ref{biresolve_tac}).
+tried first (see {\S}\ref{biresolve_tac}).
For elimination and destruction rules there are variants of the add operations
adding a rule in a way such that it is applied only if also its second premise
@@ -337,7 +337,7 @@
inferences as possible; or else, apply certain safe rules, allowing
instantiation of unknowns; or else, apply an unsafe rule. The tactics also
eliminate assumptions of the form $x=t$ by substitution if they have been set
-up to do so (see \texttt{hyp_subst_tacs} in~\S\ref{sec:classical-setup} below).
+up to do so (see \texttt{hyp_subst_tacs} in~{\S}\ref{sec:classical-setup} below).
They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
and~$P$, then replace $P\imp Q$ by~$Q$.
@@ -362,12 +362,12 @@
addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
addSbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
-addSaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
+addSafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
delSWrapper : claset * string -> claset \hfill{\bf infix 4}
addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
addbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
-addaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
+addafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
delWrapper : claset * string -> claset \hfill{\bf infix 4}
addSss : claset * simpset -> claset \hfill{\bf infix 4}
@@ -384,7 +384,7 @@
adds the given tactic as a safe wrapper, such that it is tried
{\em before} each safe step of the search.
-\item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern}
+\item[$cs$ addSafter $(name,tac)$] \indexbold{*addSafter}
adds the given tactic as a safe wrapper, such that it is tried
when a safe step of the search would fail.
@@ -398,7 +398,7 @@
adds the given tactic as an unsafe wrapper, such that it its result is
concatenated {\em before} the result of each unsafe step.
-\item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern}
+\item[$cs$ addafter $(name,tac)$] \indexbold{*addafter}
adds the given tactic as an unsafe wrapper, such that it its result is
concatenated {\em after} the result of each unsafe step.
@@ -419,7 +419,7 @@
Strictly speaking, the operators \texttt{addss} and \texttt{addSss}
are not part of the classical reasoner.
, which are used as primitives
-for the automatic tactics described in \S\ref{sec:automatic-tactics}, are
+for the automatic tactics described in {\S}\ref{sec:automatic-tactics}, are
implemented as wrapper tacticals.
they
\begin{warn}
@@ -433,7 +433,7 @@
\section{The classical tactics}
\index{classical reasoner!tactics} If installed, the classical module provides
powerful theorem-proving tactics. Most of them have capitalized analogues
-that use the default claset; see \S\ref{sec:current-claset}.
+that use the default claset; see {\S}\ref{sec:current-claset}.
\subsection{The tableau prover}
@@ -504,7 +504,7 @@
\end{ttdescription}
They must be supplied both a simpset and a claset; therefore
they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which
-use the default claset and simpset (see \S\ref{sec:current-claset} below).
+use the default claset and simpset (see {\S}\ref{sec:current-claset} below).
For interactive use,
the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;}
while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);}
@@ -629,7 +629,7 @@
Each theory is equipped with an implicit \emph{current claset}
\index{claset!current}. This is a default set of classical
rules. The underlying idea is quite similar to that of a current
-simpset described in \S\ref{sec:simp-for-dummies}; please read that
+simpset described in {\S}\ref{sec:simp-for-dummies}; please read that
section, including its warnings.
The tactics
--- a/doc-src/Ref/simp.tex Fri Feb 23 16:31:18 2001 +0100
+++ b/doc-src/Ref/simp.tex Fri Feb 23 16:31:21 2001 +0100
@@ -410,7 +410,7 @@
\[
\begin{array}{l@{}r@{\quad\mapsto\quad}l}
\mbox{create formula rewrites:}& P & [P \bimp True] \\[.5ex]
-\mbox{remove negations:}& \lnot P & [P \bimp False] \\[.5ex]
+\mbox{remove negations:}& \neg P & [P \bimp False] \\[.5ex]
\mbox{create conditional rewrites:}& P\imp s\gg t & [P\Imp s\gg t] \\[.5ex]
\mbox{break up conjunctions:}&
(s@1 \gg@1 t@1) \conj (s@2 \gg@2 t@2) & [s@1 \gg@1 t@1, s@2 \gg@2 t@2]
@@ -431,7 +431,7 @@
supplies expansion rules for case splits. The simplifier is designed
for rules roughly of the kind
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
-\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))
+\conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))
\]
but is insensitive to the form of the right-hand side. Other examples
include product types, where $split ::
@@ -501,7 +501,7 @@
val red2 = \(\List{\Var{P}\bimp\Var{Q}; \Var{Q}} \Imp \Var{P}\)
val mk_rew_rules = ...
val case_splits = [ \(\Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp\)
- \((\Var{Q} \imp \Var{P}(\Var{x})) \conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))\) ]
+ \((\Var{Q} \imp \Var{P}(\Var{x})) \conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))\) ]
val norm_thms = [ (\(\Var{x}=norm(\Var{x})\),\(norm(\Var{x})=\Var{x}\)),
(\(\Var{P}\bimp{}NORM(\Var{P}\)), \(NORM(\Var{P})\bimp\Var{P}\)) ]
val subst_thms = [ \(\List{\Var{x}=\Var{y}; \Var{P}(\Var{x})}\Imp\Var{P}(\Var{y})\) ]
--- a/doc-src/Ref/simplifier.tex Fri Feb 23 16:31:18 2001 +0100
+++ b/doc-src/Ref/simplifier.tex Fri Feb 23 16:31:21 2001 +0100
@@ -117,7 +117,7 @@
\end{ttbox}
\verb$Asm_full_simp_tac$ will not simplify the \texttt{f a} on the left.
This problem can be overcome by reordering assumptions (see
-\S\ref{sec:reordering-asms}). Future versions of \verb$Asm_full_simp_tac$
+{\S}\ref{sec:reordering-asms}). Future versions of \verb$Asm_full_simp_tac$
will not suffer from this deficiency.
\end{warn}
@@ -150,7 +150,7 @@
source of rewrite rules are \emph{simplification procedures}, that is
\ML\ functions that produce suitable theorems on demand, depending on
the current redex. Congruences are a more advanced feature; see
-\S\ref{sec:simp-congs}.
+{\S}\ref{sec:simp-congs}.
\begin{ttdescription}
@@ -340,10 +340,10 @@
Internally, all rewrite rules are translated into meta-equalities,
theorems with conclusion $lhs \equiv rhs$. Each simpset contains a
function for extracting equalities from arbitrary theorems. For
-example, $\lnot(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
+example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
\equiv False$. This function can be installed using
\ttindex{setmksimps} but only the definer of a logic should need to do
-this; see \S\ref{sec:setmksimps}. The function processes theorems
+this; see {\S}\ref{sec:setmksimps}. The function processes theorems
added by \texttt{addsimps} as well as local assumptions.
\begin{ttdescription}
@@ -450,7 +450,7 @@
rules from it when simplifying~$P@2$. Such local assumptions are
effective for rewriting formulae such as $x=0\imp y+x=y$. The local
assumptions are also provided as theorems to the solver; see
-\S~\ref{sec:simp-solver} below.
+{\S}~\ref{sec:simp-solver} below.
\begin{ttdescription}
@@ -485,7 +485,7 @@
The congruence rule for conditional expressions can supply contextual
information for simplifying the arms:
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
- \lnot\Var{q} \Imp \Var{b}=\Var{d}} \Imp
+ \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
\]
A congruence rule can also {\em prevent\/} simplification of some arguments.
@@ -605,7 +605,7 @@
\medskip
-As explained in \S\ref{sec:simp-subgoaler}, the subgoaler is also used
+As explained in {\S}\ref{sec:simp-subgoaler}, the subgoaler is also used
to solve the premises of congruence rules. These are usually of the
form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$
needs to be instantiated with the result. Typically, the subgoaler
@@ -617,8 +617,8 @@
It may even happen that due to simplification the subgoal is no longer
an equality. For example $False \bimp \Var{Q}$ could be rewritten to
-$\lnot\Var{Q}$. To cover this case, the solver could try resolving
-with the theorem $\lnot False$.
+$\neg\Var{Q}$. To cover this case, the solver could try resolving
+with the theorem $\neg False$.
\medskip
@@ -674,7 +674,7 @@
of the replacement can be anything. For example, here is a splitting rule
for conditional expressions:
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
-\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))
+\conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))
\]
Another example is the elimination operator for Cartesian products (which
happens to be called~$split$):
@@ -733,7 +733,7 @@
gives direct access to the various simplification modes:
\begin{itemize}
\item if $safe$ is {\tt true}, the safe solver is used as explained in
- \S\ref{sec:simp-solver},
+ {\S}\ref{sec:simp-solver},
\item $simp\_asm$ determines whether the local assumptions are simplified,
\item $use\_asm$ determines whether the assumptions are used as local rewrite
rules, and
@@ -747,7 +747,7 @@
\item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
\ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are
the basic simplification tactics that work exactly like their
- namesakes in \S\ref{sec:simp-for-dummies}, except that they are
+ namesakes in {\S}\ref{sec:simp-for-dummies}, except that they are
explicitly supplied with a simpset.
\end{ttdescription}
@@ -771,7 +771,7 @@
Also note that functions depending implicitly on the current theory
context (like capital \texttt{Simp_tac} and the other commands of
-\S\ref{sec:simp-for-dummies}) should be considered harmful outside of
+{\S}\ref{sec:simp-for-dummies}) should be considered harmful outside of
actual proof scripts. In particular, ML programs like theory
definition packages or special tactics should refer to simpsets only
explicitly, via the above tactics used in conjunction with
@@ -793,10 +793,10 @@
The first four of these functions provide \emph{forward} rules for
simplification. Their effect is analogous to the corresponding
-tactics described in \S\ref{simp-tactics}, but affect the whole
+tactics described in {\S}\ref{simp-tactics}, but affect the whole
theorem instead of just a certain subgoal. Also note that the
-looper~/ solver process as described in \S\ref{sec:simp-looper} and
-\S\ref{sec:simp-solver} is omitted in forward simplification.
+looper~/ solver process as described in {\S}\ref{sec:simp-looper} and
+{\S}\ref{sec:simp-solver} is omitted in forward simplification.
The latter four are \emph{conversions}, establishing proven equations
of the form $t \equiv u$ where the l.h.s.\ $t$ has been given as
@@ -979,7 +979,7 @@
\label{sec:reordering-asms}
\index{assumptions!reordering}
-As mentioned in \S\ref{sec:simp-for-dummies-tacs},
+As mentioned in {\S}\ref{sec:simp-for-dummies-tacs},
\ttindex{asm_full_simp_tac} may require the assumptions to be permuted
to be more effective. Given the subgoal
\begin{ttbox}
@@ -1169,7 +1169,7 @@
re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
conclusion by~$f(a)$.
-Another example is the goal $\lnot(t=u) \imp \lnot(u=t)$.
+Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
The differing orientations make this appear difficult to prove. Ordered
rewriting with \texttt{symmetry} makes the equalities agree. (Without
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
@@ -1378,7 +1378,7 @@
The simplified rewrites must now be converted into meta-equalities. The
rule \texttt{eq_reflection} converts equality rewrites, while {\tt
iff_reflection} converts if-and-only-if rewrites. The latter possibility
-can arise in two other ways: the negative theorem~$\lnot P$ is converted to
+can arise in two other ways: the negative theorem~$\neg P$ is converted to
$P\equiv\texttt{False}$, and any other theorem~$P$ is converted to
$P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt
iff_reflection_T} accomplish this conversion.
@@ -1436,7 +1436,7 @@
Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later
-extend \texttt{IFOL_ss} with classical rewrite rules such as $\lnot\lnot
+extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg
P\bimp P$.
\index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
\index{*addsimps}\index{*addcongs}
--- a/src/HOL/NatArith.thy Fri Feb 23 16:31:18 2001 +0100
+++ b/src/HOL/NatArith.thy Fri Feb 23 16:31:21 2001 +0100
@@ -18,7 +18,7 @@
val nat_diff_split = thm "nat_diff_split";
(* TODO: use this for force_tac in Provers/clasip.ML *)
-fun add_arith cs = cs addaltern ("arith_tac", arith_tac);
+fun add_arith cs = cs addafter ("arith_tac", arith_tac);
*}
lemmas [arith_split] = nat_diff_split split_min split_max
--- a/src/Provers/clasimp.ML Fri Feb 23 16:31:18 2001 +0100
+++ b/src/Provers/clasimp.ML Fri Feb 23 16:31:21 2001 +0100
@@ -108,7 +108,7 @@
(*Add a simpset to a classical set!*)
(*Caution: only one simpset added can be added by each of addSss and addss*)
-fun cs addSss ss = Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
+fun cs addSss ss = Classical.addSafter (cs, ("safe_asm_full_simp_tac",
CHANGED o safe_asm_full_simp_tac ss));
fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac",
CHANGED o Simplifier.asm_full_simp_tac ss));
--- a/src/Provers/classical.ML Fri Feb 23 16:31:18 2001 +0100
+++ b/src/Provers/classical.ML Fri Feb 23 16:31:21 2001 +0100
@@ -17,7 +17,7 @@
(*higher precedence than := facilitates use of references*)
infix 4 addSIs addSEs addSDs addIs addEs addDs addXIs addXEs addXDs delrules
addSWrapper delSWrapper addWrapper delWrapper
- addSbefore addSaltern addbefore addaltern
+ addSbefore addSafter addbefore addafter
addD2 addE2 addSD2 addSE2;
@@ -66,9 +66,9 @@
val addWrapper : claset * (string * wrapper) -> claset
val delWrapper : claset * string -> claset
val addSbefore : claset * (string * (int -> tactic)) -> claset
- val addSaltern : claset * (string * (int -> tactic)) -> claset
+ val addSafter : claset * (string * (int -> tactic)) -> claset
val addbefore : claset * (string * (int -> tactic)) -> claset
- val addaltern : claset * (string * (int -> tactic)) -> claset
+ val addafter : claset * (string * (int -> tactic)) -> claset
val addD2 : claset * (string * thm) -> claset
val addE2 : claset * (string * thm) -> claset
val addSD2 : claset * (string * thm) -> claset
@@ -715,23 +715,23 @@
(* compose a safe tactic alternatively before/after safe_step_tac *)
fun cs addSbefore (name, tac1) =
cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
-fun cs addSaltern (name, tac2) =
+fun cs addSafter (name, tac2) =
cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
(*compose a tactic alternatively before/after the step tactic *)
fun cs addbefore (name, tac1) =
cs addWrapper (name, fn tac2 => tac1 APPEND' tac2);
-fun cs addaltern (name, tac2) =
+fun cs addafter (name, tac2) =
cs addWrapper (name, fn tac1 => tac1 APPEND' tac2);
fun cs addD2 (name, thm) =
- cs addaltern (name, dtac thm THEN' atac);
+ cs addafter (name, datac thm 1);
fun cs addE2 (name, thm) =
- cs addaltern (name, etac thm THEN' atac);
-fun cs addSD2 (name, thm) =
- cs addSaltern (name, dmatch_tac [thm] THEN' eq_assume_tac);
-fun cs addSE2 (name, thm) =
- cs addSaltern (name, ematch_tac [thm] THEN' eq_assume_tac);
+ cs addafter (name, eatac thm 1);
+fun cs addSD2 (name, thm) =
+ cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
+fun cs addSE2 (name, thm) =
+ cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
(*Merge works by adding all new rules of the 2nd claset into the 1st claset.
Merging the term nets may look more efficient, but the rather delicate