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

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Josef Urban wrote:

> 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?

I would like to discuss it, at least. I am a bit uneasy about it (even if it is
definetely in Mizar style). It does solve the problem put by Freek: the concepts
must be introduced idenpendently for real numbers and for monoids, but at least
theorems about real numbers can be used for elements of <REAL,+> and vice versa,
but then most of them will be proved for reals.

The identification is maybe wrong name. We already overuse it (identification of
identifiers, identification of symbols).

Regards,
Andrzej