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