[isabelle-dev] recursive datatype measure

[Alexander Krauss]

Dear Chris,

At first glance, this looks provable to me...

Can you give us the concrete function definition?

Note that for "xs :: T list" there is a difference between "size xs" 
(length of the list) and "list_size size xs" (sum of sizes of elements).

Chris Capel wrote:
> I have a recursive datatype,
> 
> datatype prod =
>     PTrm nat
>   | Prod "prod list list"
> 
> and I've defined a recursive function in it using foldl. I'm trying to
> prove termination, but I'm not sure how. I think my key difficulty
> might be that I need to prove that p :: prod : set (pl :: prod) ==>
> size p < size pl. (This is also where the automatic termination proof
> fails.) Can this be done? I think this is equivalent to the question
> of whether circular structures can be created out of datatypes in
> Isabelle.

This has nothing to do with circular structures, which are not possible 
with inductive datatypes.

> More details: after I apply
> 
> termination
> apply (rule local.termination, auto)
> 
> I get the following subgoal:
> 
> goal (1 subgoal):
>  1. !!(pll::prod list list) (toks::nat list) (pl::prod list) (len::int)
>        (p::prod) l::nat list.
>        [| pl : set pll; (p, l) : set (zip pl toks); len ~= (-1::int) |]
>        ==> ?f7 (p, l) < ?f7 (prod.Prod pll, toks)
> variables:
>   ?f7 :: prod * nat list => nat
> 
> Applying instead relation "measure (%(p, l). size p)" yields the
> conclusion (with the same assumptions), "size p < Suc (list_size
> (list_size size) pll)".
> 
> Chris Capel

Alex