[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? 


> 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