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



Hi Andreas,
It's not really defined what it means for a subgoal to "arise" out of a method which applies to all subgoals.
In the general case a method can perform arbitrary modifications to the collection of subgoals
(including changing the number), and so the "new" subgoals would need to be all of them.

In the restricted case, it is clear which subgoals are new because it is exactly those which are on
top of the subgoal stack.

One possible solution to your problem is to expose "ALLGOALS" as a method combinator. This can be done relatively easily with some
simple Eisbach-provided functionality (I didn't get around to including this in the release):

~~~
method_setup all =
  âMethod_Closure.parse_method >> (fn m => fn ctxt => fn facts =>
    let
      fun tac i st' =
        Goal.restrict i 1 st'
        |> Method_Closure.method_evaluate m ctxt facts
        |> Seq.map (Goal.unrestrict i o snd)

    in EMPTY_CASES (ALLGOALS tac) end)
â


lemma
  assumes B: B
  shows
  "A â (A â B)" "A â (A â B)" "A â (A â B)"
  apply -
  by (all âsafe; rule Bâ)
~~~
In this example, "safe" is executed in isolation against each subgoal, and "rule B" applied to each emerging one.

Although this implementation throws away rule cases, you probably get the idea. You could also use PARALLEL_ALLGOALS if desired.

As a side note, something like "(x; simp_all)" never makes sense, the second argument is run against each resulting subgoal in isolation.
You almost certainly mean "(x; simp)".

-Dan



> On 4 Jun 2015, at 8:24 pm, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
>
> Dear all,
>
> 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?
>
> Cheers,
> Andreas
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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