|
1 (*<*) |
1 theory RECDEF = Main: |
2 theory RECDEF = Main: |
|
3 (*>*) |
2 |
4 |
3 subsection{*Wellfounded Recursion*} |
5 subsection{*Wellfounded Recursion*} |
4 |
6 |
5 subsubsection{*Examples*} |
7 subsubsection{*Examples*} |
6 |
8 |
7 consts fib :: "nat \<Rightarrow> nat"; |
9 consts fib :: "nat \<Rightarrow> nat"; |
8 recdef fib "measure(\<lambda>n. n)" |
10 recdef fib "measure(\<lambda>n. n)" |
9 "fib 0 = 0" |
11 "fib 0 = 0" |
10 "fib 1 = 1" |
12 "fib (Suc 0) = 1" |
11 "fib (Suc(Suc x)) = fib x + fib (Suc x)"; |
13 "fib (Suc(Suc x)) = fib x + fib (Suc x)"; |
12 |
14 |
13 consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list"; |
15 consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list"; |
14 recdef sep "measure (\<lambda>(a,xs). length xs)" |
16 recdef sep "measure (\<lambda>(a,xs). length xs)" |
15 "sep(a, []) = []" |
17 "sep(a, []) = []" |
19 consts last :: "'a list \<Rightarrow> 'a"; |
21 consts last :: "'a list \<Rightarrow> 'a"; |
20 recdef last "measure (\<lambda>xs. length xs)" |
22 recdef last "measure (\<lambda>xs. length xs)" |
21 "last [x] = x" |
23 "last [x] = x" |
22 "last (x#y#zs) = last (y#zs)"; |
24 "last (x#y#zs) = last (y#zs)"; |
23 |
25 |
24 |
|
25 consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list"; |
26 consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list"; |
26 recdef sep1 "measure (\<lambda>(a,xs). length xs)" |
27 recdef sep1 "measure (\<lambda>(a,xs). length xs)" |
27 "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)" |
28 "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)" |
28 "sep1(a, xs) = xs"; |
29 "sep1(a, xs) = xs"; |
29 |
30 |
|
31 text{* |
|
32 This is what the rules for @{term sep1} are turned into: |
|
33 @{thm[display,indent=5] sep1.simps[no_vars]} |
|
34 *} |
|
35 (*<*) |
30 thm sep1.simps |
36 thm sep1.simps |
|
37 (*>*) |
31 |
38 |
|
39 text{* |
|
40 Pattern matching is also useful for nonrecursive functions: |
|
41 *} |
32 |
42 |
33 consts swap12 :: "'a list \<Rightarrow> 'a list"; |
43 consts swap12 :: "'a list \<Rightarrow> 'a list"; |
34 recdef swap12 "{}" |
44 recdef swap12 "{}" |
35 "swap12 (x#y#zs) = y#x#zs" |
45 "swap12 (x#y#zs) = y#x#zs" |
36 "swap12 zs = zs"; |
46 "swap12 zs = zs"; |
37 |
47 |
38 |
48 |
39 subsubsection{*Beyond Measure*} |
49 subsubsection{*Beyond Measure*} |
|
50 |
|
51 text{* |
|
52 The lexicographic product of two relations: |
|
53 *} |
40 |
54 |
41 consts ack :: "nat\<times>nat \<Rightarrow> nat"; |
55 consts ack :: "nat\<times>nat \<Rightarrow> nat"; |
42 recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)" |
56 recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)" |
43 "ack(0,n) = Suc n" |
57 "ack(0,n) = Suc n" |
44 "ack(Suc m,0) = ack(m, 1)" |
58 "ack(Suc m,0) = ack(m, 1)" |
75 apply(induct_tac t rule: mirror.induct) |
89 apply(induct_tac t rule: mirror.induct) |
76 apply(simp add: rev_map sym[OF map_compose] cong: map_cong) |
90 apply(simp add: rev_map sym[OF map_compose] cong: map_cong) |
77 done |
91 done |
78 |
92 |
79 text{* |
93 text{* |
|
94 Figure out how that proof worked! |
|
95 |
80 \begin{exercise} |
96 \begin{exercise} |
81 Define a function for merging two ordered lists (of natural numbers) and |
97 Define a function for merging two ordered lists (of natural numbers) and |
82 show that if the two input lists are ordered, so is the output. |
98 show that if the two input lists are ordered, so is the output. |
83 \end{exercise} |
99 \end{exercise} |
84 *} |
100 *} |
85 |
101 (*<*) |
86 end |
102 end |
|
103 (*>*) |