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