documented size_change in isar-ref manual
authorkrauss
Mon Nov 23 15:06:38 2009 +0100 (2009-11-23)
changeset 338580c348f7997f7
parent 33857 0cb5002c52db
child 33859 033ce4cafba6
documented size_change in isar-ref manual
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     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  
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:37 2009 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:38 2009 +0100
     2.3 @@ -512,6 +512,7 @@
     2.4      \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isa{method} \\
     2.5      \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
     2.6      \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isa{method} \\
     2.7 +    \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}}} & : & \isa{method} \\
     2.8    \end{matharray}
     2.9  
    2.10    \begin{rail}
    2.11 @@ -519,6 +520,9 @@
    2.12      ;
    2.13      'lexicographic\_order' ( clasimpmod * )
    2.14      ;
    2.15 +    'size\_change' ( orders ( clasimpmod * ) )
    2.16 +    ;
    2.17 +    orders: ( 'max' | 'min' | 'ms' ) *
    2.18    \end{rail}
    2.19  
    2.20    \begin{description}
    2.21 @@ -546,6 +550,17 @@
    2.22    In case of failure, extensive information is printed, which can help
    2.23    to analyse the situation (cf.\ \cite{isabelle-function}).
    2.24  
    2.25 +  \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}} also works on termination goals,
    2.26 +  using a variation of the size-change principle, together with a
    2.27 +  graph decomposition technique (see \cite{krauss_phd} for details).
    2.28 +  Three kinds of orders are used internally: \isa{max}, \isa{min},
    2.29 +  and \isa{ms} (multiset), which is only available when the theory
    2.30 +  \isa{Multiset} is loaded. When no order kinds are given, they are
    2.31 +  tried in order. The search for a termination proof uses SAT solving
    2.32 +  internally.
    2.33 +
    2.34 + For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
    2.35 +
    2.36    \end{description}%
    2.37  \end{isamarkuptext}%
    2.38  \isamarkuptrue%