equal
deleted
inserted
replaced
120 |
120 |
121 lemma bulkload_tabulate: |
121 lemma bulkload_tabulate: |
122 "bulkload xs = tabulate [0..<length xs] (nth xs)" |
122 "bulkload xs = tabulate [0..<length xs] (nth xs)" |
123 by (rule mapping_eqI) (simp add: expand_fun_eq) |
123 by (rule mapping_eqI) (simp add: expand_fun_eq) |
124 |
124 |
|
125 lemma is_empty_empty: |
|
126 "is_empty m \<longleftrightarrow> m = Mapping Map.empty" |
|
127 by (cases m) (simp add: is_empty_def) |
|
128 |
125 |
129 |
126 subsection {* Some technical code lemmas *} |
130 subsection {* Some technical code lemmas *} |
127 |
131 |
128 lemma [code]: |
132 lemma [code]: |
129 "mapping_case f m = f (Mapping.lookup m)" |
133 "mapping_case f m = f (Mapping.lookup m)" |