Let's say I define a datatype as follows:

```
datatype mydata = A | B
```

and I'm in an apply-style proof where my goal looks like

```
1. ⋀x :: mydata. P x ⟹ Q x
```

If I apply(induct_tac x) I get

```
proof (prove)
goal (2 subgoals):
1. ⋀x. P x ⟹ Q A
2. ⋀x. P x ⟹ Q B
```

and if I apply(rule mydata.induct) I get the same thing. Notice x isn't replaced in the hypothesis. Induct_tac even warns me about this:

```
Induction variable occurs also among premises: "x"⌂
```

The reason I'm using an apply style proof is because what I'm trying to do is automated in a method I'm writing Eisbach style. Is there no way to split into cases on the meta quantified variable, including in the hypotheses, or am I missing something?

Note that this might look a little familiar, since I had a similar question a while back with a more complicated induction, where the resolution was (somewhat frustratingly) just "don't use an apply style proof". Is that still the case here? Like I said, this is deep in an automated method I'm working on, and so it's not a matter of just breaking into an Isar style proof unfortunately

Can you do something like:

```
subgoal for x
apply (induct x rule: mydata.induct)
```

?

(I have never really investigated into what is possible in Eisbach...)

Last updated: Aug 15 2022 at 02:13 UTC