author paulson Tue Mar 03 15:12:57 1998 +0100 (1998-03-03) changeset 4674 248b876c2fa8 parent 4673 59d80bacee62 child 4675 6efc56450d09
New theorems
 src/HOL/Vimage.ML file | annotate | diff | revisions src/HOL/equalities.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Vimage.ML	Tue Mar 03 15:12:25 1998 +0100
1.2 +++ b/src/HOL/Vimage.ML	Tue Mar 03 15:12:57 1998 +0100
1.3 @@ -46,7 +46,11 @@
1.4  by (Blast_tac 1);
1.5  qed "vimage_Un";
1.6
1.8 +goal thy "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
1.9 +by (Blast_tac 1);
1.10 +qed "vimage_UN";
1.11 +
1.13
1.14  (*NOT suitable for rewriting because of the recurrence of {a}*)
1.15  goal thy "f-``(insert a B) = (f-``{a}) Un (f-``B)";
```
```     2.1 --- a/src/HOL/equalities.ML	Tue Mar 03 15:12:25 1998 +0100
2.2 +++ b/src/HOL/equalities.ML	Tue Mar 03 15:12:57 1998 +0100
2.3 @@ -504,6 +504,10 @@
2.4  by (Blast_tac 1);
2.5  qed "Int_Union";
2.6
2.7 +goal thy "Union(B) Int A = (UN C:B. C Int A)";
2.8 +by (Blast_tac 1);
2.9 +qed "Int_Union2";
2.10 +
2.11  (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
2.12     Union of a family of unions **)
2.13  goal thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
2.14 @@ -573,6 +577,10 @@
2.15  qed "Diff_cancel";