Induction on nonempty lists · Beginner Questions

In Isar, I'm trying to do induction over nonempty lists. I've made up a tiny example reflecting this problem: show that the sum of a nonempty list of positive integers is in fact positive. I'd like to do this without defining the sum of an empty list, because in my actual use-case, there's no reasonable way to define the function-value for an empty list.

theory Scratch
   imports Complex_Main
begin

fun listsum:: "(int list) ⇒ int" where
"listsum [] = undefined"
| "listsum [n] = n"
| "listsum (n # ns) = n + listsum ns"

fun good::"(int list) ⇒ bool" where
"good [] = undefined" |
"good [n] = (n > 0)" |
"good (n # ns) = ((n > 0) ∧ (good ns))"

lemma "good ns ⟹ listsum ns > 0"
proof (induction ns)
  case Nil
  then show ?case sorry
next
  case (Cons a ns)
  then show ?case sorry
qed

end

Isabelle offered up the usual induction proof-structure (case Nil and case (Cons a ns)) but that obviously isn't the way to go here, because the lemma's assertion isn't even true for the Nil case.

Programming and Proving doesn't seem to discuss this particular problem, so I'm at a bit of a loss.

Maximilian Schäffeler (Feb 05 2026 at 18:18):

You may want to try to add the assumption that ns is non-empty to the lemma and then try: proof (induction ns rule: list_nonempty_induct). You can find such specialized induction rules using e.g. find_theorems name: induct name: list.

John Hughes (Feb 05 2026 at 18:25):

Thanks; that does, indeed, seem to work. And thanks for the tip about finding specialized induction rules --- "where to look" and "how to look" are my biggest beginning-user problems at this point.

Maximilian Schäffeler (Feb 05 2026 at 18:28):

Joe Watt (Feb 06 2026 at 01:35):

I just want to point here that knowing that the assumption good ns in the Nil case, i.e. when ns = [] only lets us conclude that true = good [] = undefined which is unhelpful because we can't really say anything about undefined. This is why you need an extra nonempty assumption. I recall getting tripped up on undefined like so when I was newer to Isabelle.

Regarding search, I also recommend using the Find Facts search engine, as it lets you do a more fuzzy search (think google search) over everything in the core libraries and the AFP. On the other hand, find_theorems is much better for targeted searches where you already have a pattern in mind, but it only searches over those theories which you already imported (directly or transitively).

irvin (Feb 06 2026 at 06:27):

I would like to also note that in case your theorem state should seem to suggest that using functional induction via good.induct seems very natural to me.

John Hughes (Feb 06 2026 at 10:43):

Joe Watt: "I just want to point here that knowing that the assumption good ns in the Nil case, i.e. when ns = [] only lets us conclude that true = good [] = undefined which is unhelpful because we can't really say anything about undefined."

You're completely right... I was trying to write an example parallel to my actual proof, and screwed up -- I should have written good[] = False, which is what I did write in the actual proof.

John Hughes (Feb 06 2026 at 10:46):

Irvin: I don't know what 'functional induction' is, and a search in Programming and Proving doesn't yield anything. Can you perhaps show what a "functional induction" proof looks like in this simple case, after altering my definition of good to say good [] = False ?

Lukas Stevens (Feb 06 2026 at 10:48):

I don't know it as functional induction but as computation induction. Anyways, it is the induction scheme that corresponds to the recursion scheme of a recursively defined function. For a function f the computation induction scheme is called f.induct.

John Hughes (Feb 06 2026 at 10:51):

Lukas: As so often happens with Isabelle stuff, I feel as if I'm reading interesting things in a language that I don't actually know. I'll see whether a search on "computation induction" leads to any insight. I've tried typing thm good.induct and the resulting thing doesn't mean much to me; I'm a little surprised to not see good anywhere in the output, for instance. Perhaps when I'm a bit more awake it'll mean more. but thanks for the pointer.

Lukas Stevens (Feb 06 2026 at 10:57):

The function good does not appear in the output since the induction rule is just derived from the recursion scheme. The recursion scheme is independent of the function itself. For example, if I have two functions defined as f 0 = 0 | f n = Suc (f (n -1)) and g 0 = 0 | g n = Suc (g (n -1)) both of them have the same recursion scheme and you get the same induction rule. In fact, for this simple example the induction rule f.induct is equivalent to nat.induct.

Stream: Beginner Questions

Topic: Induction on nonempty lists

John Hughes (Feb 05 2026 at 18:09):