[isabelle-dev] find_theorems and type class axioms

[Lawrence Paulson]

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...