Email Gateway (Aug 22 2022 at 14:12): Email Gateway (Aug 22 2022 at 14:12):From: Peter Lammich <lammich@in.tum.de>
Hi,
for exactly this usecase (induction proofs), I use a custom method
rprems:
apply rprems
also does what you want, without the subgoal overhead. It resolves the
conclusion with the first premise, even if this premise is of form
"!!_.[|_|] ==> _".
It's currently in $AFP/Automatic_Refinement/Lib/Refine_Util, but if
more people find this useful, maybe one could move it to Isabelle?
Email Gateway (Aug 22 2022 at 14:13):From: Makarius <makarius@sketis.net>
I just want to point out that the 'subgoal' command has no overhead: on
the contrary, it allows to check proofs compositionally and thus in
parallel. The explicit proof structure is also an advantage for
maintainability.
In some situations, 'subgoal' cannot be used, though. One example are
schematic goal states. Then one really needs to go back to old-style
tactical means.
Makarius
Email Gateway (Aug 22 2022 at 14:14):From: Peter Lammich <lammich@in.tum.de>
I just want to point out that the 'subgoal' command has no overhead:
Sorry, I meant textual overhead (boilerplate), not computational
overhead.
Email Gateway (Aug 22 2022 at 14:20):From: Edward Pierzchalski <e.a.pierzchalski@gmail.com>
Hi all,
Say my current goal looks like:
A v ==>
(!! x. B x ==> C x) ==>
C v
Here, I have an assumption that I could easily use as an introduction rule
for my conclusion, resulting in the new goal
A v ==>
B v ==>
C v
If I were in Isar mode, the rule-shaped assumption would have a name that I
could apply using the rule tactic. Is there an easy way to do this in apply
mode? At the moment I'm repeatedly using meta_allE (my case has a few more
bound variables), but this seems dirty.
Regards,
--Ed
Email Gateway (Aug 22 2022 at 14:21):From: Simon Wimmer <wimmersimon@gmail.com>
Hi Ed,
I'm not sure if you really want the rule to appear in your goal anyways.
However, you could use something like
subgoal premises prems
apply (rule prems(2))
to apply the rule in apply-style.
Simon
Email Gateway (Aug 22 2022 at 14:23):From: Edward Pierzchalski <e.a.pierzchalski@gmail.com>
Thanks for the tip, Simon! That worked quite nicely.
The reason I have intro-like rules is because I'm inside some simple
induction proofs in apply mode, where the overhead from doing it "properly"
in Isar just isn't worth it.
Last updated: Apr 26 2024 at 12:28 UTC