[isabelle-dev] [isabelle] Higher-order matching against schematic variables
makarius at sketis.net
Fri Nov 19 22:35:39 CET 2010
On Fri, 19 Nov 2010, Lawrence Paulson wrote:
> Indeed I find the code peculiar, in that it delivers the higher-order
> matchers followed by the first-order ones. But these are different
> things. And I imagine there is often redundancy.
Unify.matchers started as Isar-specific ProofContext.simult_matches many
years ago. The main idea is to make Isar "is" patterns behave as sensible
as possible. Browsing a little through the changset history, you can see
how I have struggled with it over the years.
In 2000 everything is still relatively plain and simple, e.g. see
Around 2006 I've made some further revisions, and things became much more
227a01b8db80 moved to unify.ML
8257e52164a1 matchers: try pattern_matchers only *after* general
matching (The pattern version is not a faithful approximation because
it falls back on first-order matching!);
9e7d3d06c643 matchers: fall back on plain first_order_matchers, not pattern;
Etc. Maybe you find some more explanations.
More information about the isabelle-dev