# HG changeset patch
# User paulson
# Date 936797892 -7200
# Node ID 3235863a069a02b16f1c0d8f894346135a5b8af3
# Parent  879ae27f5e6f2146c7674b25b7b6848157744f0a
images and preimages of the identity function

diff -r 879ae27f5e6f -r 3235863a069a src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Sep 08 15:37:31 1999 +0200
+++ b/src/HOL/Fun.ML	Wed Sep 08 15:38:12 1999 +0200
@@ -228,6 +228,27 @@
 by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
 qed "surj_imp_inj_inv";
 
+(** We seem to need both the id-forms and the (%x. x) forms; the latter can
+    arise by rewriting, while id may be used explicitly. **)
+
+Goal "(%x. x) `` Y = Y";
+by (Blast_tac 1);
+qed "image_ident";
+
+Goalw [id_def] "id `` Y = Y";
+by (Blast_tac 1);
+qed "image_id";
+Addsimps [image_ident, image_id];
+
+Goal "(%x. x) -`` Y = Y";
+by (Blast_tac 1);
+qed "vimage_ident";
+
+Goalw [id_def] "id -`` A = A";
+by Auto_tac;
+qed "vimage_id";
+Addsimps [vimage_ident, vimage_id];
+
 Goal "f``(A Int B) <= f``A Int f``B";
 by (Blast_tac 1);
 qed "image_Int_subset";