[isabelle] Termination Proof ``fun'' ;)



Hello all,

I have recently been trying to write a function, which Isabelle would like to know terminates. The basic task is to find reachability, but I don't have an explicit graph, I have a function which returns children of the current node.

So I recursively define this function to essentially be something like:

all_children :: obj => obj set => obj set
all_children src seen =
  if src \<in> seen
    then seen
    else
      foldr all_children (children src) (seen \<union> {src})

I can't for the life of me figure out what the measure function should be in this case. Been thinking on it for a few days and I don't know how to state a termination proof in a way that Isabelle will understand. I should preface that by saying I only know of the "measure" method... and even then, not really well.

If anyone could provide some hint on how to go about this, then that would be great.

Regards,
Scott





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