{
* File: 00-oHome.sml.txt
* Author: Manfred Jeusfeld
* Created: 2023-03-01/M.Jeusfeld (2024-03-10/M.Jeusfeld)
* ------------------------------------------------------
* Some basic constructs for cardinalities, transitivity etc.
* Taken from the ConceptBase Forum
* The single constraint works on values here. 
* (C) Manfred Jeusfeld
*
}




Proposition with
  attribute
    single: Proposition;
    necessary: Proposition;
    revsingle: Proposition;
    revnecessary: Proposition
end

AdditionalConstraints in Class with
   constraint
      singleConstraintV :
          $ forall c,d/Proposition p/Proposition!single x,m/VAR
              P(p,c,m,d) and (x in c) ==>
                (forall y1,y2/VAR (x m y1) and (x m y2) ==> (y1=y2)) $;
      necConstraint:
          $ forall c,d/Proposition p/Proposition!necessary x,m/VAR
            P(p,c,m,d) and (x in c) ==>
             exists y/VAR (y in d) and (x m y) $;
      revsingleConstraint :
          $ forall c,d/Proposition p/Proposition!revsingle y,m/VAR
              P(p,c,m,d) and (y in d) ==>
                (
                  forall x1,x2/VAR
                    (x1 in c) and (x2 in c) and (x1 m y) and (x2 m y) ==>
                   (x1=x2)
                ) $;
      revnecConstraint:
          $ forall c,d/Proposition p/Proposition!necessary y,m/VAR
            P(p,c,m,d) and (y in d) ==>
             exists x/VAR (x in c) and (x m y) $
end


AdditionalConstraints!singleConstraintV with
 comment
   hint:
"The attribute/relation {m} of {c} is single-valued (right-unique). Any instance of {c} may have at most one attribute of category {m}!"
end


AdditionalConstraints!necConstraint with
 comment
   hint:
"The attribute/relation {m} of {c} is defined necessary (left-total). Any instance of {c} must have at least one instance of {d} for the attribute {m}!"
end

AdditionalConstraints!revsingleConstraint with
 comment
   hint:
"The attribute/relation {m} of {c} is reverse single-valued (left-unique). Any instance of {d} may have at most one instance of {c} connected to it via an attribute of category {m}!"
end

AdditionalConstraints!revnecConstraint with
 comment
   hint:
"The attribute/relation {m} of {c} is defined reverse necessary (right-total). Any instance of {d} must have at least one instance of {c} for the attribute {m}!"
end




Proposition with
  attribute
    injective: Proposition;   {* at most one filler for an attribute   *}
    surjective: Proposition;  {* all objects of the target class are also attribute values *}
    reflexive:  Proposition;  {* any object is related to itself       *}
    transitive: Proposition;  {* relation is closed under transitivity *}
    symmetric: Proposition;   {* if x rel y then also y rel x          *}
    antisymmetric: Proposition;     {* if x rel y and (y rel x) then x=y *}
    asymmetric: Proposition;        {* if x rel y then not (y rel x)     *}
    total: Proposition;             {* for all x,y: x rel y or y rel x   *}
    inv_injective: Proposition;     {* reverse relation is injective     *}
    makeTransitive: Proposition;    {* transitive by deduction           *}
    makeReflexive: Proposition;     {* reflexive by deduction            *}
    makeSymmetric: Proposition      {* symmetric by deduction            *}
end


RelationSemantics in Class with
  constraint
    inj_IC: $ forall AC/Proposition!injective a,b,x/Proposition
                 (a in AC) and (b in AC) and From(a,x) and From(b,x)  ==> (a = b) $;
    surj_IC: $ forall AC/Proposition!surjective C,D/Proposition M/VAR y/Proposition
                  P(AC,C,M,D) and (y in D) ==> exists a/Proposition (a in AC) and To(a,y) $;
    refl_IC: $ forall AC/Proposition!reflexive C,D/Proposition x,M/VAR
                        P(AC,C,M,D) and (x in C) ==> (x M x) $;
    trans_IC: $ forall AC/Proposition!transitive C/Proposition x,y,z/VAR M/VAR
                     P(AC,C,M,C) and (x in C) and (y in C) and (z in C) and
                     (x M y) and (y M z) ==> (x M z) $;
    symm_IC: $ forall AC/Proposition!symmetric C/Proposition x,y/VAR M/VAR
                     P(AC,C,M,C) and (x in C) and (y in C) and
                     (x M y)  ==> (y M x) $;
    asym_IC: $ forall AC/Proposition!asymmetric C/Proposition x,y/VAR M/VAR
                     P(AC,C,M,C) and (x in C) and (y in C) and
                     (x M y)  ==> not (y M x) $;
    antis_IC: $ forall AC/Proposition!antisymmetric C/Proposition x,y/VAR M/VAR
                     P(AC,C,M,C) and (x in C) and (y in C) and
                     (x M y) and (y M x)  ==> (x = y) $;
    total_IC: $ forall AC/Proposition!total C/Proposition x,y/VAR M/VAR
                     P(AC,C,M,C) and (x in C) and (y in C) ==>
                     ((x M y) or (y M x)) $;
    invinj_IC: $ forall AC/Proposition!inv_injective a,b,x/Proposition
                 (a in AC) and (b in AC) and To(a,x) and To(b,x)  ==> (a = b) $
end


{* some so-called hints for constraints. They are to be returned to the user when *}
{* an integrity violation occurs.                                                 *}

RelationSemantics!surj_IC with
 comment
   hint: "The relation {M} of {C} is surjective. Each instance of {D} must be the target of at least one attribute {M}."
end

RelationSemantics!refl_IC with
 comment
   hint: "The relation {M} of {C} is reflexive. Any object of class {C} must be linked to itself via the {M} relation."
end

RelationSemantics!trans_IC with
 comment
   hint: "The relation {M} of {C} is transitive. The facts (x {M} y) and (y {M} z) must imply that (x {M} z) holds."
end


RelationSemantics!symm_IC with
 comment
   hint: "The relation {M} of {C} must be symmetric, i.e. (x {M} y) implies (y {M} x)."
end



RelationSemantics in Class with
  rule
   trans_R: $ forall x,y,z,M/VAR 
                     AC/Proposition!makeTransitive C/Proposition
                     P(AC,C,M,C) and (x in C) and (y in C) and (z in C) and
                     (x M y) and (y M z) ==> (x M z) $;
   refl_R: $ forall x,M/VAR 
                    AC/Proposition!makeReflexive C/Proposition
                    P(AC,C,M,C) and (x in C)
                    ==> (x M x) $;
   symm_R: $ forall x,y,M/VAR 
                    AC/Proposition!makeSymmetric C/Proposition
                     P(AC,C,M,C) and (x in C) and (y in C) and
                     (x M y)  ==> (y M x) $
end

{---}


{* MultiDim in Module end *}