481 lemma map_ran_simps [simp]: |
481 lemma map_ran_simps [simp]: |
482 "map_ran f [] = []" |
482 "map_ran f [] = []" |
483 "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps" |
483 "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps" |
484 by (simp_all add: map_ran_def) |
484 by (simp_all add: map_ran_def) |
485 |
485 |
|
486 lemma map_ran_Cons_sel: "map_ran f (p # ps) = (fst p, f (fst p) (snd p)) # map_ran f ps" |
|
487 by (simp add: map_ran_def case_prod_beta) |
|
488 |
|
489 lemma length_map_ran[simp]: "length (map_ran f al) = length al" |
|
490 by (simp add: map_ran_def) |
|
491 |
|
492 lemma map_fst_map_ran[simp]: "map fst (map_ran f al) = map fst al" |
|
493 by (simp add: map_ran_def case_prod_beta) |
|
494 |
486 lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al" |
495 lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al" |
487 by (simp add: map_ran_def image_image split_def) |
496 by (simp add: map_ran_def image_image split_def) |
488 |
497 |
489 lemma map_ran_conv: "map_of (map_ran f al) k = map_option (f k) (map_of al k)" |
498 lemma map_ran_conv: "map_of (map_ran f al) k = map_option (f k) (map_of al k)" |
490 by (induct al) auto |
499 by (induct al) auto |
491 |
500 |
492 lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))" |
501 lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))" |
493 by (simp add: map_ran_def split_def comp_def) |
502 by simp |
494 |
503 |
495 lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]" |
504 lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]" |
496 by (simp add: map_ran_def filter_map split_def comp_def) |
505 by (simp add: map_ran_def filter_map split_def comp_def) |
497 |
506 |
498 lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)" |
507 lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)" |