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