Reference manual / Z-related commands / In situ replacement commands / commutation

The commutation command swaps the operands of commutative operators. There are two categories of commutations: elementary ones that are built-in to cadiz, and ones that are coded explicitly as Z rewrite rules. An example of the latter is as follows.

union_commutation ==

[X] \vdash? \forall S, T : \power X @ S \cup T = T \cup S

The form of a rewrite rule must be as specified in rewrite by rule, and moreover its name must have commutation as a sub-string. The effect of a rewrite rule is also explained in rewrite by rule.

The built-in elementary commutations are as follows. They take precedence over any matching explicit rewrite rule.

e1 = e2   \trarrow   e2 = e1
p1 \land p2   \trarrow   p2 \land p1
e1 \land e2   \trarrow   e2 \land e1
p1 \lor p2   \trarrow   p2 \lor p1
e1 \lor e2   \trarrow   e2 \lor e1
p1 \iff p2   \trarrow   p2 \iff p1
e1 \iff e2   \trarrow   e2 \iff e1
p1 \xor p2   \trarrow   p2 \xor p1
e1 \xor e2   \trarrow   e2 \xor e1

Tactic example

"commutation" p3 p4

This example applies the commutation command to predicates p3 and p4.

IT 6-Jul-2000