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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.