Re: [isabelle] match_tac, schematic and bound variables



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.


	Makarius




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