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: Dec 07 2024 at 16:22 UTC