# HG changeset patch
# User oheimb
# Date 894054505 -7200
# Node ID c1aec06d1dcad838cd09c6a0df633bfc2918d7e8
# Parent  379314255a04e24836ea4980623320481f586b53
added finite_dom_map_of and ran_update

diff -r 379314255a04 -r c1aec06d1dca src/HOL/Map.ML
--- a/src/HOL/Map.ML	Fri May 01 22:27:43 1998 +0200
+++ b/src/HOL/Map.ML	Fri May 01 22:28:25 1998 +0200
@@ -24,6 +24,7 @@
 	(K [rtac ext 1, Asm_simp_tac 1]);
 (*Addsimps [update_same, update_other, update_triv];*)
 
+
 section "++";
 
 goalw thy [override_def] "m ++ empty = m";
@@ -80,6 +81,12 @@
 qed "dom_update";
 Addsimps [dom_update];
 
+qed_goalw "finite_dom_map_of" Map.thy [dom_def] "finite (dom (map_of l))" (K[
+	list.induct_tac "l" 1,
+	 ALLGOALS Simp_tac,
+	stac (insert_Collect RS sym) 1,
+	Asm_simp_tac 1]);
+
 goalw thy [dom_def] "dom(m++n) = dom n Un dom m";
 by (Blast_tac 1);
 qed "dom_override";
@@ -91,3 +98,10 @@
 by (Simp_tac 1);
 qed "ran_empty";
 Addsimps [ran_empty];
+
+goalw thy [ran_def] "!!X. m a = None ==> ran(m[a|->b]) = insert b (ran m)";
+by Auto_tac;
+by (subgoal_tac "~(aa = a)" 1);
+by Auto_tac;
+qed "ran_update";
+Addsimps [ran_update];