Re: [Hol-info] defining mutually recursive functions that use two categories of variables

[Michael N. <Mic...@ni...>]

w_...@en... wrote:
> I am trying to define mutually recursive functions that use two  
> categories of variables: time and space coordinates. HOL did not  
> distinguish between arguments when trying to prove termination. Is it  
> possible to specify the set of arguments that need to be considered  
> for proofing termination.

Absolutely.

> In the following simple example, The time argument of the calling  
> function is always strictly greater than those of the called functions.
> This should be enough for the functions to terminate.

It is indeed sufficient.

>   To define them using HOL, we have to prove that the summation of the  
> arguments  of each of the called functions is strictly less than the  
> summation of the arguments of the calling function, which is not true  
> here.

This statement is false.


> val defn = Hol_defn "fn1fn2"
> `(fn1 t x y =
>       if ((t = 0) \/ (x = 0) \/ (y = 0)) then 1 else
>     (fn1 (t - 1) x y ) + (fn2 (t - 1) x (y+1)))
> /\
> (fn2 t x y  =
>       if ((t = 0) \/ (x = 0) \/ (y = 0)) then 1 else
> 	(fn2 (t - 1) x y) + (fn1 (t - 1) x (y+1)))
> `;

This tactic:

  WF_REL_TAC `measure (\s. case s of INL trip -> FST trip
                                  || INR trip -> FST trip)`);

solves the termination goal (assuming that the first argument of each 
function is a natural number).

Michael.