# HG changeset patch
# User berghofe
# Date 899232029 -7200
# Node ID 4436c62efcebda1b68a14de71a26586b5d3781af
# Parent  ddcc3c114a0eb0416c73a740c4e92e4373b13038
Added additional theorems needed for inductive definitions.

diff -r ddcc3c114a0e -r 4436c62efceb src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Tue Jun 30 20:39:43 1998 +0200
+++ b/src/HOL/Vimage.ML	Tue Jun 30 20:40:29 1998 +0200
@@ -24,12 +24,20 @@
     "!!A B f. [| f a = b;  b:B |] ==> a : f-``B"
  (fn _ => [ (Blast_tac 1) ]);
 
+Goalw [vimage_def] "f a : A ==> a : f -`` A";
+by (Fast_tac 1);
+qed "vimageI2";
+
 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) ]);
 
+Goalw [vimage_def] "a : f -`` A ==> f a : A";
+by (Fast_tac 1);
+qed "vimageD";
+
 AddIs  [vimageI];
 AddSEs [vimageE];
 
@@ -53,11 +61,19 @@
 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-``(UN x:A. B x) = (UN x:A. f -`` B x)";
 by (Blast_tac 1);
 qed "vimage_UN";
 
-Addsimps [vimage_empty, vimage_Un];
+bind_thm ("vimage_Collect", allI RS prove_goalw thy [vimage_def]
+  "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
+    (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
+
+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)";