src/HOL/Inverse_Image.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Inverse_Image.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,108 @@
+(*  Title:      HOL/Inverse_Image.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Inverse image of a function
+*)
+
+(** Basic rules **)
+
+Goalw [vimage_def] "(a : f-``B) = (f a : B)";
+by (Blast_tac 1) ;
+qed "vimage_eq";
+
+Addsimps [vimage_eq];
+
+Goal "(a : f-``{b}) = (f a = b)";
+by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
+qed "vimage_singleton_eq";
+
+Goalw [vimage_def]
+    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B";
+by (Blast_tac 1) ;
+qed "vimageI";
+
+Goalw [vimage_def] "f a : A ==> a : f -`` A";
+by (Fast_tac 1);
+qed "vimageI2";
+
+val major::prems = Goalw [vimage_def]
+    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
+by (rtac (major RS CollectE) 1);
+by (blast_tac (claset() addIs prems) 1) ;
+qed "vimageE";
+
+Goalw [vimage_def] "a : f -`` A ==> f a : A";
+by (Fast_tac 1);
+qed "vimageD";
+
+AddIs  [vimageI];
+AddSEs [vimageE];
+
+
+(*** Equations ***)
+
+Goal "f-``{} = {}";
+by (Blast_tac 1);
+qed "vimage_empty";
+
+Goal "f-``(-A) = -(f-``A)";
+by (Blast_tac 1);
+qed "vimage_Compl";
+
+Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
+by (Blast_tac 1);
+qed "vimage_Un";
+
+Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
+by (Fast_tac 1);
+qed "vimage_Int";
+
+Goal "f -`` (Union A) = (UN X:A. f -`` X)";
+by (Blast_tac 1);
+qed "vimage_Union";
+
+Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
+by (Blast_tac 1);
+qed "vimage_UN";
+
+Goal "f-``(INT x:A. B x) = (INT x:A. f -`` B x)";
+by (Blast_tac 1);
+qed "vimage_INT";
+
+Goal "f -`` Collect P = {y. P (f y)}";
+by (Blast_tac 1);
+qed "vimage_Collect_eq";
+Addsimps [vimage_Collect_eq];
+
+(*A strange result used in Tools/inductive_package*)
+val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q";
+by (force_tac (claset(), simpset() addsimps prems) 1);
+qed "vimage_Collect";
+
+Addsimps [vimage_empty, vimage_Un, vimage_Int];
+
+(*NOT suitable for rewriting because of the recurrence of {a}*)
+Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
+by (Blast_tac 1);
+qed "vimage_insert";
+
+Goal "f-``(A-B) = (f-``A) - (f-``B)";
+by (Blast_tac 1);
+qed "vimage_Diff";
+
+Goal "f-``UNIV = UNIV";
+by (Blast_tac 1);
+qed "vimage_UNIV";
+Addsimps [vimage_UNIV];
+
+(*NOT suitable for rewriting*)
+Goal "f-``B = (UN y: B. f-``{y})";
+by (Blast_tac 1);
+qed "vimage_eq_UN";
+
+(*monotonicity*)
+Goal "A<=B ==> f-``A <= f-``B";
+by (Blast_tac 1);
+qed "vimage_mono";