CODEWITHSUNDEEP
isabelleset-comprehension
Alicia M.
Alicia M.

Reputation: 39

Complex set comprehension

I am running into an issue and I don't know if it's Isabelle way of managing set comprehension or I am having a really slow moment.

This lemma goes on just fine

lemma "{x | x. P x} ∩ {x | x y. (Q x y)} = {x | x y. (P x) ∧ (Q x y)}"
  by auto

And this one just doesn't

lemma "{x | x y. (P x y)} ∩ {x | x y z. (Q x y z)} = {x | x y z. (P x y) ∧ (Q x y z)}"

There must be a difference between the two and I don't see it. Obviously, I need the 2nd one, my (P x y) and (Q x y z) are quite complex and it will be hard for me to simplify it.

As usual, any help (or redirecting me into some healthier direction) is greatly appreciated.

Upvotes: 0

Views: 66

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8278

The left hand side {x | x y. P x y} ∩ {x | x y z. Q x y z} contains all x for which it holds that (∃y. P x y) ∧ (∃y z. Q x y z).

The right-hand side {x | x y z. P x y ∧ Q x y z} contains all x for which it holds that ∃y z. P x y ∧ Q x y z.

The difference is that the former restriction is weaker, since the y that makes P x y happen and the y that makes Q x y z happen do not have to be the same.

In {x | x. P x} ∩ {x | x y. (Q x y)} = {x | x y. (P x) ∧ (Q x y)} the situation is different since the only shared variable is the x, but the x is a bit special.

If you reduce the above statements to quantifiers it is perhaps a bit clearer: The first one essentially says that, for all x:

P x ∧ (∃y. Q x y) ⟷ (∃y. P x ∧ Q x y)

Whereas the second one says that, for all X:

(∃y z. P x y) ∧ (∃y z. Q x y z) ⟷ (∃y z. P x y ∧ Q x y z)

Upvotes: 2

Related Questions