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.


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