LP, the Larch Prover -- Induction rules

Syntax

<induction-rule> ::= sort <sort> generated [ freely ] by <operator>+,
                       | well founded <operator>

Examples

sort Nat generated freely by 0, s
sort Set generated by {}, insert
sort Set generated by {}, {__}, \U
well founded <

Usage

Assertions like sort Nat generated by 0, s specify sets of generators for use in proofs by structural induction. The listed operators (e.g, 0 and s) must have the named sort (e.g., Nat) as their range. If none of the domain sorts of an operator is the same as its range sort, the operator is a basis generator (e.g., 0); otherwise, it is an inductive generator (e.g, s). Structural induction rules are logically equivalent to infinite sets of first-order formulas of the form

P(0) /\ \A x (P(x) => P(s(x))) => \A x P(x)

The use of freely supplements a structural induction rule with a set of formulas asserting that the named operators are one-to-one and have disjoint ranges. For example, sort Nat generated freely by 0, s gives rise to the formulas s(x) = s(y) <=> x = y and 0 ~= s(x).

Assertions like well founded < specify a binary relation for use in proofs by well-founded induction. The listed operator must have a signature of the form S,S->Bool for some sort S. Well-founded induction rules are logically equivalent to infinite sets of first-order formulas of the form

\A x (\A y (y < x => P(y)) => P(x)) => \A x P(x)

To display the induction rules that LP currently has available for use, type display induction-rules (or disp i-r for short).