Email Gateway (Jan 16 2024 at 13:50): Email Gateway (Jan 16 2024 at 13:50):From: Gunnar Teege <gunnar.teege@unibw.de>
Dear Makarius,
thanks for the clarification, that was helpful, in particular the hint
to the subgoal command. I was not aware, that it can be used to do what
I was looking for: consume an assumption which is already in the goal
state, by extracting all assumptions and inputting them to the cases method.
I had already tried the goal_cases method, but that adds all assumptions
present in the split goals to the cases, not only those stemming from
the elimination rule (i.e., not only the hyps but also the prems, using
the names given by the induct method). Moreover, I did not succeed to
apply it specifically to the goals created by applying the elimination rule:
In the form
apply(erule r) apply(goal_cases)
it creates (of course) cases for all existing goals.
In the form
apply(erule r; goal_cases)
it seems to create a case only for the first goal, even if application
of r creates more than one goal (?)
Regards
Gunnar Teege
Last updated: Apr 29 2024 at 04:18 UTC