equal
deleted
inserted
replaced
126 by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric]) |
126 by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric]) |
127 |
127 |
128 lemma bulkload_tabulate: |
128 lemma bulkload_tabulate: |
129 "bulkload xs = tabulate [0..<length xs] (nth xs)" |
129 "bulkload xs = tabulate [0..<length xs] (nth xs)" |
130 by (rule sym) |
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) |
131 (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff comp_def) |
132 |
132 |
133 |
133 |
134 subsection {* Some technical code lemmas *} |
134 subsection {* Some technical code lemmas *} |
135 |
135 |
136 lemma [code]: |
136 lemma [code]: |