doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 30240 5b25fee0362c
parent 29560 fa6c5d62adf5
child 30242 aea5d7fa7ef5
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -771,6 +771,55 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +section {* Intuitionistic proof search *}
     1.8 +
     1.9 +text {*
    1.10 +  \begin{matharray}{rcl}
    1.11 +    @{method_def (HOL) iprover} & : & @{text method} \\
    1.12 +  \end{matharray}
    1.13 +
    1.14 +  \begin{rail}
    1.15 +    'iprover' ('!' ?) (rulemod *)
    1.16 +    ;
    1.17 +  \end{rail}
    1.18 +
    1.19 +  The @{method (HOL) iprover} method performs intuitionistic proof
    1.20 +  search, depending on specifically declared rules from the context,
    1.21 +  or given as explicit arguments.  Chained facts are inserted into the
    1.22 +  goal before commencing proof search; ``@{method (HOL) iprover}@{text
    1.23 +  "!"}''  means to include the current @{fact prems} as well.
    1.24 +  
    1.25 +  Rules need to be classified as @{attribute (Pure) intro},
    1.26 +  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
    1.27 +  ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
    1.28 +  applied aggressively (without considering back-tracking later).
    1.29 +  Rules declared with ``@{text "?"}'' are ignored in proof search (the
    1.30 +  single-step @{method rule} method still observes these).  An
    1.31 +  explicit weight annotation may be given as well; otherwise the
    1.32 +  number of rule premises will be taken into account here.
    1.33 +*}
    1.34 +
    1.35 +
    1.36 +section {* Coherent Logic *}
    1.37 +
    1.38 +text {*
    1.39 +  \begin{matharray}{rcl}
    1.40 +    @{method_def (HOL) "coherent"} & : & @{text method} \\
    1.41 +  \end{matharray}
    1.42 +
    1.43 +  \begin{rail}
    1.44 +    'coherent' thmrefs?
    1.45 +    ;
    1.46 +  \end{rail}
    1.47 +
    1.48 +  The @{method (HOL) coherent} method solves problems of
    1.49 +  \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
    1.50 +  applications in confluence theory, lattice theory and projective
    1.51 +  geometry.  See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some
    1.52 +  examples.
    1.53 +*}
    1.54 +
    1.55 +
    1.56  section {* Invoking automated reasoning tools -- The Sledgehammer *}
    1.57  
    1.58  text {*