Quelle WFrec.thy

Sprache: Isabelle

(*<*)theory WFrec imports Main begin(*>*)

text‹\noindent
far, all recursive definitions were shown to terminate via measure
. Sometimes this can be inconvenient or
. Fortunately, \isacommand{recdef} supports much more
definitions. For example, termination of Ackermann's function
be shown by means of the \rmindex{lexicographic product} ‹<*lex*>›:
›

consts ack :: "nat×nat ==> nat"
recdef ack "measure(λm. m) <*lex*> measure(λn. n)"
  "ack(0,n) = Suc n"
  "ack(Suc m,0) = ack(m, 1)"
  "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"

text‹\noindent
lexicographic product decreases if either its first component
(as in the second equation and in the outer call in the
equation) or its first component stays the same and the second
decreases (as in the inner call in the third equation).

general, \isacommand{recdef} supports termination proofs based on
well-founded relations as introduced in \S\ref{sec:Well-founded}.
is called \textbf{well-founded
}\indexbold{recursion!well-founded}. A function definition
total if and only if the set of
pairs $(r,l)$, where $l$ is the argument on the
-hand side of an equation and $r$ the argument of some recursive call on
corresponding right-hand side, induces a well-founded relation. For a
account of termination proofs via well-founded relations see, for
, Baader and Nipkow~@{cite "Baader-Nipkow"}.

\isacommand{recdef} definition should be accompanied (after the function's
) by a well-founded relation on the function's argument type.
/HOL formalizes some of the most important
of well-founded relations (see \S\ref{sec:Well-founded}). For
, @{term"measure f"} is always well-founded. The lexicographic
of two well-founded relations is again well-founded, which we relied
when defining Ackermann's function above.
course the lexicographic product can also be iterated:
›

consts contrived :: "nat × nat × nat ==> nat"
recdef contrived
  "measure(λi. i) <*lex*> measure(λj. j) <*lex*> measure(λk. k)"
"contrived(i,j,Suc k) = contrived(i,j,k)"
"contrived(i,Suc j,0) = contrived(i,j,j)"
"contrived(Suc i,0,0) = contrived(i,i,i)"
"contrived(0,0,0) = 0"

text‹
products of measure functions already go a long
. Furthermore, you may embed a type in an
well-founded relation via the inverse image construction @{term
}. All these constructions are known to \isacommand{recdef}. Thus you
never have to prove well-foundedness of any relation composed
of these building blocks. But of course the proof of
of your function definition --- that the arguments
with every recursive call --- may still require you to provide
lemmas.

is also possible to use your own well-founded relations with
isacommand{recdef}. For example, the greater-than relation can be made
-founded by cutting it off at a certain point. Here is an example
a recursive function that calls itself with increasing values up to ten:
›

consts f :: "nat ==> nat"
recdef (*<*)(permissive)(*>*)f "{(i,j). j<i \<and> i \<le> (10::nat)}"
"f i = (if 10 ≤ i then 0 else i * f(Suc i))"

text‹\noindent
\isacommand{recdef} is not prepared for the relation supplied above,
rejects the definition. We should first have proved that
relation was well-founded:
›

lemma wf_greater: "wf {(i,j). j<i ∧ i ≤ (N::nat)}"

txt‹\noindent
proof is by showing that our relation is a subset of another well-founded
: one given by a measure function.\index{*wf_subset (theorem)}
›

apply (rule wf_subset [of "measure (λk::nat. N-k)"], blast)

txt‹
{subgoals[display,indent=0,margin=65]}

noindent
inclusion remains to be proved. After unfolding some definitions,
are left with simple arithmetic that is dispatched automatically.
›

by (clarify, simp add: measure_def inv_image_def)

text‹\noindent

with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
hint\cmmdx{hints} to our definition:
›
(*<*)
consts g :: "nat ==> nat"
recdef g "{(i,j). j<i ∧ i ≤ (10::nat)}"
"g i = (if 10 ≤ i then 0 else i * g(Suc i))"
(*>*)
(hints recdef_wf: wf_greater)

text‹\noindent
, we could have given ‹measure (λk::nat. 10-k)› for the
-founded relation in our \isacommand{recdef}. However, the arithmetic
in the lemma above would have arisen instead in the \isacommand{recdef}
proof, where we have less control. A tailor-made termination
makes even more sense when it can be used in several function
.
›

(*<*)end(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.13 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.