LP, the Larch Prover -- Proofs of induction rules

LP permits users to prove induction rules as well as assert them. To prove a structural induction rule such as

sort Set generated by {}, {__}, \U

LP creates a single subgoal that involves proving the formula isGenerated(x) using the hypotheses

isGenerated({})
isGenerated({e})
isGenerated(s1) /\ isGenerated(s2) => isGenerated(s1 /\ s2)

where isGenerated is a new operator with signature Set->Bool. The names of the hypotheses have the form <simpleId>GenHyp.<number>, where <simpleId> is the current value of the name-prefix setting. User guidance is generally required to finish the proof, for example, by using the induction rule sort Set generated by {}, insert.

To prove a structural induction rule such as

sort Nat generated freely by 0:->Nat, f:Nat->Nat, g:Nat->Nat

LP also attempts to prove the subgoals

f(n) ~= 0          f(n) = f(n1) <=> n = n1          f(n) ~= g(n1)
g(n) ~= 0          g(n) = g(n1) <=> n = n1

in addition to the subgoal isGenerated(n).

To prove a well-founded induction rule such as well founded <, LP creates a single subgoal that involves proving the formula isGenerated(x) using the hypothesis

\A n1 (n1 < n => isGenerated(n1)) => isGenerated(n)