--- a/src/HOL/Library/AssocList.thy Wed Feb 17 13:48:13 2010 +0100
+++ b/src/HOL/Library/AssocList.thy Wed Feb 17 16:49:37 2010 +0100
@@ -688,6 +688,10 @@
"Mapping.keys (AList xs) = set (map fst xs)"
by (simp add: keys_def dom_map_of_conv_image_fst)
+lemma ordered_keys_AList [code]:
+ "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))"
+ by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups)
+
lemma size_AList [code]:
"Mapping.size (AList xs) = length (remdups (map fst xs))"
by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
--- a/src/HOL/Library/Mapping.thy Wed Feb 17 13:48:13 2010 +0100
+++ b/src/HOL/Library/Mapping.thy Wed Feb 17 16:49:37 2010 +0100
@@ -28,6 +28,9 @@
definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
"keys m = dom (lookup m)"
+definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
+ "ordered_keys m = sorted_list_of_set (keys m)"
+
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where
"is_empty m \<longleftrightarrow> dom (lookup m) = {}"
@@ -139,6 +142,6 @@
by (cases m) simp
-hide (open) const empty is_empty lookup update delete keys size replace tabulate bulkload
+hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
end
\ No newline at end of file