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 

35157

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


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


33 


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


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


36 


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

29814

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


39 

35157

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


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

29708

42 

35157

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


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

29826

45 

29708

46 


47 
subsection {* Properties *}


48 

35157

49 
lemma lookup_inject [simp]:

29708

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


51 
by (cases m, cases n) simp


52 

35157

53 
lemma mapping_eqI:


54 
assumes "lookup m = lookup n"


55 
shows "m = n"


56 
using assms by simp


57 

29708

58 
lemma lookup_empty [simp]:


59 
"lookup empty = Map.empty"


60 
by (simp add: empty_def)


61 


62 
lemma lookup_update [simp]:


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


64 
by (cases m) simp


65 

35157

66 
lemma lookup_delete [simp]:


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


68 
by (cases m) simp

29708

69 

35157

70 
lemma lookup_tabulate [simp]:

29708

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


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


73 

35157

74 
lemma lookup_bulkload [simp]:

29826

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

35157

76 
by (simp add: bulkload_def)

29826

77 

29708

78 
lemma update_update:


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


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

35157

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

29708

82 

35157

83 
lemma update_delete [simp]:


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


85 
by (rule mapping_eqI) simp

29708

86 


87 
lemma delete_update:


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


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

35157

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

29708

91 

35157

92 
lemma delete_empty [simp]:


93 
"delete k empty = empty"


94 
by (rule mapping_eqI) simp

29708

95 

35157

96 
lemma replace_update:


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


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


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

29708

100 


101 
lemma size_empty [simp]:


102 
"size empty = 0"

35157

103 
by (simp add: size_def)

29708

104 


105 
lemma size_update:

35157

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


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


108 
by (auto simp add: size_def insert_dom)

29708

109 


110 
lemma size_delete:

35157

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


112 
by (simp add: size_def)

29708

113 


114 
lemma size_tabulate:


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

35157

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

29708

117 

29831

118 
lemma bulkload_tabulate:

29826

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

35157

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

29826

121 

31459

122 


123 
subsection {* Some technical code lemmas *}


124 


125 
lemma [code]:

35157

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

31459

127 
by (cases m) simp


128 


129 
lemma [code]:

35157

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

31459

131 
by (cases m) simp


132 


133 
lemma [code]:

35157

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

31459

135 
by (cases m) simp


136 


137 
lemma [code]:

35157

138 
"mapping_size f g m = 0"

31459

139 
by (cases m) simp


140 

35157

141 


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


143 

29708

144 
end 