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

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

Hi,

I will probably just repeat what Grzegorz has written earlier:

(D1)
> 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;
> 
(D2)
> definition
>  let A be set;
>  mode Subset of A is Element of bool A;
> end;

Note that tha "bool" in (D2) is the original "bool" (let's call it 
"bool#1"), not the redefined ("bool#2") from (D1),
and it behaves "statically", i.e. even if you later have 
A being Subset of B, Subset of A will still expand to Element of bool#1 A.

To get bool#2 here, you would have to write in (D2):
let B be set;
let A be Subset of B; 
instead (i.e. what Adam suggests).

So (D2) adds a new pattern for Subset of A, and this pattern overrides the 
old one from SUBSET_1, but there is no difference berween the two, so 
(D2) in the original form is redundant.


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

If you do in Emacs: 
Mizar->Const. Explanations->Verbosity->translated formula, 
and Shift-mouse3 on the final semicolon after processing,
this one expands to:

"for HIDDEN:mode.1 ;for SUBSET_1:mode.1 ZFMISC_1:func.1 B1 ;; 
 for SUBSET_1:mode.1 ZFMISC_1:func.1 B2 ;;B3 is HIDDEN:mode.1 ;"

(but you will get e.g. \235 instaed of "for", or \220 instead of "is" 
there - I was lazy to translate them too).

So X (= B3, the third quantification) is 
"SUBSET_1:mode.1 ZFMISC_1:func.1 B2" here, which is 
"Element bool#1 A". 
Similarily, A ( = B2) is "Element bool#1 B".

So (D1) and bool#2 really were not employed here.

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

Now the translation is:
"for HIDDEN:mode.1 ;for SUBSET_1:mode.1 ZFMISC_1:func.1 B1 ;;
 for SUBSET_1:mode.2 ZFMISC_1:func.1 B1 ;FRTEST:func.1 B1 B2 ;;
 B3 is HIDDEN:mode.1 ;"

So A is as before, but X made it to:
"SUBSET_1:mode.2 ZFMISC_1:func.1 B1 ;FRTEST:func.1 B1 B2"

where FRTEST:func.1 is absolute name for "bool#2", and SUBSET_1:mode.2 is
the second Element from SUBSET_1 (which has one hidden argument), 
so X is:
Element#2(bool#1(B), bool#3(B,A) )

So (D1) could fire here (because you wrote "bool" explicitly), and since 
its result type is "(non empty) Element#1 bool#1 bool#1 B", Element#2 
could fire here too ("bool#1 B" is also non empty). The widening of 
"Element#2(bool#1(B), bool#3(B,A) )" is "Element#1 bool#1 B", which is 
exactly what you required by the "qua".
I hope I have clouded this enough :-).

> I repeat the expandable definition of "Subset of" and still
> it doesn't work?  What should I do to get the nice
> transitivity of "Subset of"?  I'm very confused.

I am not sure that these features are so nice. Actually, I added the 
Constructor Explanations, because I was terribly lost in such problems 
when writing articles in a bit richer environment. It seems to me that as 
the MML grows, the user that would (naively) want to use a bit more of it 
in one place, will be mostly facing such problems instead of doing 
mathematics.

Josef