1 (*<*) |
|
2 theory RECDEF = Main: |
|
3 (*>*) |
|
4 |
|
5 subsection{*Wellfounded Recursion*} |
|
6 |
|
7 subsubsection{*Examples*} |
|
8 |
|
9 consts fib :: "nat \<Rightarrow> nat"; |
|
10 recdef fib "measure(\<lambda>n. n)" |
|
11 "fib 0 = 0" |
|
12 "fib (Suc 0) = 1" |
|
13 "fib (Suc(Suc x)) = fib x + fib (Suc x)"; |
|
14 |
|
15 consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list"; |
|
16 recdef sep "measure (\<lambda>(a,xs). length xs)" |
|
17 "sep(a, []) = []" |
|
18 "sep(a, [x]) = [x]" |
|
19 "sep(a, x#y#zs) = x # a # sep(a,y#zs)"; |
|
20 |
|
21 consts last :: "'a list \<Rightarrow> 'a"; |
|
22 recdef last "measure (\<lambda>xs. length xs)" |
|
23 "last [x] = x" |
|
24 "last (x#y#zs) = last (y#zs)"; |
|
25 |
|
26 consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list"; |
|
27 recdef sep1 "measure (\<lambda>(a,xs). length xs)" |
|
28 "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)" |
|
29 "sep1(a, xs) = xs"; |
|
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 (*<*) |
|
36 thm sep1.simps |
|
37 (*>*) |
|
38 |
|
39 text{* |
|
40 Pattern matching is also useful for nonrecursive functions: |
|
41 *} |
|
42 |
|
43 consts swap12 :: "'a list \<Rightarrow> 'a list"; |
|
44 recdef swap12 "{}" |
|
45 "swap12 (x#y#zs) = y#x#zs" |
|
46 "swap12 zs = zs"; |
|
47 |
|
48 |
|
49 subsubsection{*Beyond Measure*} |
|
50 |
|
51 text{* |
|
52 The lexicographic product of two relations: |
|
53 *} |
|
54 |
|
55 consts ack :: "nat\<times>nat \<Rightarrow> nat"; |
|
56 recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)" |
|
57 "ack(0,n) = Suc n" |
|
58 "ack(Suc m,0) = ack(m, 1)" |
|
59 "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"; |
|
60 |
|
61 |
|
62 subsubsection{*Induction*} |
|
63 |
|
64 text{* |
|
65 Every recursive definition provides an induction theorem, for example |
|
66 @{thm[source]sep.induct}: |
|
67 @{thm[display,margin=70] sep.induct[no_vars]} |
|
68 *} |
|
69 (*<*)thm sep.induct[no_vars](*>*) |
|
70 |
|
71 lemma "map f (sep(x,xs)) = sep(f x, map f xs)" |
|
72 apply(induct_tac x xs rule: sep.induct) |
|
73 apply simp_all |
|
74 done |
|
75 |
|
76 lemma ack_incr2: "n < ack(m,n)" |
|
77 apply(induct_tac m n rule: ack.induct) |
|
78 apply simp_all |
|
79 done |
|
80 |
|
81 |
|
82 subsubsection{*Recursion Over Nested Datatypes*} |
|
83 |
|
84 datatype tree = C "tree list" |
|
85 |
|
86 lemma termi_lem: "t \<in> set ts \<longrightarrow> size t < Suc(tree_list_size ts)" |
|
87 by(induct_tac ts, auto) |
|
88 |
|
89 consts mirror :: "tree \<Rightarrow> tree" |
|
90 recdef mirror "measure size" |
|
91 "mirror(C ts) = C(rev(map mirror ts))" |
|
92 (hints recdef_simp: termi_lem) |
|
93 |
|
94 lemma "mirror(mirror t) = t" |
|
95 apply(induct_tac t rule: mirror.induct) |
|
96 apply(simp add: rev_map sym[OF map_compose] cong: map_cong) |
|
97 done |
|
98 |
|
99 text{* |
|
100 Figure out how that proof worked! |
|
101 |
|
102 \begin{exercise} |
|
103 Define a function for merging two ordered lists (of natural numbers) and |
|
104 show that if the two input lists are ordered, so is the output. |
|
105 \end{exercise} |
|
106 *} |
|
107 (*<*) |
|
108 end |
|
109 (*>*) |
|