Juan Perna wrote:
> I have defined a simple extension of the normal list type: [...]
> val genLast_def =
> Hol_defn "genLast" [...]
> I have to prove the termination of this function ('Define' is not
> able to do it automatically). I think the natural measure should be
> the second argument (that always get reduced, even when calling the
> mutually recursive functions). I defined a "length" operator over my
> sequences as: [...]
You're right that the size of the second argument decreases. (It's a
little surprising that Define doesn't get this; it may be a bug.) The
problem you're having with types is that you have to provide a measure
over a sum type, where each component of the sum corresponds to a
different recursive function. In your particular case, there are
three recursive functions, so you end up dealing with a sum type
: A + B + C
where each of the A, B and C is a pair, and where the second component
of each pair is the seq value that decreases. You don't need to set
up a size function of your own to prove termination, because there is
already one in the system, with name seq_size. (This is a general
rule for types declared with Hol_datatype.)
I proved termination this way:
val (genLast_thm, genLast_ind) = Defn.tprove(
genLast_def,
WF_REL_TAC `measure (\s.
case s of
INL p -> seq_size (SND p)
|| INR (INL p) -> seq_size (SND p)
|| INR (INR p) -> seq_size (SND p))` );
The INL and INR constructors are how you access the components of a
sum.
Michael.
-------------------------------------------------------------------------
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems? Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >> http://get.splunk.com/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
