--- a/src/HOL/Map.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Map.ML Wed Oct 27 19:32:19 1999 +0200
@@ -44,7 +44,25 @@
Addsimps[chg_map_new, chg_map_upd];
-section "option_map";
+section "map_of";
+
+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);
+qed_spec_mp "map_of_SomeD";
+
+Goal "[| map_of xs k = Some z; P z |] ==> map_of [(k,z):xs . P z] k = Some z";
+br mp 1;
+ba 2;
+by (etac thin_rl 1);
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "map_of_filter_in";
+
+
+section "option_map related";
qed_goal "option_map_o_empty" thy
"option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
@@ -54,7 +72,6 @@
(K [rtac ext 1, Simp_tac 1]);
Addsimps[option_map_o_empty, option_map_o_map_upd];
-
section "++";
Goalw [override_def] "m ++ empty = m";
@@ -78,6 +95,12 @@
bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
AddSDs[override_SomeD];
+Goal "!!xx. n k = Some xx ==> (m ++ n) k = Some xx";
+by (stac override_Some_iff 1);
+by (Fast_tac 1);
+qed "override_find_right";
+Addsimps[override_find_right];
+
Goalw [override_def] "((m ++ n) k = None) = (n k = None & m k = None)";
by (simp_tac (simpset() addsplits [option.split]) 1);
qed "override_None";
@@ -92,13 +115,6 @@
qed "map_of_override";
Addsimps [map_of_override];
-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);
-qed_spec_mp "map_of_SomeD";
-
section "dom";