src/Doc/Tutorial/Fun/fun0.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 58620 7435b6a3f72e
child 62392 747d36865c2c
permissions -rw-r--r--
eliminated spurious semicolons;
nipkow@25260
     1
(*<*)
nipkow@25260
     2
theory fun0 imports Main begin
nipkow@25260
     3
(*>*)
nipkow@25260
     4
nipkow@25260
     5
text{*
nipkow@25260
     6
\subsection{Definition}
nipkow@25260
     7
\label{sec:fun-examples}
nipkow@25260
     8
nipkow@25260
     9
Here is a simple example, the \rmindex{Fibonacci function}:
nipkow@25260
    10
*}
nipkow@25260
    11
nipkow@25260
    12
fun fib :: "nat \<Rightarrow> nat" where
nipkow@27015
    13
"fib 0 = 0" |
nipkow@27015
    14
"fib (Suc 0) = 1" |
nipkow@27015
    15
"fib (Suc(Suc x)) = fib x + fib (Suc x)"
nipkow@25260
    16
nipkow@25260
    17
text{*\noindent
nipkow@25260
    18
This resembles ordinary functional programming languages. Note the obligatory
nipkow@25260
    19
\isacommand{where} and \isa{|}. Command \isacommand{fun} declares and
nipkow@25260
    20
defines the function in one go. Isabelle establishes termination automatically
nipkow@25260
    21
because @{const fib}'s argument decreases in every recursive call.
nipkow@25260
    22
nipkow@25260
    23
Slightly more interesting is the insertion of a fixed element
nipkow@25260
    24
between any two elements of a list:
nipkow@25260
    25
*}
nipkow@25260
    26
nipkow@25260
    27
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
nipkow@27015
    28
"sep a []     = []" |
nipkow@27015
    29
"sep a [x]    = [x]" |
wenzelm@58860
    30
"sep a (x#y#zs) = x # a # sep a (y#zs)"
nipkow@25260
    31
nipkow@25260
    32
text{*\noindent
nipkow@25260
    33
This time the length of the list decreases with the
nipkow@25260
    34
recursive call; the first argument is irrelevant for termination.
nipkow@25260
    35
nipkow@25260
    36
Pattern matching\index{pattern matching!and \isacommand{fun}}
nipkow@25260
    37
need not be exhaustive and may employ wildcards:
nipkow@25260
    38
*}
nipkow@25260
    39
nipkow@25260
    40
fun last :: "'a list \<Rightarrow> 'a" where
nipkow@27015
    41
"last [x]      = x" |
nipkow@27015
    42
"last (_#y#zs) = last (y#zs)"
nipkow@25260
    43
nipkow@25260
    44
text{*
nipkow@25260
    45
Overlapping patterns are disambiguated by taking the order of equations into
nipkow@25260
    46
account, just as in functional programming:
nipkow@25260
    47
*}
nipkow@25260
    48
nipkow@25260
    49
fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
nipkow@27015
    50
"sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |
nipkow@27015
    51
"sep1 _ xs       = xs"
nipkow@25260
    52
nipkow@25260
    53
text{*\noindent
nipkow@25260
    54
To guarantee that the second equation can only be applied if the first
nipkow@25260
    55
one does not match, Isabelle internally replaces the second equation
nipkow@25260
    56
by the two possibilities that are left: @{prop"sep1 a [] = []"} and
nipkow@25260
    57
@{prop"sep1 a [x] = [x]"}.  Thus the functions @{const sep} and
nipkow@25260
    58
@{const sep1} are identical.
nipkow@25260
    59
nipkow@25263
    60
Because of its pattern matching syntax, \isacommand{fun} is also useful
nipkow@25260
    61
for the definition of non-recursive functions:
nipkow@25260
    62
*}
nipkow@25260
    63
nipkow@25260
    64
fun swap12 :: "'a list \<Rightarrow> 'a list" where
nipkow@27015
    65
"swap12 (x#y#zs) = y#x#zs" |
nipkow@27015
    66
"swap12 zs       = zs"
nipkow@25260
    67
nipkow@25260
    68
text{*
nipkow@25260
    69
After a function~$f$ has been defined via \isacommand{fun},
nipkow@25260
    70
its defining equations (or variants derived from them) are available
nipkow@25260
    71
under the name $f$@{text".simps"} as theorems.
nipkow@25260
    72
For example, look (via \isacommand{thm}) at
nipkow@25260
    73
@{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define
nipkow@25260
    74
the same function. What is more, those equations are automatically declared as
nipkow@25260
    75
simplification rules.
nipkow@25260
    76
nipkow@25260
    77
\subsection{Termination}
nipkow@25260
    78
nipkow@25260
    79
Isabelle's automatic termination prover for \isacommand{fun} has a
nipkow@25260
    80
fixed notion of the \emph{size} (of type @{typ nat}) of an
nipkow@25260
    81
argument. The size of a natural number is the number itself. The size
nipkow@25339
    82
of a list is its length. For the general case see \S\ref{sec:general-datatype}.
nipkow@25339
    83
A recursive function is accepted if \isacommand{fun} can
nipkow@25260
    84
show that the size of one fixed argument becomes smaller with each
nipkow@25260
    85
recursive call.
nipkow@25260
    86
nipkow@25261
    87
More generally, \isacommand{fun} allows any \emph{lexicographic
nipkow@25260
    88
combination} of size measures in case there are multiple
nipkow@25261
    89
arguments. For example, the following version of \rmindex{Ackermann's
nipkow@25260
    90
function} is accepted: *}
nipkow@25260
    91
nipkow@25260
    92
fun ack2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
nipkow@27015
    93
"ack2 n 0 = Suc n" |
nipkow@27015
    94
"ack2 0 (Suc m) = ack2 (Suc 0) m" |
nipkow@27015
    95
"ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"
nipkow@25260
    96
nipkow@25263
    97
text{* The order of arguments has no influence on whether
nipkow@25260
    98
\isacommand{fun} can prove termination of a function. For more details
wenzelm@58620
    99
see elsewhere~@{cite bulwahnKN07}.
nipkow@25260
   100
nipkow@25260
   101
\subsection{Simplification}
nipkow@25260
   102
\label{sec:fun-simplification}
nipkow@25260
   103
paulson@25265
   104
Upon a successful termination proof, the recursion equations become
nipkow@25260
   105
simplification rules, just as with \isacommand{primrec}.
nipkow@25260
   106
In most cases this works fine, but there is a subtle
nipkow@25260
   107
problem that must be mentioned: simplification may not
nipkow@25260
   108
terminate because of automatic splitting of @{text "if"}.
nipkow@25260
   109
\index{*if expressions!splitting of}
nipkow@25260
   110
Let us look at an example:
nipkow@25260
   111
*}
nipkow@25260
   112
nipkow@25261
   113
fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
nipkow@27015
   114
"gcd m n = (if n=0 then m else gcd n (m mod n))"
nipkow@25260
   115
nipkow@25260
   116
text{*\noindent
nipkow@25260
   117
The second argument decreases with each recursive call.
nipkow@25260
   118
The termination condition
nipkow@25260
   119
@{prop[display]"n ~= (0::nat) ==> m mod n < n"}
nipkow@25260
   120
is proved automatically because it is already present as a lemma in
nipkow@25260
   121
HOL\@.  Thus the recursion equation becomes a simplification
nipkow@25260
   122
rule. Of course the equation is nonterminating if we are allowed to unfold
nipkow@25260
   123
the recursive call inside the @{text else} branch, which is why programming
nipkow@25260
   124
languages and our simplifier don't do that. Unfortunately the simplifier does
nipkow@25260
   125
something else that leads to the same problem: it splits 
nipkow@25260
   126
each @{text "if"}-expression unless its
nipkow@25260
   127
condition simplifies to @{term True} or @{term False}.  For
nipkow@25260
   128
example, simplification reduces
nipkow@25261
   129
@{prop[display]"gcd m n = k"}
nipkow@25260
   130
in one step to
nipkow@25261
   131
@{prop[display]"(if n=0 then m else gcd n (m mod n)) = k"}
nipkow@25260
   132
where the condition cannot be reduced further, and splitting leads to
nipkow@25261
   133
@{prop[display]"(n=0 --> m=k) & (n ~= 0 --> gcd n (m mod n)=k)"}
nipkow@25261
   134
Since the recursive call @{term"gcd n (m mod n)"} is no longer protected by
nipkow@25260
   135
an @{text "if"}, it is unfolded again, which leads to an infinite chain of
nipkow@25260
   136
simplification steps. Fortunately, this problem can be avoided in many
nipkow@25260
   137
different ways.
nipkow@25260
   138
nipkow@25260
   139
The most radical solution is to disable the offending theorem
nipkow@25260
   140
@{thm[source]split_if},
nipkow@25260
   141
as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
nipkow@25260
   142
approach: you will often have to invoke the rule explicitly when
nipkow@25260
   143
@{text "if"} is involved.
nipkow@25260
   144
nipkow@25260
   145
If possible, the definition should be given by pattern matching on the left
nipkow@25260
   146
rather than @{text "if"} on the right. In the case of @{term gcd} the
nipkow@25260
   147
following alternative definition suggests itself:
nipkow@25260
   148
*}
nipkow@25260
   149
nipkow@25260
   150
fun gcd1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
nipkow@27015
   151
"gcd1 m 0 = m" |
nipkow@27015
   152
"gcd1 m n = gcd1 n (m mod n)"
nipkow@25260
   153
nipkow@25260
   154
text{*\noindent
nipkow@25260
   155
The order of equations is important: it hides the side condition
nipkow@25263
   156
@{prop"n ~= (0::nat)"}.  Unfortunately, not all conditionals can be
nipkow@25263
   157
expressed by pattern matching.
nipkow@25260
   158
nipkow@25260
   159
A simple alternative is to replace @{text "if"} by @{text case}, 
nipkow@25260
   160
which is also available for @{typ bool} and is not split automatically:
nipkow@25260
   161
*}
nipkow@25260
   162
nipkow@25260
   163
fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
nipkow@27015
   164
"gcd2 m n = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2 n (m mod n))"
nipkow@25260
   165
nipkow@25260
   166
text{*\noindent
nipkow@25260
   167
This is probably the neatest solution next to pattern matching, and it is
nipkow@25260
   168
always available.
nipkow@25260
   169
nipkow@25260
   170
A final alternative is to replace the offending simplification rules by
nipkow@25260
   171
derived conditional ones. For @{term gcd} it means we have to prove
nipkow@25260
   172
these lemmas:
nipkow@25260
   173
*}
nipkow@25260
   174
nipkow@25261
   175
lemma [simp]: "gcd m 0 = m"
nipkow@25260
   176
apply(simp)
nipkow@25260
   177
done
nipkow@25260
   178
nipkow@25261
   179
lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
nipkow@25260
   180
apply(simp)
nipkow@25260
   181
done
nipkow@25260
   182
nipkow@25260
   183
text{*\noindent
nipkow@25260
   184
Simplification terminates for these proofs because the condition of the @{text
nipkow@25260
   185
"if"} simplifies to @{term True} or @{term False}.
nipkow@25260
   186
Now we can disable the original simplification rule:
nipkow@25260
   187
*}
nipkow@25260
   188
nipkow@25260
   189
declare gcd.simps [simp del]
nipkow@25260
   190
nipkow@25260
   191
text{*
nipkow@25260
   192
\index{induction!recursion|(}
nipkow@25260
   193
\index{recursion induction|(}
nipkow@25260
   194
nipkow@25260
   195
\subsection{Induction}
nipkow@25260
   196
\label{sec:fun-induction}
nipkow@25260
   197
nipkow@25260
   198
Having defined a function we might like to prove something about it.
nipkow@25260
   199
Since the function is recursive, the natural proof principle is
nipkow@25260
   200
again induction. But this time the structural form of induction that comes
nipkow@25260
   201
with datatypes is unlikely to work well --- otherwise we could have defined the
nipkow@25260
   202
function by \isacommand{primrec}. Therefore \isacommand{fun} automatically
nipkow@25260
   203
proves a suitable induction rule $f$@{text".induct"} that follows the
nipkow@25260
   204
recursion pattern of the particular function $f$. We call this
nipkow@25260
   205
\textbf{recursion induction}. Roughly speaking, it
nipkow@25260
   206
requires you to prove for each \isacommand{fun} equation that the property
nipkow@25260
   207
you are trying to establish holds for the left-hand side provided it holds
nipkow@25260
   208
for all recursive calls on the right-hand side. Here is a simple example
nipkow@25260
   209
involving the predefined @{term"map"} functional on lists:
nipkow@25260
   210
*}
nipkow@25260
   211
nipkow@25260
   212
lemma "map f (sep x xs) = sep (f x) (map f xs)"
nipkow@25260
   213
nipkow@25260
   214
txt{*\noindent
nipkow@25260
   215
Note that @{term"map f xs"}
nipkow@25260
   216
is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove
nipkow@25260
   217
this lemma by recursion induction over @{term"sep"}:
nipkow@25260
   218
*}
nipkow@25260
   219
wenzelm@58860
   220
apply(induct_tac x xs rule: sep.induct)
nipkow@25260
   221
nipkow@25260
   222
txt{*\noindent
nipkow@25260
   223
The resulting proof state has three subgoals corresponding to the three
nipkow@25260
   224
clauses for @{term"sep"}:
nipkow@25260
   225
@{subgoals[display,indent=0]}
nipkow@25260
   226
The rest is pure simplification:
nipkow@25260
   227
*}
nipkow@25260
   228
wenzelm@58860
   229
apply simp_all
nipkow@25260
   230
done
nipkow@25260
   231
nipkow@25263
   232
text{*\noindent The proof goes smoothly because the induction rule
nipkow@25263
   233
follows the recursion of @{const sep}.  Try proving the above lemma by
nipkow@25263
   234
structural induction, and you find that you need an additional case
nipkow@25263
   235
distinction.
nipkow@25260
   236
nipkow@25260
   237
In general, the format of invoking recursion induction is
nipkow@25260
   238
\begin{quote}
nipkow@25260
   239
\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
nipkow@25260
   240
\end{quote}\index{*induct_tac (method)}%
nipkow@25260
   241
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
nipkow@27167
   242
name of a function that takes $n$ arguments. Usually the subgoal will
nipkow@25263
   243
contain the term $f x@1 \dots x@n$ but this need not be the case. The
nipkow@25260
   244
induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
nipkow@25260
   245
\begin{isabelle}
nipkow@25260
   246
{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
nipkow@25260
   247
~~{\isasymAnd}a~x.~P~a~[x];\isanewline
nipkow@25260
   248
~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
nipkow@25260
   249
{\isasymLongrightarrow}~P~u~v%
nipkow@25260
   250
\end{isabelle}
nipkow@25260
   251
It merely says that in order to prove a property @{term"P"} of @{term"u"} and
nipkow@25260
   252
@{term"v"} you need to prove it for the three cases where @{term"v"} is the
nipkow@25260
   253
empty list, the singleton list, and the list with at least two elements.
nipkow@25260
   254
The final case has an induction hypothesis:  you may assume that @{term"P"}
nipkow@25260
   255
holds for the tail of that list.
nipkow@25260
   256
\index{induction!recursion|)}
nipkow@25260
   257
\index{recursion induction|)}
nipkow@25260
   258
*}
nipkow@25260
   259
(*<*)
nipkow@25260
   260
end
nipkow@25260
   261
(*>*)