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.