Quelle termination.thy

Sprache: Isabelle

(*<*)
theory "termination" imports examples begin
(*>*)

text‹
a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove
termination with the help of the user-supplied measure. Each of the examples
is simple enough that Isabelle can automatically prove that the
's measure decreases in each recursive call. As a result,
f$‹.simps› will contain the defining equations (or variants derived
them) as theorems. For example, look (via \isacommand{thm}) at
{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define
same function. What is more, those equations are automatically declared as
rules.

may fail to prove the termination condition for some
call. Let us try to define Quicksort:›

consts qs :: "nat list ==> nat list"
recdef(*<*)(permissive)(*>*) qs "measure length"
"qs [] = []"
"qs(x#xs) = qs(filter (λy. y≤x) xs) @ [x] @ qs(filter (λy. x<y) xs)"

text‹\noindent where @{term filter} is predefined and @{term"filter P xs"}
the list of elements of @{term xs} satisfying @{term P}.
definition of @{term qs} fails, and Isabelle prints an error message
you what it was unable to prove:
{text[display]"length (filter ... xs) < Suc (length xs)"}
can either prove this as a separate lemma, or try to figure out which
lemmas may help. We opt for the second alternative. The theory of
contains the simplification rule @{thm length_filter_le[no_vars]},
is what we need, provided we turn \mbox{‹< Suc›}

‹≤› so that the rule applies. Lemma
{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}.

we retry the above definition but supply the lemma(s) just found (or
). Because \isacommand{recdef}'s termination prover involves
, we include in our second attempt a hint: the
attrdx{recdef_simp} attribute says to use @{thm[source]less_Suc_eq_le} as a
rule.\cmmdx{hints}›

(*<*)global consts qs :: "nat list \<Rightarrow> nat list" (*>*)
recdef qs "measure length"
"qs [] = []"
"qs(x#xs) = qs(filter (λy. y≤x) xs) @ [x] @ qs(filter (λy. x<y) xs)"
(hints recdef_simp: less_Suc_eq_le)
(*<*)local(*>*)
text‹\noindent
time everything works fine. Now @{thm[source]qs.simps} contains precisely
stated recursion equations for ‹qs› and they have become
rules.
we can automatically prove results such as this one:
›

theorem "qs[2,3,0] = qs[3,0,2]"
apply(simp)
done

text‹\noindent
exciting theorems require induction, which is discussed below.

the termination proof requires a lemma that is of general use, you can
it permanently into a simplification rule, in which case the above
isacommand{hint} is not necessary. But in the case of
{thm[source]less_Suc_eq_le} this would be of dubious value.
›
(*<*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.