[isabelle] recursive functions and set comprehension



Hello all, consider the (admittedly strange) fragment:

datatype tm = Z | S "tm"

consts foo :: "tm => tm set"
recdef foo "measure size"
"foo x = { Z. (x = Z) } \<union>
         { (S x1) | x1. x = S x1 /\ x1 : (foo x1) }";

Isabelle cannot prove monotonicity, because the equation "x = S x1"
seems to not be available. In particular, she tries to prove to me that:

    forall x1. size x1 < size x
instead of:
    forall x1. (x = S x1) --> (size x1 < size x)

Why is this happening? Why aren't the rest of the equations in the comprehension used to derive the monotonicity requirement? Here's my
explanation:
Such a thing would still be sound. Because if the "x = S x1" was false
no call to "foo x1" would have to be done and hence no monotonicity
check would be necessary. The whole predicate (x = S x1 /\ x1: foo x1)
would be false and the particular set component empty. But the problem
would be that checking that the predicate is false would require in the
general case validating the predicate in a particular order (one that
does not attempt to run foo first) and perhaps there's no internal
mechanism in Isabelle to do such a thing. Is this the reason? Or is such
a thing not sound alltogether? It would be nice if such a definition was
possible.

Thanks!

--dimitris

ps: I know that I can rewrite the function in other ways that will make
it work but I really want to keep this style (basically because with
this style I do not have to write explicit pattern match cases for
fail-through cases---when the predicate fails, the set is empty and
that's it)





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