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