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