cover method "deepen" concisely;
authorwenzelm
Sat Jun 11 16:05:17 2011 +0200 (2011-06-11)
changeset 433673f1469de9e47
parent 43366 9cbcab5c780a
child 43368 0dc67b3cf8a5
cover method "deepen" concisely;
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/Ref/classical.tex
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 15:36:46 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 16:05:17 2011 +0200
     1.3 @@ -935,6 +935,7 @@
     1.4      @{method_def fastsimp} & : & @{text method} \\
     1.5      @{method_def slowsimp} & : & @{text method} \\
     1.6      @{method_def bestsimp} & : & @{text method} \\
     1.7 +    @{method_def deepen} & : & @{text method} \\
     1.8    \end{matharray}
     1.9  
    1.10    @{rail "
    1.11 @@ -949,6 +950,8 @@
    1.12      (@@{method fastsimp} | @@{method slowsimp} | @@{method bestsimp})
    1.13        (@{syntax clasimpmod} * )
    1.14      ;
    1.15 +    @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
    1.16 +    ;
    1.17      @{syntax_def clamod}:
    1.18        (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
    1.19      ;
    1.20 @@ -1033,6 +1036,14 @@
    1.21    like @{method fast}, @{method slow}, @{method best}, respectively,
    1.22    but use the Simplifier as additional wrapper.
    1.23  
    1.24 +  \item @{method deepen} works by exhaustive search up to a certain
    1.25 +  depth.  The start depth is 4 (unless specified explicitly), and the
    1.26 +  depth is increased iteratively up to 10.  Unsafe rules are modified
    1.27 +  to preserve the formula they act on, so that it be used repeatedly.
    1.28 +  This method can prove more goals than @{method fast}, but is much
    1.29 +  slower, for example if the assumptions have many universal
    1.30 +  quantifiers.
    1.31 +
    1.32    \end{description}
    1.33  
    1.34    Any of the above methods support additional modifiers of the context
     2.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 15:36:46 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 16:05:17 2011 +0200
     2.3 @@ -1387,6 +1387,7 @@
     2.4      \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
     2.5      \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
     2.6      \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
     2.7 +    \indexdef{}{method}{deepen}\hypertarget{method.deepen}{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}} & : & \isa{method} \\
     2.8    \end{matharray}
     2.9  
    2.10    \begin{railoutput}
    2.11 @@ -1446,6 +1447,17 @@
    2.12  \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
    2.13  \rail@endplus
    2.14  \rail@end
    2.15 +\rail@begin{2}{}
    2.16 +\rail@term{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}}[]
    2.17 +\rail@bar
    2.18 +\rail@nextbar{1}
    2.19 +\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
    2.20 +\rail@endbar
    2.21 +\rail@plus
    2.22 +\rail@nextplus{1}
    2.23 +\rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
    2.24 +\rail@endplus
    2.25 +\rail@end
    2.26  \rail@begin{4}{\indexdef{}{syntax}{clamod}\hypertarget{syntax.clamod}{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}}
    2.27  \rail@bar
    2.28  \rail@bar
    2.29 @@ -1602,6 +1614,14 @@
    2.30    like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively,
    2.31    but use the Simplifier as additional wrapper.
    2.32  
    2.33 +  \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain
    2.34 +  depth.  The start depth is 4 (unless specified explicitly), and the
    2.35 +  depth is increased iteratively up to 10.  Unsafe rules are modified
    2.36 +  to preserve the formula they act on, so that it be used repeatedly.
    2.37 +  This method can prove more goals than \hyperlink{method.fast}{\mbox{\isa{fast}}}, but is much
    2.38 +  slower, for example if the assumptions have many universal
    2.39 +  quantifiers.
    2.40 +
    2.41    \end{description}
    2.42  
    2.43    Any of the above methods support additional modifiers of the context
     3.1 --- a/doc-src/Ref/classical.tex	Sat Jun 11 15:36:46 2011 +0200
     3.2 +++ b/doc-src/Ref/classical.tex	Sat Jun 11 16:05:17 2011 +0200
     3.3 @@ -136,28 +136,6 @@
     3.4  \end{ttdescription}
     3.5  
     3.6  
     3.7 -\subsection{Depth-limited automatic tactics}
     3.8 -\begin{ttbox} 
     3.9 -depth_tac  : claset -> int -> int -> tactic
    3.10 -deepen_tac : claset -> int -> int -> tactic
    3.11 -\end{ttbox}
    3.12 -These work by exhaustive search up to a specified depth.  Unsafe rules are
    3.13 -modified to preserve the formula they act on, so that it be used repeatedly.
    3.14 -They can prove more goals than \texttt{fast_tac} can but are much
    3.15 -slower, for example if the assumptions have many universal quantifiers.
    3.16 -
    3.17 -The depth limits the number of unsafe steps.  If you can estimate the minimum
    3.18 -number of unsafe steps needed, supply this value as~$m$ to save time.
    3.19 -\begin{ttdescription}
    3.20 -\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
    3.21 -tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
    3.22 -
    3.23 -\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
    3.24 -tries to prove subgoal~$i$ by iterative deepening.  It calls \texttt{depth_tac}
    3.25 -repeatedly with increasing depths, starting with~$m$.
    3.26 -\end{ttdescription}
    3.27 -
    3.28 -
    3.29  \subsection{Other useful tactics}
    3.30  \index{tactics!for contradiction}
    3.31  \index{tactics!for Modus Ponens}