# HG changeset patch # User oheimb # Date 949067340 -3600 # Node ID 837a6b515005ec85de08ea9d1078a2dd50534318 # Parent 64c2725043839e784644fba4dd71ad4dc36d1e51 added finite_range_updI, finite_range_map_of, finite_range_map_of_override added, also to simpset: override_upd, ran_empty' diff -r 64c272504383 -r 837a6b515005 src/HOL/Map.ML --- 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);