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

```On Thu, 20 Dec 2012, John Wickerson wrote:

```
```When I type...

```
```lemma assumes "A ∧ B" shows "A" "B"
using assms
apply rule
```
```
...I obtain the following proof state...

```
```goal (2 subgoals):
1. A ⟹ B ⟹ A
2. B
```
```
... which is insoluble. I think the "apply rule" step is using the conjE rule. Which rule should I apply in order to obtain the preferred proof state below? I briefly tried conjunctionI but that doesn't seem quite to fit.

```
```goal (2 subgoals):
1. A ⟹ B ⟹ A
2. A ⟹ B ⟹ B
```
```
```
By the way, I know I can solve this lemma via auto; my question is pedagogical rather than practical.
```
```
Automated tools are indeed obstructing the understanding how formal proof really works. Here is my version of the above example:
```
begin

assume ab: "A & B"
from ab have A and A
apply rule
apply assumption
using ab
apply rule
apply assumption
done

from ab obtain A and B ..

end

General notes on it:

* 'notepad' is better for experimentation than old-fashioned 'lemma',
because it gives you the full proof language.  In top-level theorem
statements your possibilities to indicate proof structure are more
limited and one has to simulate things, and obscure the main points
more than necessary.  There is also the initial goal hanging around,
but proof is not primarily about goals.

* The fact "ab" (or your assms) need to be eliminated twice to work on
the two goals "A" and "B".  The "rule" method implicitly refers to
conjE, but it works on the head goal only.  Note that in old-fashioned
tactical reasoning, you would simulate a local fact like "ab" via some
goal premise "A & B ==> ...", and "apply (erule conjE)" would consume
that, and the result would indeed become insoluble as you've said.
In proper Isar, the context grows monotonically, and things can be
used again as required.

* My second proof above via 'obtain' does the elimination of fact "ab"
in a single step, saying that it is possible to assume A and B
simultaneously thanks to the (implicit) conjE rule.  Recall that ".."
abbreviates "by rule" (actually "by default", which is a bit more).

Formally, there is only one goal behind 'obtain', so it works in a
single rule application step, not two.  It would be more awkward to
prove:

from ab have A and B sorry

which are two goals again.

Since the context of assumptions is commutative, you may swap the
obtain result in-place like this:

from ab obtain B and A ..

Putting it all together, here is my canonical starter proof for Isar:

assume "A & B"
then obtain B and A ..
then have "B & A" ..

You can also make implicit rules explicit like this:

assume "A & B"
then obtain B and A by (rule conjE)
then have "B & A" by (rule conjI)

```
Using the projections conjD1/conjD2 instead, it becomes a bit more awkward and artificial:
```
assume ab: "A & B"
from ab have a: A by (rule conjD1)
from ab have b: B by (rule conjD2)
from b and a have "B & A" by (rule conjI)

```
To be more fair, here is another variant that minimizes the spaghetti of fact references:
```
assume "A & B"
then have B ..
from `A & B` have A ..
with `B` have "B & A" ..

```
I usually prefer the first-class support of eliminations in Isar via 'obtain' to reduce the formal noise and expose the reasoning more directly.
```

Makarius```

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