# HG changeset patch
# User oheimb
# Date 884277890 -3600
# Node ID 6be35399125ad3b5ce92d26fa982da7e35689ef1
# Parent  b96b513c6c658890950b57bee2d1d2b69bdfe9fe
added update_same, update_other, update_triv, and map_of_SomeD

diff -r b96b513c6c65 -r 6be35399125a src/HOL/Map.ML
--- a/src/HOL/Map.ML	Thu Jan 08 17:42:26 1998 +0100
+++ b/src/HOL/Map.ML	Thu Jan 08 17:44:50 1998 +0100
@@ -16,6 +16,14 @@
 qed "update_def2";
 Addsimps [update_def2];
 
+qed_goal "update_same" thy "(t[k|->x]) k = Some x" 
+	(K [Simp_tac 1]);
+qed_goal "update_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
+	(K [Asm_simp_tac 1]);
+qed_goal "update_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
+	(K [rtac ext 1, asm_simp_tac (simpset() addsplits [expand_if]) 1]);
+(*Addsimps [update_same, update_other, update_triv];*)
+
 section "++";
 
 goalw thy [override_def] "m ++ empty = m";
@@ -52,6 +60,14 @@
 qed "map_of_append";
 Addsimps [map_of_append];
 
+goal thy "map_of xs k = Some y --> (k,y):set xs";
+by (list.induct_tac "xs" 1);
+by  (Simp_tac 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (split_all_tac 1);
+by (Simp_tac 1);
+qed_spec_mp "map_of_SomeD";
+
 section "dom";
 
 goalw thy [dom_def] "dom empty = {}";