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.