Stream: Beginner Questions

Topic: How can I invoke Sledgehammer to finish an induction proof?

Adam Dingle (Mar 21 2026 at 11:59):

As an exercise, I defined my own version of the natural numbers, along with a recursive addition function:

datatype nat = One | S nat

fun add :: "nat ⇒ nat ⇒ nat" (infixl ‹'_+› 65) where
  "add x One = S x" |
  "add x (S y) = S (x _+ y)"

Now I want to prove that x + 1 = 1 + x for all x. This should not be difficult to show by induction on x, so I'd like to specify that induction, then let Sledgehammer finish the details. I tried typing

lemma "x _+ One = One _+ x"
proof (induction x)

But if I put my cursor after that point and press Sledgehammer's Apply button, I see

Illegal application of proof command in "state" mode

As another attempt, I typed

lemma "x _+ One = One _+ x"
by (induction x)

If I put my cursor after that and try to apply Sledgehammer, I see

Unknown proof context

What am I doing wrong?

Last updated: Mar 25 2026 at 02:29 UTC