[EMAIL PROTECTED] 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.
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
