Ah, after I read Gerwin's email, I thought it was really a problem with
find_theorems. But now you reminded me that it was the setup of
dist_norm.
As far as I remember the reason is that you want to have the syntactic
type classes when you instantiate a type to have dist and norm. But
later when you prove you always want to have metric_space or
real_normed_vector.
Why is the instantiation easier? You only need to define dist as
dist_norm governs, and otherwise you do not show anything about dist.
You only proof real_normed_vector axioms for norm, and then you know
that metric_space is a subclass of real_normed_vector.
The other options I can think of are:
1) you have special type classes like:
* toplogical_metric_space (open is defined with dist)
* metric_real_normed_vector (dist_norm holds)
2) you repeat always the proof that your dist defined with norm is
actually a metric space...
A solution for the dist_norm (and also open_dist) problem would be to
just add a theorem:
lemma dist_norm:
fixes x y :: "'a :: real_normed_vector"
shows "dist x y = norm (x - y)" by (rule dist_norm)
(and of course rename the original one to something like
dist_norm_syntactical) Then at least that one gets found...
- Johannes
Am Donnerstag, den 26.11.2015, 15:07 +0100 schrieb 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.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/isabel
> le-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
