author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63649  e690d6f2185b 
permissions  rwrr 
63462  1 
(* Title: HOL/Library/AList_Mapping.thy 
2 
Author: Florian Haftmann, TU Muenchen 

44897
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 

60500  5 
section \<open>Implementation of mappings with Association Lists\<close> 
44897
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 
63462  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 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

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

12 

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

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

14 

63462  15 
lemma lookup_Mapping [simp, code]: "Mapping.lookup (Mapping xs) = map_of xs" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

16 
by transfer rule 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

17 

63462  18 
lemma keys_Mapping [simp, code]: "Mapping.keys (Mapping xs) = set (map fst xs)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

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

20 

63462  21 
lemma empty_Mapping [code]: "Mapping.empty = Mapping []" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

22 
by transfer simp 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

23 

63462  24 
lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs" 
63649  25 
by (cases xs) (simp_all add: is_empty_def null_def) 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

26 

63462  27 
lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

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

29 

63462  30 
lemma delete_Mapping [code]: "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

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

32 

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

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

34 
"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

35 
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

36 

63462  37 
lemma size_Mapping [code]: "Mapping.size (Mapping xs) = length (remdups (map fst xs))" 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

38 
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

39 

63462  40 
lemma tabulate_Mapping [code]: "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

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

42 

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

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

44 
"Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

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

46 

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

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

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

49 
(let ks = map fst xs; ls = map fst ys 
63462  50 
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))" 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

51 
proof  
63462  52 
have *: "(a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" for a b xs 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

53 
by (auto simp add: image_def intro!: bexI) 
63476  54 
show ?thesis 
55 
apply transfer 

56 
apply (auto intro!: map_of_eqI) 

57 
apply (auto dest!: map_of_eq_dom intro: *) 

58 
done 

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

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

60 

63194  61 
lemma map_values_Mapping [code]: 
63462  62 
"Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f x y)) xs)" 
63 
for f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list" 

64 
apply transfer 

65 
apply (rule ext) 

66 
subgoal for f xs x by (induct xs) auto 

67 
done 

63194  68 

63462  69 
lemma combine_with_key_code [code]: 
63195  70 
"Mapping.combine_with_key f (Mapping xs) (Mapping ys) = 
63462  71 
Mapping.tabulate (remdups (map fst xs @ map fst ys)) 
63195  72 
(\<lambda>x. the (combine_options (f x) (map_of xs x) (map_of ys x)))" 
63462  73 
apply transfer 
74 
apply (rule ext) 

75 
apply (rule sym) 

76 
subgoal for f xs ys x 

77 
apply (cases "map_of xs x"; cases "map_of ys x"; simp) 

63476  78 
apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff 
79 
dest: map_of_SomeD split: option.splits)+ 

63462  80 
done 
81 
done 

63195  82 

63462  83 
lemma combine_code [code]: 
63194  84 
"Mapping.combine f (Mapping xs) (Mapping ys) = 
63462  85 
Mapping.tabulate (remdups (map fst xs @ map fst ys)) 
63194  86 
(\<lambda>x. the (combine_options f (map_of xs x) (map_of ys x)))" 
63462  87 
apply transfer 
88 
apply (rule ext) 

89 
apply (rule sym) 

90 
subgoal for f xs ys x 

91 
apply (cases "map_of xs x"; cases "map_of ys x"; simp) 

63476  92 
apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff 
93 
dest: map_of_SomeD split: option.splits)+ 

63462  94 
done 
95 
done 

63194  96 

63462  97 
lemma map_of_filter_distinct: (* TODO: move? *) 
63194  98 
assumes "distinct (map fst xs)" 
63462  99 
shows "map_of (filter P xs) x = 
100 
(case map_of xs x of 

101 
None \<Rightarrow> None 

102 
 Some y \<Rightarrow> if P (x,y) then Some y else None)" 

63194  103 
using assms 
104 
by (auto simp: map_of_eq_None_iff filter_map distinct_map_filter dest: map_of_SomeD 

63462  105 
simp del: map_of_eq_Some_iff intro!: map_of_is_SomeI split: option.splits) 
106 

63194  107 
lemma filter_Mapping [code]: 
108 
"Mapping.filter P (Mapping xs) = Mapping (filter (\<lambda>(k,v). P k v) (AList.clearjunk xs))" 

63462  109 
apply transfer 
110 
apply (rule ext) 

111 
apply (subst map_of_filter_distinct) 

63476  112 
apply (simp_all add: map_of_clearjunk split: option.split) 
63462  113 
done 
63194  114 

63462  115 
lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

116 
by (fact equal_refl) 
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
58881
diff
changeset

117 

44913  118 
end 