Stream: Beginner Questions

Topic: Understanding a particular instance of the induction method

Alexander Pach (May 25 2025 at 16:14):

I've stumbled across a use of an induction rule I don't quite understand and got stuck there. The Original is found in $AFP/thy/Goodstein_Lambda/Goodstein_Lambda.thy@554

It is an Instance of less_Suc_induct:

less_Suc_induct [consumes 1]:
  assumes less: "i < j"
    and step: "⋀i. P i (Suc i)"
    and trans: "⋀i j k. i < j ⟹ j < k ⟹ P i j ⟹ P j k ⟹ P i k"
  shows "P i j"

and takes the form (plus auxiliary facts with free variables n, m, which I've dropped for simplicity)

const evalC :: "nat => 'a => nat"

show "evalC (Suc b) n < evalC (Suc b) m" using ‹evalC b n < evalC b m›
proof (induct "evalC b n" "evalC b m" arbitrary: n m rule: less_Suc_induct)

and returns the goal state

 1. ⋀n m. Suc (evalC b n) = evalC b m ⟹
           evalC (Suc b) n < evalC (Suc b) m
 2. ⋀j n m.
       ⟦evalC b n < j; j < evalC b m;
        ⋀na m. ⟦evalC b n = evalC b na; j = evalC b m⟧ ⟹ evalC (Suc b) na < evalC (Suc b) m ;
        ⋀n ma. ⟦j = evalC b n; evalC b m = evalC b ma⟧ ⟹ evalC (Suc b) n < evalC (Suc b) ma⟧
       ⟹ evalC (Suc b) n < evalC (Suc b) m

Naively, i and j in the induction rule would be "evalC b n" and "evalC b m" respectively, but how would write down P then, since i'd have to deconstruct a function application?
(Sidenote: in fact, the rule doesn't add any premises, if "evalC b n" and "evalC b m" are not explicitly given)

My best guess is that isabelle interprets this a kind of measure function we are inducting along, but what is actually happening here?

Last updated: May 31 2025 at 04:25 UTC