# HG changeset patch # User wenzelm # Date 1352286878 -3600 # Node ID 959548c3b9476d739c755f20aaa1b91a65898889 # Parent e447ad4d6edd788143abce3903d06b15922cf8bc moved classical wrappers to IsarRef; removed somewhat pointless historic material; diff -r e447ad4d6edd -r 959548c3b947 src/Doc/IsarRef/Generic.thy --- 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 \ Q"} and + @{text "P"}, then replace @{text "P \ 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 {* diff -r e447ad4d6edd -r 959548c3b947 src/Doc/ROOT --- 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" diff -r e447ad4d6edd -r 959548c3b947 src/Doc/Ref/document/classical.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: diff -r e447ad4d6edd -r 959548c3b947 src/Doc/Ref/document/root.tex --- 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}}