[mizar] Re: a term representing the extension of a type

[Jesse Alama <alama@stanford.edu>]

Hi Josef,

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> On Wed, 29 Nov 2006, Jesse Alama wrote:
>
>> Andrzej Trybulec <trybulec@math.uwb.edu.pl> writes:
>>
>>> you probably need in the Environment Declaration
>>>
>>>   registrations FRAENKEL;
>>
>> Why?
>
> Because the registrations in FRAENKEL ensure that the type Element of
> Funcs(A,B) widens to the "type" Function. "Function" is actually just
> syntactic sugar ("expandable mode") for attributes Function-like and
> Relation-like
> (http://mmlquery.mizar.org/mml/4.66.942/funct_1.html#NM1).
>
> When you import the needed registrations from FRAENKEL, i.e.
>
> registration let A, B be set;
>  cluster Funcs(A,B) -> functional;
> end;
>
> registration let P be functional set;
>   cluster -> Function-like Relation-like Element of P;
> end;
>
> the attribute "functional" will be automatically added to any
> "Funcs(A,B)" term, and the attributes "Function-like" and
> "Relation-like" will be automatically added to any term which already
> has the "functional" attribute, making it a "Function" (needed for the
> "." functor).

Thanks; I appreciate your help.  It still seems that I'm missing
something, though.

In the MIZAR file in question the registerations directive is

registrations FRAENKEL, FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1, SUBSET_1, NAT_1, INT_1, VECTSP_1;

Here's my definition of 1-chain of p:

definition let p be polyhedron;
  mode 1-chain of p is Element of Funcs(edges(p),{0,1});
end;

Here's the problematic definition:

definition let p be polyhedron, c be 1-chain of p, v be vertex of p;
  func ENumSet(p,c,v) -> Subset of {0,1} means
  ex X being Subset of {0,1} st X = { aa(p,v,e) where e is edge of p : c.e = 1 } & it = sum(X);
::>                                                                     *103
  existence;
  uniqueness;
end;

Error 103 is "Unknown functor".  I'm pretty sure that the problem here
is that c does not have type `Function'.  (Evidence:

definition let p be polyhedron, c be 1-chain of p, v be vertex of p;
  func ENumSet(p,c,v) -> Subset of {0,1} means
  ex X being Subset of {0,1} st X = { aa(p,v,e) where e is edge of p : (c qua Function).e = 1 } & it = sum(X);
::>                                                                         *116
  existence;
  uniqueness;
end;

Error 116 is "Invalid `qua'".)

Here's what I think is happening. The term `Funcs(edges(p),{0,1})' has
type `functional' thanks to

registration let A, B be set;
 cluster Funcs(A,B) -> functional;
end;

in FRAENKEL.  Also, `Element of Funcs(edges(p),{0,1})' has type
`Function-like Relation-like Element of P', thanks to

registration let P be functional set;
 cluster -> Function-like Relation-like Element of P;
end;

in FRAENKEL.  (Does this statement say that any term that has type
Element of P, where P has type functional set, gets types
Function-like and Relation-like?) Finally, we have

definition
  mode Function is Function-like Relation-like set;
end;

from FUNCT_1, which is in my definitions directive.  (FUNCT_1 is also
in my registrations directive.)

Is this a correct reconstruction of what's happening?
What might account for the error that I'm getting?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*393: Incorrect beginning of a reasoning item