Quelle examples.thy

Sprache: Isabelle

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

text‹
Here is a simple example, the \rmindex{Fibonacci function}:
›

consts fib :: "nat ==> nat"
recdef fib "measure(λn. n)"
  "fib 0 = 0"
  "fib (Suc 0) = 1"
  "fib (Suc(Suc x)) = fib x + fib (Suc x)"

text‹\noindent
\index{measure functions}%
The definition of @{term"fib"} is accompanied by a \textbf{measure function}
@{term"%n. n"} which maps the argument of @{term"fib"} to a
natural number. The requirement is that in each equation the measure of the
argument on the left-hand side is strictly greater than the measure of the
argument of each recursive call. In the case of @{term"fib"} this is
obviously true because the measure function is the identity and
@{term"Suc(Suc x)"} is strictly greater than both @{term"x"} and
@{term"Suc x"}.

Slightly more interesting is the insertion of a fixed element
between any two elements of a list:
›

consts sep :: "'a × 'a list ==> 'a list"
recdef sep "measure (λ(a,xs). length xs)"
  "sep(a, []) = []"
  "sep(a, [x]) = [x]"
  "sep(a, x#y#zs) = x # a # sep(a,y#zs)"

text‹\noindent
This time the measure is the length of the list, which decreases with the
recursive call; the first component of the argument tuple is irrelevant.
The details of tupled $\lambda$-abstractions ‹λ(x🪙1,…,x🪙n)› a
explained in \S\ref{sec:products}, but for now your intuition is all you need.

Pattern matching\index{pattern matching!and \isacommand{recdef}}
need not be exhaustive:
›

consts last :: "'a list ==> 'a"
recdef last "measure (λxs. length xs)"
  "last [x] = x"
  "last (x#y#zs) = last (y#zs)"

text‹
Overlapping patterns are disambiguated by taking the order of equations into
account, just as in functional programming:
›

consts sep1 :: "'a × 'a list ==> 'a list"
recdef sep1 "measure (λ(a,xs). length xs)"
  "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
  "sep1(a, xs) = xs"

text‹\noindent
To guarantee that the second equation can only be applied if the first
one does not match, Isabelle internally replaces the second equation
by the two possibilities that are left: @{prop"sep1(a,[]) = []"} and
@{prop"sep1(a, [x]) = [x]"}. Thus the functions @{term sep} and
@{const sep1} are identical.

\begin{warn}
\isacommand{recdef} only takes the first argument of a (curried)
recursive function into account. This means both the termination measure
and pattern matching can only use that first argument. In general, you will
therefore have to combine several arguments into a tuple. In case only one
argument is relevant for termination, you can also rearrange the order of
arguments as in the following definition:
\end{warn}
›
consts sep2 :: "'a list ==> 'a ==> 'a list"
recdef sep2 "measure length"
  "sep2 (x#y#zs) = (λa. x # a # sep2 (y#zs) a)"
  "sep2 xs = (λa. xs)"

text‹
Because of its pattern-matching syntax, \isacommand{recdef} is also useful
for the definition of non-recursive functions, where the termination measure
degenerates to the empty set @{term"{}"}:
›

consts swap12 :: "'a list ==> 'a list"
recdef swap12 "{}"
  "swap12 (x#y#zs) = y#x#zs"
  "swap12 zs = zs"

(*<*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet am 2026-04-29) ¤

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.