CADiZ

Reference manual / Z-related commands / Proof rule commands / properties


The properties command is applicable to a name in a goal, where the name refers to a top-level declaration in the specification about which the specification provides some constraints (excepting names declared in the specification using the == notation, and also the names of schema paragraphs, for which use the expansion command). It makes the specification's constraints on that name available as antecedents in the sub-goal. Constraints that are newline-separated in the specification become comma-separated in the sub-goal. If the name is declared generically, the new antecedents are the specification's constraints instantiated according to the instantiation of the name in the goal.

In the case of a name that is declared in an axiomatic paragraph, properties makes available the constraint implicit in the declaration, along with the explicit constraints from the axiomatic paragraph.


i : e
\where
ps

| i \in e, ps \vdash?
\vdash?

Global constraints on the name can be made available using the separate constraint command.

In the case of a name that is declared in a free type paragraph (as the name of either a free type, an element, or an injection), properties makes available the constraints from the paragraphs that the Z standard defines the free type paragraph as abbreviating.

f1 ::= h1,1 ... h1,m1 | g1,1 \ldata e1,1 \rdata ... g1,n \ldata e1,n \rdata
& ... &
fr ::= hr,1 ... hr,mr | gr,1 \ldata er,1 \rdata ... gr,nr \ldata er,nr \rdata

-- membership
hi,j \in fi,
gi,k \in \power (ei,k \cross fi),
-- totality
\forall x : ei,k @ \exists1 y : gi,k @ y . 1 = x,
-- injectivity
\forall x, y : ei,k | gi,k x = gi,k y @ x = y,
-- disjointness
\forall b1, b2 : \nat @
    \forall e : fi |
    (b1 = 1 \land e = hi,1 \lor ... \lor b1 = mi \land e = hi,mi \lor
    b1 = mi+1 \land e \in {i : gi,1 @ i . 2} \lor ... \lor b1 = mi+ni \land e \in {i : gi,ni @ i . 2}) \land
    (b2 = 1 \land e = hi,1 \lor ... \lor b2 = mi \land e = hi,mi \lor
    b2 = mi+1 \land e \in {i : gi,1 @ i . 2} \lor ... \lor b2 = mi+ni \land e \in {i : gi,ni @ i . 2}) @
    b1 = b2
-- induction
\forall f1' : \power f1; ...; fr' : \power fr |
    h1,1 \in f1' \land ... \land h1,m1 \in f1' \land
    ... \land
    hr,1 \in fr' \land ... \land hr,mr \in fr' \land
    (\forall y1,1 : \mu f1 == f1'; ...; fr == fr' @ e1,1 @ g1,1 y{1,1} \in f1') \land
    ... \land
    (\forall y1,n1 : \mu f1 == f1'; ...; fr == fr' @ e1,n1 @ g1,n1 y1,n1 \in f1') \land
    ... \land
    (\forall yr,1 : \mu f1 == f1'; ...; fr == fr' @ er,1 @ gr,1 yr,1 \in fr') \land
    ... \land
    (\forall yr,nr : \mu f1 == f1'; ...; fr == fr' @ er,nr @ gr,nr y{r,nr} \in fr') @
    f1' = f1 \land ... \land fr' = fr
\vdash?

Tactic example

"properties" e1 e2

This example applies the properties command to expressions e1 and e2.


IT 27-Sep-1999