[isabelle-dev] Fwd: [isabelle] find_theorems and locales

[Larry Paulson]

Nobody has commented on this issue, and I would like to re-raise it, as it affects the development version.

It simply doesn’t make sense that fundamental axioms such as dist_norm are concealed from find_theorems. I imagine it would be very easy to change this behaviour.

Larry

> Begin forwarded message:
> 
> From: Larry Paulson <lp15 at cam.ac.uk>
> Subject: Re: [isabelle] find_theorems and locales
> Date: 19 June 2015 16:22:53 BST
> To: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
> Cc: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>, cl-isabelle-users at lists.cam.ac.uk
> 
> I've stumbled across a related issue with find_theorems that certainly seems wrong. I was searching for the theorem Real_Vector_Spaces.dist_norm_class.dist_norm, which is introduced as a type class axiom here:
> 
> class dist_norm = dist + norm + minus +
>  assumes dist_norm: "dist x y = norm (x - y)"
> 
> Calling find_theorems with suitable patterns, such as 
> 
> 	dist "norm (_-_)”
> 
> does not return this theorem among the results, but clearly it should.
> 
> Larry