8 |
8 |
9 Here is a simple example, the \rmindex{Fibonacci function}: |
9 Here is a simple example, the \rmindex{Fibonacci function}: |
10 *} |
10 *} |
11 |
11 |
12 fun fib :: "nat \<Rightarrow> nat" where |
12 fun fib :: "nat \<Rightarrow> nat" where |
13 "fib 0 = 0" | |
13 "fib 0 = 0" | |
14 "fib (Suc 0) = 1" | |
14 "fib (Suc 0) = 1" | |
15 "fib (Suc(Suc x)) = fib x + fib (Suc x)" |
15 "fib (Suc(Suc x)) = fib x + fib (Suc x)" |
16 |
16 |
17 text{*\noindent |
17 text{*\noindent |
18 This resembles ordinary functional programming languages. Note the obligatory |
18 This resembles ordinary functional programming languages. Note the obligatory |
19 \isacommand{where} and \isa{|}. Command \isacommand{fun} declares and |
19 \isacommand{where} and \isa{|}. Command \isacommand{fun} declares and |
20 defines the function in one go. Isabelle establishes termination automatically |
20 defines the function in one go. Isabelle establishes termination automatically |
23 Slightly more interesting is the insertion of a fixed element |
23 Slightly more interesting is the insertion of a fixed element |
24 between any two elements of a list: |
24 between any two elements of a list: |
25 *} |
25 *} |
26 |
26 |
27 fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
27 fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
28 "sep a [] = []" | |
28 "sep a [] = []" | |
29 "sep a [x] = [x]" | |
29 "sep a [x] = [x]" | |
30 "sep a (x#y#zs) = x # a # sep a (y#zs)"; |
30 "sep a (x#y#zs) = x # a # sep a (y#zs)"; |
31 |
31 |
32 text{*\noindent |
32 text{*\noindent |
33 This time the length of the list decreases with the |
33 This time the length of the list decreases with the |
34 recursive call; the first argument is irrelevant for termination. |
34 recursive call; the first argument is irrelevant for termination. |
35 |
35 |
36 Pattern matching\index{pattern matching!and \isacommand{fun}} |
36 Pattern matching\index{pattern matching!and \isacommand{fun}} |
37 need not be exhaustive and may employ wildcards: |
37 need not be exhaustive and may employ wildcards: |
38 *} |
38 *} |
39 |
39 |
40 fun last :: "'a list \<Rightarrow> 'a" where |
40 fun last :: "'a list \<Rightarrow> 'a" where |
41 "last [x] = x" | |
41 "last [x] = x" | |
42 "last (_#y#zs) = last (y#zs)" |
42 "last (_#y#zs) = last (y#zs)" |
43 |
43 |
44 text{* |
44 text{* |
45 Overlapping patterns are disambiguated by taking the order of equations into |
45 Overlapping patterns are disambiguated by taking the order of equations into |
46 account, just as in functional programming: |
46 account, just as in functional programming: |
47 *} |
47 *} |
48 |
48 |
49 fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
49 fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
50 "sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" | |
50 "sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" | |
51 "sep1 _ xs = xs" |
51 "sep1 _ xs = xs" |
52 |
52 |
53 text{*\noindent |
53 text{*\noindent |
54 To guarantee that the second equation can only be applied if the first |
54 To guarantee that the second equation can only be applied if the first |
55 one does not match, Isabelle internally replaces the second equation |
55 one does not match, Isabelle internally replaces the second equation |
56 by the two possibilities that are left: @{prop"sep1 a [] = []"} and |
56 by the two possibilities that are left: @{prop"sep1 a [] = []"} and |
60 Because of its pattern matching syntax, \isacommand{fun} is also useful |
60 Because of its pattern matching syntax, \isacommand{fun} is also useful |
61 for the definition of non-recursive functions: |
61 for the definition of non-recursive functions: |
62 *} |
62 *} |
63 |
63 |
64 fun swap12 :: "'a list \<Rightarrow> 'a list" where |
64 fun swap12 :: "'a list \<Rightarrow> 'a list" where |
65 "swap12 (x#y#zs) = y#x#zs" | |
65 "swap12 (x#y#zs) = y#x#zs" | |
66 "swap12 zs = zs" |
66 "swap12 zs = zs" |
67 |
67 |
68 text{* |
68 text{* |
69 After a function~$f$ has been defined via \isacommand{fun}, |
69 After a function~$f$ has been defined via \isacommand{fun}, |
70 its defining equations (or variants derived from them) are available |
70 its defining equations (or variants derived from them) are available |
71 under the name $f$@{text".simps"} as theorems. |
71 under the name $f$@{text".simps"} as theorems. |
88 combination} of size measures in case there are multiple |
88 combination} of size measures in case there are multiple |
89 arguments. For example, the following version of \rmindex{Ackermann's |
89 arguments. For example, the following version of \rmindex{Ackermann's |
90 function} is accepted: *} |
90 function} is accepted: *} |
91 |
91 |
92 fun ack2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
92 fun ack2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
93 "ack2 n 0 = Suc n" | |
93 "ack2 n 0 = Suc n" | |
94 "ack2 0 (Suc m) = ack2 (Suc 0) m" | |
94 "ack2 0 (Suc m) = ack2 (Suc 0) m" | |
95 "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m" |
95 "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m" |
96 |
96 |
97 text{* The order of arguments has no influence on whether |
97 text{* The order of arguments has no influence on whether |
98 \isacommand{fun} can prove termination of a function. For more details |
98 \isacommand{fun} can prove termination of a function. For more details |
99 see elsewhere~\cite{bulwahnKN07}. |
99 see elsewhere~\cite{bulwahnKN07}. |
100 |
100 |
109 \index{*if expressions!splitting of} |
109 \index{*if expressions!splitting of} |
110 Let us look at an example: |
110 Let us look at an example: |
111 *} |
111 *} |
112 |
112 |
113 fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
113 fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
114 "gcd m n = (if n=0 then m else gcd n (m mod n))" |
114 "gcd m n = (if n=0 then m else gcd n (m mod n))" |
115 |
115 |
116 text{*\noindent |
116 text{*\noindent |
117 The second argument decreases with each recursive call. |
117 The second argument decreases with each recursive call. |
118 The termination condition |
118 The termination condition |
119 @{prop[display]"n ~= (0::nat) ==> m mod n < n"} |
119 @{prop[display]"n ~= (0::nat) ==> m mod n < n"} |
146 rather than @{text "if"} on the right. In the case of @{term gcd} the |
146 rather than @{text "if"} on the right. In the case of @{term gcd} the |
147 following alternative definition suggests itself: |
147 following alternative definition suggests itself: |
148 *} |
148 *} |
149 |
149 |
150 fun gcd1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
150 fun gcd1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
151 "gcd1 m 0 = m" | |
151 "gcd1 m 0 = m" | |
152 "gcd1 m n = gcd1 n (m mod n)" |
152 "gcd1 m n = gcd1 n (m mod n)" |
153 |
153 |
154 text{*\noindent |
154 text{*\noindent |
155 The order of equations is important: it hides the side condition |
155 The order of equations is important: it hides the side condition |
156 @{prop"n ~= (0::nat)"}. Unfortunately, not all conditionals can be |
156 @{prop"n ~= (0::nat)"}. Unfortunately, not all conditionals can be |
157 expressed by pattern matching. |
157 expressed by pattern matching. |
159 A simple alternative is to replace @{text "if"} by @{text case}, |
159 A simple alternative is to replace @{text "if"} by @{text case}, |
160 which is also available for @{typ bool} and is not split automatically: |
160 which is also available for @{typ bool} and is not split automatically: |
161 *} |
161 *} |
162 |
162 |
163 fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
163 fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
164 "gcd2 m n = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2 n (m mod n))" |
164 "gcd2 m n = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2 n (m mod n))" |
165 |
165 |
166 text{*\noindent |
166 text{*\noindent |
167 This is probably the neatest solution next to pattern matching, and it is |
167 This is probably the neatest solution next to pattern matching, and it is |
168 always available. |
168 always available. |
169 |
169 |