--- a/doc-src/Functions/Thy/Functions.thy Mon Nov 23 15:05:59 2009 +0100
+++ b/doc-src/Functions/Thy/Functions.thy Mon Nov 23 15:06:34 2009 +0100
@@ -309,8 +309,6 @@
*** At command "fun".\newline
\end{isabelle}
*}
-
-
text {*
The key to this error message is the matrix at the bottom. The rows
of that matrix correspond to the different recursive calls (In our
@@ -326,27 +324,30 @@
For the failed proof attempts, the unfinished subgoals are also
printed. Looking at these will often point to a missing lemma.
+*}
-% As a more real example, here is quicksort:
-*}
-(*
-function qs :: "nat list \<Rightarrow> nat list"
-where
- "qs [] = []"
-| "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"
-by pat_completeness auto
+subsection {* The @{text size_change} method *}
-termination apply lexicographic_order
-
-text {* If we try @{text "lexicographic_order"} method, we get the
- following error *}
-termination by (lexicographic_order simp:l2)
+text {*
+ Some termination goals that are beyond the powers of
+ @{text lexicographic_order} can be solved automatically by the
+ more powerful @{text size_change} method, which uses a variant of
+ the size-change principle, together with some other
+ techniques. While the details are discussed
+ elsewhere\cite{krauss_phd},
+ here are a few typical situations where
+ @{text lexicographic_order} has difficulties and @{text size_change}
+ may be worth a try:
+ \begin{itemize}
+ \item Arguments are permuted in a recursive call.
+ \item Several mutually recursive functions with multiple arguments.
+ \item Unusual control flow (e.g., when some recursive calls cannot
+ occur in sequence).
+ \end{itemize}
-lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith
-
-function
-
-*)
+ Loading the theory @{text Multiset} makes the @{text size_change}
+ method a bit stronger: it can then use multiset orders internally.
+*}
section {* Mutual Recursion *}