# Re: [isabelle] about termination of function

Hi,

Hi, I am thinking about proving termination of function. Can anyone tell me the differences between the following two:
1)
apply(relation inv_image(finite-psubset<*lex*>less-than) ...)
2) apply(measure ...)

In fact, 2) should be
apply (relation "measure ...")

`It is the simplest way of specifying a termination relation, by giving a
``function into the natural numbers, which decreases at each recursive call.
`

`Example 1) is a bit trickier. It may help you to look at the types of
``the subexpressions (e.g. finite_psubset).
``Here, "..." must be a function that maps your function arguments into
``the type 'a set * nat for some 'a. These pairs are then compared with
``respect to the relation (finite-psubset <*lex*> less-than), which means
``that first the sets are compared with the strict subset relation and
``then the numbers are compared.
`
In other words, the relation
inv_image(finite-psubset<*lex*>less-than) (%x. (f x, g x))
is the same as
{ (x, y). (finite (f y) & f x \<subset> f y)
| (f x = f y & g x < g y) }

`While in the second version it is easier to see what is going on, the
``first version can be proved well-founded automatically, since it is
``built from combinators (inv_image, <*lex*>, finite_psubset, less_than)
``that already come with the relevant lemmas.
`
Hope this helps...
Alex

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*