author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 67929 | 30486b96274d |
child 70629 | 2bbd945728e2 |
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 |
||
33 |
lemmas isin_simps = sorted_lems 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 |
||
67929 | 43 |
lemma set_ins_list: "set (ins_list x xs) = insert x (set xs)" |
61640 | 44 |
by(induction xs) auto |
45 |
||
46 |
lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs" |
|
67168 | 47 |
apply(induction xs rule: induct_list012) |
61640 | 48 |
apply auto |
49 |
by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2) |
|
50 |
||
51 |
lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)" |
|
67168 | 52 |
by(induction xs rule: induct_list012) auto |
61640 | 53 |
|
54 |
lemma ins_list_sorted: "sorted (xs @ [a]) \<Longrightarrow> |
|
55 |
ins_list x (xs @ a # ys) = |
|
61642 | 56 |
(if x < a then ins_list x xs @ (a#ys) else xs @ ins_list x (a#ys))" |
61640 | 57 |
by(induction xs) (auto simp: sorted_lems) |
58 |
||
59 |
text\<open>In principle, @{thm ins_list_sorted} suffices, but the following two |
|
60 |
corollaries speed up proofs.\<close> |
|
61 |
||
62 |
corollary ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> |
|
63 |
ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)" |
|
61642 | 64 |
by(auto simp add: ins_list_sorted) |
61640 | 65 |
|
66 |
corollary ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow> |
|
67 |
ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)" |
|
68 |
by(auto simp: ins_list_sorted) |
|
69 |
||
70 |
lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 |
|
71 |
||
69597 | 72 |
text\<open>Splay trees need two additional \<^const>\<open>ins_list\<close> lemmas:\<close> |
61696 | 73 |
|
74 |
lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs" |
|
75 |
by (induction xs) auto |
|
76 |
||
77 |
lemma ins_list_snoc: "sorted (xs @ [x]) \<Longrightarrow> ins_list x xs = xs @ [x]" |
|
78 |
by(induction xs) (auto simp add: sorted_mid_iff2) |
|
79 |
||
61640 | 80 |
|
81 |
subsection \<open>Delete one occurrence of an element from a list:\<close> |
|
82 |
||
83 |
fun 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 |
||
67929 | 87 |
lemma del_list_idem: "x \<notin> set xs \<Longrightarrow> del_list x xs = xs" |
61640 | 88 |
by (induct xs) simp_all |
89 |
||
67929 | 90 |
lemma set_del_list_eq: |
91 |
"distinct xs \<Longrightarrow> set (del_list x xs) = set xs - {x}" |
|
92 |
by(induct xs) auto |
|
61640 | 93 |
|
94 |
lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)" |
|
67168 | 95 |
apply(induction xs rule: induct_list012) |
61640 | 96 |
apply auto |
97 |
by (meson order.strict_trans sorted_Cons_iff) |
|
98 |
||
99 |
lemma 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))" |
|
101 |
by(induction xs) |
|
67929 | 102 |
(fastforce simp: sorted_lems sorted_Cons_iff intro!: del_list_idem)+ |
61640 | 103 |
|
104 |
text\<open>In principle, @{thm del_list_sorted} suffices, but the following |
|
105 |
corollaries speed up proofs.\<close> |
|
106 |
||
107 |
corollary 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)" |
|
109 |
by (auto simp: del_list_sorted) |
|
110 |
||
111 |
corollary del_list_sorted2: "sorted (xs @ a # ys) \<Longrightarrow> x < a \<Longrightarrow> |
|
112 |
del_list x (xs @ a # ys) = del_list x xs @ a # ys" |
|
113 |
by (auto simp: del_list_sorted) |
|
114 |
||
115 |
corollary 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" |
|
118 |
by (auto simp: del_list_sorted sorted_lems) |
|
119 |
||
120 |
corollary 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" |
|
123 |
by (auto simp: del_list_sorted sorted_lems) |
|
124 |
||
125 |
corollary 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" |
|
129 |
by (auto simp: del_list_sorted sorted_lems) |
|
130 |
||
131 |
lemmas 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 |
||
69597 | 138 |
text\<open>Splay trees need two additional \<^const>\<open>del_list\<close> lemmas:\<close> |
61696 | 139 |
|
140 |
lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs" |
|
66441 | 141 |
by(induction xs)(fastforce simp: sorted_Cons_iff)+ |
61696 | 142 |
|
143 |
lemma del_list_sorted_app: |
|
144 |
"sorted(xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys" |
|
145 |
by (induction xs) (auto simp: sorted_mid_iff2) |
|
146 |
||
61640 | 147 |
end |