1.1 --- a/doc-src/Functions/Thy/Functions.thy	Mon Nov 23 15:05:59 2009 +0100
     1.2 +++ b/doc-src/Functions/Thy/Functions.thy	Mon Nov 23 15:06:34 2009 +0100
     1.3 @@ -309,8 +309,6 @@
     1.4  *** At command "fun".\newline
     1.5  \end{isabelle}
     1.6  *}
     1.7 -
     1.8 -
     1.9  text {*
    1.10    The key to this error message is the matrix at the bottom. The rows
    1.11    of that matrix correspond to the different recursive calls (In our
    1.12 @@ -326,27 +324,30 @@
    1.13  
    1.14    For the failed proof attempts, the unfinished subgoals are also
    1.15    printed. Looking at these will often point to a missing lemma.
    1.16 +*}
    1.17  
    1.18 -%  As a more real example, here is quicksort:
    1.19 +subsection {* The @{text size_change} method *}
    1.20 +
    1.21 +text {*
    1.22 +  Some termination goals that are beyond the powers of
    1.23 +  @{text lexicographic_order} can be solved automatically by the
    1.24 +  more powerful @{text size_change} method, which uses a variant of
    1.25 +  the size-change principle, together with some other
    1.26 +  techniques. While the details are discussed
    1.27 +  elsewhere\cite{krauss_phd},
    1.28 +  here are a few typical situations where
    1.29 +  @{text lexicographic_order} has difficulties and @{text size_change}
    1.30 +  may be worth a try:
    1.31 +  \begin{itemize}
    1.32 +  \item Arguments are permuted in a recursive call.
    1.33 +  \item Several mutually recursive functions with multiple arguments.
    1.34 +  \item Unusual control flow (e.g., when some recursive calls cannot
    1.35 +  occur in sequence).
    1.36 +  \end{itemize}
    1.37 +
    1.38 +  Loading the theory @{text Multiset} makes the @{text size_change}
    1.39 +  method a bit stronger: it can then use multiset orders internally.
    1.40  *}
    1.41 -(*
    1.42 -function qs :: "nat list \<Rightarrow> nat list"
    1.43 -where
    1.44 -  "qs [] = []"
    1.45 -| "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"
    1.46 -by pat_completeness auto
    1.47 -
    1.48 -termination apply lexicographic_order
    1.49 -
    1.50 -text {* If we try @{text "lexicographic_order"} method, we get the
    1.51 -  following error *}
    1.52 -termination by (lexicographic_order simp:l2)
    1.53 -
    1.54 -lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith
    1.55 -
    1.56 -function 
    1.57 -
    1.58 -*)
    1.59  
    1.60  section {* Mutual Recursion *}
    1.61  

     2.1 --- a/doc-src/Functions/Thy/document/Functions.tex	Mon Nov 23 15:05:59 2009 +0100
     2.2 +++ b/doc-src/Functions/Thy/document/Functions.tex	Mon Nov 23 15:06:34 2009 +0100
     2.3 @@ -453,9 +453,33 @@
     2.4    \isa{{\isacharless}}, \isa{{\isacharless}{\isacharequal}} and \isa{{\isacharquery}}.
     2.5  
     2.6    For the failed proof attempts, the unfinished subgoals are also
     2.7 -  printed. Looking at these will often point to a missing lemma.
     2.8 +  printed. Looking at these will often point to a missing lemma.%
     2.9 +\end{isamarkuptext}%
    2.10 +\isamarkuptrue%
    2.11 +%
    2.12 +\isamarkupsubsection{The \isa{size{\isacharunderscore}change} method%
    2.13 +}
    2.14 +\isamarkuptrue%
    2.15 +%
    2.16 +\begin{isamarkuptext}%
    2.17 +Some termination goals that are beyond the powers of
    2.18 +  \isa{lexicographic{\isacharunderscore}order} can be solved automatically by the
    2.19 +  more powerful \isa{size{\isacharunderscore}change} method, which uses a variant of
    2.20 +  the size-change principle, together with some other
    2.21 +  techniques. While the details are discussed
    2.22 +  elsewhere\cite{krauss_phd},
    2.23 +  here are a few typical situations where
    2.24 +  \isa{lexicographic{\isacharunderscore}order} has difficulties and \isa{size{\isacharunderscore}change}
    2.25 +  may be worth a try:
    2.26 +  \begin{itemize}
    2.27 +  \item Arguments are permuted in a recursive call.
    2.28 +  \item Several mutually recursive functions with multiple arguments.
    2.29 +  \item Unusual control flow (e.g., when some recursive calls cannot
    2.30 +  occur in sequence).
    2.31 +  \end{itemize}
    2.32  
    2.33 -%  As a more real example, here is quicksort:%
    2.34 +  Loading the theory \isa{Multiset} makes the \isa{size{\isacharunderscore}change}
    2.35 +  method a bit stronger: it can then use multiset orders internally.%
    2.36  \end{isamarkuptext}%
    2.37  \isamarkuptrue%
    2.38  %

     3.1 --- a/doc-src/manual.bib	Mon Nov 23 15:05:59 2009 +0100
     3.2 +++ b/doc-src/manual.bib	Mon Nov 23 15:06:34 2009 +0100
     3.3 @@ -660,6 +660,14 @@
     3.4    crossref =  {ijcar2006},
     3.5    pages =     {589--603}}
     3.6  
     3.7 +@PhdThesis{krauss_phd,
     3.8 +	author = {Alexander Krauss},
     3.9 +	title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
    3.10 +  school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
    3.11 +	year = {2009},
    3.12 +	address = {Germany}
    3.13 +}
    3.14 +
    3.15  @manual{isabelle-function,
    3.16    author        = {Alexander Krauss},
    3.17    title         = {Defining Recursive Functions in {Isabelle/HOL}},