[isabelle] Method combinator ; restricts to first subgoal · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 10:13):

From: Makarius <makarius@sketis.net>
Dan has already explained most aspects of this. Just for completeness,
here is the relevant snippet from the isar-ref manual:

Structural composition ``@{text m1}@{verbatim ";"}~@{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

Email Gateway (Aug 22 2022 at 10:30):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 10:31):

From: Daniel Matichuk <daniel.matichuk@nicta.com.au>
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

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.

Email Gateway (Aug 22 2022 at 10:31):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 10:31):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
An aside on this thread: the ';' combinator provides a nice way for
transferring class instances to parametric types, e.g. in
~~/src/HOL/NSA/StarDef.thy

instance star :: (order) order
apply (intro_classes)
apply (transfer, rule less_le_not_le)
apply (transfer, rule order_refl)
apply (transfer, erule (1) order_trans)
apply (transfer, erule (1) order_antisym)
done

can now be simply written as

instance star :: (order) order
by (intro_classes; transfer) (fact less_le_not_le order_refl order_trans order_antisym)+

Cheers,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 10:33):

From: Daniel Matichuk <daniel.matichuk@nicta.com.au>

On 5 Jun 2015, at 4:47 pm, Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch> wrote:

Hi Daniel,

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 vague.

I had the same thought. The naive solution works in most cases but there are a fair number of edge cases where it breaks down or is unclear. For example, if m1 rotates all subgoals by 1,
does "m1;m2" apply m2 to all subgoals or none? I think without the ability to have a method officially declare what is a "new" subgoal, it will be difficult to address this generally.

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.

I agree that it's a bit strange to suddenly have this implicit [1] restriction. I think, however, that such an application of ";" is improper and should either result in an error or just be considered bad style (if auto is not explicitly restricted to the first subgoal).

I would argue that the introduction of the ";" combinator should result a shift away from using all-subgoal methods as anything but sole terminal methods. If, for example, you chained your long method expression
using ";" to the method which originally produced the subgoals then you would not need to rely on the fact that "auto" applies to all subgoals:
i.e
apply (cases ..; auto intro: .. simp add: ... ; blast elim: ...)

In this case the scope and intent of "auto ..." is much more clear, and avoids clobbering additional subgoals that sneak in during regular proof maintenance.

Regards,
Dan

Email Gateway (Aug 22 2022 at 10:33):

From: Daniel Matichuk <daniel.matichuk@nicta.com.au>

On 6 Jun 2015, at 3:52 am, Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de> wrote:

An aside on this thread: the ';' combinator provides a nice way for
transferring class instances to parametric types, e.g. in
~~/src/HOL/NSA/StarDef.thy

instance star :: (order) order
apply (intro_classes)
apply (transfer, rule less_le_not_le)
apply (transfer, rule order_refl)
apply (transfer, erule (1) order_trans)
apply (transfer, erule (1) order_antisym)
done

can now be simply written as

instance star :: (order) order
by (intro_classes; transfer) (fact less_le_not_le order_refl order_trans order_antisym)+

You could also write it as

(intro_classes; transfer; fact less_le_not_le order_refl order_trans order_antisym)

Which is not that useful here, but generally more appropriate in an apply-script (where "+" has a tendency to over-step).

Regards,
Dan

Last updated: Nov 21 2024 at 12:39 UTC