Matthew Torrence (Dec 29 2021 at 19:53): 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: Dec 21 2024 at 12:33 UTC