equal
deleted
inserted
replaced
288 syntax |
288 syntax |
289 |
289 |
290 init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table" |
290 init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table" |
291 |
291 |
292 translations |
292 translations |
293 "init_vals vs" == "option_map default_val \<circ> vs" |
293 "init_vals vs" == "CONST option_map default_val \<circ> vs" |
294 |
294 |
295 lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty" |
295 lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty" |
296 apply (unfold arr_comps_def in_bounds_def) |
296 apply (unfold arr_comps_def in_bounds_def) |
297 apply (rule ext) |
297 apply (rule ext) |
298 apply auto |
298 apply auto |