equal
deleted
inserted
replaced
7 *} |
7 *} |
8 |
8 |
9 consts fib :: "nat \<Rightarrow> nat"; |
9 consts fib :: "nat \<Rightarrow> nat"; |
10 recdef fib "measure(\<lambda>n. n)" |
10 recdef fib "measure(\<lambda>n. n)" |
11 "fib 0 = 0" |
11 "fib 0 = 0" |
12 "fib 1' = 1" |
12 "fib (Suc 0) = 1" |
13 "fib (Suc(Suc x)) = fib x + fib (Suc x)"; |
13 "fib (Suc(Suc x)) = fib x + fib (Suc x)"; |
14 |
14 |
15 text{*\noindent |
15 text{*\noindent |
16 \index{measure functions}% |
16 \index{measure functions}% |
17 The definition of @{term"fib"} is accompanied by a \textbf{measure function} |
17 The definition of @{term"fib"} is accompanied by a \textbf{measure function} |