[isabelle-dev] recursive datatype measure

[Chris Capel]

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.

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
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)