# HG changeset patch
# User haftmann
# Date 1266421777 -3600
# Node ID a6c573d133851e3b2ce6788f10bff185323d167f
# Parent  a57ef2cd22368a94aa52c05fb940a2c8c756552b
added ordered_keys

diff -r a57ef2cd2236 -r a6c573d13385 src/HOL/Library/AssocList.thy
--- 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)
diff -r a57ef2cd2236 -r a6c573d13385 src/HOL/Library/Mapping.thy
--- 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