I have a proof by structural induction where several (28 of 29) cases can be proved directly with a terminal backward proof:
by cases auto (* which is just syntactic sugar for: proof cases qed auto *)
Now I'd like to omit these cases and just use a single method after the top level
qed. Is there a way to translate this simple terminal proof into a single method that does all the goal refinement normally done by
by and which can be used directly with
proof(induction _) qed (cases; auto)
does not work?
No, unfortunately not.
Ah, of course that does not work. What about
proof(induction _; cases) qed auto
proof(induction _) qed ((cases; auto)+)
I was able to change the setup of a few elimination rules in the meantime and now at least some of the subgoals can be proven with
auto. Yet, there are still some which require
cases auto and together with these your other suggestions also don't work.
While it would be very helpful to see the lemma you are trying to prove, I could suggest trying
proof(induction _; cases) qed (auto | assumption)+
by makes implicit calls to
assumption after applying the proof method
Well, nevermind what I wrote above.. assumption are of course being resolved in the simplification process of auto.. my bad!
Thanks for the input. Unfortunately, by putting
induction, Isabelle only splits the value of some undefined predicate instead of splitting the correct data.
The formalization I'm working on is a bit too involved to post in one piece and not yet published to a public repository, but it's a rather direct port of the Iris framework's HeapLang formalization and the corresponding Coq lemma can be found here.
I just published the first draft of the port and the corresponding lemma can now be found here.
Last updated: Aug 15 2022 at 02:13 UTC