equal
deleted
inserted
replaced
166 (if n < m then coast n (m - 1) (c + n) |
166 (if n < m then coast n (m - 1) (c + n) |
167 else pedal n m (c + n))" |
167 else pedal n m (c + n))" |
168 |
168 |
169 |
169 |
170 |
170 |
171 subsection {* Refined analysis: The @{text sizechange} method *} |
171 subsection {* Refined analysis: The @{text size_change} method *} |
172 |
172 |
173 text {* Unsolvable for @{text lexicographic_order} *} |
173 text {* Unsolvable for @{text lexicographic_order} *} |
174 |
174 |
175 function fun1 :: "nat * nat \<Rightarrow> nat" |
175 function fun1 :: "nat * nat \<Rightarrow> nat" |
176 where |
176 where |
177 "fun1 (0,0) = 1" |
177 "fun1 (0,0) = 1" |
178 | "fun1 (0, Suc b) = 0" |
178 | "fun1 (0, Suc b) = 0" |
179 | "fun1 (Suc a, 0) = 0" |
179 | "fun1 (Suc a, 0) = 0" |
180 | "fun1 (Suc a, Suc b) = fun1 (b, a)" |
180 | "fun1 (Suc a, Suc b) = fun1 (b, a)" |
181 by pat_completeness auto |
181 by pat_completeness auto |
182 termination by sizechange |
182 termination by size_change |
183 |
183 |
184 |
184 |
185 text {* |
185 text {* |
186 @{text lexicographic_order} can do the following, but it is much slower. |
186 @{text lexicographic_order} can do the following, but it is much slower. |
187 *} |
187 *} |
193 where |
193 where |
194 "prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)" |
194 "prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)" |
195 | "oprod x y z = eprod x (y - 1) (z+x)" |
195 | "oprod x y z = eprod x (y - 1) (z+x)" |
196 | "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)" |
196 | "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)" |
197 by pat_completeness auto |
197 by pat_completeness auto |
198 termination by sizechange |
198 termination by size_change |
199 |
199 |
200 text {* |
200 text {* |
201 Permutations of arguments: |
201 Permutations of arguments: |
202 *} |
202 *} |
203 |
203 |
205 where |
205 where |
206 "perm m n r = (if r > 0 then perm m (r - 1) n |
206 "perm m n r = (if r > 0 then perm m (r - 1) n |
207 else if n > 0 then perm r (n - 1) m |
207 else if n > 0 then perm r (n - 1) m |
208 else m)" |
208 else m)" |
209 by auto |
209 by auto |
210 termination by sizechange |
210 termination by size_change |
211 |
211 |
212 text {* |
212 text {* |
213 Artificial examples and regression tests: |
213 Artificial examples and regression tests: |
214 *} |
214 *} |
215 |
215 |
225 fun2 (min y (z - 1)) x x |
225 fun2 (min y (z - 1)) x x |
226 else |
226 else |
227 0 |
227 0 |
228 )" |
228 )" |
229 by pat_completeness auto |
229 by pat_completeness auto |
230 termination by sizechange -- {* requires Multiset *} |
230 termination by size_change -- {* requires Multiset *} |
231 |
231 |
232 end |
232 end |