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