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

[Makarius]

On Wed, 12 Oct 2011, Makarius 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.)

Here are some partial answers from the first round of investigation.

I have tried the inversion of ca56111fe69c empirically against the 
existing applications (including AFP) with the following observations:

   (1) There are some spurious cases of vacuous "induct arbitrary: ..." 
uses that I have already eliminated in Isabelle/1fce03e3e8ad.  These 
examples mostly involve "out-of-scope" variables, that are already 
hilighted by other means (e.g. as undeclared frees), without the extra 
warning of the proof method.

   (2) There are situations where the warning was just wrong.  Typically 
where simultaneous goals are involved -- not multiple goals for 
simultanous rules.  When multiple goals are addressed by a single 
induction rule, "arbitrary" variables do not have to occur in all parts. 
There might be additional cases involving variables in assumptions, but 
not in conclusions, which I did not follow-up yet.

See also 
http://isabelle.in.tum.de/repos/isabelle/file/1fce03e3e8ad/src/HOL/Induct/Common_Patterns.thy#l170

These patterns are from the MKM2006 paper about the state of the induct 
method in 2006.  Back then I've reworked the whole setup significantly and 
was fluent in its workings.  This might explain the terseness of 
ca56111fe69c to address a detail that was "too obviously wrong" to record 
another half-sentence in the history.  Technically it meant to reduce the 
"smartness" of the method, to avoid user confusion by wrong warnings.


Back to the situation now.  I can't say on the spot what fix_tac does 
exactly in conjunction with several additional layers that have stacked up 
in the meantime.  It requires some further rounds of investigation ...


 	Makarius