38 lemma map_of_append: "map_of (ps @ qs) x = |
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)" |
39 (case map_of ps x of None \<Rightarrow> map_of qs x | Some y \<Rightarrow> Some y)" |
40 by(induction ps)(auto) |
40 by(induction ps)(auto) |
41 |
41 |
42 lemma map_of_None: "sorted (x # map fst ps) \<Longrightarrow> map_of ps x = None" |
42 lemma map_of_None: "sorted (x # map fst ps) \<Longrightarrow> map_of ps x = None" |
43 by (induction ps) (auto simp: sorted_lems sorted_Cons_iff) |
43 by (induction ps) (fastforce simp: sorted_lems sorted_wrt_Cons)+ |
44 |
44 |
45 lemma map_of_None2: "sorted (map fst ps @ [x]) \<Longrightarrow> map_of ps x = None" |
45 lemma map_of_None2: "sorted (map fst ps @ [x]) \<Longrightarrow> map_of ps x = None" |
46 by (induction ps) (auto simp: sorted_lems) |
46 by (induction ps) (auto simp: sorted_lems) |
47 |
47 |
48 lemma map_of_del_list: "sorted1 ps \<Longrightarrow> |
48 lemma map_of_del_list: "sorted1 ps \<Longrightarrow> |
49 map_of(del_list x ps) = (map_of ps)(x := None)" |
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) |
50 by(induction ps) (auto simp: map_of_None sorted_lems fun_eq_iff) |
51 |
51 |
52 lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow> |
52 lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow> |
53 map_of ps x = None" |
53 map_of ps x = None" |
54 by (meson less_trans map_of_None sorted_Cons_iff) |
54 by (simp add: map_of_None sorted_Cons_le) |
55 |
55 |
56 lemma map_of_sorted_snoc: "sorted (map fst ps @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> |
56 lemma map_of_sorted_snoc: "sorted (map fst ps @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> |
57 map_of ps x = None" |
57 map_of ps x = None" |
58 by (meson le_less_trans map_of_None2 not_less sorted_snoc_iff) |
58 by (simp add: map_of_None2 sorted_snoc_le) |
59 |
59 |
60 lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc |
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 |
61 lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds |
62 |
62 |
63 |
63 |
104 |
104 |
105 lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)" |
105 lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)" |
106 apply(induction ps) |
106 apply(induction ps) |
107 apply simp |
107 apply simp |
108 apply(case_tac ps) |
108 apply(case_tac ps) |
109 apply auto |
109 apply (auto simp: sorted_Cons_le) |
110 by (meson order.strict_trans sorted_Cons_iff) |
110 done |
111 |
111 |
112 lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs" |
112 lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs" |
113 by (induct xs) auto |
113 by (induct xs) auto |
114 |
114 |
115 lemma del_list_sorted: "sorted1 (ps @ (a,b) # qs) \<Longrightarrow> |
115 lemma del_list_sorted: "sorted1 (ps @ (a,b) # qs) \<Longrightarrow> |
116 del_list x (ps @ (a,b) # qs) = |
116 del_list x (ps @ (a,b) # qs) = |
117 (if x < a then 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))" |
118 else ps @ del_list x ((a,b) # qs))" |
119 by(induction ps) |
119 by(induction ps) |
120 (fastforce simp: sorted_lems sorted_Cons_iff intro!: del_list_idem)+ |
120 (fastforce simp: sorted_lems sorted_wrt_Cons intro!: del_list_idem)+ |
121 |
121 |
122 text\<open>In principle, @{thm del_list_sorted} suffices, but the following |
122 text\<open>In principle, @{thm del_list_sorted} suffices, but the following |
123 corollaries speed up proofs.\<close> |
123 corollaries speed up proofs.\<close> |
124 |
124 |
125 corollary del_list_sorted1: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> a \<le> x \<Longrightarrow> |
125 corollary del_list_sorted1: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> a \<le> x \<Longrightarrow> |
154 del_list_sorted5 |
154 del_list_sorted5 |
155 |
155 |
156 text\<open>Splay trees need two additional @{const del_list} lemmas:\<close> |
156 text\<open>Splay trees need two additional @{const del_list} lemmas:\<close> |
157 |
157 |
158 lemma del_list_notin_Cons: "sorted (x # map fst xs) \<Longrightarrow> del_list x xs = xs" |
158 lemma del_list_notin_Cons: "sorted (x # map fst xs) \<Longrightarrow> del_list x xs = xs" |
159 by(induction xs)(auto simp: sorted_Cons_iff) |
159 by(induction xs)(fastforce simp: sorted_wrt_Cons)+ |
160 |
160 |
161 lemma del_list_sorted_app: |
161 lemma del_list_sorted_app: |
162 "sorted(map fst xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys" |
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) |
163 by (induction xs) (auto simp: sorted_mid_iff2) |
164 |
164 |