[isabelle-dev] find_theorems and type class axioms

[Andreas Lochbihler]

Hi Larry,

Type inferences assigns to "dist" the type "'a => 'a => real" where 'a :: metric_space, 
and to "norm" the type "'b => real" where 'b :: real_normed_vector (due to the type 
constraint manipulations in Real_Vector_Spaces.thy. The theorem dist_norm uses dist and 
norm with the sort dist_norm. Consequently, it can find this theorem only if metric_space 
and real_normed_vector are both subclasses of dist_norm, but they are not. Thus, it is not 
found.

In your concrete application, you can nevertheless apply the theorem dist_norm, because 
you have a concrete type (e.g. real) which instantiates both real_normed_vector and 
metric_space.

As Florian said, the problem here is really the manipulation of the type for dist and 
norm. Maybe Johannes can remember why Brian introduced this.

Best,
Andreas

On 26/11/15 14:34, Lawrence Paulson wrote:
>> On 26 Nov 2015, at 11:58, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>>
>> The sort constraints of constants play *no* role for
>> searching theorems.  The sort constraints of terms to be searched *do*,
>> and in my view this is the desired behaviour:  if I formulate a property
>> on partial orders, I do not want to be bothered by facts which only
>> apply to linear orders.
>
> I’m not sure that I understand this statement. At what point do constants become terms anyway? Consider the following search:
>
> "_<=_" "_=_”
>
> There are two terms, but they are nothing but constants. No theory is implied (I’m not sure how one could express a search that was specifically about partial orders that were not linear), and there are more than 2000 hits. They include statements involving natural numbers, integers and sets. In fact it would be good to find a way of excluding some of those.
>
> Meanwhile, the search
>
> 	norm dist
>
> contains only constants, and nevertheless it fails to pick up dist_norm: "dist x y = norm (x - y)”.
>
> Larry
>
>