[isabelle-dev] find_theorems and type class axioms

[Lawrence Paulson]

Perhaps the question relates to how polymorphism is interpreted in these searches. I’m getting the idea that the search for “dist” and “norm” somehow produces a combination of type classes that doesn’t precisely match the instances in the axiom “dist_norm”, where they are too specific to be picked up. And yet, searching for “op<“ picks up a lot of theorems about natural numbers even though the original search is polymorphic. So it may be that our interpretation of “too specific” needs to be revisited.

Larry

> On 22 Dec 2015, at 08:38, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> I think the misunderstanding is that »find_theorems foo« searches for
> theorems containing a constant named »foo«.  This is not the case – it
> searches for theorems containing a subterm matching »foo«.  I guess it
> would be possible to implement searching for constants as a separate
> criterion;  this could also ignore sort constraints in the first place.
> 
> Cheers,
> 	Florian
> 
>> 
>> Larry