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

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrzej,

>> Maybe there could be a requirement that gives all expressions
>> of type "real number" also the type "Real" (and the same for
>> "natural number" versus "Nat", etc.), and then it doesn't
>> matter anymore what you choose?
>
>Too much adhocness for me.

What I would like: if you can prove a theorem of the shape

  for x st x is T1 holds x is T2

then you can "register" it in some way, and the type checker
will then always add "T2" to the collection of types if "T1"
is in that collection already.  Something like a generalized
cluster.

Of course you'd then lose the property that each expression
has just one "radix type" (that's the word?)  I don't know
how bad that would be.

>Only I do not understand 'Archimedean'

The idea is that for any field (even: every ring with unit)
there's a natural mapping from NAT to that field.  So, if you
call this mapping "nring", then the Archimedean property
becomes:

  for x being Element of the carrier of F
    ex n being Nat st x < nring n

where < is the order of the ordered field F.  There are many
non-Archimedean ordered fields, but I think that the field of
the real numbers is the unique Archimedean complete ordered
field.

Freek