[mizar] Structures and strictness

[Gilbert Lee <gilbert@cs.ualberta.ca>]

Hi

I am having a number of problems with Mizar structures and "strictness"
and would like some opinons about possible work-arounds.

I've created a hierarchy of structures based on the MultiGraphStruct
(defined in GRAPH_1) by the addition of 3 selectors: Weight, ELabel, and
VLabel, which represent weights on an edge, edge labels, and vertex
labels.  For purposes of generality, the sets from which weights and
labels come from are given as parameters to the structure:

========================================================================
definition let WL be set;
  struct (MultiGraphStruct) WGraphStruct over WL
   (# Vertices, Edges -> set,
      Source, Target -> Function of the Edges, the Vertices,
      Weight -> Function of the Edges, WL #);
 end;

definition let EL be set;
 struct (MultiGraphStruct) EGraphStruct over EL
  (# Vertices, Edges -> set,
     Source, Target -> Function of the Edges, the Vertices,
     ELabel -> PartFunc of the Edges, EL #);
end;

definition let VL be set;
  struct (MultiGraphStruct) VGraphStruct over VL
  (# Vertices, Edges -> set,
     Source, Target -> Function of the Edges, the Vertices,
     VLabel -> PartFunc of the Vertices, VL #);
end;
========================================================================

Inheritance is as follows:

        WGraph over WL - WEGraph over WL,EL
      /                X                    \
Graph - EGraph over EL   WVGraph over WL,VL - WEVGraph over WL,EL,VL
      \                X                    /
        VGraph over VL - EVGraph over EL,VL

An example of a function I would like to define assigns a label to a
particular vertex in a VGraph.

for example:
definition let VL be set, G be VGraph of VL, v, val be set;
  func G.labelVertex(v, val) -> strict VGraph of VL means
   the MultiGraphStruct of it = the MultiGraphStruct of G &
   the VLabel of it = (the VLabel of G) +* (v .--> val) if
   (v in the Vertices of G & val in VL) otherwise
   the VGraphStruct of it = the VGraphStruct of G;

As far as I know, in order to prove uniqueness, the return type for this
kind of function must be a strict VGraph of VL. However, this means that
I will need three more nearly identical functions to deal with WVGraphs,
EVGraphs, and WEVGraphs.  Three is still manageable, however this becomes
a larger problem as more selectors are introduced.

What are current methods are there to work around this problem?  I have 
played with not using structures, and emulating selectors using 
attributes, which seems to work well.

Thanks and have a Happy New Year

Gilbert Lee