[isabelle-dev] find_theorems and type class axioms
andreas.lochbihler at inf.ethz.ch
Thu Nov 26 15:07:59 CET 2015
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
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
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.
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)”.
More information about the isabelle-dev