equal
deleted
inserted
replaced
748 Goal "{x:cons(a,B). P(x)} = \ |
748 Goal "{x:cons(a,B). P(x)} = \ |
749 \ (if P(a) then cons(a, {x:B. P(x)}) else {x:B. P(x)})"; |
749 \ (if P(a) then cons(a, {x:B. P(x)}) else {x:B. P(x)})"; |
750 by (simp_tac (simpset() addsplits [split_if]) 1); |
750 by (simp_tac (simpset() addsplits [split_if]) 1); |
751 by (Blast_tac 1); |
751 by (Blast_tac 1); |
752 qed "Collect_cons"; |
752 qed "Collect_cons"; |
|
753 |
|
754 Goal "A Int Collect(A,P) = Collect(A,P)"; |
|
755 by (Blast_tac 1); |
|
756 qed "Int_Collect_self_eq"; |
|
757 |
|
758 Goal "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))"; |
|
759 by (Blast_tac 1); |
|
760 qed "Collect_Collect_eq"; |
|
761 Addsimps [Collect_Collect_eq]; |
|
762 |
|
763 Goal "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"; |
|
764 by (Blast_tac 1); |
|
765 qed "Collect_Int_Collect_eq"; |