Re: [mizar] How to search for a lemma?

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Dear dr. Trybulec,

On Mon, 17 Mar 2003, Andrzej Trybulec wrote:

> I believe the problem is not with the concept of 'Element of ...' but with
> the other concepts. E.g. how should I know that the addition in the monoid
> of real numbers is the same as the additional of real numbers (that is
> defined separately).

I think your idea of term identifications (as I understood it) could 
be used. Here it would be st. like:

identification
   let x,y be Real;
   let a,b be Element of the carrier of <REAL,+>;
:: only atomic equalities allowed in assumption
   assume that A1: a = x and A2:  b = y;  
:: only atomic equalities allowed in identification
   identify   a*b = x+y;
   proof  :: as in MONOID:40
   end;
end;

This is exported and used in the equalizer (if user wishes so, e.g. by 
some directive). I would restrict the equalizer to use it only when _both_ 
sides of the equality already exist, since using for generating new terms 
brings about complications with termination (e.g. 0 = 0+0 =0+0+0...).

Are you planning/working on st. like that?

It could be used to solve some structure-only problems too, but I think we 
could have more implicit mechanism for identification in related 
structures.

Regards,
Josef