doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 33858 0c348f7997f7
parent 33857 0cb5002c52db
child 34172 4301e9ea1c54
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Nov 23 15:06:37 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Nov 23 15:06:38 2009 +0100
     1.3 @@ -506,6 +506,7 @@
     1.4      @{method_def (HOL) pat_completeness} & : & @{text method} \\
     1.5      @{method_def (HOL) relation} & : & @{text method} \\
     1.6      @{method_def (HOL) lexicographic_order} & : & @{text method} \\
     1.7 +    @{method_def (HOL) size_change} & : & @{text method} \\
     1.8    \end{matharray}
     1.9  
    1.10    \begin{rail}
    1.11 @@ -513,6 +514,9 @@
    1.12      ;
    1.13      'lexicographic\_order' ( clasimpmod * )
    1.14      ;
    1.15 +    'size\_change' ( orders ( clasimpmod * ) )
    1.16 +    ;
    1.17 +    orders: ( 'max' | 'min' | 'ms' ) *
    1.18    \end{rail}
    1.19  
    1.20    \begin{description}
    1.21 @@ -540,6 +544,18 @@
    1.22    In case of failure, extensive information is printed, which can help
    1.23    to analyse the situation (cf.\ \cite{isabelle-function}).
    1.24  
    1.25 +  \item @{method (HOL) "size_change"} also works on termination goals,
    1.26 +  using a variation of the size-change principle, together with a
    1.27 +  graph decomposition technique (see \cite{krauss_phd} for details).
    1.28 +  Three kinds of orders are used internally: @{text max}, @{text min},
    1.29 +  and @{text ms} (multiset), which is only available when the theory
    1.30 +  @{text Multiset} is loaded. When no order kinds are given, they are
    1.31 +  tried in order. The search for a termination proof uses SAT solving
    1.32 +  internally.
    1.33 +
    1.34 + For local descent proofs, the same context modifiers as for @{method
    1.35 +  auto} are accepted, see \secref{sec:clasimp}.
    1.36 +
    1.37    \end{description}
    1.38  *}
    1.39