doc-src/Functions/intro.tex
author wenzelm
Tue, 22 May 2012 19:02:17 +0200
changeset 47885 b987aa8b9310
parent 30226 2f4684e2ea95
permissions -rw-r--r--
Added tag Isabelle2012 for changeset 21c42b095c84
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23004
6658911db679 added files
krauss
parents:
diff changeset
     1
\section{Introduction}
6658911db679 added files
krauss
parents:
diff changeset
     2
27026
3602b81665b5 Updated function tutorial.
krauss
parents: 26851
diff changeset
     3
Starting from Isabelle 2007, new facilities for recursive
26851
0242c9c980df slight tuning of the 1st paragraph
urbanc
parents: 23805
diff changeset
     4
function definitions~\cite{krauss2006} are available. They provide
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
     5
better support for general recursive definitions than previous
26851
0242c9c980df slight tuning of the 1st paragraph
urbanc
parents: 23805
diff changeset
     6
packages.  But despite all tool support, function definitions can
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
     7
sometimes be a difficult thing. 
23004
6658911db679 added files
krauss
parents:
diff changeset
     8
23188
595a0e24bd8e updated
krauss
parents: 23004
diff changeset
     9
This tutorial is an example-guided introduction to the practical use
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    10
of the package and related tools. It should help you get started with
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    11
defining functions quickly. For the more difficult definitions we will
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    12
discuss what problems can arise, and how they can be solved.
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    13
27026
3602b81665b5 Updated function tutorial.
krauss
parents: 26851
diff changeset
    14
We assume that you have mastered the fundamentals of Isabelle/HOL
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    15
and are able to write basic specifications and proofs. To start out
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    16
with Isabelle in general, consult the Isabelle/HOL tutorial
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    17
\cite{isa-tutorial}.
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    18
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    19
23004
6658911db679 added files
krauss
parents:
diff changeset
    20
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    21
\paragraph{Structure of this tutorial.}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    22
Section 2 introduces the syntax and basic operation of the \cmd{fun}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    23
command, which provides full automation with reasonable default
27026
3602b81665b5 Updated function tutorial.
krauss
parents: 26851
diff changeset
    24
behavior.  The impatient reader can stop after that
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    25
section, and consult the remaining sections only when needed.
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    26
Section 3 introduces the more verbose \cmd{function} command which
27026
3602b81665b5 Updated function tutorial.
krauss
parents: 26851
diff changeset
    27
gives fine-grained control. This form should be used
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    28
whenever the short form fails.
27026
3602b81665b5 Updated function tutorial.
krauss
parents: 26851
diff changeset
    29
After that we discuss more specialized issues:
3602b81665b5 Updated function tutorial.
krauss
parents: 26851
diff changeset
    30
termination, mutual, nested and higher-order recursion, partiality, pattern matching
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    31
and others.
23004
6658911db679 added files
krauss
parents:
diff changeset
    32
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    33
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    34
\paragraph{Some background.}
23004
6658911db679 added files
krauss
parents:
diff changeset
    35
Following the LCF tradition, the package is realized as a definitional
6658911db679 added files
krauss
parents:
diff changeset
    36
extension: Recursive definitions are internally transformed into a
6658911db679 added files
krauss
parents:
diff changeset
    37
non-recursive form, such that the function can be defined using
6658911db679 added files
krauss
parents:
diff changeset
    38
standard definition facilities. Then the recursive specification is
6658911db679 added files
krauss
parents:
diff changeset
    39
derived from the primitive definition.  This is a complex task, but it
6658911db679 added files
krauss
parents:
diff changeset
    40
is fully automated and mostly transparent to the user. Definitional
6658911db679 added files
krauss
parents:
diff changeset
    41
extensions are valuable because they are conservative by construction:
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    42
The \qt{new} concept of general wellfounded recursion is completely reduced
23004
6658911db679 added files
krauss
parents:
diff changeset
    43
to existing principles.
6658911db679 added files
krauss
parents:
diff changeset
    44
6658911db679 added files
krauss
parents:
diff changeset
    45
6658911db679 added files
krauss
parents:
diff changeset
    46
6658911db679 added files
krauss
parents:
diff changeset
    47
27026
3602b81665b5 Updated function tutorial.
krauss
parents: 26851
diff changeset
    48
The new \cmd{function} command, and its short form \cmd{fun} have mostly
3602b81665b5 Updated function tutorial.
krauss
parents: 26851
diff changeset
    49
replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
3602b81665b5 Updated function tutorial.
krauss
parents: 26851
diff changeset
    50
a few of technical issues around \cmd{recdef}, and allow definitions
23004
6658911db679 added files
krauss
parents:
diff changeset
    51
which were not previously possible.
6658911db679 added files
krauss
parents:
diff changeset
    52
6658911db679 added files
krauss
parents:
diff changeset
    53
6658911db679 added files
krauss
parents:
diff changeset
    54
23188
595a0e24bd8e updated
krauss
parents: 23004
diff changeset
    55