Stream: Beginner Questions

Topic: A style of stating a theorem

Gergely Buday (Jun 21 2023 at 10:32):

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?

Gergely Buday (Jun 21 2023 at 10:39):

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?

Jan van Brügge (Jun 21 2023 at 11:03):

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

Maximilian Schäffeler (Jun 21 2023 at 14:06):

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 21 2024 at 16:20 UTC