added ordered_keys
authorhaftmann
Wed Feb 17 16:49:37 2010 +0100 (2010-02-17)
changeset 35194a6c573d13385
parent 35166 a57ef2cd2236
child 35195 5163c2d00904
added ordered_keys
src/HOL/Library/AssocList.thy
src/HOL/Library/Mapping.thy
     1.1 --- a/src/HOL/Library/AssocList.thy	Wed Feb 17 13:48:13 2010 +0100
     1.2 +++ b/src/HOL/Library/AssocList.thy	Wed Feb 17 16:49:37 2010 +0100
     1.3 @@ -688,6 +688,10 @@
     1.4    "Mapping.keys (AList xs) = set (map fst xs)"
     1.5    by (simp add: keys_def dom_map_of_conv_image_fst)
     1.6  
     1.7 +lemma ordered_keys_AList [code]:
     1.8 +  "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))"
     1.9 +  by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups)
    1.10 +
    1.11  lemma size_AList [code]:
    1.12    "Mapping.size (AList xs) = length (remdups (map fst xs))"
    1.13    by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
     2.1 --- a/src/HOL/Library/Mapping.thy	Wed Feb 17 13:48:13 2010 +0100
     2.2 +++ b/src/HOL/Library/Mapping.thy	Wed Feb 17 16:49:37 2010 +0100
     2.3 @@ -28,6 +28,9 @@
     2.4  definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
     2.5    "keys m = dom (lookup m)"
     2.6  
     2.7 +definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
     2.8 +  "ordered_keys m = sorted_list_of_set (keys m)"
     2.9 +
    2.10  definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where
    2.11    "is_empty m \<longleftrightarrow> dom (lookup m) = {}"
    2.12  
    2.13 @@ -139,6 +142,6 @@
    2.14    by (cases m) simp
    2.15  
    2.16  
    2.17 -hide (open) const empty is_empty lookup update delete keys size replace tabulate bulkload
    2.18 +hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
    2.19  
    2.20  end
    2.21 \ No newline at end of file