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
