# HG changeset patch
# User oheimb
# Date 959960732 -7200
# Node ID b16bc0b5ad21ee339d14e39e191232b03868f49b
# Parent  ff259b415c4de192019c990be29d0d879b37046f
added map_of_mapk_SomeI and weak_map_of_SomeI

diff -r ff259b415c4d -r b16bc0b5ad21 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Fri Jun 02 17:42:43 2000 +0200
+++ b/src/HOL/Map.ML	Fri Jun 02 17:45:32 2000 +0200
@@ -60,11 +60,20 @@
 
 Goal "map_of xs k = Some y --> (k,y):set xs";
 by (induct_tac "xs" 1);
-by  (Simp_tac 1);
-by (split_all_tac 1);
-by (Asm_simp_tac 1);
+by  Auto_tac;
 qed_spec_mp "map_of_SomeD";
 
+Goal "inj f ==> map_of t k = Some x --> \
+\  map_of (map (split (%k. Pair (f k))) t) (f k) = Some x";
+by (induct_tac "t" 1);
+by  (auto_tac (claset(),simpset()addsimps[inj_eq]));
+qed_spec_mp "map_of_mapk_SomeI";
+
+Goal "(k, x) : set l --> (? x. map_of l k = Some x)";
+by (induct_tac "l" 1);
+by  Auto_tac;
+qed_spec_mp "weak_map_of_SomeI";
+
 Goal "[| map_of xs k = Some z; P z |] ==> map_of [(k,z):xs . P z] k = Some z";
 by (rtac mp 1);
 by (assume_tac 2);
@@ -81,6 +90,7 @@
 by Auto_tac;
 qed "finite_range_map_of";
 
+
 section "option_map related";
 
 Goal "option_map f o empty = empty";