Predicates

definition
  let X, Y be set;
  redefine pred X c= Y means phi_1[X,Y];
  compatibility
  proof
    thus X c= Y iff phi_1[X,Y];
  end;
end;

definition
  let X, Y be set;
  redefine pred X c= Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  compatibility
  proof
    thus C1[X,Y] implies (X c= Y iff phi_1[X,Y]);
    thus C2[X,Y] implies (X c= Y iff phi_2[X,Y]);
    thus C3[X,Y] implies (X c= Y iff phi_3[X,Y]);
    thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] implies
         (X c= Y iff phi_4[X,Y]);
  end;
end;

Modes

definition
  let X be set;
  redefine mode Subset of X -> new_type;
  coherence
  proof
    thus for A being Subset of X holds A is new_type;
  end;
end;

definition
  let X be set;
  redefine mode Subset of X means phi_1[it,X];
  compatibility
  proof
    let A be set;
    thus A is Subset of X iff phi_1[A,X];
  end;
end;

definition
  let X be set;
  redefine mode Subset of X means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  compatibility
  proof
    let A be set;
    thus G1[X] implies (A is Subset of X iff phi_1[A,X]);
    thus G2[X] implies (A is Subset of X iff phi_2[A,X]);
    thus G3[X] implies (A is Subset of X iff phi_3[A,X]);
    thus not G1[X] & not G2[X] & not G3[X] implies
         (A is Subset of X iff phi_4[A,X]);
  end;
  consistency;
end;

Functors

definition
  let X be set;
  redefine func +X -> new_type;
  coherence
  proof
    thus +X is new_type;
  end;
end;

definition
  let X be set;
  redefine func +X means phi_1[it,X];
  compatibility
  proof
    let A be set;
    thus A = +X iff phi_1[A,X];
  end;  
end;

definition
  let X be set;
  redefine func +X means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  consistency;
  compatibility
  proof
    let A be set;
    thus G1[X] implies (A = +X iff phi_1[A,X]);
    thus G2[X] implies (A = +X iff phi_2[A,X]);
    thus G3[X] implies (A = +X iff phi_3[A,X]);
    thus not G1[X] & not G2[X] & not G3[X] implies (A = +X iff phi_4[A,X]);
  end;
end;

definition
  let X be set;
  redefine func +X equals tau_1(X);
  compatibility
  proof
    let A be set;
    thus A = +X iff A = tau_1(X);
  end;  
end;

definition
  let X be set;
  redefine func +X equals
    tau_1(X) if G1[X],
    tau_2(X) if G2[X],
    tau_3(X) if G3[X]
    otherwise tau_4(X);
  consistency;
  compatibility
  proof
    let A be set;
    thus G1[X] implies (A = +X iff A = tau_1(A));
    thus G2[X] implies (A = +X iff A = tau_2(A));
    thus G3[X] implies (A = +X iff A = tau_3(A));
    thus not G1[X] & not G2[X] & not G3[X] implies (A = +X iff A = tau_4(A));
  end;
end;

Attributes

definition
  let X be set;
  redefine attr X is empty means phi_1[X];
  compatibility
  proof
    thus X is empty iff phi_1[X];
  end;
end;

definition
  let X be set;
  redefine attr X is empty means
    phi_1[X] if C1[X],
    phi_2[X] if C2[X],
    phi_3[X] if C3[X]
    otherwise phi_4[X];
  compatibility
  proof
    thus C1[X] implies (X is empty iff phi_1[X]);
    thus C2[X] implies (X is empty iff phi_2[X]);
    thus C3[X] implies (X is empty iff phi_3[X]);
    thus not C1[X] & not C2[X] & not C3[X] implies (X is empty iff phi_4[X]);
  end;
  consistency;
end;