added finite_range_updI, finite_range_map_of, finite_range_map_of_override
added, also to simpset: override_upd, ran_empty'

--- a/src/HOL/Map.ML	Fri Jan 28 14:42:46 2000 +0100
+++ b/src/HOL/Map.ML	Fri Jan 28 14:49:00 2000 +0100
@@ -20,6 +20,13 @@
 	(K [rtac ext 1, Asm_simp_tac 1]);
 (*Addsimps [map_upd_triv];*)
 
+Goalw [image_def] "finite (range f) ==> finite (range (f(a|->b)))";
+by (full_simp_tac (simpset() addsimps [full_SetCompr_eq]) 1);
+br finite_subset 1;
+ba  2;
+by Auto_tac;
+qed "finite_range_updI";
+
 
 section "map_upds";
 
@@ -61,6 +68,13 @@
 by  Auto_tac;
 qed "map_of_filter_in";
 
+Goal "finite (range (map_of l))";
+by (induct_tac "l" 1);
+by  (ALLGOALS (simp_tac (simpset() addsimps [image_constant])));
+br finite_subset 1;
+ba  2;
+by Auto_tac;
+qed "finite_range_map_of";
 
 section "option_map related";
 
@@ -106,6 +120,12 @@
 qed "override_None";
 AddIffs [override_None];
 
+Goalw [override_def] "f ++ g(x|->y) = (f ++ g)(x|->y)";
+br ext 1;
+by (auto_tac (claset_of Map.thy, simpset_of Map.thy));
+qed "override_upd";
+Addsimps[override_upd];
+
 Goalw [override_def] "map_of ys ++ map_of xs = map_of (xs@ys)";
 by (rtac sym 1);
 by (induct_tac "xs" 1);
@@ -115,6 +135,16 @@
 qed "map_of_override";
 Addsimps [map_of_override];
 
+Delsimps[fun_upd_apply];
+Goal "finite (range f) ==> finite (range (f ++ map_of l))";
+by (induct_tac "l" 1);
+by  Auto_tac;
+by  (fold_goals_tac [empty_def]);
+by  (Asm_simp_tac 1);
+by (etac finite_range_updI 1);
+qed "finite_range_map_of_override";
+Addsimps [fun_upd_apply];
+
 
 section "dom";
 
@@ -148,6 +178,11 @@
 qed "ran_empty";
 Addsimps [ran_empty];
 
+Goalw [ran_def] "ran (%u. None) = {}";
+by Auto_tac;
+qed "ran_empty'";
+Addsimps[ran_empty'];
+
 Goalw [ran_def] "m a = None ==> ran(m(a|->b)) = insert b (ran m)";
 by Auto_tac;
 by (subgoal_tac "~(aa = a)" 1);