In an ancient theory I see

```
lemma MPair_parts:
"[| ⦃X,Y⦄ ∈ parts H;
[| X ∈ parts H; Y ∈ parts H |] ==> P |] ==> P"
```

a more direct version of it could be

```
⦃X,Y⦄ ∈ parts H ==> X ∈ parts H /\ Y ∈ parts H
```

but I guess the above style is useful for automation.

Is there a name for this style, and what should I know about it?

Another example is

```
lemma parts_emptyE [elim!]: "X∈ parts{} ==> P
```

which is stating the impossible, something is an element of an empty set, and from false implies anything. Again, why is this formulation?

Your first example is an elimination rule, to be used with the `erule`

tactic (or the `elim:`

attribute to auto) while your second is a destruct rule (for `drule`

or `dest:`

for auto). The elim rule is more convenient in this case because it can add the two new assumptions as two seperate ones, ie you can directly use one or the other. The destruct rule will give you a conjuction in your assumptions which you would then need to spit with either the destruct rules `conjunct1`

(or 2) or with the elim rule `conjE`

```
lemma MPair_parts':
assumes ‹⦃X,Y⦄ ∈ parts H›
obtains ‹X ∈ parts H› ‹Y ∈ parts H›
```

is equivalent, you may find it a bit easier to read.

Last updated: Jun 20 2024 at 08:21 UTC