# Re: [isabelle] match_tac, schematic and bound variables

On Mon, 12 Aug 2013, Tobias Nipkow wrote:


Am 12/08/2013 18:13, schrieb Makarius:

On Mon, 12 Aug 2013, Lars Noschinski wrote:


I stumbled upon some odd behaviour of match_tac.


Larry is the one to explain what really happens.

When I came across match_tac for the first time as a very young student in 1993,
I was already wondering about it -- but it was always document in the manner of
what is now in "implementation" manual (section 4.2.1):

\item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},
@{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do
not instantiate schematic variables in the goal state.

Flexible subgoals are not updated at will, but are left alone.
Strictly speaking, matching means to treat the unknowns in the goal
state as constants; these tactics merely discard unifiers that would
update the goal state.

This sounds like it is better not to lean out of the window too far.


It is the documentation that is leaning too far out of the window. The
difference between


The documentation is also going back to Larry.


I don't complain about anything he did there many years ago. One needs to be realistic about what certain parts of a system can do and what not.


Makarius



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