Re: [isabelle] Method combinator ; restricts to first subgoal
On 05/06/15 07:23, Daniel Matichuk wrote:
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
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.
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
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 =>
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)
assumes B: B
"A â (A â B)" "A â (A â B)" "A â (A â B)"
by (all âsafe; rule Bâ)
In this example, "safe" is executed in isolation against each subgoal, and "rule B" applied to each emerging one.
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  added
after the closing parenthesis is much easier to spot.
You are right, although I in fact have a few instances of "...; simp_all" in my code. This
stems from transforming something like
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)".
apply(rule ...; simp_all)
I still have to get my head around to then change simp_all into simp.
This archive was generated by a fusion of
Pipermail (Mailman edition) and