In a mizar proof that I'm working on I consider the extension of a
type; the problem is that the fraenkel term I use to denote that
extension doesn't seem to be acceptable. In my mizar file I've
defined the modes `polyhedron' and `0-chain of p', where the term p
has type `polyhedron'. I then try to define a functor, 0-chains, that
denotes the extension of the (parameterized) type. My definition is
as follows:
definition let p be polyhedron;
func 0-chains(p) equals
{ c where c is 0-chain of p : not contradiction };
::> *129
correctness;
end;
Error 129 is "Invalid free variables in a Fraenkel operator".
How can I make the transformation from a type to its extension?
After looking around on the mizar wiki, it seems that what's going on
here (please correct me if I'm wrong) is that mizar isn't recognizing
that the term c of type 0-chain of p widens to the type `Element of X'
for some term X of type `non empty'. Intuitively, though, c can widen
to that type, since I've proved (earlier in the file, and this proof
is accepted) that the mode `0-chain of p' has a non-empty extension.
In other words: I believe I see, from a syntactic point of view, why
`0-chain of p' doesn't widen to `Element of X' for some term X of type
`non empty'. But semantically it seems that `0-chain of p' does
"widen" to `Element of X' for some non-empty X, namely the extension
of the type `0-chain of p', which was proved to be a non-empty set.
Any comments would be appreciated!
Thanks,
Jesse
--
Jesse Alama (alama@stanford.edu)
*4: This inference is not accepted