[isabelle] tactical combinators
I'm trying to write the (recursive) tactic described as below:
A - apply some elimination rule to the subgoal n producing 3 subgoals
(n, n+1, n+2), then :
1 - simultaneously apply some elimination rules to the 3
2 - apply the same tactic to the 3 subgoals (with different
parameters for each case).
My problem is that when applying the elimination rules in 1, this can
lead to 0 or more subgoals,
so I cannot apply the tactics in 2 to the subgoals (n, n+1, n+2).
My question is: Wich combinator should I use in step 1 and 2 in order to
apply (locally) these steps with rules (n, n+1, n+2) whatever the result
of applying the rule 1.
Thanks a lot,
This archive was generated by a fusion of
Pipermail (Mailman edition) and