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



> On 5 Jun 2015, at 4:47 pm, Andreas Lochbihler <andreas.lochbihler at 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

________________________________

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.