Definitional Expansions

Definitional Expansions - Predicates

definition
  let X, Y be set;
  pred X c= Y means phi_1[X,Y];
end;

X c= Y
proof
  thus phi_1[X,Y];
end;

definition
  let X, Y be set;
  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;
  connectedness;
end;

X c= Y
proof
  per cases;
  case C1[X,Y];
  thus phi_1[X,Y];
  case C2[X,Y];
  thus phi_2[X,Y];
  case C3[X,Y];
  thus phi_3[X,Y];
  case not C1[X,Y] & not C2[X,Y] & not C3[X,Y];
  thus phi_4[X,Y];
end;

definition
  let X, Y be set;
  assume alpha[X,Y];
  pred X c= Y means phi_1[X,Y];
end;

X c= Y
proof
  thus alpha[X,Y];
  thus phi_1[X,Y];
end;

definition
  let X, Y be set;
  assume alpha[X,Y];
  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;
end;

X c= Y
proof
  thus alpha[X,Y];
  per cases;
  case C1[X,Y];
  thus phi_1[X,Y];
  case C2[X,Y];
  thus phi_2[X,Y];
  case C3[X,Y];
  thus phi_3[X,Y];
  case not C1[X,Y] & not C2[X,Y] & not C3[X,Y];
  thus phi_4[X,Y];
end;

Definitional Expansions - Modes

definition
  let X be set;
  mode Subset of X -> set means phi_1[it,X];
  existence;
end;

Y is Subset of X
proof
  thus phi_1[Y,X];
end;

definition
  let X be set;
  mode Subset of X -> set 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];
  existence;
  consistency;
end;

Y is Subset of X
proof
  per cases;
  case G1[X];
  thus phi_1[Y,X];
  case G2[X];
  thus phi_2[Y,X];
  case G3[X];
  thus phi_3[Y,X];
  case not G1[X] & not G2[X] & not G3[X];
  thus phi_4[Y,X];
end;

definition
  let X be set;
  assume beta[X];
  mode Subset of X -> set means phi_1[it,X];
  existence;
end;

Y is Subset of X
proof
  thus beta[X];
  thus phi_1[Y,X];
end;

definition
  let X be set;
  assume beta[X];
  mode Subset of X -> set 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];
  existence;
  consistency;
end;

Y is Subset of X
proof
  thus beta[X];
  per cases;
  case G1[X];
  thus phi_1[Y,X];
  case G2[X];
  thus phi_2[Y,X];
  case G3[X];
  thus phi_3[Y,X];
  case not G1[X] & not G2[X] & not G3[X];
  thus phi_4[Y,X];
end;

Definitional Expansions - Attributes

definition
  let X be set;
  attr X is empty means phi_1[X];
end;

X is empty
proof
  thus phi_1[X];
end;

definition
  let X be set;
  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];
  consistency;
end;

X is empty
proof
  per cases;
  case C1[X];
  thus phi_1[X];
  case C2[X];
  thus phi_2[X];
  case C3[X];
  thus phi_3[X];
  case not C1[X] & not C2[X] & not C3[X];
  thus phi_4[X];
end;

definition
  let X be set;
  assume beta[X];
  attr X is empty means phi_1[X];
end;

X is empty
proof
  thus beta[X];
  thus phi_1[X];
end;

definition
  let X be set;
  assume beta[X];
  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];
  consistency;
end;

X is empty
proof
  thus beta[X];
  per cases;
  case C1[X];
  thus phi_1[X];
  case C2[X];
  thus phi_2[X];
  case C3[X];
  thus phi_3[X];
  case not C1[X] & not C2[X] & not C3[X];
  thus phi_4[X];
end;