moved classical wrappers to IsarRef;
removed somewhat pointless historic material;
--- a/src/Doc/IsarRef/Generic.thy Sun Nov 04 20:23:26 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy Wed Nov 07 12:14:38 2012 +0100
@@ -1362,13 +1362,13 @@
subsection {* Single-step tactics *}
text {*
- \begin{matharray}{rcl}
+ \begin{mldecls}
@{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
@{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
@{index_ML step_tac: "Proof.context -> int -> tactic"} \\
@{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
@{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
- \end{matharray}
+ \end{mldecls}
These are the primitive tactics behind the automated proof methods
of the Classical Reasoner. By calling them yourself, you can
@@ -1405,6 +1405,94 @@
*}
+subsection {* Modifying the search step *}
+
+text {*
+ \begin{mldecls}
+ @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
+ @{index_ML_op addSWrapper: "claset * (string * (Proof.context -> wrapper))
+ -> claset"} \\
+ @{index_ML_op addSbefore: "claset * (string * (int -> tactic)) -> claset"} \\
+ @{index_ML_op addSafter: "claset * (string * (int -> tactic)) -> claset"} \\
+ @{index_ML_op delSWrapper: "claset * string -> claset"} \\[0.5ex]
+ @{index_ML_op addWrapper: "claset * (string * (Proof.context -> wrapper))
+ -> claset"} \\
+ @{index_ML_op addbefore: "claset * (string * (int -> tactic)) -> claset"} \\
+ @{index_ML_op addafter: "claset * (string * (int -> tactic)) -> claset"} \\
+ @{index_ML_op delWrapper: "claset * string -> claset"} \\[0.5ex]
+ @{index_ML addSss: "Proof.context -> Proof.context"} \\
+ @{index_ML addss: "Proof.context -> Proof.context"} \\
+ \end{mldecls}
+
+ The proof strategy of the Classical Reasoner is simple. Perform as
+ many safe 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 @{text "x = t"}
+ by substitution if they have been set up to do so. They may perform
+ a form of Modus Ponens: if there are assumptions @{text "P \<longrightarrow> Q"} and
+ @{text "P"}, then replace @{text "P \<longrightarrow> Q"} by @{text "Q"}.
+
+ The classical reasoning tools --- except @{method blast} --- allow
+ to modify this basic proof strategy by applying two lists of
+ arbitrary \emph{wrapper tacticals} to it. The first wrapper list,
+ which is considered to contain safe wrappers only, affects @{ML
+ safe_step_tac} and all the tactics that call it. The second one,
+ which may contain unsafe wrappers, affects the unsafe parts of @{ML
+ step_tac}, @{ML slow_step_tac}, and the tactics that call them. A
+ wrapper transforms each step of the search, for example by
+ attempting other tactics before or after the original step tactic.
+ All members of a wrapper list are applied in turn to the respective
+ step tactic.
+
+ Initially the two wrapper lists are empty, which means no
+ modification of the step tactics. Safe and unsafe wrappers are added
+ to a claset with the functions given below, supplying them with
+ wrapper names. These names may be used to selectively delete
+ wrappers.
+
+ \begin{description}
+
+ \item @{text "cs addSWrapper (name, wrapper)"} adds a new wrapper,
+ which should yield a safe tactic, to modify the existing safe step
+ tactic.
+
+ \item @{text "cs addSbefore (name, tac)"} adds the given tactic as a
+ safe wrapper, such that it is tried \emph{before} each safe step of
+ the search.
+
+ \item @{text "cs addSafter (name, tac)"} adds the given tactic as a
+ safe wrapper, such that it is tried when a safe step of the search
+ would fail.
+
+ \item @{text "cs delSWrapper name"} deletes the safe wrapper with
+ the given name.
+
+ \item @{text "cs addWrapper (name, wrapper)"} adds a new wrapper to
+ modify the existing (unsafe) step tactic.
+
+ \item @{text "cs addbefore (name, tac)"} adds the given tactic as an
+ unsafe wrapper, such that it its result is concatenated
+ \emph{before} the result of each unsafe step.
+
+ \item @{text "cs addafter (name, tac)"} adds the given tactic as an
+ unsafe wrapper, such that it its result is concatenated \emph{after}
+ the result of each unsafe step.
+
+ \item @{text "cs delWrapper name"} deletes the unsafe wrapper with
+ the given name.
+
+ \item @{text "addSss"} adds the simpset of the context to its
+ classical set. The assumptions and goal will be simplified, in a
+ rather safe way, after each safe step of the search.
+
+ \item @{text "addss"} adds the simpset of the context to its
+ classical set. The assumptions and goal will be simplified, before
+ the each unsafe step of the search.
+
+ \end{description}
+*}
+
+
section {* Object-logic setup \label{sec:object-logic} *}
text {*
--- a/src/Doc/ROOT Sun Nov 04 20:23:26 2012 +0100
+++ b/src/Doc/ROOT Wed Nov 07 12:14:38 2012 +0100
@@ -261,7 +261,6 @@
"../proof.sty"
"../manual.bib"
"document/build"
- "document/classical.tex"
"document/root.tex"
"document/simplifier.tex"
"document/substitution.tex"
--- a/src/Doc/Ref/document/classical.tex Sun Nov 04 20:23:26 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,178 +0,0 @@
-
-\chapter{The Classical Reasoner}\label{chap:classical}
-\index{classical reasoner|(}
-\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
-
-\section{Classical rule sets}
-\index{classical sets}
-
-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
-can be unified with an assumption of the current proof state:
-\indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2}
-\begin{ttbox}
-addSE2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
-addSD2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
-addE2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
-addD2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
-\end{ttbox}
-\begin{warn}
- A rule to be added in this special way must be given a name, which is used
- to delete it again -- when desired -- using \texttt{delSWrappers} or
- \texttt{delWrappers}, respectively. This is because these add operations
- are implemented as wrappers (see \ref{sec:modifying-search} below).
-\end{warn}
-
-
-\subsection{Modifying the search step}
-\label{sec:modifying-search}
-For a given classical set, the proof strategy is simple. Perform as many safe
-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).
-They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
-and~$P$, then replace $P\imp Q$ by~$Q$.
-
-The classical reasoning tactics --- except \texttt{blast_tac}! --- allow
-you to modify this basic proof strategy by applying two lists of arbitrary
-{\bf wrapper tacticals} to it.
-The first wrapper list, which is considered to contain safe wrappers only,
-affects \ttindex{safe_step_tac} and all the tactics that call it.
-The second one, which may contain unsafe wrappers, affects the unsafe parts
-of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them.
-A wrapper transforms each step of the search, for example
-by attempting other tactics before or after the original step tactic.
-All members of a wrapper list are applied in turn to the respective step tactic.
-
-Initially the two wrapper lists are empty, which means no modification of the
-step tactics. Safe and unsafe wrappers are added to a claset
-with the functions given below, supplying them with wrapper names.
-These names may be used to selectively delete wrappers.
-
-\begin{ttbox}
-type wrapper = (int -> tactic) -> (int -> tactic);
-
-addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
-addSbefore : 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}
-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}
-addss : claset * simpset -> claset \hfill{\bf infix 4}
-\end{ttbox}
-%
-
-\begin{ttdescription}
-\item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper}
-adds a new wrapper, which should yield a safe tactic,
-to modify the existing safe step tactic.
-
-\item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}
-adds the given tactic as a safe wrapper, such that it is tried
-{\em before} each safe step of the search.
-
-\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.
-
-\item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}
-deletes the safe wrapper with the given name.
-
-\item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper}
-adds a new wrapper to modify the existing (unsafe) step tactic.
-
-\item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}
-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$ 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.
-
-\item[$cs$ delWrapper $name$] \indexbold{*delWrapper}
-deletes the unsafe wrapper with the given name.
-
-\item[$cs$ addSss $ss$] \indexbold{*addss}
-adds the simpset~$ss$ to the classical set. The assumptions and goal will be
-simplified, in a rather safe way, after each safe step of the search.
-
-\item[$cs$ addss $ss$] \indexbold{*addss}
-adds the simpset~$ss$ to the classical set. The assumptions and goal will be
-simplified, before the each unsafe step of the search.
-
-\end{ttdescription}
-
-\index{simplification!from classical reasoner}
-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
-implemented as wrapper tacticals.
-they
-\begin{warn}
-Being defined as wrappers, these operators are inappropriate for adding more
-than one simpset at a time: the simpset added last overwrites any earlier ones.
-When a simpset combined with a claset is to be augmented, this should done
-{\em before} combining it with the claset.
-\end{warn}
-
-
-\section{The classical tactics}
-
-\subsection{Other classical tactics}
-\begin{ttbox}
-slow_best_tac : claset -> int -> tactic
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
-best-first search to prove subgoal~$i$.
-\end{ttdescription}
-
-
-\subsection{Other useful tactics}
-\index{tactics!for contradiction}
-\index{tactics!for Modus Ponens}
-\begin{ttbox}
-contr_tac : int -> tactic
-mp_tac : int -> tactic
-eq_mp_tac : int -> tactic
-swap_res_tac : thm list -> int -> tactic
-\end{ttbox}
-These can be used in the body of a specialized search.
-\begin{ttdescription}
-\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
- solves subgoal~$i$ by detecting a contradiction among two assumptions of
- the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The
- tactic can produce multiple outcomes, enumerating all possible
- contradictions.
-
-\item[\ttindexbold{mp_tac} {\it i}]
-is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in
-subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces
-$P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do
-nothing.
-
-\item[\ttindexbold{eq_mp_tac} {\it i}]
-is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
-is safe.
-
-\item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
-the proof state using {\it thms}, which should be a list of introduction
-rules. First, it attempts to prove the goal using \texttt{assume_tac} or
-\texttt{contr_tac}. It then attempts to apply each rule in turn, attempting
-resolution and also elim-resolution with the swapped form.
-\end{ttdescription}
-
-\index{classical reasoner|)}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End:
--- a/src/Doc/Ref/document/root.tex Sun Nov 04 20:23:26 2012 +0100
+++ b/src/Doc/Ref/document/root.tex Wed Nov 07 12:14:38 2012 +0100
@@ -45,7 +45,6 @@
\input{syntax}
\input{substitution}
\input{simplifier}
-\input{classical}
%%seealso's must be last so that they appear last in the index entries
\index{meta-rewriting|seealso{tactics, theorems}}