Estou me deparando com um problema e não sei se é a maneira de Isabelle gerenciar a compreensão do conjunto ou se estou tendo um momento muito lento.
Este lema continua muito bem
lemma "{x | x. P x} ∩ {x | x y. (Q x y)} = {x | x y. (P x) ∧ (Q x y)}"
by auto
E este simplesmente não
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)}"
Deve haver uma diferença entre os dois e não vejo isso. Obviamente, preciso do segundo, meu (P x y)e (Q x y z)é bastante complexo e será difícil simplificá-lo.
Como sempre, qualquer ajuda (ou redirecionamento para alguma direção mais saudável) é muito apreciada.