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.haftm...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
