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



Hi Daniel,

On 05/06/15 07:23, Daniel Matichuk wrote:
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.
I see. My naive intuition was that new subgoals are those that are there but were not there before (and their relative order must be the same), but that is probably a bit too vague.

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.
The all combinator is nice, thanks. Still, I am not really comfortable with it. I am used to auto and safe working on all goals. Now, if read something like

apply(auto intro: ... simp add: ... simp del: ...; blast elim: ...)

I am still tempted to think that it works on all subgoals, because the restriction operator ";" is well hidden between two method invocations (and visually not so much different from ",", which does not restrict auto). The restriction operator [3] added after the closing parenthesis is much easier to spot.

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)".
You are right, although I in fact have a few instances of "...; simp_all" in my code. This stems from transforming something like

  apply(rule ...)
  apply simp_all

into

  apply(rule ...; simp_all)

I still have to get my head around to then change simp_all into simp.

Best,
Andreas




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