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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
