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  added after the closing parenthesis is much easier to spot.
I agree that it's a bit strange to suddenly have this implicit  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:
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.
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