[isabelle-dev] find_theorems and type class axioms
florian.haftmann at informatik.tu-muenchen.de
Tue Dec 22 09:38:53 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?
I think the misunderstanding is that »find_theorems foo« searches for
theorems containing a constant named »foo«. This is not the case – it
searches for theorems containing a subterm matching »foo«. I guess it
would be possible to implement searching for constants as a separate
criterion; this could also ignore sort constraints in the first place.
>> 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
>> 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
>> 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-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev