src/HOL/Library/AList.thy
changeset 60043 177d740a0d48
parent 59990 a81dc82ecba3
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/AList.thy	Sun Apr 12 20:05:35 2015 +0200
     1.2 +++ b/src/HOL/Library/AList.thy	Mon Apr 13 10:36:06 2015 +0200
     1.3 @@ -215,6 +215,87 @@
     1.4    by (simp add: delete_eq)
     1.5  
     1.6  
     1.7 +subsection {* @{text update_with_aux} and @{text delete_aux}*}
     1.8 +
     1.9 +qualified primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.10 +where
    1.11 +  "update_with_aux v k f [] = [(k, f v)]"
    1.12 +| "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)"
    1.13 +
    1.14 +text {*
    1.15 +  The above @{term "delete"} traverses all the list even if it has found the key.
    1.16 +  This one does not have to keep going because is assumes the invariant that keys are distinct.
    1.17 +*}
    1.18 +qualified fun delete_aux :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.19 +where
    1.20 +  "delete_aux k [] = []"
    1.21 +| "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"
    1.22 +
    1.23 +lemma map_of_update_with_aux':
    1.24 +  "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'"
    1.25 +by(induct ps) auto
    1.26 +
    1.27 +lemma map_of_update_with_aux:
    1.28 +  "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))"
    1.29 +by(simp add: fun_eq_iff map_of_update_with_aux')
    1.30 +
    1.31 +lemma dom_update_with_aux: "fst ` set (update_with_aux v k f ps) = {k} \<union> fst ` set ps"
    1.32 +  by (induct ps) auto
    1.33 +
    1.34 +lemma distinct_update_with_aux [simp]:
    1.35 +  "distinct (map fst (update_with_aux v k f ps)) = distinct (map fst ps)"
    1.36 +by(induct ps)(auto simp add: dom_update_with_aux)
    1.37 +
    1.38 +lemma set_update_with_aux:
    1.39 +  "distinct (map fst xs) 
    1.40 +  \<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))})"
    1.41 +by(induct xs)(auto intro: rev_image_eqI)
    1.42 +
    1.43 +lemma set_delete_aux: "distinct (map fst xs) \<Longrightarrow> set (delete_aux k xs) = set xs - {k} \<times> UNIV"
    1.44 +apply(induct xs)
    1.45 +apply simp_all
    1.46 +apply clarsimp
    1.47 +apply(fastforce intro: rev_image_eqI)
    1.48 +done
    1.49 +
    1.50 +lemma dom_delete_aux: "distinct (map fst ps) \<Longrightarrow> fst ` set (delete_aux k ps) = fst ` set ps - {k}"
    1.51 +by(auto simp add: set_delete_aux)
    1.52 +
    1.53 +lemma distinct_delete_aux [simp]:
    1.54 +  "distinct (map fst ps) \<Longrightarrow> distinct (map fst (delete_aux k ps))"
    1.55 +proof(induct ps)
    1.56 +  case Nil thus ?case by simp
    1.57 +next
    1.58 +  case (Cons a ps)
    1.59 +  obtain k' v where a: "a = (k', v)" by(cases a)
    1.60 +  show ?case
    1.61 +  proof(cases "k' = k")
    1.62 +    case True with Cons a show ?thesis by simp
    1.63 +  next
    1.64 +    case False
    1.65 +    with Cons a have "k' \<notin> fst ` set ps" "distinct (map fst ps)" by simp_all
    1.66 +    with False a have "k' \<notin> fst ` set (delete_aux k ps)"
    1.67 +      by(auto dest!: dom_delete_aux[where k=k])
    1.68 +    with Cons a show ?thesis by simp
    1.69 +  qed
    1.70 +qed
    1.71 +
    1.72 +lemma map_of_delete_aux':
    1.73 +  "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) = (map_of xs)(k := None)"
    1.74 +  apply (induct xs)
    1.75 +  apply (fastforce simp add: map_of_eq_None_iff fun_upd_twist)
    1.76 +  apply (auto intro!: ext)
    1.77 +  apply (simp add: map_of_eq_None_iff)
    1.78 +  done
    1.79 +
    1.80 +lemma map_of_delete_aux:
    1.81 +  "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
    1.82 +by(simp add: map_of_delete_aux')
    1.83 +
    1.84 +lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
    1.85 +by(cases ts)(auto split: split_if_asm)
    1.86 +
    1.87 +
    1.88  subsection {* @{text restrict} *}
    1.89  
    1.90  qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"