--- a/doc-src/TutorialI/Recdef/termination.thy Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/Recdef/termination.thy Thu Dec 13 16:48:34 2001 +0100
@@ -14,55 +14,57 @@
simplification rules.
Isabelle may fail to prove the termination condition for some
-recursive call. Let us try the following artificial function:*}
+recursive call. Let us try to define Quicksort:*}
-consts f :: "nat\<times>nat \<Rightarrow> nat"
-recdef (*<*)(permissive)(*>*)f "measure(\<lambda>(x,y). x-y)"
- "f(x,y) = (if x \<le> y then x else f(x,y+1))"
+consts qs :: "nat list \<Rightarrow> nat list"
+recdef(*<*)(permissive)(*>*) qs "measure length"
+ "qs [] = []"
+ "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)"
-text{*\noindent This definition fails, and Isabelle prints an error message
-showing you what it was unable to prove. You will then have to prove it as a
-separate lemma before you attempt the definition of your function once
-more. In our case the required lemma is the obvious one: *}
+text{*\noindent where @{term filter} is predefined and @{term"filter P xs"}
+is the list of elements of @{term xs} satisfying @{term P}.
+This definition of @{term qs} fails, and Isabelle prints an error message
+showing you what it was unable to prove:
+@{text[display]"length (filter ... xs) < Suc (length xs)"}
+We can either prove this as a separate lemma, or try to figure out which
+existing lemmas may help. We opt for the second alternative. The theory of
+lists contains the simplification rule @{thm length_filter[no_vars]},
+which is already
+close to what we need, except that we still need to turn \mbox{@{text"< Suc"}}
+into
+@{text"\<le>"} for the simplification rule to apply. Lemma
+@{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}.
-lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y"
+Now we retry the above definition but supply the lemma(s) just found (or
+proved). Because \isacommand{recdef}'s termination prover involves
+simplification, we include in our second attempt a hint: the
+\attrdx{recdef_simp} attribute says to use @{thm[source]less_Suc_eq_le} as a
+simplification rule. *}
-txt{*\noindent
-It was not proved automatically because of the awkward behaviour of subtraction
-on type @{typ"nat"}. This requires more arithmetic than is tried by default:
+(*<*)global consts qs :: "nat list \<Rightarrow> nat list" (*>*)
+recdef qs "measure length"
+ "qs [] = []"
+ "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)"
+(hints recdef_simp: less_Suc_eq_le)
+(*<*)local(*>*)
+text{*\noindent
+This time everything works fine. Now @{thm[source]qs.simps} contains precisely
+the stated recursion equations for @{text qs} and they have become
+simplification rules.
+Thus we can automatically prove results such as this one:
*}
-apply(arith)
-done
-
-text{*\noindent
-Because \isacommand{recdef}'s termination prover involves simplification,
-we include in our second attempt a hint: the \attrdx{recdef_simp} attribute
-says to use @{thm[source]termi_lem} as a simplification rule.
-*}
-
-(*<*)global consts f :: "nat\<times>nat \<Rightarrow> nat" (*>*)
-recdef f "measure(\<lambda>(x,y). x-y)"
- "f(x,y) = (if x \<le> y then x else f(x,y+1))"
-(hints recdef_simp: termi_lem)
-(*<*)local(*>*)
-text{*\noindent
-This time everything works fine. Now @{thm[source]f.simps} contains precisely
-the stated recursion equation for @{text f}, which has been turned into a
-simplification rule. Thus we can automatically prove results such as this one:
-*}
-
-theorem "f(1,0) = f(1,1)"
+theorem "qs[2,3,0] = qs[3,0,2]"
apply(simp)
done
text{*\noindent
More exciting theorems require induction, which is discussed below.
-If the termination proof requires a new lemma that is of general use, you can
+If the termination proof requires a lemma that is of general use, you can
turn it permanently into a simplification rule, in which case the above
-\isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not
-sufficiently general to warrant this distinction.
+\isacommand{hint} is not necessary. But in the case of
+@{thm[source]less_Suc_eq_le} this would be of dubious value.
*}
(*<*)
end