# [isabelle] recdef problem

In `Isabelle/HOL - A Proof Assistant for Higher-Order Logic' ([1] 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 [1] 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?
Thanks in advance.
cheers
christian sternagel

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*