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

[Jesse Alama <alama@stanford.edu>]

Hi Adam,

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Wed, 22 Nov 2006, Jesse Alama wrote:
>
>> 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?
>
> The problem here is that a mode redefinition cannot change the type
> completely arbitrarily - it is only allowed if the new type widens to
> the original type - as I understand this ensures unique widening
> paths.

Oh, I see, that explains things.  Let me see if I understand: `Element
of Funcs(vertices(p),{0,1})' doesn't widen to `Function', which is the
supertype I initially gave to `0-chain of p'.  Is that right?

> Still, in your case you can probably put the type which is needed for
> the Fraenkel operator to work correctly directly into the definition
> of '0-chain of p' without any need for redefining - am I right?

That's right -- I discovered that shortly after sending my message.
By simply defining

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

the error with the fraenkel terms goes away.  But then I have a new
problem: elsewhere in my file terms of the form

c.x

where c has type `0-chain of p' and x has type `vertex of p' (which is
defined as `Element of vertices(p)') are no longer well-formed.  The
problem, I think, is that c does not have type `Function'.  I suppose
one approach to this problem would be to redefine `.' for terms of
type `Element of Funcs(vertices(p),{0,1})', but that doesn't seem
appealing.  What can be done?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*4: This inference is not accepted