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

[Makarius]

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