equal
deleted
inserted
replaced
518 |
518 |
519 (*Look: it has an EXISTENTIAL quantifier*) |
519 (*Look: it has an EXISTENTIAL quantifier*) |
520 Goal "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})"; |
520 Goal "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})"; |
521 by (Blast_tac 1); |
521 by (Blast_tac 1); |
522 qed "INT_eq"; |
522 qed "INT_eq"; |
523 |
|
524 Goalw [o_def] "UNION A (g o f) = UNION (f``A) g"; |
|
525 by (Blast_tac 1); |
|
526 qed "UNION_o"; |
|
527 |
523 |
528 |
524 |
529 (*Distributive laws...*) |
525 (*Distributive laws...*) |
530 |
526 |
531 Goal "A Int Union(B) = (UN C:B. A Int C)"; |
527 Goal "A Int Union(B) = (UN C:B. A Int C)"; |