Isabelle: Use of the "induct" or "induct_tac" methods

Question

Let's say I have a lemma about a simple inductively-defined set:

inductive_set foo :: "'a ⇒ 'a list set" for x :: 'a where
  "[] ∈ foo x" | "[x] ∈ foo x"

lemma "⋀x y. y ∈ foo x ⟹ qux x y ⟹ baz x y"

(It's important to me that the "⋀x y" bit stays, because the lemma is actually stating the state of my proof in the middle of a long apply chain.)

I'm having trouble starting the proof of this lemma. I would like to proceed by rule induction.

First attempt

I tried writing

apply (induct rule: foo.induct)

but that doesn't work: the induct method fails. I find I can get around this by fixing x and y explicitly, and then invoking the induct method, like so:

proof -
  fix x :: 'a
  fix y :: "'a list"
  assume "y ∈ foo x" and "qux x y"
  thus "baz x y"
  apply (induct rule: foo.induct)
oops

However, since I'm actually in the middle of an apply chain, I would rather not enter a structured proof block.

Second attempt

I tried using the induct_tac method instead, but unfortunately induct_tac does not apply the foo.induct rule in the way I would like. If I type

apply (induct_tac rule: foo.induct, assumption)

then the first subgoal is

⋀x y. y ∈ foo x ⟹ qux x y ⟹ baz x []

which is not what I want: I wanted qux x [] instead of qux x y. The induct method got this right, but had other problems, discussed above.

Answer 1

If you first transform your goal to look like this:

⋀x y. y ∈ foo x ⟹ qux x y ⟶ baz x []

then apply (induct_tac rule: foo.induct) will instantiate the induction rule in the way that you want. (It will also leave the object-level implications in the resulting goals, to which you will need to apply (rule impI).)

The induct method does these extra steps dealing with implications automatically, which is one of its major advantages.

On the other hand, induct_tac rule: foo.induct doesn't do anything more than apply (rule foo.induct). (In general, induct_tac can match the variables you specify, and automatically choose an induction rule based on their types, but you're not taking advantage of those features here.)

I think your best option is to go ahead and use a proof block at the end of your apply chain. If you are worried that all the fix, assume and show statements are too verbose, then you can use the little-advertised case goaln feature:

apply ...
apply ...
proof -
  case goal1 thus ?case
    apply induct
    ...
qed