[isabelle-dev] Reviving an old thread: [isabelle] structured induction: mutual definitions and "arbitrary" in inductions?

[Brian Huffman]

Hello all,

This is a follow-up to the conversation on the isabelle-users list
from a few months ago, about confusion that arises when using mutual
induction with the "arbitrary" option.

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-June/msg00001.html

At the time I suggested that their ought to be a warning message when
you specify an "arbitrary" variable, if that variable does not
actually appear in the goal. Today I finally tried implementing this
warning message; it turns out that it requires only a simple
modification to function fix_tac in src/Tools/induct.ML.

After implementing the warning, I dug through the revision history and
was surprised to find that my "new" feature actually used to exist! It
was removed in January 2006:

http://isabelle.in.tum.de/repos/isabelle/rev/ca56111fe69c

I don't understand why the warning message was ever removed. The
commit message "fix_tac: no warning" is unhelpful.

Is there any good reason why we shouldn't put the warning back in?

- Brian