31459

1 
(* Author: Florian Haftmann, TU Muenchen *)

29708

2 


3 
header {* An abstract view on maps for code generation. *}


4 


5 
theory Mapping

35157

6 
imports Main

29708

7 
begin


8 


9 
subsection {* Type definition and primitive operations *}


10 

35157

11 
datatype ('a, 'b) mapping = Mapping "'a \<rightharpoonup> 'b"

29708

12 

35157

13 
definition empty :: "('a, 'b) mapping" where


14 
"empty = Mapping (\<lambda>_. None)"

29708

15 

35157

16 
primrec lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<rightharpoonup> 'b" where


17 
"lookup (Mapping f) = f"

29708

18 

35157

19 
primrec update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where


20 
"update k v (Mapping f) = Mapping (f (k \<mapsto> v))"

29708

21 

35157

22 
primrec delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where


23 
"delete k (Mapping f) = Mapping (f (k := None))"

29708

24 


25 


26 
subsection {* Derived operations *}


27 

35157

28 
definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where


29 
"keys m = dom (lookup m)"

29708

30 

35194

31 
definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where


32 
"ordered_keys m = sorted_list_of_set (keys m)"


33 

35157

34 
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where


35 
"is_empty m \<longleftrightarrow> dom (lookup m) = {}"


36 


37 
definition size :: "('a, 'b) mapping \<Rightarrow> nat" where


38 
"size m = (if finite (dom (lookup m)) then card (dom (lookup m)) else 0)"


39 


40 
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where

29814

41 
"replace k v m = (if lookup m k = None then m else update k v m)"


42 

35157

43 
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where


44 
"tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))"

29708

45 

35157

46 
definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" where


47 
"bulkload xs = Mapping (\<lambda>k. if k < length xs then Some (xs ! k) else None)"

29826

48 

29708

49 


50 
subsection {* Properties *}


51 

35157

52 
lemma lookup_inject [simp]:

29708

53 
"lookup m = lookup n \<longleftrightarrow> m = n"


54 
by (cases m, cases n) simp


55 

35157

56 
lemma mapping_eqI:


57 
assumes "lookup m = lookup n"


58 
shows "m = n"


59 
using assms by simp


60 

29708

61 
lemma lookup_empty [simp]:


62 
"lookup empty = Map.empty"


63 
by (simp add: empty_def)


64 


65 
lemma lookup_update [simp]:


66 
"lookup (update k v m) = (lookup m) (k \<mapsto> v)"


67 
by (cases m) simp


68 

35157

69 
lemma lookup_delete [simp]:


70 
"lookup (delete k m) = (lookup m) (k := None)"


71 
by (cases m) simp

29708

72 

35157

73 
lemma lookup_tabulate [simp]:

29708

74 
"lookup (tabulate ks f) = (Some o f) ` set ks"


75 
by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)


76 

35157

77 
lemma lookup_bulkload [simp]:

29826

78 
"lookup (bulkload xs) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)"

35157

79 
by (simp add: bulkload_def)

29826

80 

29708

81 
lemma update_update:


82 
"update k v (update k w m) = update k v m"


83 
"k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"

35157

84 
by (rule mapping_eqI, simp add: fun_upd_twist)+

29708

85 

35157

86 
lemma update_delete [simp]:


87 
"update k v (delete k m) = update k v m"


88 
by (rule mapping_eqI) simp

29708

89 


90 
lemma delete_update:


91 
"delete k (update k v m) = delete k m"


92 
"k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)"

35157

93 
by (rule mapping_eqI, simp add: fun_upd_twist)+

29708

94 

35157

95 
lemma delete_empty [simp]:


96 
"delete k empty = empty"


97 
by (rule mapping_eqI) simp

29708

98 

35157

99 
lemma replace_update:


100 
"k \<notin> dom (lookup m) \<Longrightarrow> replace k v m = m"


101 
"k \<in> dom (lookup m) \<Longrightarrow> replace k v m = update k v m"


102 
by (rule mapping_eqI, auto simp add: replace_def fun_upd_twist)+

29708

103 


104 
lemma size_empty [simp]:


105 
"size empty = 0"

35157

106 
by (simp add: size_def)

29708

107 


108 
lemma size_update:

35157

109 
"finite (dom (lookup m)) \<Longrightarrow> size (update k v m) =


110 
(if k \<in> dom (lookup m) then size m else Suc (size m))"


111 
by (auto simp add: size_def insert_dom)

29708

112 


113 
lemma size_delete:

35157

114 
"size (delete k m) = (if k \<in> dom (lookup m) then size m  1 else size m)"


115 
by (simp add: size_def)

29708

116 


117 
lemma size_tabulate:


118 
"size (tabulate ks f) = length (remdups ks)"

35157

119 
by (simp add: size_def distinct_card [of "remdups ks", symmetric] comp_def)

29708

120 

29831

121 
lemma bulkload_tabulate:

29826

122 
"bulkload xs = tabulate [0..<length xs] (nth xs)"

35157

123 
by (rule mapping_eqI) (simp add: expand_fun_eq)

29826

124 

31459

125 


126 
subsection {* Some technical code lemmas *}


127 


128 
lemma [code]:

35157

129 
"mapping_case f m = f (Mapping.lookup m)"

31459

130 
by (cases m) simp


131 


132 
lemma [code]:

35157

133 
"mapping_rec f m = f (Mapping.lookup m)"

31459

134 
by (cases m) simp


135 


136 
lemma [code]:

35157

137 
"Nat.size (m :: (_, _) mapping) = 0"

31459

138 
by (cases m) simp


139 


140 
lemma [code]:

35157

141 
"mapping_size f g m = 0"

31459

142 
by (cases m) simp


143 

35157

144 

35194

145 
hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload

35157

146 

29708

147 
end 