Re: If A=B & (A contains C), why mizar doesn't infer (B contains C)

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

On Mon, 25 Jun 2001, Andrzej Trybulec wrote:

> What to do with fictitious loci? I believe we need a revision program that
> removes them. But what to do when fictitious loci are visible. Look to the
> example:
> 
> definition
> let C be non empty set;
> let h,g be Membership_Func of C;
> let A be FuzzySet of C,h;
> let B be FuzzySet of C,g;
> pred A=B means
> :: FUZZY_1:def 3
> for c being Element of C holds h.c = g.c;
> end;
> 
> What you propose to with this?

I did not write about REMOVING fictitious arguments, in general case, it
could probably get quite complicated (I mean the implementation). I meant
treating them exactly the same way, as the superfluous arguments of
redefinitions (i.e. temporarily forgetting about them, when we check
equality of two redefined constructors). So the proposal for FUZZY_1:def 3
is to have the normal predicate FUZZY_1:pred1 with arity 5, and
additionally, to remember that the arguments A and B (the last 2
arguments) do not have to be checked.

> > I think the real problem is understanding hidden variables. It is a nice
> > feature to have them, and not to have to mention all of the "implicit
> > context" in the notation, but it may be confusing when one is learning
> > Mizar. Maybe adding the possibility to view items in the inner cnstructors
> > notation (e.g. as in Grzegorz's Encyclopedia) would help this.
> >
> 
> I am so accustomed to them ... BTW Lego has them, too. Has not?

I don't know (yet :-)). I did not mean to throw away a nice feature, just
because it is a little complicated; only to add some utility that helps to
explain it.     

Best Regards
Josef