author  bulwahn 
Tue, 13 Sep 2011 09:28:03 +0200  
changeset 44913  48240fb48980 
parent 44897  787983a08bfb 
child 45873  37ffb8797a63 
permissions  rwrr 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

1 
(* Title: HOL/Library/AList_Mapping.thy 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

2 
Author: Florian Haftmann, TU Muenchen 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

3 
*) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

4 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

5 
header {* Implementation of mappings with Association Lists *} 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

6 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

7 
theory AList_Mapping 
44913  8 
imports AList Mapping 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

9 
begin 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

10 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

11 
definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

12 
"Mapping xs = Mapping.Mapping (map_of xs)" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

13 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

14 
code_datatype Mapping 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

15 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

16 
lemma lookup_Mapping [simp, code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

17 
"Mapping.lookup (Mapping xs) = map_of xs" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

18 
by (simp add: Mapping_def) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

19 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

20 
lemma keys_Mapping [simp, code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

21 
"Mapping.keys (Mapping xs) = set (map fst xs)" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

22 
by (simp add: keys_def dom_map_of_conv_image_fst) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

23 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

24 
lemma empty_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

25 
"Mapping.empty = Mapping []" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

26 
by (rule mapping_eqI) simp 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

27 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

28 
lemma is_empty_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

29 
"Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

30 
by (cases xs) (simp_all add: is_empty_def null_def) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

31 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

32 
lemma update_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

33 
"Mapping.update k v (Mapping xs) = Mapping (update k v xs)" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

34 
by (rule mapping_eqI) (simp add: update_conv') 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

35 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

36 
lemma delete_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

37 
"Mapping.delete k (Mapping xs) = Mapping (delete k xs)" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

38 
by (rule mapping_eqI) (simp add: delete_conv') 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

39 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

40 
lemma ordered_keys_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

41 
"Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

42 
by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

43 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

44 
lemma size_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

45 
"Mapping.size (Mapping xs) = length (remdups (map fst xs))" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

46 
by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

47 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

48 
lemma tabulate_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

49 
"Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

50 
by (rule mapping_eqI) (simp add: map_of_map_restrict) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

51 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

52 
lemma bulkload_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

53 
"Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

54 
by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

55 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

56 
lemma equal_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

57 
"HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow> 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

58 
(let ks = map fst xs; ls = map fst ys 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

59 
in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

60 
proof  
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

61 
have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

62 
by (auto simp add: image_def intro!: bexI) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

63 
show ?thesis 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

64 
by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

65 
(auto dest!: map_of_eq_dom intro: aux) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

66 
qed 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

67 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

68 
lemma [code nbe]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

69 
"HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

70 
by (fact equal_refl) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

71 

44913  72 
end 