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

[Brian Huffman]

On Wed, Oct 12, 2011 at 4:01 PM, Makarius <makarius at sketis.net> wrote:
> On Wed, 12 Oct 2011, Brian Huffman wrote:
>
>> 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.
>
> This needs some further investigation.  My log message from 2006 is an
> example of how not to do it -- just parroting the change without any
> explanation.  (2006 was a bad year in Isabelle development.)

I can think of two potential reasons for dropping the warning:

First, since fix_tac is an exported function, it might be used by
other tactics besides induction. If the warning is triggered in other
contexts, the wording of the message might be inappropriate or
misleading.

Second, it is possible that induction with "arbitrary" variables might
be used by other ML packages for internal proofs. Warnings are
obviously not helpful for users if they were not caused by those
users' proof scripts.

> Does your own change do anything different from the old version?

The warning message is worded differently, but otherwise my changeset
is almost exactly the reverse of ca56111fe69c.

- Brian