Proved insert_image
authorpaulson
Fri Jul 26 12:18:50 1996 +0200 (1996-07-26)
changeset 18845a1f81da3e12
parent 1883 00b4b6992945
child 1885 a18a6dc14f76
Proved insert_image
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Fri Jul 26 12:17:04 1996 +0200
     1.2 +++ b/src/HOL/equalities.ML	Fri Jul 26 12:18:50 1996 +0200
     1.3 @@ -97,6 +97,11 @@
     1.4  qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
     1.5   (fn _ => [Fast_tac 1]);
     1.6  
     1.7 +goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
     1.8 +by (Fast_tac 1);
     1.9 +qed "insert_image";
    1.10 +Addsimps [insert_image];
    1.11 +
    1.12  goalw Set.thy [image_def]
    1.13  "(%x. if P x then f x else g x) `` S                    \
    1.14  \ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
    1.15 @@ -111,10 +116,9 @@
    1.16  qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
    1.17   (fn _ => [Fast_tac 1]);
    1.18  
    1.19 -qed_goalw "image_range" Set.thy [image_def, range_def]
    1.20 - "f``range g = range (%x. f (g x))" (fn _ => [
    1.21 -        rtac Collect_cong 1,
    1.22 -        Fast_tac 1]);
    1.23 +qed_goalw "image_range" Set.thy [image_def]
    1.24 + "f``range g = range (%x. f (g x))" 
    1.25 + (fn _ => [rtac Collect_cong 1, Fast_tac 1]);
    1.26  
    1.27  section "Int";
    1.28