--- a/src/HOL/Library/AssocList.thy Fri May 21 11:50:34 2010 +0200
+++ b/src/HOL/Library/AssocList.thy Fri May 21 15:22:36 2010 +0200
@@ -668,6 +668,10 @@
"Mapping.lookup (Mapping xs) = map_of xs"
by (simp add: Mapping_def)
+lemma keys_Mapping [simp, code]:
+ "Mapping.keys (Mapping xs) = set (map fst xs)"
+ by (simp add: keys_def dom_map_of_conv_image_fst)
+
lemma empty_Mapping [code]:
"Mapping.empty = Mapping []"
by (rule mapping_eqI) simp
@@ -684,13 +688,9 @@
"Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
by (rule mapping_eqI) (simp add: delete_conv')
-lemma keys_Mapping [code]:
- "Mapping.keys (Mapping xs) = set (map fst xs)"
- by (simp add: keys_def dom_map_of_conv_image_fst)
-
lemma ordered_keys_Mapping [code]:
"Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
- by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups)
+ by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
lemma size_Mapping [code]:
"Mapping.size (Mapping xs) = length (remdups (map fst xs))"
@@ -704,4 +704,7 @@
"Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
+lemma [code, code del]:
+ "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
+
end