# HG changeset patch
# User haftmann
# Date 1274448156 -7200
# Node ID d3ad914e3e029ba5a5cbaecd564ababb14a5f9b5
# Parent  4a021f6be77c39d7149b8e05690ade32a6fcb0c9
refined

diff -r 4a021f6be77c -r d3ad914e3e02 src/HOL/Library/AssocList.thy
--- 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