[isabelle-dev] find_theorems and type class axioms

[Florian Haftmann]

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 <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...
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20151222/7ad5a969/attachment.asc>