[isabelle-dev] Abbreviations and find_theorems

[Makarius]

On Sat, 15 Nov 2014, Gerwin Klein wrote:

> I agree that it would be nice to support that, esp since find_theorems 
> is supposed to help beginners find things.
>
> Applying underscores will have unwanted side effects for other terms, 
> esp constants, though, so one would have to be careful to apply this to 
> abbreviations only. AFAIR this is the reason nobody has done it yet.

The behaviour of find_theorems in this respect stems from 
Pattern.matches_subterm. In 1998 that was introduced for the Simplifier 
(6328d427a339), but Stefan Berghofer changed that in his great reform from 
2000 (5b33e732e459).

So the only use of it is now find_theorems.ML, which means it defines its 
intended meaning.  You could adapt it accordingly, to find abstractions in 
beta-applied form etc.

If Pattern.matches_subterm changes semantically, the usual way is to 
change its name as well.  It could also move to find_theorems.ML.


Independently of that, current 30b8a5825a9c already moves various add-ons 
to pattern.ML and unify.ML to a place where they are outside of modules 
that are relevant to the inference kernel.  (In the past there were 
occasional confusions about what is actually critical code and what not.)


 	Makarius

----------------------------------------------------------------------------
                   http://stop-ttip.org  927,552 people so far
----------------------------------------------------------------------------