# HG changeset patch
# User krauss
# Date 1258985194 -3600
# Node ID 14a658faadb6bb2d75191bd09ba5a2f1555f6406
# Parent  cd8acf137c9c9a54d746ede368a015fd977cc4f8
mentioned method size_change in function tutorial

diff -r cd8acf137c9c -r 14a658faadb6 doc-src/Functions/Thy/Functions.thy
--- 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 *}
 
diff -r cd8acf137c9c -r 14a658faadb6 doc-src/Functions/Thy/document/Functions.tex
--- a/doc-src/Functions/Thy/document/Functions.tex	Mon Nov 23 15:05:59 2009 +0100
+++ b/doc-src/Functions/Thy/document/Functions.tex	Mon Nov 23 15:06:34 2009 +0100
@@ -453,9 +453,33 @@
   \isa{{\isacharless}}, \isa{{\isacharless}{\isacharequal}} and \isa{{\isacharquery}}.
 
   For the failed proof attempts, the unfinished subgoals are also
-  printed. Looking at these will often point to a missing lemma.
+  printed. Looking at these will often point to a missing lemma.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The \isa{size{\isacharunderscore}change} method%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Some termination goals that are beyond the powers of
+  \isa{lexicographic{\isacharunderscore}order} can be solved automatically by the
+  more powerful \isa{size{\isacharunderscore}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
+  \isa{lexicographic{\isacharunderscore}order} has difficulties and \isa{size{\isacharunderscore}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}
 
-%  As a more real example, here is quicksort:%
+  Loading the theory \isa{Multiset} makes the \isa{size{\isacharunderscore}change}
+  method a bit stronger: it can then use multiset orders internally.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r cd8acf137c9c -r 14a658faadb6 doc-src/manual.bib
--- a/doc-src/manual.bib	Mon Nov 23 15:05:59 2009 +0100
+++ b/doc-src/manual.bib	Mon Nov 23 15:06:34 2009 +0100
@@ -660,6 +660,14 @@
   crossref =  {ijcar2006},
   pages =     {589--603}}
 
+@PhdThesis{krauss_phd,
+	author = {Alexander Krauss},
+	title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
+  school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
+	year = {2009},
+	address = {Germany}
+}
+
 @manual{isabelle-function,
   author        = {Alexander Krauss},
   title         = {Defining Recursive Functions in {Isabelle/HOL}},