Stream: General

Topic: Splitting cases in Universally quantified goals

Matthew Torrence (Dec 29 2021 at 19:53):

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?

Matthew Torrence (Dec 29 2021 at 19:54):

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

Mathias Fleury (Dec 31 2021 at 14:27):

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: Apr 25 2024 at 20:15 UTC