[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.