# Re: [isabelle] intro rule for &&&

On Thu, 20 Dec 2012, Joachim Breitner wrote:

lemma assumes "A ∧ B" shows "A" "B"
using assms
apply rule

I was told, but don’t understand the reasons, that this works as an
intro rule for &&&:

`&&& is merely funny Pure notation to say that there are several
``simultaneous goals to be proven.
`

`The system needs to retain this structure for advanced methods like
``"induct", so it cannot be split into several goals by default. The
``splitting happends implicitly for any other proof method like "rule",
``which then acts on the first resulting subgoal only. There are other
``proof methods like "auto" that operate on all available subgoals, and
``consequently insert used facts into all of them at the start, so the above
``example will work here.
`

`You can see the difference again in "simp" vs. "simp_all", which is the
``same tool acting either on the head goal or all goals: "apply simp_all"
``will solve the above, but not "apply simp".
`
Further fine points:
assume "A & B"
then have A and B by (simp, simp) -- works
assume "A & B"
then have A and B by simp simp -- fails
assume "A & B"
then have A and B apply simp apply simp done -- fails
assume "A & B"
then have A and B
apply simp
using `A & B`
apply simp
done -- works

`The first one works, because the method expression with sequential
``composition "," uses the same facts each time: both simp steps will insert
``the given facts into the respective head subgoal before doing
``simplification.
`

`The second version puts one simp in the "initial" slot of 'by', and the
``other in the "terminal" slot. Only the initial method expressions sees
``the used facts, they are reset afterwards.
`

`The third version imitates the same operationally, using two separate
``'apply' steps. The 'apply' command essentially "consumes" the used facts,
``so the second simp won't see them and fail.
`

`The fourth version refreshes the consumed facts by explicit 'using' in the
``apply script, so it works again.
`

`This illustrates that "by method1 method2" is structurally different from
``"by (method1, method2). I always emphasize the importance to do canonical
``"by induct auto" or "by cases auto" steps that way, and not "optimize"
``special cases where old-fashioned sequential composition via "," happens
``to work. The latter is merely an odd imitation of tactical proof style in
``Isar, and should have disappeared already 10 years ago.
`
Makarius

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