[isabelle] fun termination, mutual-recursive datatype



Dear Isabelle,

I am using a groovy mutually-recursive datatype a bit like the following one:

> datatype jack = A "int" | B "jill"
> and jill = C "int => jack" "int list"

I would like to write a (mutually-recursive) function over my datatype, something like this:

> datatype jack = A "int" | B "jill"
> and jill = C "int => jack" "int list"
> 
> fun 
>   foo_jack :: "jack => int" and
>   foo_jill :: "jill => int"
> where
>   "foo_jack (A n) = n"
> | "foo_jack (B j) = foo_jill j"
> | "foo_jill (C f ns) = listsum (map (foo_jack \<circ> f) ns)"

But the <fun> command says: "Could not find lexicographic termination order." Does anybody know how one might prove that such a function terminates? 

Thanks very much!
John

ps. I wondered whether the problem was the (infinite) "int => jack" in the C-constructor. I replaced it with a (finite) association list "(int * jack) list", and changed foo_jill so

> "foo_jill (C f ns) = listsum (map (foo_jack \<circ> (lookup f)) ns)"

where

> "lookup A x == (map snd A) ! (THE i. (map fst A) ! i = x)"

but it didn't help.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.