Re: [isabelle] size_changes raises Option and Bind



On 04/27/2012 11:33 AM, Andreas Lochbihler wrote:
In Isabelle 2011-1, size_change raises the exception Option (line 81 in
general/basics.ML) and Bind (line 277 of termination.ML) for the
following function definitions. The NOT operator seems to cause the
trouble, because size_change (and lexicographic_order) work perfectly
well when I unfold NOT i = -i - 1.

This either seems like a bug in termination or some bad setup for NOT.

Thanks for reporting this. It is a bug in size_change (more precisely,
the dependency graph construction). Embarrasingly, the edges in the
graph seem to have the wrong direction, which got unnoticed several
years. This shows that size_change still isn't used/tested much.

I am preparing a fix.

Now done, in Isabelle/2d48bf79b725.

The correct behaviour is that in the first function, some progress is made by removing one of the calls, and in the second function, nothing can be done, because a priori, the termination prover knows nothing about NOT. So unfolding it is probably a good idea. Note that you can do this locally in the termination proof, e.g. by (lexicographic_order simp: ...).

Alex





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