57 solely of these building blocks. But of course the proof of |
57 solely of these building blocks. But of course the proof of |
58 termination of your function definition, i.e.\ that the arguments |
58 termination of your function definition, i.e.\ that the arguments |
59 decrease with every recursive call, may still require you to provide |
59 decrease with every recursive call, may still require you to provide |
60 additional lemmas. |
60 additional lemmas. |
61 |
61 |
62 It is also possible to use your own well-founded relations with \isacommand{recdef}. |
62 It is also possible to use your own well-founded relations with |
63 Here is a simplistic example: |
63 \isacommand{recdef}. For example, the greater-than relation can be made |
|
64 well-founded by cutting it off at a certain point. Here is an example |
|
65 of a recursive function that calls itself with increasing values up to ten: |
64 *} |
66 *} |
65 |
67 |
66 consts f :: "nat \<Rightarrow> nat" |
68 consts f :: "nat \<Rightarrow> nat" |
67 recdef f "id(less_than)" |
69 recdef f "{(i,j). j<i \<and> i \<le> (#10::nat)}" |
68 "f 0 = 0" |
70 "f i = (if #10 \<le> i then 0 else i * f(Suc i))"; |
69 "f (Suc n) = f n" |
|
70 |
71 |
71 text{*\noindent |
72 text{*\noindent |
72 Since \isacommand{recdef} is not prepared for @{term id}, the identity |
73 Since \isacommand{recdef} is not prepared for the relation supplied above, |
73 function, this leads to the complaint that it could not prove |
74 Isabelle rejects the definition. We should first have proved that |
74 @{prop"wf (id less_than)"}. |
75 our relation was well-founded: |
75 We should first have proved that @{term id} preserves well-foundedness |
|
76 *} |
76 *} |
77 |
77 |
78 lemma wf_id: "wf r \<Longrightarrow> wf(id r)" |
78 lemma wf_greater: "wf {(i,j). j<i \<and> i \<le> (N::nat)}" |
79 by simp; |
79 |
|
80 txt{* |
|
81 The proof is by showing that our relation is a subset of another well-founded |
|
82 relation: one given by a measure function. |
|
83 *}; |
|
84 |
|
85 apply (rule wf_subset [of "measure (\<lambda>k::nat. N-k)"], blast); |
|
86 |
|
87 txt{* |
|
88 @{subgoals[display,indent=0,margin=65]} |
|
89 |
|
90 \noindent |
|
91 The inclusion remains to be proved. After unfolding some definitions, |
|
92 we are left with simple arithmetic: |
|
93 *}; |
|
94 |
|
95 apply (clarify, simp add: measure_def inv_image_def) |
|
96 |
|
97 txt{* |
|
98 @{subgoals[display,indent=0,margin=65]} |
|
99 |
|
100 \noindent |
|
101 And that is dispatched automatically: |
|
102 *}; |
|
103 |
|
104 by arith; |
80 |
105 |
81 text{*\noindent |
106 text{*\noindent |
82 and should have appended the following hint to our definition above: |
107 |
|
108 Armed with this lemma, we can append a crucial hint to our definition: |
83 \indexbold{*recdef_wf} |
109 \indexbold{*recdef_wf} |
84 *} |
110 *} |
85 (*<*) |
111 (*<*) |
86 consts g :: "nat \<Rightarrow> nat" |
112 consts g :: "nat \<Rightarrow> nat" |
87 recdef g "id(less_than)" |
113 recdef g "{(i,j). j<i \<and> i \<le> (#10::nat)}" |
88 "g 0 = 0" |
114 "g i = (if #10 \<le> i then 0 else i * g(Suc i))" |
89 "g (Suc n) = g n" |
|
90 (*>*) |
115 (*>*) |
91 (hints recdef_wf: wf_id) |
116 (hints recdef_wf: wf_greater); |
|
117 |
|
118 text{*\noindent |
|
119 Alternatively, we could have given @{text "measure (\<lambda>k::nat. #10-k)"} for the |
|
120 well-founded relation in our \isacommand{recdef}. However, the arithmetic |
|
121 goal in the lemma above would have arisen instead in the \isacommand{recdef} |
|
122 termination proof, where we have less control. A tailor-made termination |
|
123 relation makes even more sense when it can be used in several function |
|
124 declarations. |
|
125 *} |
|
126 |
92 (*<*)end(*>*) |
127 (*<*)end(*>*) |