Re: [isabelle] match_tac, schematic and bound variables
On Tue, 13 Aug 2013, Tobias Nipkow wrote:
Am 12/08/2013 22:39, schrieb Lawrence Paulson:
I see that match_tac is basically part of the classical reasoner. It is for applying rules safely without affecting the proof state. Any significant change in its behaviour would breaks lots of things, but it's conceivable that there's a bug in this example. Or else the documentation isn't quite accurate.
The term "match" has precisely the definition you quote in the
documentation, and that should be the specifiation of anything called
"match". If the implementation does not conform, it should be fixed. I
agree this may be hard in this case and it is not a top priority.
Alternatively the documentation should carry a warning.
Larry is of course welcome to reformulate this snippet of the
documentation to fit better to the implementation, whatever it really is.
A warning like "the documentation might be inaccurate" does not make any
sense, because this always applies by default to *any* documentation.
Whenever someone sees a function somewhere, and some documentation
elsewhere, maybe together with some real-world uses of it in some working
application, one always needs to apply common-sense to estimate if it will
do a different job in a different context.
This principle applies to any complex software system, library, framework,
etc. For Isabelle the level of precision is actually above average -- I
am working routinely with more industrial things like the Java Standard
libraries that are much worse. And what Apple, Oracle, IBM usually do in
cases of uncertainty is to adapt the manual only.
This archive was generated by a fusion of
Pipermail (Mailman edition) and