# HG changeset patch
# User paulson
# Date 838376330 -7200
# Node ID 5a1f81da3e12a02409667a6312eb80a16bef8fb9
# Parent  00b4b69929458976e57205b6e2345674cfb64402
Proved insert_image

diff -r 00b4b6992945 -r 5a1f81da3e12 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Jul 26 12:17:04 1996 +0200
+++ b/src/HOL/equalities.ML	Fri Jul 26 12:18:50 1996 +0200
@@ -97,6 +97,11 @@
 qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
  (fn _ => [Fast_tac 1]);
 
+goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
+by (Fast_tac 1);
+qed "insert_image";
+Addsimps [insert_image];
+
 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)}))";
@@ -111,10 +116,9 @@
 qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
  (fn _ => [Fast_tac 1]);
 
-qed_goalw "image_range" Set.thy [image_def, range_def]
- "f``range g = range (%x. f (g x))" (fn _ => [
-        rtac Collect_cong 1,
-        Fast_tac 1]);
+qed_goalw "image_range" Set.thy [image_def]
+ "f``range g = range (%x. f (g x))" 
+ (fn _ => [rtac Collect_cong 1, Fast_tac 1]);
 
 section "Int";