1(* Author: Tobias Nipkow *) 2 3section \<open>List Insertion and Deletion\<close> 4 5theory List_Ins_Del 6imports Sorted_Less 7begin 8 9subsection \<open>Elements in a list\<close> 10 11lemma sorted_Cons_iff: 12 "sorted(x # xs) = ((\<forall>y \<in> set xs. x < y) \<and> sorted xs)" 13by(simp add: sorted_wrt_Cons) 14 15lemma sorted_snoc_iff: 16 "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> set xs. y < x))" 17by(simp add: sorted_wrt_append) 18(* 19text\<open>The above two rules introduce quantifiers. It turns out 20that in practice this is not a problem because of the simplicity of 21the "isin" functions that implement @{const set}. Nevertheless 22it is possible to avoid the quantifiers with the help of some rewrite rules:\<close> 23 24lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<le> y \<Longrightarrow> x \<notin> set xs" 25by (auto simp: sorted_Cons_iff) 26 27lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> x \<notin> set xs" 28by (auto simp: sorted_snoc_iff) 29 30lemmas isin_simps2 = sorted_lems sorted_ConsD sorted_snocD 31*) 32 33lemmas isin_simps = sorted_lems sorted_Cons_iff sorted_snoc_iff 34 35 36subsection \<open>Inserting into an ordered list without duplicates:\<close> 37 38fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where 39"ins_list x [] = [x]" | 40"ins_list x (a#xs) = 41 (if x < a then x#a#xs else if x=a then a#xs else a # ins_list x xs)" 42 43lemma set_ins_list: "set (ins_list x xs) = insert x (set xs)" 44by(induction xs) auto 45 46lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs" 47apply(induction xs rule: induct_list012) 48apply auto 49by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2) 50 51lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)" 52by(induction xs rule: induct_list012) auto 53 54lemma ins_list_sorted: "sorted (xs @ [a]) \<Longrightarrow> 55 ins_list x (xs @ a # ys) = 56 (if x < a then ins_list x xs @ (a#ys) else xs @ ins_list x (a#ys))" 57by(induction xs) (auto simp: sorted_lems) 58 59text\<open>In principle, @{thm ins_list_sorted} suffices, but the following two 60corollaries speed up proofs.\<close> 61 62corollary ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> 63 ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)" 64by(auto simp add: ins_list_sorted) 65 66corollary ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow> 67 ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)" 68by(auto simp: ins_list_sorted) 69 70lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 71 72text\<open>Splay trees need two additional @{const ins_list} lemmas:\<close> 73 74lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs" 75by (induction xs) auto 76 77lemma ins_list_snoc: "sorted (xs @ [x]) \<Longrightarrow> ins_list x xs = xs @ [x]" 78by(induction xs) (auto simp add: sorted_mid_iff2) 79 80 81subsection \<open>Delete one occurrence of an element from a list:\<close> 82 83fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 84"del_list x [] = []" | 85"del_list x (a#xs) = (if x=a then xs else a # del_list x xs)" 86 87lemma del_list_idem: "x \<notin> set xs \<Longrightarrow> del_list x xs = xs" 88by (induct xs) simp_all 89 90lemma set_del_list_eq: 91 "distinct xs \<Longrightarrow> set (del_list x xs) = set xs - {x}" 92by(induct xs) auto 93 94lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)" 95apply(induction xs rule: induct_list012) 96apply auto 97by (meson order.strict_trans sorted_Cons_iff) 98 99lemma del_list_sorted: "sorted (xs @ a # ys) \<Longrightarrow> 100 del_list x (xs @ a # ys) = (if x < a then del_list x xs @ a # ys else xs @ del_list x (a # ys))" 101by(induction xs) 102 (fastforce simp: sorted_lems sorted_Cons_iff intro!: del_list_idem)+ 103 104text\<open>In principle, @{thm del_list_sorted} suffices, but the following 105corollaries speed up proofs.\<close> 106 107corollary del_list_sorted1: "sorted (xs @ a # ys) \<Longrightarrow> a \<le> x \<Longrightarrow> 108 del_list x (xs @ a # ys) = xs @ del_list x (a # ys)" 109by (auto simp: del_list_sorted) 110 111corollary del_list_sorted2: "sorted (xs @ a # ys) \<Longrightarrow> x < a \<Longrightarrow> 112 del_list x (xs @ a # ys) = del_list x xs @ a # ys" 113by (auto simp: del_list_sorted) 114 115corollary del_list_sorted3: 116 "sorted (xs @ a # ys @ b # zs) \<Longrightarrow> x < b \<Longrightarrow> 117 del_list x (xs @ a # ys @ b # zs) = del_list x (xs @ a # ys) @ b # zs" 118by (auto simp: del_list_sorted sorted_lems) 119 120corollary del_list_sorted4: 121 "sorted (xs @ a # ys @ b # zs @ c # us) \<Longrightarrow> x < c \<Longrightarrow> 122 del_list x (xs @ a # ys @ b # zs @ c # us) = del_list x (xs @ a # ys @ b # zs) @ c # us" 123by (auto simp: del_list_sorted sorted_lems) 124 125corollary del_list_sorted5: 126 "sorted (xs @ a # ys @ b # zs @ c # us @ d # vs) \<Longrightarrow> x < d \<Longrightarrow> 127 del_list x (xs @ a # ys @ b # zs @ c # us @ d # vs) = 128 del_list x (xs @ a # ys @ b # zs @ c # us) @ d # vs" 129by (auto simp: del_list_sorted sorted_lems) 130 131lemmas del_list_simps = sorted_lems 132 del_list_sorted1 133 del_list_sorted2 134 del_list_sorted3 135 del_list_sorted4 136 del_list_sorted5 137 138text\<open>Splay trees need two additional @{const del_list} lemmas:\<close> 139 140lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs" 141by(induction xs)(fastforce simp: sorted_Cons_iff)+ 142 143lemma del_list_sorted_app: 144 "sorted(xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys" 145by (induction xs) (auto simp: sorted_mid_iff2) 146 147end 148