--- a/src/HOL/Library/AList.thy Sun Apr 12 20:05:35 2015 +0200
+++ b/src/HOL/Library/AList.thy Mon Apr 13 10:36:06 2015 +0200
@@ -215,6 +215,87 @@
by (simp add: delete_eq)
+subsection {* @{text update_with_aux} and @{text delete_aux}*}
+
+qualified primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+where
+ "update_with_aux v k f [] = [(k, f v)]"
+| "update_with_aux v k f (p # ps) = (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"
+
+text {*
+ The above @{term "delete"} traverses all the list even if it has found the key.
+ This one does not have to keep going because is assumes the invariant that keys are distinct.
+*}
+qualified fun delete_aux :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+where
+ "delete_aux k [] = []"
+| "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"
+
+lemma map_of_update_with_aux':
+ "map_of (update_with_aux v k f ps) k' = ((map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))) k'"
+by(induct ps) auto
+
+lemma map_of_update_with_aux:
+ "map_of (update_with_aux v k f ps) = (map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))"
+by(simp add: fun_eq_iff map_of_update_with_aux')
+
+lemma dom_update_with_aux: "fst ` set (update_with_aux v k f ps) = {k} \<union> fst ` set ps"
+ by (induct ps) auto
+
+lemma distinct_update_with_aux [simp]:
+ "distinct (map fst (update_with_aux v k f ps)) = distinct (map fst ps)"
+by(induct ps)(auto simp add: dom_update_with_aux)
+
+lemma set_update_with_aux:
+ "distinct (map fst xs)
+ \<Longrightarrow> set (update_with_aux v k f xs) = (set xs - {k} \<times> UNIV \<union> {(k, f (case map_of xs k of None \<Rightarrow> v | Some v \<Rightarrow> v))})"
+by(induct xs)(auto intro: rev_image_eqI)
+
+lemma set_delete_aux: "distinct (map fst xs) \<Longrightarrow> set (delete_aux k xs) = set xs - {k} \<times> UNIV"
+apply(induct xs)
+apply simp_all
+apply clarsimp
+apply(fastforce intro: rev_image_eqI)
+done
+
+lemma dom_delete_aux: "distinct (map fst ps) \<Longrightarrow> fst ` set (delete_aux k ps) = fst ` set ps - {k}"
+by(auto simp add: set_delete_aux)
+
+lemma distinct_delete_aux [simp]:
+ "distinct (map fst ps) \<Longrightarrow> distinct (map fst (delete_aux k ps))"
+proof(induct ps)
+ case Nil thus ?case by simp
+next
+ case (Cons a ps)
+ obtain k' v where a: "a = (k', v)" by(cases a)
+ show ?case
+ proof(cases "k' = k")
+ case True with Cons a show ?thesis by simp
+ next
+ case False
+ with Cons a have "k' \<notin> fst ` set ps" "distinct (map fst ps)" by simp_all
+ with False a have "k' \<notin> fst ` set (delete_aux k ps)"
+ by(auto dest!: dom_delete_aux[where k=k])
+ with Cons a show ?thesis by simp
+ qed
+qed
+
+lemma map_of_delete_aux':
+ "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) = (map_of xs)(k := None)"
+ apply (induct xs)
+ apply (fastforce simp add: map_of_eq_None_iff fun_upd_twist)
+ apply (auto intro!: ext)
+ apply (simp add: map_of_eq_None_iff)
+ done
+
+lemma map_of_delete_aux:
+ "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
+by(simp add: map_of_delete_aux')
+
+lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
+by(cases ts)(auto split: split_if_asm)
+
+
subsection {* @{text restrict} *}
qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"