Email Gateway (Aug 18 2022 at 19:31): Email Gateway (Aug 18 2022 at 19:31):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hello,
when I use apply(insert thm), thm gets inserted into all subgoals.
cluttering up premises is usually unwanted.
now i use subgoal_tac and prove the resulting new subgoal to achieve
getting a thm inserted in just one subgoal, but maybe there is an easier
way, something like insert1?
what is the reason for insert inserting into all subgoals?
Best Regards
Nils
Email Gateway (Aug 18 2022 at 19:32):From: Peter Lammich <lammich@in.tum.de>
Hi,
try "apply (insert xxx) []".
The []-Syntax restricts the effect of any apply-command to the first
subgoal. There is also [n] to restrict the effect to the first n
subgoals.
No idea what the reason is why some commands (auto, insert, etc) work on
all goals, while others (blast, force, etc. ) do not.
Best
Peter
Email Gateway (Aug 18 2022 at 19:32):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
wow, this is uber-useful. especially apply auto []
thank you, Peter.
this is not in the tutorial, isn't it? i think it should.
(i found only the direct subgoal addressing with [n] of *_tac)
Email Gateway (Aug 18 2022 at 19:32):From: Makarius <makarius@sketis.net>
The reason is to make things work most of the time, without the explicit
goal addressing of the pre-Isar tactical proof style.
This question shows up only every 5 years or so, which means Isar was
successful here.
Makarius
Email Gateway (Aug 18 2022 at 19:32):From: Makarius <makarius@sketis.net>
Better see the isar-ref manual for all the details. If something is wrong
or outdated there, do say so.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC