src/HOL/Library/AssocList.thy
changeset 37051 d3ad914e3e02
parent 36109 1028cf8c0d1b
child 37458 4a76497f2eaa
     1.1 --- a/src/HOL/Library/AssocList.thy	Fri May 21 11:50:34 2010 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Fri May 21 15:22:36 2010 +0200
     1.3 @@ -668,6 +668,10 @@
     1.4    "Mapping.lookup (Mapping xs) = map_of xs"
     1.5    by (simp add: Mapping_def)
     1.6  
     1.7 +lemma keys_Mapping [simp, code]:
     1.8 +  "Mapping.keys (Mapping xs) = set (map fst xs)"
     1.9 +  by (simp add: keys_def dom_map_of_conv_image_fst)
    1.10 +
    1.11  lemma empty_Mapping [code]:
    1.12    "Mapping.empty = Mapping []"
    1.13    by (rule mapping_eqI) simp
    1.14 @@ -684,13 +688,9 @@
    1.15    "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
    1.16    by (rule mapping_eqI) (simp add: delete_conv')
    1.17  
    1.18 -lemma keys_Mapping [code]:
    1.19 -  "Mapping.keys (Mapping xs) = set (map fst xs)"
    1.20 -  by (simp add: keys_def dom_map_of_conv_image_fst)
    1.21 -
    1.22  lemma ordered_keys_Mapping [code]:
    1.23    "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
    1.24 -  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups)
    1.25 +  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
    1.26  
    1.27  lemma size_Mapping [code]:
    1.28    "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
    1.29 @@ -704,4 +704,7 @@
    1.30    "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
    1.31    by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
    1.32  
    1.33 +lemma [code, code del]:
    1.34 +  "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
    1.35 +
    1.36  end