[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Isn't "Subset of" the same as "Element of bool"?

Hi,

Freek Wiedijk wrote:

  definition
   let B be set;
   let A be Subset of B;
   redefine func bool A -> Subset of bool B;
   coherence by ZFMISC_1:79;
  end;

  for B being set, A being Subset of B, X being Subset of A holds
   X qua Subset of B is set;
  ::>  *116

  for B being set, A being Subset of B, X being Element of bool A holds
   X qua Subset of B is set;

  ::>
  ::> 116: Invalid "qua"

I've been looking, but I couldn't find this redefinition
elsewhere (did I miss it?)

But the main question: why doesn't this work when X is
Subset of A, but it _does_ work when X is Element of bool A?
I thought that both were the same!  Because in SUBSET_1 it says:

  definition let X;
   mode Subset of X is Element of bool X;
  end;


Expandable definitions are "static", i.e., any redefinition of
constructors which are given after "is" has no impact on
identification. They are stored in terms of constructors and
no any connection with notation is recognized.
So  Subset of A is identified (according to MML Query)
   SUBSET_1:mode 1(ZFMISC_1:func 1(A))
even if   bool A is identified now as
   NEWTEXT:func 1(A)

It is better to repeat expandable definition after redefinition
of "bool".

Grzegorz