src/HOL/Library/AList.thy

--- 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"