# [isabelle-dev] recursive datatype measure

Chris Capel pdf23ds at gmail.com
Mon Feb 16 19:55:22 CET 2009

```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)

```