# [isabelle] recdef problem

```In `Isabelle/HOL - A Proof Assistant for Higher-Order Logic' ( in the following) `recdef' is used to define functions for the datatype

datatype ('v,'f)"term" =
Var 'v
| Fun 'f "('v,'f)term list"

For me it gets interesting as soon as higher-order functions can be used to define functions with `recdef'. In  there is following example:

consts trev :: "('v,'f)term => ('v,'f)term"
recdef trev "measure size"
"trev (Var x) = Var x"
"trev (Fun f ts) = Fun f (rev (map trev ts))"

which could be proved terminating after the hint

t : set ts --> size t < Suc (term_list_size ts)

I wanted to define following function (which gives the set of positions of a term---where a position is a possibly empty list of natural numbers):

consts pos :: "('v,'f)term => nat list set"
recdef pos "measure (% t. size t)"
"pos (Var v) = {[]}"
"pos (Fun f ts) =
{[]} Un {(i#p) | i p. i : {0..<length ts} & p : pos (ts!i)}"

which is not possible automatically because of the unsolved goal:

\<forall> :001 ts. size (ts ! :001) < Suc (term_list_size ts)

now my questions:
1) what does :001 mean (I just assumed its the index variable i from my definition).
2) why is the information i : {0..<length ts} lost, which would make the unsolved goal equivalent to:

t : set ts --> size t < Suc (term_list_size ts)

3) is it possible to do a termination proof for a recdef definition fully by hand in order to make sure, that i : {0..<length ts} is used?