Email Gateway (Aug 18 2022 at 09:47): Email Gateway (Aug 18 2022 at 09:47):From: Julien <julien@cs.uni-sb.de>
Hi All,
In isar proofs I am chaining facts with moreover like this
from hyp1 have foo1 .
moreover
from hyp2 have foo2 .
...
ultimately have main ...
Then, I have a goal and a bunch of facts in "using this".
For technical reasons I need to have the same behavior as if I would type:
main
apply (insert foo1)
apply (insert foo2)
...
That is, to move the facts from "using this" to the goal.
My current "trick" is to add "apply (simp)" or "apply clarsimp" after
"ultimately have main".
This puts the hypotheses within the goal (at least this is my
understanding). But, if there is nothing to simplify, the trick does not
work. I can use the "apply insert" within isar proofs, but it's not so
nice :-)
Does anyone have an idea how I can put the hypotheses within the goal
(another trick like "apply simp" that would work even if there is
nothing to simplify would work :-) ?
Thanks,
Julien
Email Gateway (Aug 18 2022 at 09:49):From: Norbert Schirmer <norbert.schirmer@web.de>
Hi Julien,
a neat way is the empty proof-method "-". It only has the effect of inserting
the chained facts to the goal:
...
ultimately have main
apply -
apply ...
Since the by command accepts an initial and an final method the following
pattern may also occur:
ultimately have main
by - (...)
Norbert
Email Gateway (Aug 18 2022 at 09:51):From: Makarius <makarius@sketis.net>
Just do ``apply -'' here.
Makarius
Last updated: May 03 2024 at 08:18 UTC