# HG changeset patch
# User nipkow
# Date 832342086 -7200
# Node ID 88650ba93c10f08f58bb853e15437c69a0f621f9
# Parent  f20c9abe4b50b264c0932f829eeea03dfcd41332
Added if_image_distrib.

diff -r f20c9abe4b50 -r 88650ba93c10 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri May 17 12:24:47 1996 +0200
+++ b/src/HOL/equalities.ML	Fri May 17 16:08:06 1996 +0200
@@ -84,6 +84,15 @@
 qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
  (fn _ => [fast_tac set_cs 1]);
 
+goalw Set.thy [image_def]
+"(%x. if P x then f x else g x) `` S			\
+\ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
+by(split_tac [expand_if] 1);
+by(fast_tac eq_cs 1);
+qed "if_image_distrib";
+Addsimps[if_image_distrib];
+
+
 section "range";
 
 qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"