equal
deleted
inserted
replaced
686 |
686 |
687 lemma keys_AList [code]: |
687 lemma keys_AList [code]: |
688 "Mapping.keys (AList xs) = set (map fst xs)" |
688 "Mapping.keys (AList xs) = set (map fst xs)" |
689 by (simp add: keys_def dom_map_of_conv_image_fst) |
689 by (simp add: keys_def dom_map_of_conv_image_fst) |
690 |
690 |
|
691 lemma ordered_keys_AList [code]: |
|
692 "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))" |
|
693 by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups) |
|
694 |
691 lemma size_AList [code]: |
695 lemma size_AList [code]: |
692 "Mapping.size (AList xs) = length (remdups (map fst xs))" |
696 "Mapping.size (AList xs) = length (remdups (map fst xs))" |
693 by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst) |
697 by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst) |
694 |
698 |
695 lemma tabulate_AList [code]: |
699 lemma tabulate_AList [code]: |