Email Gateway (Aug 22 2022 at 15:52): Email Gateway (Aug 22 2022 at 15:52):From: "Jähnig, Nils Erik" <nils.jaehnig@tu-berlin.de>
Dear Isabelle Users,
is there something like clarsimp_all, when auto is too much, but I still want to simplify all subgoals?
And is there a nice way to implement "explode_conj", i.e. make a subgoal for each conjunct in the conclusion.
Related: Is there a way to achieve this in Eisbach? From what I've read, I think it is not.
In general I would be interested, if multiple subgoals can be addressed.
Have a nice weekend
Nils
Email Gateway (Aug 22 2022 at 15:52):From: Simon Wimmer <wimmersimon@gmail.com>
Hi Nils,
there is a method 'clarsimp_all'.
Maybe
apply (intro conjI)
achieves what you want from explode_conj?
Cheers,
Simon
Email Gateway (Aug 22 2022 at 15:52):From: Peter Lammich <lammich@in.tum.de>
I have a clarsimp_all in my refinement framework, just import
$AFP/Automatic_Refinement/Lib/Refine_Lib
apply (intro conjI) explodes all conjunctions
I heard the nicta guys had a allgoals eisbach combinator, but I never used it
Peter
Email Gateway (Aug 22 2022 at 15:53):From: Peter Lammich <lammich@in.tum.de>
Sorry, the theory name for clarsimp_all is Refine_Util
Email Gateway (Aug 22 2022 at 15:54):From: "Jähnig, Nils Erik" <nils.jaehnig@tu-berlin.de>
Thank you!
explode conj: apply(intro conjI)
and clarsimp_all from $AFP/Automatic_Refinement/Lib/Refine_Util
are what I was looking for.
Nils
Last updated: Apr 18 2024 at 20:16 UTC