# [isabelle-dev] [isabelle] match_tac, schematic and bound variables

Makarius makarius at sketis.net
Mon Aug 19 23:41:48 CEST 2013

On Mon, 19 Aug 2013, Lawrence Paulson wrote:

> I was about to change the documentation to say just that, only to
> discover that almost exactly the same change was made in November 2008.
>
> wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100     src/Doc/IsarImplementation/Tactic.thy:321:   \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
> wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100     src/Doc/IsarImplementation/Tactic.thy:322:   bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},
> wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100     src/Doc/IsarImplementation/Tactic.thy:323:   @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do
> wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100     src/Doc/IsarImplementation/Tactic.thy:324:   not instantiate schematic variables in the goal state.
> wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:321:
> wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:322:   Flexible subgoals are not updated at will, but are left alone.
> wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:323:   Strictly speaking, matching means to treat the unknowns in the goal
> wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:324:   state as constants; these tactics merely discard unifiers that would
> wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:325:   update the goal state.

I cannot read the above copy paste from what you see on your screen.  When
pointing to the history you need to tell the changeset id (abbreviated
hashkey) not the phyical index or date.

Refurbishing all these old manuals over several years, I have moved around
things between different files and directories, so that match_tac is now
in the "implementation" manual here:
http://isabelle.in.tum.de/repos/isabelle/file/15fe0ca088b3/src/Doc/IsarImplementation/Tactic.thy#l336

It originally comes from your initial version of the "ref" manual
http://isabelle.in.tum.de/repos/isabelle/annotate/d8205bb279a7/doc-src/Ref/tactic.tex#l74

This text from Nov 1993 gives a sense of the anciety of this stuff.
Clearly the system around it has improved way beyond the "research
prototype" nature of the original "Isabelle" with unify.ML at its core.
(I am still convinced that it was a very good approach, and don't want to
see it destroyed at the very core.)

Of course you are welcome to update your documentation snippet on
match_tac.  I am also ready to remove it from the documentation
altogether.  Brushing up the old "ref" material since 2008 for the
"implementation" manual has introduced some bias towards vintage
operations. E.g. some readers have pointed out the relative insignificance
of the res_inst_tac family just after I had reconstructed that section --
and they were right about it.

Makarius