[isabelle-dev] recursive datatype measure
krauss at in.tum.de
Mon Feb 16 21:44:10 CET 2009
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
This has nothing to do with circular structures, which are not possible
with inductive datatypes.
> More details: after I apply
> 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)
> ?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
More information about the isabelle-dev