summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/Recdef/examples.thy

author | nipkow |

Sun Aug 06 15:26:53 2000 +0200 (2000-08-06) | |

changeset 9541 | d17c0b34d5c8 |

parent 8771 | 026f37a86ea7 |

child 9792 | bbefb6ce5cb2 |

permissions | -rw-r--r-- |

*** empty log message ***

1 (*<*)

2 theory examples = Main:;

3 (*>*)

5 text{*

6 Here is a simple example, the Fibonacci function:

7 *}

9 consts fib :: "nat \\<Rightarrow> nat";

10 recdef fib "measure(\\<lambda>n. n)"

11 "fib 0 = 0"

12 "fib 1 = 1"

13 "fib (Suc(Suc x)) = fib x + fib (Suc x)";

15 text{*\noindent

16 The definition of \isa{fib} is accompanied by a \bfindex{measure function}

17 @{term"%n. n"} which maps the argument of \isa{fib} to a

18 natural number. The requirement is that in each equation the measure of the

19 argument on the left-hand side is strictly greater than the measure of the

20 argument of each recursive call. In the case of \isa{fib} this is

21 obviously true because the measure function is the identity and

22 @{term"Suc(Suc x)"} is strictly greater than both \isa{x} and

23 @{term"Suc x"}.

25 Slightly more interesting is the insertion of a fixed element

26 between any two elements of a list:

27 *}

29 consts sep :: "'a * 'a list \\<Rightarrow> 'a list";

30 recdef sep "measure (\\<lambda>(a,xs). length xs)"

31 "sep(a, []) = []"

32 "sep(a, [x]) = [x]"

33 "sep(a, x#y#zs) = x # a # sep(a,y#zs)";

35 text{*\noindent

36 This time the measure is the length of the list, which decreases with the

37 recursive call; the first component of the argument tuple is irrelevant.

39 Pattern matching need not be exhaustive:

40 *}

42 consts last :: "'a list \\<Rightarrow> 'a";

43 recdef last "measure (\\<lambda>xs. length xs)"

44 "last [x] = x"

45 "last (x#y#zs) = last (y#zs)";

47 text{*

48 Overlapping patterns are disambiguated by taking the order of equations into

49 account, just as in functional programming:

50 *}

52 consts sep1 :: "'a * 'a list \\<Rightarrow> 'a list";

53 recdef sep1 "measure (\\<lambda>(a,xs). length xs)"

54 "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"

55 "sep1(a, xs) = xs";

57 text{*\noindent

58 This defines exactly the same function as \isa{sep} above, i.e.\

59 \isa{sep1 = sep}.

61 \begin{warn}

62 \isacommand{recdef} only takes the first argument of a (curried)

63 recursive function into account. This means both the termination measure

64 and pattern matching can only use that first argument. In general, you will

65 therefore have to combine several arguments into a tuple. In case only one

66 argument is relevant for termination, you can also rearrange the order of

67 arguments as in the following definition:

68 \end{warn}

69 *}

70 consts sep2 :: "'a list \\<Rightarrow> 'a \\<Rightarrow> 'a list";

71 recdef sep2 "measure length"

72 "sep2 (x#y#zs) = (\\<lambda>a. x # a # sep2 zs a)"

73 "sep2 xs = (\\<lambda>a. xs)";

75 text{*

76 Because of its pattern-matching syntax, \isacommand{recdef} is also useful

77 for the definition of non-recursive functions:

78 *}

80 consts swap12 :: "'a list \\<Rightarrow> 'a list";

81 recdef swap12 "{}"

82 "swap12 (x#y#zs) = y#x#zs"

83 "swap12 zs = zs";

85 text{*\noindent

86 For non-recursive functions the termination measure degenerates to the empty

87 set \isa{\{\}}.

88 *}

90 (*<*)

91 end

92 (*>*)