# HG changeset patch
# User desharna
# Date 1620804678 -7200
# Node ID 50437744eb1c51f8ddddc9df8b157318f8188540
# Parent  71c45d60a90a0d937243d7143a655d5bd24ad447
added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran

diff -r 71c45d60a90a -r 50437744eb1c src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/Library/AList.thy	Wed May 12 09:31:18 2021 +0200
@@ -483,6 +483,15 @@
   "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
   by (simp_all add: map_ran_def)
 
+lemma map_ran_Cons_sel: "map_ran f (p # ps) = (fst p, f (fst p) (snd p)) # map_ran f ps"
+  by (simp add: map_ran_def case_prod_beta)
+
+lemma length_map_ran[simp]: "length (map_ran f al) = length al"
+  by (simp add: map_ran_def)
+
+lemma map_fst_map_ran[simp]: "map fst (map_ran f al) = map fst al"
+  by (simp add: map_ran_def case_prod_beta)
+
 lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
   by (simp add: map_ran_def image_image split_def)
 
@@ -490,7 +499,7 @@
   by (induct al) auto
 
 lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
-  by (simp add: map_ran_def split_def comp_def)
+  by simp
 
 lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
   by (simp add: map_ran_def filter_map split_def comp_def)