(*
$Id$
 part of:
ISO TC184/SC4/WG12 N3213 - ISO/IS 10303-54 Classification and set theory - EXPRESS
Supersedes ISO TC184/SC4/WG12 N1510
*) 


SCHEMA set_theory_schema;

REFERENCE FROM classification_schema   -- ISO 10303-54
  (class); 

REFERENCE FROM support_resource_schema   -- ISO 10303-41
  (identifier,
   label,
   text); 


ENTITY complement;
  id : identifier;
  name : label;
  description : OPTIONAL text;
  set_1 : class;
  set_2 : class;
  universe : class;
WHERE
  complement_different: NOT identical_sets(set_1, set_2);
END_ENTITY;

ENTITY intersection;
  id : identifier;
  name : label;
  description : OPTIONAL text;
  operand : SET[2:?] OF class;
  resultant : class;
END_ENTITY;

ENTITY power_set;
  id : identifier;
  name : label;
  description : OPTIONAL text;
  base : class;
  derived : class;
WHERE
  derived_different: NOT identical_sets(base, derived);
END_ENTITY;

ENTITY proper_subset
  SUBTYPE OF (subset);
WHERE
  subset_different: NOT identical_sets(superset, subset);
END_ENTITY;

ENTITY same_membership;
  id : identifier;
  name : label;
  description : OPTIONAL text;
  set_1 : class;
  set_2 : class;
END_ENTITY;

ENTITY subset;
  id : identifier;
  name : label;
  description : OPTIONAL text;
  subset : class;
  superset : class;
END_ENTITY;

ENTITY union;
  id : identifier;
  name : label;
  description : OPTIONAL text;
  operand : SET[2:?] OF class;
  resultant : class;
END_ENTITY;

ENTITY union_of_all_members;
  id : identifier;
  name : label;
  description : OPTIONAL text;
  operand : class;
  resultant : class;
WHERE
  resultant_different: NOT identical_sets(operand, resultant);
END_ENTITY;

FUNCTION identical_sets
 (set_a : class; set_b : class) : BOOLEAN; 
  LOCAL
    set_of_sets : SET OF class := [];
  END_LOCAL;
  
  IF (set_a = set_b) THEN
    RETURN (TRUE);
  END_IF;
  
  set_of_sets := set_of_sets + set_b;
  RETURN (identical_to_one_of_set_of_sets(set_a, set_of_sets));
      END_FUNCTION; 

FUNCTION identical_to_one_of_set_of_sets
 (set_a : class; set_of_sets : SET OF class) : BOOLEAN; 
  LOCAL
    i                            : INTEGER;
    initial_size                 : INTEGER;
    augmented_size               : INTEGER;
    set_of_forward_equivalences  : SET OF same_membership := [];
    set_of_backward_equivalences : SET OF same_membership := [];
    augmented_set_of_sets        : SET OF class := [];
  END_LOCAL;
  
  --  test membership of the specified set of sets
  
  IF (set_a IN set_of_sets) THEN
    RETURN (TRUE);
  END_IF;
  
  --  extend the specified set to include all sets that have the same membership
  --  as an existing member
  
  initial_size := SIZEOF(set_of_sets);
  IF (initial_size = 0) THEN
    RETURN (FALSE);
  END_IF;
  REPEAT i := 1 TO initial_size;
    set_of_forward_equivalences := set_of_forward_equivalences +
      USEDIN(set_of_sets[i], 'SET_THEORY_SCHEMA.SAME_MEMBERSHIP.SET_1');
    set_of_backward_equivalences := set_of_forward_equivalences +
      USEDIN(set_of_sets[i], 'SET_THEORY_SCHEMA.SAME_MEMBERSHIP.SET_2');
  END_REPEAT;
  
  augmented_set_of_sets := set_of_sets;
  IF (SIZEOF(set_of_forward_equivalences) > 0) THEN
    REPEAT i := 1 to HIINDEX(set_of_forward_equivalences);
      augmented_set_of_sets := augmented_set_of_sets +
        set_of_forward_equivalences[i].set_2;
    END_REPEAT;
  END_IF;
  IF (SIZEOF(set_of_backward_equivalences) > 0) THEN
    REPEAT i := 1 to HIINDEX(set_of_backward_equivalences);
      augmented_set_of_sets := augmented_set_of_sets +
        set_of_backward_equivalences[i].set_1;
    END_REPEAT;
  END_IF;
  
  -- if the specified set of sets has been augmented, then test membership
  
  augmented_size := SIZEOF(augmented_set_of_sets);
  IF augmented_size = initial_size THEN
    RETURN (FALSE);
  END_IF;
  
  RETURN (identical_to_one_of_set_of_sets(set_a, augmented_set_of_sets));
      END_FUNCTION; 

END_SCHEMA;  -- set_theory_schema
