Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:
> On Wed, 22 Nov 2006, Jesse Alama wrote:
>
>> Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:
>>
>>> I think the problem is that the type "0-chain of p" does not
>>> syntactically widen to "Element of ..." . I checked just now, and it
>>> seems that non-emptiness is no longer a problem. So yes, this really
>>> has to be done syntactically in the (re)definition of "0-chain of"
>>> like
>>>
>>> mode 0-chain of p -> Element of foo means ....
>>>
>>> If it is e.g. just a proved theorem, Mizar will take no notice.
>>
>> I see now, thanks. If I choose to not redefine 0-chain of p, what
>> form should the theorem take?
>
> just to repeat for sure: if you choose not to have the type widened
> through (re) definitions into Element of ..., the fraenkel term will
> not work (with the current implementation)
Oh, I see, I misunderstood: I thought that there were two approaches
to solving the problem (redefinition, prove a theorem), but now I see
that only one of these (redefinition) solves the problem.
I've written the redefinition as follows:
definition let p be polyhedron;
redefine mode 0-chain of p -> Element of Funcs(vertices(p),{0,1});
::> *118
end;
Error 118 is: "Invalid specification". The redefinition is broken but
the error I had with the fraenkel term goes away. I'm not sure what
the problem is with my redefinition. Curiously, I also get the same
error when I replace `Element of Funcs(vertices(p),{0,1})' with a much
wider type:
definition let p be polyhedron;
redefine mode 0-chain of p -> set;
::> *118
end;
What might be going on here?
Thanks,
Jesse
--
Jesse Alama (alama@stanford.edu)
*4: This inference is not accepted