Hi Larry, > 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.
Cheers,
Florian
>
> 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
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
