# HG changeset patch
# User paulson
# Date 951731319 -3600
# Node ID a054d5c98b21be3b64a04ce2086c99a2f3c15b72
# Parent  45e11d3ccbe4c20810a8a8b5f4c9b2aa725809df
more bijection theorems

diff -r 45e11d3ccbe4 -r a054d5c98b21 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Sun Feb 27 15:33:35 2000 +0100
+++ b/src/HOL/Fun.ML	Mon Feb 28 10:48:39 2000 +0100
@@ -392,6 +392,25 @@
 by (Blast_tac 1);
 qed "image_INT";
 
+(*Compare with image_INT: no use of inj_on, and if f is surjective then
+  it doesn't matter whether A is empty*)
+Goalw [bij_def] "bij f ==> f `` (INTER A B) = (INT x:A. f `` B x)";
+by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], 
+	       simpset()) 1);
+qed "bij_image_INT";
+
+Goal "bij f ==> f `` Collect P = {y. P (inv f y)}";
+by Auto_tac;
+by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
+by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
+qed "bij_image_Collect_eq";
+
+Goal "bij f ==> f -`` A = inv f `` A";
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
+by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
+qed "bij_vimage_eq_inv_image";
+
 val set_cs = claset() delrules [equalityI];