# 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";