doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 30172 afdf7808cfd0
parent 29560 fa6c5d62adf5
child 30863 5dc392a59bb7
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Feb 28 17:08:33 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Feb 28 17:09:32 2009 +0100
     1.3 @@ -779,6 +779,58 @@
     1.4  \end{isamarkuptext}%
     1.5  \isamarkuptrue%
     1.6  %
     1.7 +\isamarkupsection{Intuitionistic proof search%
     1.8 +}
     1.9 +\isamarkuptrue%
    1.10 +%
    1.11 +\begin{isamarkuptext}%
    1.12 +\begin{matharray}{rcl}
    1.13 +    \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\
    1.14 +  \end{matharray}
    1.15 +
    1.16 +  \begin{rail}
    1.17 +    'iprover' ('!' ?) (rulemod *)
    1.18 +    ;
    1.19 +  \end{rail}
    1.20 +
    1.21 +  The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
    1.22 +  search, depending on specifically declared rules from the context,
    1.23 +  or given as explicit arguments.  Chained facts are inserted into the
    1.24 +  goal before commencing proof search; ``\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
    1.25 +  
    1.26 +  Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
    1.27 +  \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
    1.28 +  ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
    1.29 +  applied aggressively (without considering back-tracking later).
    1.30 +  Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
    1.31 +  single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these).  An
    1.32 +  explicit weight annotation may be given as well; otherwise the
    1.33 +  number of rule premises will be taken into account here.%
    1.34 +\end{isamarkuptext}%
    1.35 +\isamarkuptrue%
    1.36 +%
    1.37 +\isamarkupsection{Coherent Logic%
    1.38 +}
    1.39 +\isamarkuptrue%
    1.40 +%
    1.41 +\begin{isamarkuptext}%
    1.42 +\begin{matharray}{rcl}
    1.43 +    \indexdef{HOL}{method}{coherent}\hypertarget{method.HOL.coherent}{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}} & : & \isa{method} \\
    1.44 +  \end{matharray}
    1.45 +
    1.46 +  \begin{rail}
    1.47 +    'coherent' thmrefs?
    1.48 +    ;
    1.49 +  \end{rail}
    1.50 +
    1.51 +  The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
    1.52 +  \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
    1.53 +  applications in confluence theory, lattice theory and projective
    1.54 +  geometry.  See \hyperlink{file.~~/src/HOL/ex/Coherent.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex{\isacharslash}Coherent{\isachardot}thy}}}} for some
    1.55 +  examples.%
    1.56 +\end{isamarkuptext}%
    1.57 +\isamarkuptrue%
    1.58 +%
    1.59  \isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
    1.60  }
    1.61  \isamarkuptrue%