moved classical wrappers to IsarRef;
authorwenzelm
Wed Nov 07 12:14:38 2012 +0100 (2012-11-07)
changeset 50071959548c3b947
parent 50070 e447ad4d6edd
child 50072 775445d65e17
moved classical wrappers to IsarRef;
removed somewhat pointless historic material;
src/Doc/IsarRef/Generic.thy
src/Doc/ROOT
src/Doc/Ref/document/classical.tex
src/Doc/Ref/document/root.tex
     1.1 --- a/src/Doc/IsarRef/Generic.thy	Sun Nov 04 20:23:26 2012 +0100
     1.2 +++ b/src/Doc/IsarRef/Generic.thy	Wed Nov 07 12:14:38 2012 +0100
     1.3 @@ -1362,13 +1362,13 @@
     1.4  subsection {* Single-step tactics *}
     1.5  
     1.6  text {*
     1.7 -  \begin{matharray}{rcl}
     1.8 +  \begin{mldecls}
     1.9      @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
    1.10      @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
    1.11      @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
    1.12      @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
    1.13      @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
    1.14 -  \end{matharray}
    1.15 +  \end{mldecls}
    1.16  
    1.17    These are the primitive tactics behind the automated proof methods
    1.18    of the Classical Reasoner.  By calling them yourself, you can
    1.19 @@ -1405,6 +1405,94 @@
    1.20  *}
    1.21  
    1.22  
    1.23 +subsection {* Modifying the search step *}
    1.24 +
    1.25 +text {*
    1.26 +  \begin{mldecls}
    1.27 +    @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
    1.28 +    @{index_ML_op addSWrapper: "claset * (string * (Proof.context -> wrapper))
    1.29 +  -> claset"} \\
    1.30 +    @{index_ML_op addSbefore: "claset * (string * (int -> tactic)) -> claset"} \\
    1.31 +    @{index_ML_op addSafter: "claset * (string * (int -> tactic)) -> claset"} \\
    1.32 +    @{index_ML_op delSWrapper: "claset * string -> claset"} \\[0.5ex]
    1.33 +    @{index_ML_op addWrapper: "claset * (string * (Proof.context -> wrapper))
    1.34 +  -> claset"} \\
    1.35 +    @{index_ML_op addbefore: "claset * (string * (int -> tactic)) -> claset"} \\
    1.36 +    @{index_ML_op addafter: "claset * (string * (int -> tactic)) -> claset"} \\
    1.37 +    @{index_ML_op delWrapper: "claset * string -> claset"} \\[0.5ex]
    1.38 +    @{index_ML addSss: "Proof.context -> Proof.context"} \\
    1.39 +    @{index_ML addss: "Proof.context -> Proof.context"} \\
    1.40 +  \end{mldecls}
    1.41 +
    1.42 +  The proof strategy of the Classical Reasoner is simple.  Perform as
    1.43 +  many safe inferences as possible; or else, apply certain safe rules,
    1.44 +  allowing instantiation of unknowns; or else, apply an unsafe rule.
    1.45 +  The tactics also eliminate assumptions of the form @{text "x = t"}
    1.46 +  by substitution if they have been set up to do so.  They may perform
    1.47 +  a form of Modus Ponens: if there are assumptions @{text "P \<longrightarrow> Q"} and
    1.48 +  @{text "P"}, then replace @{text "P \<longrightarrow> Q"} by @{text "Q"}.
    1.49 +
    1.50 +  The classical reasoning tools --- except @{method blast} --- allow
    1.51 +  to modify this basic proof strategy by applying two lists of
    1.52 +  arbitrary \emph{wrapper tacticals} to it.  The first wrapper list,
    1.53 +  which is considered to contain safe wrappers only, affects @{ML
    1.54 +  safe_step_tac} and all the tactics that call it.  The second one,
    1.55 +  which may contain unsafe wrappers, affects the unsafe parts of @{ML
    1.56 +  step_tac}, @{ML slow_step_tac}, and the tactics that call them.  A
    1.57 +  wrapper transforms each step of the search, for example by
    1.58 +  attempting other tactics before or after the original step tactic.
    1.59 +  All members of a wrapper list are applied in turn to the respective
    1.60 +  step tactic.
    1.61 +
    1.62 +  Initially the two wrapper lists are empty, which means no
    1.63 +  modification of the step tactics. Safe and unsafe wrappers are added
    1.64 +  to a claset with the functions given below, supplying them with
    1.65 +  wrapper names.  These names may be used to selectively delete
    1.66 +  wrappers.
    1.67 +
    1.68 +  \begin{description}
    1.69 +
    1.70 +  \item @{text "cs addSWrapper (name, wrapper)"} adds a new wrapper,
    1.71 +  which should yield a safe tactic, to modify the existing safe step
    1.72 +  tactic.
    1.73 +
    1.74 +  \item @{text "cs addSbefore (name, tac)"} adds the given tactic as a
    1.75 +  safe wrapper, such that it is tried \emph{before} each safe step of
    1.76 +  the search.
    1.77 +
    1.78 +  \item @{text "cs addSafter (name, tac)"} adds the given tactic as a
    1.79 +  safe wrapper, such that it is tried when a safe step of the search
    1.80 +  would fail.
    1.81 +
    1.82 +  \item @{text "cs delSWrapper name"} deletes the safe wrapper with
    1.83 +  the given name.
    1.84 +
    1.85 +  \item @{text "cs addWrapper (name, wrapper)"} adds a new wrapper to
    1.86 +  modify the existing (unsafe) step tactic.
    1.87 +
    1.88 +  \item @{text "cs addbefore (name, tac)"} adds the given tactic as an
    1.89 +  unsafe wrapper, such that it its result is concatenated
    1.90 +  \emph{before} the result of each unsafe step.
    1.91 +
    1.92 +  \item @{text "cs addafter (name, tac)"} adds the given tactic as an
    1.93 +  unsafe wrapper, such that it its result is concatenated \emph{after}
    1.94 +  the result of each unsafe step.
    1.95 +
    1.96 +  \item @{text "cs delWrapper name"} deletes the unsafe wrapper with
    1.97 +  the given name.
    1.98 +
    1.99 +  \item @{text "addSss"} adds the simpset of the context to its
   1.100 +  classical set. The assumptions and goal will be simplified, in a
   1.101 +  rather safe way, after each safe step of the search.
   1.102 +
   1.103 +  \item @{text "addss"} adds the simpset of the context to its
   1.104 +  classical set. The assumptions and goal will be simplified, before
   1.105 +  the each unsafe step of the search.
   1.106 +
   1.107 +  \end{description}
   1.108 +*}
   1.109 +
   1.110 +
   1.111  section {* Object-logic setup \label{sec:object-logic} *}
   1.112  
   1.113  text {*
     2.1 --- a/src/Doc/ROOT	Sun Nov 04 20:23:26 2012 +0100
     2.2 +++ b/src/Doc/ROOT	Wed Nov 07 12:14:38 2012 +0100
     2.3 @@ -261,7 +261,6 @@
     2.4      "../proof.sty"
     2.5      "../manual.bib"
     2.6      "document/build"
     2.7 -    "document/classical.tex"
     2.8      "document/root.tex"
     2.9      "document/simplifier.tex"
    2.10      "document/substitution.tex"
     3.1 --- a/src/Doc/Ref/document/classical.tex	Sun Nov 04 20:23:26 2012 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,178 +0,0 @@
     3.4 -
     3.5 -\chapter{The Classical Reasoner}\label{chap:classical}
     3.6 -\index{classical reasoner|(}
     3.7 -\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
     3.8 -
     3.9 -\section{Classical rule sets}
    3.10 -\index{classical sets}
    3.11 -
    3.12 -For elimination and destruction rules there are variants of the add operations
    3.13 -adding a rule in a way such that it is applied only if also its second premise
    3.14 -can be unified with an assumption of the current proof state:
    3.15 -\indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2}
    3.16 -\begin{ttbox}
    3.17 -addSE2      : claset * (string * thm) -> claset           \hfill{\bf infix 4}
    3.18 -addSD2      : claset * (string * thm) -> claset           \hfill{\bf infix 4}
    3.19 -addE2       : claset * (string * thm) -> claset           \hfill{\bf infix 4}
    3.20 -addD2       : claset * (string * thm) -> claset           \hfill{\bf infix 4}
    3.21 -\end{ttbox}
    3.22 -\begin{warn}
    3.23 -  A rule to be added in this special way must be given a name, which is used 
    3.24 -  to delete it again -- when desired -- using \texttt{delSWrappers} or 
    3.25 -  \texttt{delWrappers}, respectively. This is because these add operations
    3.26 -  are implemented as wrappers (see \ref{sec:modifying-search} below).
    3.27 -\end{warn}
    3.28 -
    3.29 -
    3.30 -\subsection{Modifying the search step}
    3.31 -\label{sec:modifying-search}
    3.32 -For a given classical set, the proof strategy is simple.  Perform as many safe
    3.33 -inferences as possible; or else, apply certain safe rules, allowing
    3.34 -instantiation of unknowns; or else, apply an unsafe rule.  The tactics also
    3.35 -eliminate assumptions of the form $x=t$ by substitution if they have been set
    3.36 -up to do so (see \texttt{hyp_subst_tacs} in~{\S}\ref{sec:classical-setup} below).
    3.37 -They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
    3.38 -and~$P$, then replace $P\imp Q$ by~$Q$.
    3.39 -
    3.40 -The classical reasoning tactics --- except \texttt{blast_tac}! --- allow
    3.41 -you to modify this basic proof strategy by applying two lists of arbitrary 
    3.42 -{\bf wrapper tacticals} to it. 
    3.43 -The first wrapper list, which is considered to contain safe wrappers only, 
    3.44 -affects \ttindex{safe_step_tac} and all the tactics that call it.  
    3.45 -The second one, which may contain unsafe wrappers, affects the unsafe parts
    3.46 -of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them.
    3.47 -A wrapper transforms each step of the search, for example 
    3.48 -by attempting other tactics before or after the original step tactic. 
    3.49 -All members of a wrapper list are applied in turn to the respective step tactic.
    3.50 -
    3.51 -Initially the two wrapper lists are empty, which means no modification of the
    3.52 -step tactics. Safe and unsafe wrappers are added to a claset 
    3.53 -with the functions given below, supplying them with wrapper names. 
    3.54 -These names may be used to selectively delete wrappers.
    3.55 -
    3.56 -\begin{ttbox} 
    3.57 -type wrapper = (int -> tactic) -> (int -> tactic);
    3.58 -
    3.59 -addSWrapper  : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}
    3.60 -addSbefore   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
    3.61 -addSafter    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
    3.62 -delSWrapper  : claset *  string                    -> claset \hfill{\bf infix 4}
    3.63 -
    3.64 -addWrapper   : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}
    3.65 -addbefore    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
    3.66 -addafter     : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
    3.67 -delWrapper   : claset *  string                    -> claset \hfill{\bf infix 4}
    3.68 -
    3.69 -addSss       : claset * simpset -> claset                 \hfill{\bf infix 4}
    3.70 -addss        : claset * simpset -> claset                 \hfill{\bf infix 4}
    3.71 -\end{ttbox}
    3.72 -%
    3.73 -
    3.74 -\begin{ttdescription}
    3.75 -\item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper}
    3.76 -adds a new wrapper, which should yield a safe tactic, 
    3.77 -to modify the existing safe step tactic.
    3.78 -
    3.79 -\item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}
    3.80 -adds the given tactic as a safe wrapper, such that it is tried 
    3.81 -{\em before} each safe step of the search.
    3.82 -
    3.83 -\item[$cs$ addSafter $(name,tac)$] \indexbold{*addSafter}
    3.84 -adds the given tactic as a safe wrapper, such that it is tried 
    3.85 -when a safe step of the search would fail.
    3.86 -
    3.87 -\item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}
    3.88 -deletes the safe wrapper with the given name.
    3.89 -
    3.90 -\item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper}
    3.91 -adds a new wrapper to modify the existing (unsafe) step tactic.
    3.92 -
    3.93 -\item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}
    3.94 -adds the given tactic as an unsafe wrapper, such that it its result is 
    3.95 -concatenated {\em before} the result of each unsafe step.
    3.96 -
    3.97 -\item[$cs$ addafter $(name,tac)$] \indexbold{*addafter}
    3.98 -adds the given tactic as an unsafe wrapper, such that it its result is 
    3.99 -concatenated {\em after} the result of each unsafe step.
   3.100 -
   3.101 -\item[$cs$ delWrapper $name$] \indexbold{*delWrapper}
   3.102 -deletes the unsafe wrapper with the given name.
   3.103 -
   3.104 -\item[$cs$ addSss $ss$] \indexbold{*addss}
   3.105 -adds the simpset~$ss$ to the classical set.  The assumptions and goal will be
   3.106 -simplified, in a rather safe way, after each safe step of the search.
   3.107 -
   3.108 -\item[$cs$ addss $ss$] \indexbold{*addss}
   3.109 -adds the simpset~$ss$ to the classical set.  The assumptions and goal will be
   3.110 -simplified, before the each unsafe step of the search.
   3.111 -
   3.112 -\end{ttdescription}
   3.113 -
   3.114 -\index{simplification!from classical reasoner} 
   3.115 -Strictly speaking, the operators \texttt{addss} and \texttt{addSss}
   3.116 -are not part of the classical reasoner.
   3.117 -, which are used as primitives 
   3.118 -for the automatic tactics described in {\S}\ref{sec:automatic-tactics}, are
   3.119 -implemented as wrapper tacticals.
   3.120 -they  
   3.121 -\begin{warn}
   3.122 -Being defined as wrappers, these operators are inappropriate for adding more 
   3.123 -than one simpset at a time: the simpset added last overwrites any earlier ones.
   3.124 -When a simpset combined with a claset is to be augmented, this should done 
   3.125 -{\em before} combining it with the claset.
   3.126 -\end{warn}
   3.127 -
   3.128 -
   3.129 -\section{The classical tactics}
   3.130 -
   3.131 -\subsection{Other classical tactics}
   3.132 -\begin{ttbox} 
   3.133 -slow_best_tac : claset -> int -> tactic
   3.134 -\end{ttbox}
   3.135 -
   3.136 -\begin{ttdescription}
   3.137 -\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
   3.138 -best-first search to prove subgoal~$i$.
   3.139 -\end{ttdescription}
   3.140 -
   3.141 -
   3.142 -\subsection{Other useful tactics}
   3.143 -\index{tactics!for contradiction}
   3.144 -\index{tactics!for Modus Ponens}
   3.145 -\begin{ttbox} 
   3.146 -contr_tac    :             int -> tactic
   3.147 -mp_tac       :             int -> tactic
   3.148 -eq_mp_tac    :             int -> tactic
   3.149 -swap_res_tac : thm list -> int -> tactic
   3.150 -\end{ttbox}
   3.151 -These can be used in the body of a specialized search.
   3.152 -\begin{ttdescription}
   3.153 -\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
   3.154 -  solves subgoal~$i$ by detecting a contradiction among two assumptions of
   3.155 -  the form $P$ and~$\neg P$, or fail.  It may instantiate unknowns.  The
   3.156 -  tactic can produce multiple outcomes, enumerating all possible
   3.157 -  contradictions.
   3.158 -
   3.159 -\item[\ttindexbold{mp_tac} {\it i}] 
   3.160 -is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in
   3.161 -subgoal~$i$.  If there are assumptions $P\imp Q$ and~$P$, then it replaces
   3.162 -$P\imp Q$ by~$Q$.  It may instantiate unknowns.  It fails if it can do
   3.163 -nothing.
   3.164 -
   3.165 -\item[\ttindexbold{eq_mp_tac} {\it i}] 
   3.166 -is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
   3.167 -is safe.
   3.168 -
   3.169 -\item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
   3.170 -the proof state using {\it thms}, which should be a list of introduction
   3.171 -rules.  First, it attempts to prove the goal using \texttt{assume_tac} or
   3.172 -\texttt{contr_tac}.  It then attempts to apply each rule in turn, attempting
   3.173 -resolution and also elim-resolution with the swapped form.
   3.174 -\end{ttdescription}
   3.175 -
   3.176 -\index{classical reasoner|)}
   3.177 -
   3.178 -%%% Local Variables: 
   3.179 -%%% mode: latex
   3.180 -%%% TeX-master: "ref"
   3.181 -%%% End: 
     4.1 --- a/src/Doc/Ref/document/root.tex	Sun Nov 04 20:23:26 2012 +0100
     4.2 +++ b/src/Doc/Ref/document/root.tex	Wed Nov 07 12:14:38 2012 +0100
     4.3 @@ -45,7 +45,6 @@
     4.4  \input{syntax}
     4.5  \input{substitution}
     4.6  \input{simplifier}
     4.7 -\input{classical}
     4.8  
     4.9  %%seealso's must be last so that they appear last in the index entries
    4.10  \index{meta-rewriting|seealso{tactics, theorems}}