1(* Author: Tobias Nipkow *) 2 3section \<open>Association List Update and Deletion\<close> 4 5theory AList_Upd_Del 6imports Sorted_Less 7begin 8 9abbreviation "sorted1 ps \<equiv> sorted(map fst ps)" 10 11text\<open>Define own @{text map_of} function to avoid pulling in an unknown 12amount of lemmas implicitly (via the simpset).\<close> 13 14hide_const (open) map_of 15 16fun map_of :: "('a*'b)list \<Rightarrow> 'a \<Rightarrow> 'b option" where 17"map_of [] = (\<lambda>x. None)" | 18"map_of ((a,b)#ps) = (\<lambda>x. if x=a then Some b else map_of ps x)" 19 20text \<open>Updating an association list:\<close> 21 22fun upd_list :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) list \<Rightarrow> ('a*'b) list" where 23"upd_list x y [] = [(x,y)]" | 24"upd_list x y ((a,b)#ps) = 25 (if x < a then (x,y)#(a,b)#ps else 26 if x = a then (x,y)#ps else (a,b) # upd_list x y ps)" 27 28fun del_list :: "'a::linorder \<Rightarrow> ('a*'b)list \<Rightarrow> ('a*'b)list" where 29"del_list x [] = []" | 30"del_list x ((a,b)#ps) = (if x = a then ps else (a,b) # del_list x ps)" 31 32 33subsection \<open>Lemmas for @{const map_of}\<close> 34 35lemma map_of_ins_list: "map_of (upd_list x y ps) = (map_of ps)(x := Some y)" 36by(induction ps) auto 37 38lemma map_of_append: "map_of (ps @ qs) x = 39 (case map_of ps x of None \<Rightarrow> map_of qs x | Some y \<Rightarrow> Some y)" 40by(induction ps)(auto) 41 42lemma map_of_None: "sorted (x # map fst ps) \<Longrightarrow> map_of ps x = None" 43by (induction ps) (fastforce simp: sorted_lems sorted_wrt_Cons)+ 44 45lemma map_of_None2: "sorted (map fst ps @ [x]) \<Longrightarrow> map_of ps x = None" 46by (induction ps) (auto simp: sorted_lems) 47 48lemma map_of_del_list: "sorted1 ps \<Longrightarrow> 49 map_of(del_list x ps) = (map_of ps)(x := None)" 50by(induction ps) (auto simp: map_of_None sorted_lems fun_eq_iff) 51 52lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow> 53 map_of ps x = None" 54by (simp add: map_of_None sorted_Cons_le) 55 56lemma map_of_sorted_snoc: "sorted (map fst ps @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> 57 map_of ps x = None" 58by (simp add: map_of_None2 sorted_snoc_le) 59 60lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc 61lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds 62 63 64subsection \<open>Lemmas for @{const upd_list}\<close> 65 66lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list x y ps)" 67apply(induction ps) 68 apply simp 69apply(case_tac ps) 70 apply auto 71done 72 73lemma upd_list_sorted: "sorted1 (ps @ [(a,b)]) \<Longrightarrow> 74 upd_list x y (ps @ (a,b) # qs) = 75 (if x < a then upd_list x y ps @ (a,b) # qs 76 else ps @ upd_list x y ((a,b) # qs))" 77by(induction ps) (auto simp: sorted_lems) 78 79text\<open>In principle, @{thm upd_list_sorted} suffices, but the following two 80corollaries speed up proofs.\<close> 81 82corollary upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [a]); x < a \<rbrakk> \<Longrightarrow> 83 upd_list x y (ps @ (a,b) # qs) = upd_list x y ps @ (a,b) # qs" 84by (auto simp: upd_list_sorted) 85 86corollary upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [a]); a \<le> x \<rbrakk> \<Longrightarrow> 87 upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)" 88by (auto simp: upd_list_sorted) 89 90lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2 91 92text\<open>Splay trees need two additional @{const upd_list} lemmas:\<close> 93 94lemma upd_list_Cons: 95 "sorted1 ((x,y) # xs) \<Longrightarrow> upd_list x y xs = (x,y) # xs" 96by (induction xs) auto 97 98lemma upd_list_snoc: 99 "sorted1 (xs @ [(x,y)]) \<Longrightarrow> upd_list x y xs = xs @ [(x,y)]" 100by(induction xs) (auto simp add: sorted_mid_iff2) 101 102 103subsection \<open>Lemmas for @{const del_list}\<close> 104 105lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)" 106apply(induction ps) 107 apply simp 108apply(case_tac ps) 109apply (auto simp: sorted_Cons_le) 110done 111 112lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs" 113by (induct xs) auto 114 115lemma del_list_sorted: "sorted1 (ps @ (a,b) # qs) \<Longrightarrow> 116 del_list x (ps @ (a,b) # qs) = 117 (if x < a then del_list x ps @ (a,b) # qs 118 else ps @ del_list x ((a,b) # qs))" 119by(induction ps) 120 (fastforce simp: sorted_lems sorted_wrt_Cons intro!: del_list_idem)+ 121 122text\<open>In principle, @{thm del_list_sorted} suffices, but the following 123corollaries speed up proofs.\<close> 124 125corollary del_list_sorted1: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> a \<le> x \<Longrightarrow> 126 del_list x (xs @ (a,b) # ys) = xs @ del_list x ((a,b) # ys)" 127by (auto simp: del_list_sorted) 128 129lemma del_list_sorted2: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> x < a \<Longrightarrow> 130 del_list x (xs @ (a,b) # ys) = del_list x xs @ (a,b) # ys" 131by (auto simp: del_list_sorted) 132 133lemma del_list_sorted3: 134 "sorted1 (xs @ (a,a') # ys @ (b,b') # zs) \<Longrightarrow> x < b \<Longrightarrow> 135 del_list x (xs @ (a,a') # ys @ (b,b') # zs) = del_list x (xs @ (a,a') # ys) @ (b,b') # zs" 136by (auto simp: del_list_sorted sorted_lems) 137 138lemma del_list_sorted4: 139 "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) \<Longrightarrow> x < c \<Longrightarrow> 140 del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) = del_list x (xs @ (a,a') # ys @ (b,b') # zs) @ (c,c') # us" 141by (auto simp: del_list_sorted sorted_lems) 142 143lemma del_list_sorted5: 144 "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) \<Longrightarrow> x < d \<Longrightarrow> 145 del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) = 146 del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) @ (d,d') # vs" 147by (auto simp: del_list_sorted sorted_lems) 148 149lemmas del_list_simps = sorted_lems 150 del_list_sorted1 151 del_list_sorted2 152 del_list_sorted3 153 del_list_sorted4 154 del_list_sorted5 155 156text\<open>Splay trees need two additional @{const del_list} lemmas:\<close> 157 158lemma del_list_notin_Cons: "sorted (x # map fst xs) \<Longrightarrow> del_list x xs = xs" 159by(induction xs)(fastforce simp: sorted_wrt_Cons)+ 160 161lemma del_list_sorted_app: 162 "sorted(map fst xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys" 163by (induction xs) (auto simp: sorted_mid_iff2) 164 165end 166