# Re: [isabelle] Method combinator ; restricts to first subgoal

On Thu, 4 Jun 2015, Andreas Lochbihler wrote:

`I am wondering why the new method combinator restricts the first method to
``the first subgoal. Is there any deeper reason for this design decision?
`
I regularly attempt myself to write things like the following
apply(safe; simp_all)
apply(simp_all; blast)
apply(auto; force intro: ...)
apply(case_tac [1-3] x; simp_all)

`and then wonder why they don't work as expected (throw the first method at
``all/the specified subgoals and then invoke the second method only on subgoals
``arising from the first method). What are the use cases for the restriction to
``the first subgoal? Or am I just using bad style?
`

`Dan has already explained most aspects of this. Just for completeness,
``here is the relevant snippet from the isar-ref manual:
`
Structural composition `` at {text m1} at {verbatim ";"}~ at {text m2}'' means
that method @{text m1} is applied with restriction to the first subgoal,
then @{text m2} is applied consecutively with restriction to each
subgoal that has newly emerged due to @{text m1}. This is analogous to
the tactic combinator @{ML_op THEN_ALL_NEW} in Isabelle/ML, see also
@{cite "isabelle-implementation"}. For example, @{text "(rule r;
blast)"} applies rule @{text "r"} and then solves all new subgoals by
@{text blast}.

`The citation of isabelle-implementation is pointless, though: the manual
``does not mention it in Isabelle2015. The THEN_ALL_NEW tactical was new in
``1998, and I just thought that it is universally known and properly
``documented. See also
``http://isabelle.in.tum.de/repos/isabelle/rev/0e034d76932e
`

`In that ML definition you also see that it is just a matter of working
``with subgoal indices, without ever looking at the actual goal state. The
``assumption is that tactics / proof methods work in the way that is
``specified in the Isabelle/Isar implementation manual, sections 4.2
``"Tactics" and 7.2 "Proof methods".
`

`The Isar method combinator does some more sandboxing of proof states, to
``enforce certain policies, which was observed here in the examples.
`
Makarius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*