Hello everyone,
I have defined a simple extension of the normal list type:
Hol_datatype
`seq =
Empty
| CombBlk of num => hwAction set => seq
| ClkBlk of num => clkAction set => seq
| Link of num => hwAction set => seq`;
and now I am trying to define a "last-element" function in a way useful
for some proofs I have to do about it. My definition involves three
auxiliary functions:
val combLast_def =
Define `(combLast x a (CombBlk x1 a1 rst) =
if (x = x1)
then (CombBlk x (a UNION a1) rst)
else (CombBlk x1 a1 rst))
/\ (combLast x a Empty = (CombBlk x a Empty))
/\ (combLast x a rst = rst)`;
val clkLast_def =
Define `(clkLast x a (ClkBlk x1 a1 rst) =
if (x = x1)
then (ClkBlk x (a UNION a1) rst)
else (ClkBlk x1 a1 rst))
/\ (clkLast x a Empty = (ClkBlk x a Empty))
/\ (clkLast x a rst = rst)`;
val linkLast_def =
Define `(linkLast x a (Link x1 a1 rst) =
if (x = x1)
then (Link x (a UNION a1) rst)
else (Link x1 a1 rst))
/\ (linkLast x a Empty = (Link x a Empty))
/\ (linkLast x a rst = rst)`;
and a function that will transform a sequence (of the "seq" type) into a
(possibly nested) call to the functions defined above:
val genLast_def =
Hol_defn "genLast"
`(genCombLast x Empty = Empty)
/\ (genCombLast x (CombBlk x1 hwa rst) =
(combLast x hwa (genCombLast x rst)))
/\ (genCombLast x (ClkBlk x1 cka rst) =
(clkLast (SUC x) cka (genClkLast (SUC x) rst)))
/\ (genCombLast x (Link x1 hwa rst) =
(linkLast (SUC x) hwa (genLinkLast (SUC x) rst)))
/\ (genClkLast x Empty = Empty)
/\ (genClkLast x (CombBlk x1 hwa rst) =
(combLast (SUC x) hwa (genCombLast (SUC x) rst)))
/\ (genClkLast x (ClkBlk x1 cka rst) =
(clkLast x cka (genClkLast x rst)))
/\ (genClkLast x (Link x1 hwa rst) =
(linkLast (SUC x) hwa (genLinkLast (SUC x) rst)))
/\ (genLinkLast x Empty = Empty)
/\ (genLinkLast x (CombBlk x1 hwa rst) =
(combLast (SUC 1) hwa (genCombLast (SUC x) rst)))
/\ (genLinkLast x (ClkBlk x1 cka rst) =
(clkLast (SUC 1) cka (genClkLast (SUC x) rst)))
/\ (genLinkLast x (Link x1 hwa rst) =
(linkLast x hwa (genLinkLast x rst)))`;
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:
val len_def =
Define `(len Empty = 0)
/\ (len (CombBlk x hwa rst) = SUC (len rst))
/\ (len (ClkBlk x ca rst) = SUC (len rst))
/\ (len (Link x hwa rst) = SUC (len rst))`;
However, when trying to use it to find WF relation (i.e., by using:
(WF_REL_TAC `measure (len o SND)`)), I get this error:
Type inference failure: the term
measure (len o (SND :'a # seq -> seq))
on line 831, characters 16-34
which has type
:'a # seq -> 'a # seq -> bool
can not be constrained to be of type
:num # seq + num # seq + num # seq ->
num # seq + num # seq + num # seq -> bool
unification failure message: unify failed
Exception raised at Tactical.THEN:
at Preterm.typecheck: between
frag 0 row 0 col 1 and line 831, character 35:
failed
! Uncaught exception:
! HOL_ERR
I tried to make my "len" function as close to LENGTH as possible and I
also checked the types of the term `(len o SND)` and they seem to be the
right ones... What is what I am missing?
Thank you very much,
Juan
-------------------------------------------------------------------------
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
