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.