isabelleset-comprehension

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.


Solution

  • 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)