equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Mapping.thy |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
2 |
5 header {* An abstract view on maps for code generation. *} |
3 header {* An abstract view on maps for code generation. *} |
6 |
4 |
7 theory Mapping |
5 theory Mapping |
8 imports Map Main |
6 imports Map Main |
130 lemma bulkload_tabulate: |
128 lemma bulkload_tabulate: |
131 "bulkload xs = tabulate [0..<length xs] (nth xs)" |
129 "bulkload xs = tabulate [0..<length xs] (nth xs)" |
132 by (rule sym) |
130 by (rule sym) |
133 (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def) |
131 (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def) |
134 |
132 |
|
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 |
135 end |
152 end |