author | haftmann |
Tue, 14 Jul 2009 16:27:32 +0200 | |
changeset 32069 | 6d28bbd33e2c |
parent 31459 | ae39b7b2a68a |
child 33640 | 0d82107dc07a |
permissions | -rw-r--r-- |
31459 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
29708 | 2 |
|
3 |
header {* An abstract view on maps for code generation. *} |
|
4 |
||
5 |
theory Mapping |
|
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
29831
diff
changeset
|
6 |
imports Map Main |
29708 | 7 |
begin |
8 |
||
9 |
subsection {* Type definition and primitive operations *} |
|
10 |
||
11 |
datatype ('a, 'b) map = Map "'a \<rightharpoonup> 'b" |
|
12 |
||
13 |
definition empty :: "('a, 'b) map" where |
|
14 |
"empty = Map (\<lambda>_. None)" |
|
15 |
||
16 |
primrec lookup :: "('a, 'b) map \<Rightarrow> 'a \<rightharpoonup> 'b" where |
|
17 |
"lookup (Map f) = f" |
|
18 |
||
19 |
primrec update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where |
|
20 |
"update k v (Map f) = Map (f (k \<mapsto> v))" |
|
21 |
||
22 |
primrec delete :: "'a \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where |
|
23 |
"delete k (Map f) = Map (f (k := None))" |
|
24 |
||
25 |
primrec keys :: "('a, 'b) map \<Rightarrow> 'a set" where |
|
26 |
"keys (Map f) = dom f" |
|
27 |
||
28 |
||
29 |
subsection {* Derived operations *} |
|
30 |
||
31 |
definition size :: "('a, 'b) map \<Rightarrow> nat" where |
|
32 |
"size m = (if finite (keys m) then card (keys m) else 0)" |
|
33 |
||
29814 | 34 |
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where |
35 |
"replace k v m = (if lookup m k = None then m else update k v m)" |
|
36 |
||
29708 | 37 |
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) map" where |
38 |
"tabulate ks f = Map (map_of (map (\<lambda>k. (k, f k)) ks))" |
|
39 |
||
29826 | 40 |
definition bulkload :: "'a list \<Rightarrow> (nat, 'a) map" where |
41 |
"bulkload xs = Map (\<lambda>k. if k < length xs then Some (xs ! k) else None)" |
|
42 |
||
29708 | 43 |
|
44 |
subsection {* Properties *} |
|
45 |
||
46 |
lemma lookup_inject: |
|
47 |
"lookup m = lookup n \<longleftrightarrow> m = n" |
|
48 |
by (cases m, cases n) simp |
|
49 |
||
50 |
lemma lookup_empty [simp]: |
|
51 |
"lookup empty = Map.empty" |
|
52 |
by (simp add: empty_def) |
|
53 |
||
54 |
lemma lookup_update [simp]: |
|
55 |
"lookup (update k v m) = (lookup m) (k \<mapsto> v)" |
|
56 |
by (cases m) simp |
|
57 |
||
58 |
lemma lookup_delete: |
|
59 |
"lookup (delete k m) k = None" |
|
60 |
"k \<noteq> l \<Longrightarrow> lookup (delete k m) l = lookup m l" |
|
61 |
by (cases m, simp)+ |
|
62 |
||
63 |
lemma lookup_tabulate: |
|
64 |
"lookup (tabulate ks f) = (Some o f) |` set ks" |
|
65 |
by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq) |
|
66 |
||
29826 | 67 |
lemma lookup_bulkload: |
68 |
"lookup (bulkload xs) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)" |
|
69 |
unfolding bulkload_def by simp |
|
70 |
||
29708 | 71 |
lemma update_update: |
72 |
"update k v (update k w m) = update k v m" |
|
73 |
"k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)" |
|
74 |
by (cases m, simp add: expand_fun_eq)+ |
|
75 |
||
29814 | 76 |
lemma replace_update: |
77 |
"lookup m k = None \<Longrightarrow> replace k v m = m" |
|
78 |
"lookup m k \<noteq> None \<Longrightarrow> replace k v m = update k v m" |
|
79 |
by (auto simp add: replace_def) |
|
80 |
||
29708 | 81 |
lemma delete_empty [simp]: |
82 |
"delete k empty = empty" |
|
83 |
by (simp add: empty_def) |
|
84 |
||
85 |
lemma delete_update: |
|
86 |
"delete k (update k v m) = delete k m" |
|
87 |
"k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)" |
|
88 |
by (cases m, simp add: expand_fun_eq)+ |
|
89 |
||
90 |
lemma update_delete [simp]: |
|
91 |
"update k v (delete k m) = update k v m" |
|
92 |
by (cases m) simp |
|
93 |
||
94 |
lemma keys_empty [simp]: |
|
95 |
"keys empty = {}" |
|
96 |
unfolding empty_def by simp |
|
97 |
||
98 |
lemma keys_update [simp]: |
|
99 |
"keys (update k v m) = insert k (keys m)" |
|
100 |
by (cases m) simp |
|
101 |
||
102 |
lemma keys_delete [simp]: |
|
103 |
"keys (delete k m) = keys m - {k}" |
|
104 |
by (cases m) simp |
|
105 |
||
106 |
lemma keys_tabulate [simp]: |
|
107 |
"keys (tabulate ks f) = set ks" |
|
108 |
by (auto simp add: tabulate_def dest: map_of_SomeD intro!: weak_map_of_SomeI) |
|
109 |
||
110 |
lemma size_empty [simp]: |
|
111 |
"size empty = 0" |
|
112 |
by (simp add: size_def keys_empty) |
|
113 |
||
114 |
lemma size_update: |
|
115 |
"finite (keys m) \<Longrightarrow> size (update k v m) = |
|
116 |
(if k \<in> keys m then size m else Suc (size m))" |
|
117 |
by (simp add: size_def keys_update) |
|
118 |
(auto simp only: card_insert card_Suc_Diff1) |
|
119 |
||
120 |
lemma size_delete: |
|
121 |
"size (delete k m) = (if k \<in> keys m then size m - 1 else size m)" |
|
122 |
by (simp add: size_def keys_delete) |
|
123 |
||
124 |
lemma size_tabulate: |
|
125 |
"size (tabulate ks f) = length (remdups ks)" |
|
126 |
by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric]) |
|
127 |
||
29831 | 128 |
lemma bulkload_tabulate: |
29826 | 129 |
"bulkload xs = tabulate [0..<length xs] (nth xs)" |
29831 | 130 |
by (rule sym) |
131 |
(auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def) |
|
29826 | 132 |
|
31459 | 133 |
|
134 |
subsection {* Some technical code lemmas *} |
|
135 |
||
136 |
lemma [code]: |
|
137 |
"map_case f m = f (Mapping.lookup m)" |
|
138 |
by (cases m) simp |
|
139 |
||
140 |
lemma [code]: |
|
141 |
"map_rec f m = f (Mapping.lookup m)" |
|
142 |
by (cases m) simp |
|
143 |
||
144 |
lemma [code]: |
|
145 |
"Nat.size (m :: (_, _) map) = 0" |
|
146 |
by (cases m) simp |
|
147 |
||
148 |
lemma [code]: |
|
149 |
"map_size f g m = 0" |
|
150 |
by (cases m) simp |
|
151 |
||
29708 | 152 |
end |