New theory of the inverse image of a function

--- a/src/HOL/Fun.thy	Tue Feb 24 10:44:53 1998 +0100
+++ b/src/HOL/Fun.thy	Tue Feb 24 11:35:33 1998 +0100
@@ -6,7 +6,7 @@
 Notions about functions.
 *)
 
-Fun = Set +
+Fun = Vimage +
 
 instance set :: (term) order
                        (subset_refl,subset_trans,subset_antisym,psubset_eq)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Vimage.ML	Tue Feb 24 11:35:33 1998 +0100
@@ -0,0 +1,72 @@
+(*  Title:      HOL/Vimage
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Inverse image of a function
+*)
+
+open Vimage;
+
+(** Basic rules **)
+
+qed_goalw "vimage_eq" thy [vimage_def]
+    "(a : f-``B) = (f a : B)"
+ (fn _ => [ (Blast_tac 1) ]);
+
+qed_goal "vimage_singleton_eq" thy
+    "(a : f-``{b}) = (f a = b)"
+ (fn _ => [ simp_tac (simpset() addsimps [vimage_eq]) 1 ]);
+
+qed_goalw "vimageI" thy [vimage_def]
+    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B"
+ (fn _ => [ (Blast_tac 1) ]);
+
+qed_goalw "vimageE" thy [vimage_def]
+    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P"
+ (fn major::prems=>
+  [ (rtac (major RS CollectE) 1),
+    (blast_tac (claset() addIs prems) 1) ]);
+
+AddIs  [vimageI];
+AddSEs [vimageE];
+
+
+(*** Simple equalities ***)
+
+goal thy "f-``{} = {}";
+by (Blast_tac 1);
+qed "vimage_empty";
+
+goal thy "f-``(A Un B) = (f-``A) Un (f-``B)";
+by (Blast_tac 1);
+qed "vimage_Un";
+
+(*NOT suitable for rewriting because of the recurrence of {a}*)
+goal thy "f-``(insert a B) = (f-``{a}) Un (f-``B)";
+by (Blast_tac 1);
+qed "vimage_insert";
+
+goal thy "f-``(A Int B) <= (f-``A) Int (f-``B)";
+by (Blast_tac 1);
+qed "vimage_Int_subset";
+
+Addsimps [vimage_empty, vimage_Un];
+
+goal thy "f-``UNIV = UNIV";
+by (Blast_tac 1);
+qed "vimage_UNIV";
+
+Addsimps [vimage_UNIV];
+
+goal thy "(UN x:A. f -`` B x) = f -`` (UN x:A. B x)";
+by (Blast_tac 1);
+qed "UN_vimage";
+Addsimps [UN_vimage];
+
+
+(** monotonicity **)
+
+goal thy "!!f. A<=B ==> f-``A <= f-``B";
+by (Blast_tac 1);
+qed "vimage_mono";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Vimage.thy	Tue Feb 24 11:35:33 1998 +0100
@@ -0,0 +1,9 @@
+Vimage = Set +
+
+consts
+  "-``"          :: ['a => 'b, 'b set] => ('a set)   (infixr 90)
+
+defs
+  vimage_def     "f-``B           == {x. f(x) : B}"
+
+end