[isabelle-dev] recursive datatype measure
pdf23ds at gmail.com
Mon Feb 16 19:55:22 CET 2009
I have a recursive datatype,
datatype prod =
| 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
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)".
"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)
More information about the isabelle-dev