LP, the Larch Prover -- Proofs by structural induction

A proof of a formula F by structural induction on a variable x of sort S is based on an induction rule that specifies a set G of generators for S, that is, a set of operators with range S. LP generates subgoals for the basis and induction steps in a proof by structural induction, as follows.


assert sort Nat generated by 0, s
prove 0 + x = x by induction
  Basis subgoal:        0 + 0 = 0
  New constant:         xc
  Induction hypothesis: 0 + xc = xc
  Induction subgoal:    0 + s(xc) = s(xc)
assert sort Set generated by {}, {__}, \U
prove x \subseteq x by induction
  Basis subgoals:       {} \subseteq {},    {e} \subseteq {e}
  New constants:        xc,                 xc1
  Induction hypotheses: xc \subseteq xc,    xc1 \subseteq xc1
  Induction subgoal:    (xc \U xc1) \subseteq (xc \U xc1)

See also