Re: Proving inequality of structs ?

Hi Greg,

it has been discussed couple of times on this forum that the semantics of 
the Mizar structures is underspecified. This leads to various problems, 
and even alternative structures modelled as partial functions in Mizar by 
Lee and Rudnicki to get rid of the worst 
(http://www.springerlink.com/index/cx5518q23780417k.pdf). I hope someone 
can explain to you why is Mizar designed not to know the facts below. I 
don't think I know. The facts are probably not provable in (current) Mizar 
at all (provided Mizar is consistent :-).

The "forgetfulness" is supposed to mean that you are "forgetting" about 
some fields in a structure. There is actually no "constructor" (in the 
Mizar sense of the word) for it, and the special syntax

the 1-sorted of s

is just a shortcut for

1-sorted(# the carrier of s #)


Josef

On Wed, 14 Jan 2009, Greg Frascadore wrote:

>
>    Hello,  I could use a little help with my understanding of
>    Mizar structs and strict.
>
>    My current understanding is based on "Some Features of the Mizar
>    Language" by Trybulec. I've also seen the long email thread
>    for Jesse Alama <http://www.nabble.com/strict-to8243464.html>
>    concerning strict.
>
>    Here is my question:
>
>    reserve x for set;
>    reserve t for Subset-Family of x;
>    reserve o for 1-sorted;
>    reserve s for TopStruct;
>
>    s = TopStruct(# x, t #) & o = 1-sorted(# x #) implies
>        the 1-sorted of s = o;                          :: I understand
>
>    s is TopStruct & o is strict 1-sorted implies
>        s <> o;
>             *4
>
>    :: If o is strict, it lacks the 'topology' selector. How to
>    :: test that? maybe:
>
>    s = TopStruct(# x, t #) & o = 1-sorted(# x #) implies
>        s <> o;
>             *4                                         :: now what?
>
>    TopStruct(# x, t #) <> 1-sorted(# x #);
>                                         *4             :: confused
>
>    Also, what is 'forgetful' about the 'forgetful constructor' ?
>
>    Thanks for any insight.
>
>    -Greg Frascadore
>
>
> -- 
> View this message in context: http://www.nabble.com/Proving-inequality-of-structs---tp21459576p21459576.html
> Sent from the Mizar mailing list archive at Nabble.com.
>
>