[isabelle-dev] find_theorems and type class axioms

[Johannes Hölzl]

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