[isabelle-dev] find_theorems and type class axioms
Lawrence Paulson
lp15 at cam.ac.uk
Thu Nov 26 15:50:18 CET 2015
I still have no idea why find_theorems should refuse to find a theorem containing two named constants, no matter what the sorts say. Are there examples of searches that would deliver crazy results if this constraint were lifted?
Larry
> On 26 Nov 2015, at 14:41, Johannes Hölzl <hoelzl at in.tum.de> wrote:
>
> 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...
More information about the isabelle-dev
mailing list