Email Gateway (Aug 22 2022 at 20:34): Email Gateway (Aug 22 2022 at 20:34):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I have a lemma that I prove using induction that results in a large number
of cases. A handful of these cases I need to solve explicitly (by this I
mean with their own case block) but the rest can be discharged in the final
qed line using a proof method ie
qed (metis blah)+
I have made a change that results in this qed line failing. I suspect that
this is because one or more of my cases now need to be proved explicitly or
the qed line needs modifying.
I could go through each of the cases, make a 'case' block for it, and see
if I can prove the case but I am looking for an easier method.
What I would like to do is, at the qed line, go into 'prove' mode so that I
can then experiment with apply style lines to see which one my cases
requires an explicit proof or what I would need to the qed line. I see that
at the qed line that I am in state mode and have a set of subgoals to
prove. Is there a simple command that puts me in 'prove' mode from here.
Nothing jumps out when scanning the Isar ref manual. With have/show I need
to specify a goal which isn't what I want.
Is something like this possible?
Cheers
Mark
Email Gateway (Aug 22 2022 at 20:34):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Mark,
You can use the command "apply_end" right before the "qed" line. apply_end works like
apply except that you can use it inside an Isar proof. Of course, this is mainly for
exploratory purposes; in the end, you want your Isar document to be free of apply_end.
Best,
Andreas
Last updated: Apr 24 2024 at 08:20 UTC