LP, the Larch Prover -- Partitioned by

The partitioned-by construct provides a convenient syntax for expressing the fact that two objects of a given sort are the same if they cannot be distinguished by an operator in a given list. Operationally, a <partitioned-by> is equivalent to a deduction rule.

Syntax

<partitioned-by> ::= sort <sort> partitioned by <operator>+,

Restriction: Each of the <operator>s must have <sort> in its domain.

Examples

sort Set partitioned by \in
sort Stack partitioned by isEmpty, top, pop

Usage

Users can assert or prove a <partitioned-by>, which LP automatically translates into a deduction rule. For example, LP translates the examples into the deduction rules

when \A e (e \in s = e \in s1) yield s = s1
when isEmpty(s) = isEmpty(s1), top(s) = top(s1), pop(s) = pop(s1)
yield s = s1

In general, LP translates a statement like

sort E partitioned by op1:E->R, op2:E,A->R, op3:E,E,A->R

into to the deduction rule

when op1(e1) = op1(e2),
     \A a (op2(e1, a) = op2(e2, a)),
     \A a \A e3 (op3(e1, e3, a) = op3(e2, e3, a)),
     \A a \A e3 (op3(e3, e1, a) = op3(e3, e2, a))
yield e1 = e2

which uses auxiliary variables e1, e2, and e3 of sort E and a and a1 of sort A.