Re: [mizar] Private DB

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

Dear Andrzej,

>to be honest I do not understand the whole fuss about weak
>types.

It is very natural to have weak types.  Types often will be
"weak" when defined in the most natural way.  It is clumsy not
to allow that.

And _I_ do not understand why one would _not_ allow weak
types.  It just would make CHECKER a bit more complicated,
right?  So why object to that?  Or is there something else
that I don't see that would be a difficulty?

Of course people write better formalizations if you force them
to prove their existence correctness conditions, because that
way you force them to think hard about their defining
properties.  But that could be part of MML policy, right?  One
could decide not to accept articles in which modes are kept
"weak" for which it is obvious (to a human :-)) that they
actually never will be empty.

>So, what we do? Instead of introducing mode with possibly
>empty types we use permissive definition of the form [...]

Ah.  I understand, I think.  It would mean that "Element of"
really should be defined in the following way:

  definition let X be set;
   assume
  Z: X is non empty;
   mode Element of X -> set means
  :Def1: it in X;
   existence by Z,XBOOLE_0:def 1;
  end;

(The "X is non empty" here is a synonym of
"meaningfulness_of_Element_for X" :-))  That would follow the
scheme that you describe, right?  So would this definition be
as practical to be used everywhere throughout the MML as the
one that's currently in MML?

But even this is crazy!  "Element of {}" is a perfectly
natural thing to write, there's no good reason to forbid it.
And it really should be the empty type: anything else is
sillyness.

By the way, a question: I understand from the finite fields
example that you can "redefine" a "permissive" definition in a
way that it doesn't need an assumption anymore.  Do you do
this by repeating the "means" part, even if it actually stays
exactly the same?  (I experimented a bit, and that's how it
seems to work.)

So in the case of "Element of" this redefinition would be:

  definition let X be non empty set;
   redefine mode Element of X means
  :Def2: it in X;
   compatibility by Def1;
  end;

So then to apply Def1 you would need to prove the assumption,
but for Def2 you would not.  (Of course requirements BOOLE
gives you so much that in this case you don't gain much by the
redefinition.)

Freek