1.1 --- a/NEWS Fri Feb 23 16:31:18 2001 +0100
1.2 +++ b/NEWS Fri Feb 23 16:31:21 2001 +0100
1.3 @@ -1,6 +1,8 @@
1.4 Isabelle NEWS -- history user-relevant changes
1.5 ==============================================
1.6
1.7 +* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter
1.8 +
1.9 * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL
1.10
1.11 * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
2.1 --- a/doc-src/Ref/classical.tex Fri Feb 23 16:31:18 2001 +0100
2.2 +++ b/doc-src/Ref/classical.tex Fri Feb 23 16:31:21 2001 +0100
2.3 @@ -126,7 +126,7 @@
2.4
2.5 We can easily handle reasoning on the left.
2.6 As discussed in
2.7 -\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}},
2.8 +\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{{\S}\ref{destruct}},
2.9 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
2.10 achieves a similar effect as the corresponding sequent rules. For the
2.11 other connectives, we use sequent-style elimination rules instead of
2.12 @@ -311,7 +311,7 @@
2.13 be applied using elim-resolution. Elimination rules are applied using
2.14 elim-resolution. In a classical set, rules are sorted by the number of new
2.15 subgoals they will yield; rules that generate the fewest subgoals will be
2.16 -tried first (see \S\ref{biresolve_tac}).
2.17 +tried first (see {\S}\ref{biresolve_tac}).
2.18
2.19 For elimination and destruction rules there are variants of the add operations
2.20 adding a rule in a way such that it is applied only if also its second premise
2.21 @@ -337,7 +337,7 @@
2.22 inferences as possible; or else, apply certain safe rules, allowing
2.23 instantiation of unknowns; or else, apply an unsafe rule. The tactics also
2.24 eliminate assumptions of the form $x=t$ by substitution if they have been set
2.25 -up to do so (see \texttt{hyp_subst_tacs} in~\S\ref{sec:classical-setup} below).
2.26 +up to do so (see \texttt{hyp_subst_tacs} in~{\S}\ref{sec:classical-setup} below).
2.27 They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
2.28 and~$P$, then replace $P\imp Q$ by~$Q$.
2.29
2.30 @@ -362,12 +362,12 @@
2.31
2.32 addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
2.33 addSbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
2.34 -addSaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
2.35 +addSafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
2.36 delSWrapper : claset * string -> claset \hfill{\bf infix 4}
2.37
2.38 addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
2.39 addbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
2.40 -addaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
2.41 +addafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
2.42 delWrapper : claset * string -> claset \hfill{\bf infix 4}
2.43
2.44 addSss : claset * simpset -> claset \hfill{\bf infix 4}
2.45 @@ -384,7 +384,7 @@
2.46 adds the given tactic as a safe wrapper, such that it is tried
2.47 {\em before} each safe step of the search.
2.48
2.49 -\item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern}
2.50 +\item[$cs$ addSafter $(name,tac)$] \indexbold{*addSafter}
2.51 adds the given tactic as a safe wrapper, such that it is tried
2.52 when a safe step of the search would fail.
2.53
2.54 @@ -398,7 +398,7 @@
2.55 adds the given tactic as an unsafe wrapper, such that it its result is
2.56 concatenated {\em before} the result of each unsafe step.
2.57
2.58 -\item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern}
2.59 +\item[$cs$ addafter $(name,tac)$] \indexbold{*addafter}
2.60 adds the given tactic as an unsafe wrapper, such that it its result is
2.61 concatenated {\em after} the result of each unsafe step.
2.62
2.63 @@ -419,7 +419,7 @@
2.64 Strictly speaking, the operators \texttt{addss} and \texttt{addSss}
2.65 are not part of the classical reasoner.
2.66 , which are used as primitives
2.67 -for the automatic tactics described in \S\ref{sec:automatic-tactics}, are
2.68 +for the automatic tactics described in {\S}\ref{sec:automatic-tactics}, are
2.69 implemented as wrapper tacticals.
2.70 they
2.71 \begin{warn}
2.72 @@ -433,7 +433,7 @@
2.73 \section{The classical tactics}
2.74 \index{classical reasoner!tactics} If installed, the classical module provides
2.75 powerful theorem-proving tactics. Most of them have capitalized analogues
2.76 -that use the default claset; see \S\ref{sec:current-claset}.
2.77 +that use the default claset; see {\S}\ref{sec:current-claset}.
2.78
2.79
2.80 \subsection{The tableau prover}
2.81 @@ -504,7 +504,7 @@
2.82 \end{ttdescription}
2.83 They must be supplied both a simpset and a claset; therefore
2.84 they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which
2.85 -use the default claset and simpset (see \S\ref{sec:current-claset} below).
2.86 +use the default claset and simpset (see {\S}\ref{sec:current-claset} below).
2.87 For interactive use,
2.88 the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;}
2.89 while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);}
2.90 @@ -629,7 +629,7 @@
2.91 Each theory is equipped with an implicit \emph{current claset}
2.92 \index{claset!current}. This is a default set of classical
2.93 rules. The underlying idea is quite similar to that of a current
2.94 -simpset described in \S\ref{sec:simp-for-dummies}; please read that
2.95 +simpset described in {\S}\ref{sec:simp-for-dummies}; please read that
2.96 section, including its warnings.
2.97
2.98 The tactics
3.1 --- a/doc-src/Ref/simp.tex Fri Feb 23 16:31:18 2001 +0100
3.2 +++ b/doc-src/Ref/simp.tex Fri Feb 23 16:31:21 2001 +0100
3.3 @@ -410,7 +410,7 @@
3.4 \[
3.5 \begin{array}{l@{}r@{\quad\mapsto\quad}l}
3.6 \mbox{create formula rewrites:}& P & [P \bimp True] \\[.5ex]
3.7 -\mbox{remove negations:}& \lnot P & [P \bimp False] \\[.5ex]
3.8 +\mbox{remove negations:}& \neg P & [P \bimp False] \\[.5ex]
3.9 \mbox{create conditional rewrites:}& P\imp s\gg t & [P\Imp s\gg t] \\[.5ex]
3.10 \mbox{break up conjunctions:}&
3.11 (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]
3.12 @@ -431,7 +431,7 @@
3.13 supplies expansion rules for case splits. The simplifier is designed
3.14 for rules roughly of the kind
3.15 \[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
3.16 -\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))
3.17 +\conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))
3.18 \]
3.19 but is insensitive to the form of the right-hand side. Other examples
3.20 include product types, where $split ::
3.21 @@ -501,7 +501,7 @@
3.22 val red2 = \(\List{\Var{P}\bimp\Var{Q}; \Var{Q}} \Imp \Var{P}\)
3.23 val mk_rew_rules = ...
3.24 val case_splits = [ \(\Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp\)
3.25 - \((\Var{Q} \imp \Var{P}(\Var{x})) \conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))\) ]
3.26 + \((\Var{Q} \imp \Var{P}(\Var{x})) \conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))\) ]
3.27 val norm_thms = [ (\(\Var{x}=norm(\Var{x})\),\(norm(\Var{x})=\Var{x}\)),
3.28 (\(\Var{P}\bimp{}NORM(\Var{P}\)), \(NORM(\Var{P})\bimp\Var{P}\)) ]
3.29 val subst_thms = [ \(\List{\Var{x}=\Var{y}; \Var{P}(\Var{x})}\Imp\Var{P}(\Var{y})\) ]
4.1 --- a/doc-src/Ref/simplifier.tex Fri Feb 23 16:31:18 2001 +0100
4.2 +++ b/doc-src/Ref/simplifier.tex Fri Feb 23 16:31:21 2001 +0100
4.3 @@ -117,7 +117,7 @@
4.4 \end{ttbox}
4.5 \verb$Asm_full_simp_tac$ will not simplify the \texttt{f a} on the left.
4.6 This problem can be overcome by reordering assumptions (see
4.7 -\S\ref{sec:reordering-asms}). Future versions of \verb$Asm_full_simp_tac$
4.8 +{\S}\ref{sec:reordering-asms}). Future versions of \verb$Asm_full_simp_tac$
4.9 will not suffer from this deficiency.
4.10 \end{warn}
4.11
4.12 @@ -150,7 +150,7 @@
4.13 source of rewrite rules are \emph{simplification procedures}, that is
4.14 \ML\ functions that produce suitable theorems on demand, depending on
4.15 the current redex. Congruences are a more advanced feature; see
4.16 -\S\ref{sec:simp-congs}.
4.17 +{\S}\ref{sec:simp-congs}.
4.18
4.19 \begin{ttdescription}
4.20
4.21 @@ -340,10 +340,10 @@
4.22 Internally, all rewrite rules are translated into meta-equalities,
4.23 theorems with conclusion $lhs \equiv rhs$. Each simpset contains a
4.24 function for extracting equalities from arbitrary theorems. For
4.25 -example, $\lnot(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
4.26 +example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
4.27 \equiv False$. This function can be installed using
4.28 \ttindex{setmksimps} but only the definer of a logic should need to do
4.29 -this; see \S\ref{sec:setmksimps}. The function processes theorems
4.30 +this; see {\S}\ref{sec:setmksimps}. The function processes theorems
4.31 added by \texttt{addsimps} as well as local assumptions.
4.32
4.33 \begin{ttdescription}
4.34 @@ -450,7 +450,7 @@
4.35 rules from it when simplifying~$P@2$. Such local assumptions are
4.36 effective for rewriting formulae such as $x=0\imp y+x=y$. The local
4.37 assumptions are also provided as theorems to the solver; see
4.38 -\S~\ref{sec:simp-solver} below.
4.39 +{\S}~\ref{sec:simp-solver} below.
4.40
4.41 \begin{ttdescription}
4.42
4.43 @@ -485,7 +485,7 @@
4.44 The congruence rule for conditional expressions can supply contextual
4.45 information for simplifying the arms:
4.46 \[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
4.47 - \lnot\Var{q} \Imp \Var{b}=\Var{d}} \Imp
4.48 + \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
4.49 if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
4.50 \]
4.51 A congruence rule can also {\em prevent\/} simplification of some arguments.
4.52 @@ -605,7 +605,7 @@
4.53
4.54 \medskip
4.55
4.56 -As explained in \S\ref{sec:simp-subgoaler}, the subgoaler is also used
4.57 +As explained in {\S}\ref{sec:simp-subgoaler}, the subgoaler is also used
4.58 to solve the premises of congruence rules. These are usually of the
4.59 form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$
4.60 needs to be instantiated with the result. Typically, the subgoaler
4.61 @@ -617,8 +617,8 @@
4.62
4.63 It may even happen that due to simplification the subgoal is no longer
4.64 an equality. For example $False \bimp \Var{Q}$ could be rewritten to
4.65 -$\lnot\Var{Q}$. To cover this case, the solver could try resolving
4.66 -with the theorem $\lnot False$.
4.67 +$\neg\Var{Q}$. To cover this case, the solver could try resolving
4.68 +with the theorem $\neg False$.
4.69
4.70 \medskip
4.71
4.72 @@ -674,7 +674,7 @@
4.73 of the replacement can be anything. For example, here is a splitting rule
4.74 for conditional expressions:
4.75 \[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
4.76 -\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))
4.77 +\conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))
4.78 \]
4.79 Another example is the elimination operator for Cartesian products (which
4.80 happens to be called~$split$):
4.81 @@ -733,7 +733,7 @@
4.82 gives direct access to the various simplification modes:
4.83 \begin{itemize}
4.84 \item if $safe$ is {\tt true}, the safe solver is used as explained in
4.85 - \S\ref{sec:simp-solver},
4.86 + {\S}\ref{sec:simp-solver},
4.87 \item $simp\_asm$ determines whether the local assumptions are simplified,
4.88 \item $use\_asm$ determines whether the assumptions are used as local rewrite
4.89 rules, and
4.90 @@ -747,7 +747,7 @@
4.91 \item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
4.92 \ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are
4.93 the basic simplification tactics that work exactly like their
4.94 - namesakes in \S\ref{sec:simp-for-dummies}, except that they are
4.95 + namesakes in {\S}\ref{sec:simp-for-dummies}, except that they are
4.96 explicitly supplied with a simpset.
4.97
4.98 \end{ttdescription}
4.99 @@ -771,7 +771,7 @@
4.100
4.101 Also note that functions depending implicitly on the current theory
4.102 context (like capital \texttt{Simp_tac} and the other commands of
4.103 -\S\ref{sec:simp-for-dummies}) should be considered harmful outside of
4.104 +{\S}\ref{sec:simp-for-dummies}) should be considered harmful outside of
4.105 actual proof scripts. In particular, ML programs like theory
4.106 definition packages or special tactics should refer to simpsets only
4.107 explicitly, via the above tactics used in conjunction with
4.108 @@ -793,10 +793,10 @@
4.109
4.110 The first four of these functions provide \emph{forward} rules for
4.111 simplification. Their effect is analogous to the corresponding
4.112 -tactics described in \S\ref{simp-tactics}, but affect the whole
4.113 +tactics described in {\S}\ref{simp-tactics}, but affect the whole
4.114 theorem instead of just a certain subgoal. Also note that the
4.115 -looper~/ solver process as described in \S\ref{sec:simp-looper} and
4.116 -\S\ref{sec:simp-solver} is omitted in forward simplification.
4.117 +looper~/ solver process as described in {\S}\ref{sec:simp-looper} and
4.118 +{\S}\ref{sec:simp-solver} is omitted in forward simplification.
4.119
4.120 The latter four are \emph{conversions}, establishing proven equations
4.121 of the form $t \equiv u$ where the l.h.s.\ $t$ has been given as
4.122 @@ -979,7 +979,7 @@
4.123 \label{sec:reordering-asms}
4.124 \index{assumptions!reordering}
4.125
4.126 -As mentioned in \S\ref{sec:simp-for-dummies-tacs},
4.127 +As mentioned in {\S}\ref{sec:simp-for-dummies-tacs},
4.128 \ttindex{asm_full_simp_tac} may require the assumptions to be permuted
4.129 to be more effective. Given the subgoal
4.130 \begin{ttbox}
4.131 @@ -1169,7 +1169,7 @@
4.132 re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
4.133 conclusion by~$f(a)$.
4.134
4.135 -Another example is the goal $\lnot(t=u) \imp \lnot(u=t)$.
4.136 +Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
4.137 The differing orientations make this appear difficult to prove. Ordered
4.138 rewriting with \texttt{symmetry} makes the equalities agree. (Without
4.139 knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
4.140 @@ -1378,7 +1378,7 @@
4.141 The simplified rewrites must now be converted into meta-equalities. The
4.142 rule \texttt{eq_reflection} converts equality rewrites, while {\tt
4.143 iff_reflection} converts if-and-only-if rewrites. The latter possibility
4.144 -can arise in two other ways: the negative theorem~$\lnot P$ is converted to
4.145 +can arise in two other ways: the negative theorem~$\neg P$ is converted to
4.146 $P\equiv\texttt{False}$, and any other theorem~$P$ is converted to
4.147 $P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt
4.148 iff_reflection_T} accomplish this conversion.
4.149 @@ -1436,7 +1436,7 @@
4.150 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
4.151 In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
4.152 IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later
4.153 -extend \texttt{IFOL_ss} with classical rewrite rules such as $\lnot\lnot
4.154 +extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg
4.155 P\bimp P$.
4.156 \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
4.157 \index{*addsimps}\index{*addcongs}
5.1 --- a/src/HOL/NatArith.thy Fri Feb 23 16:31:18 2001 +0100
5.2 +++ b/src/HOL/NatArith.thy Fri Feb 23 16:31:21 2001 +0100
5.3 @@ -18,7 +18,7 @@
5.4 val nat_diff_split = thm "nat_diff_split";
5.5
5.6 (* TODO: use this for force_tac in Provers/clasip.ML *)
5.7 -fun add_arith cs = cs addaltern ("arith_tac", arith_tac);
5.8 +fun add_arith cs = cs addafter ("arith_tac", arith_tac);
5.9 *}
5.10
5.11 lemmas [arith_split] = nat_diff_split split_min split_max
6.1 --- a/src/Provers/clasimp.ML Fri Feb 23 16:31:18 2001 +0100
6.2 +++ b/src/Provers/clasimp.ML Fri Feb 23 16:31:21 2001 +0100
6.3 @@ -108,7 +108,7 @@
6.4
6.5 (*Add a simpset to a classical set!*)
6.6 (*Caution: only one simpset added can be added by each of addSss and addss*)
6.7 -fun cs addSss ss = Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
6.8 +fun cs addSss ss = Classical.addSafter (cs, ("safe_asm_full_simp_tac",
6.9 CHANGED o safe_asm_full_simp_tac ss));
6.10 fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac",
6.11 CHANGED o Simplifier.asm_full_simp_tac ss));
7.1 --- a/src/Provers/classical.ML Fri Feb 23 16:31:18 2001 +0100
7.2 +++ b/src/Provers/classical.ML Fri Feb 23 16:31:21 2001 +0100
7.3 @@ -17,7 +17,7 @@
7.4 (*higher precedence than := facilitates use of references*)
7.5 infix 4 addSIs addSEs addSDs addIs addEs addDs addXIs addXEs addXDs delrules
7.6 addSWrapper delSWrapper addWrapper delWrapper
7.7 - addSbefore addSaltern addbefore addaltern
7.8 + addSbefore addSafter addbefore addafter
7.9 addD2 addE2 addSD2 addSE2;
7.10
7.11
7.12 @@ -66,9 +66,9 @@
7.13 val addWrapper : claset * (string * wrapper) -> claset
7.14 val delWrapper : claset * string -> claset
7.15 val addSbefore : claset * (string * (int -> tactic)) -> claset
7.16 - val addSaltern : claset * (string * (int -> tactic)) -> claset
7.17 + val addSafter : claset * (string * (int -> tactic)) -> claset
7.18 val addbefore : claset * (string * (int -> tactic)) -> claset
7.19 - val addaltern : claset * (string * (int -> tactic)) -> claset
7.20 + val addafter : claset * (string * (int -> tactic)) -> claset
7.21 val addD2 : claset * (string * thm) -> claset
7.22 val addE2 : claset * (string * thm) -> claset
7.23 val addSD2 : claset * (string * thm) -> claset
7.24 @@ -715,23 +715,23 @@
7.25 (* compose a safe tactic alternatively before/after safe_step_tac *)
7.26 fun cs addSbefore (name, tac1) =
7.27 cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
7.28 -fun cs addSaltern (name, tac2) =
7.29 +fun cs addSafter (name, tac2) =
7.30 cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
7.31
7.32 (*compose a tactic alternatively before/after the step tactic *)
7.33 fun cs addbefore (name, tac1) =
7.34 cs addWrapper (name, fn tac2 => tac1 APPEND' tac2);
7.35 -fun cs addaltern (name, tac2) =
7.36 +fun cs addafter (name, tac2) =
7.37 cs addWrapper (name, fn tac1 => tac1 APPEND' tac2);
7.38
7.39 fun cs addD2 (name, thm) =
7.40 - cs addaltern (name, dtac thm THEN' atac);
7.41 + cs addafter (name, datac thm 1);
7.42 fun cs addE2 (name, thm) =
7.43 - cs addaltern (name, etac thm THEN' atac);
7.44 -fun cs addSD2 (name, thm) =
7.45 - cs addSaltern (name, dmatch_tac [thm] THEN' eq_assume_tac);
7.46 -fun cs addSE2 (name, thm) =
7.47 - cs addSaltern (name, ematch_tac [thm] THEN' eq_assume_tac);
7.48 + cs addafter (name, eatac thm 1);
7.49 +fun cs addSD2 (name, thm) =
7.50 + cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
7.51 +fun cs addSE2 (name, thm) =
7.52 + cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
7.53
7.54 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
7.55 Merging the term nets may look more efficient, but the rather delicate