65 well-founded by cutting it off at a certain point. Here is an example |
65 well-founded by cutting it off at a certain point. Here is an example |
66 of a recursive function that calls itself with increasing values up to ten: |
66 of a recursive function that calls itself with increasing values up to ten: |
67 *} |
67 *} |
68 |
68 |
69 consts f :: "nat \<Rightarrow> nat" |
69 consts f :: "nat \<Rightarrow> nat" |
70 recdef (*<*)(permissive)(*>*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}" |
70 recdef (*<*)(permissive)(*>*)f "{(i,j). j<i \<and> i \<le> (10::nat)}" |
71 "f i = (if #10 \<le> i then 0 else i * f(Suc i))" |
71 "f i = (if 10 \<le> i then 0 else i * f(Suc i))" |
72 |
72 |
73 text{*\noindent |
73 text{*\noindent |
74 Since \isacommand{recdef} is not prepared for the relation supplied above, |
74 Since \isacommand{recdef} is not prepared for the relation supplied above, |
75 Isabelle rejects the definition. We should first have proved that |
75 Isabelle rejects the definition. We should first have proved that |
76 our relation was well-founded: |
76 our relation was well-founded: |
109 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a |
109 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a |
110 crucial hint to our definition: |
110 crucial hint to our definition: |
111 *} |
111 *} |
112 (*<*) |
112 (*<*) |
113 consts g :: "nat \<Rightarrow> nat" |
113 consts g :: "nat \<Rightarrow> nat" |
114 recdef g "{(i,j). j<i \<and> i \<le> (#10::nat)}" |
114 recdef g "{(i,j). j<i \<and> i \<le> (10::nat)}" |
115 "g i = (if #10 \<le> i then 0 else i * g(Suc i))" |
115 "g i = (if 10 \<le> i then 0 else i * g(Suc i))" |
116 (*>*) |
116 (*>*) |
117 (hints recdef_wf: wf_greater) |
117 (hints recdef_wf: wf_greater) |
118 |
118 |
119 text{*\noindent |
119 text{*\noindent |
120 Alternatively, we could have given @{text "measure (\<lambda>k::nat. #10-k)"} for the |
120 Alternatively, we could have given @{text "measure (\<lambda>k::nat. 10-k)"} for the |
121 well-founded relation in our \isacommand{recdef}. However, the arithmetic |
121 well-founded relation in our \isacommand{recdef}. However, the arithmetic |
122 goal in the lemma above would have arisen instead in the \isacommand{recdef} |
122 goal in the lemma above would have arisen instead in the \isacommand{recdef} |
123 termination proof, where we have less control. A tailor-made termination |
123 termination proof, where we have less control. A tailor-made termination |
124 relation makes even more sense when it can be used in several function |
124 relation makes even more sense when it can be used in several function |
125 declarations. |
125 declarations. |