|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 section {* List Insertion and Deletion *} |
|
4 |
|
5 theory List_Ins_Del |
|
6 imports Sorted_Less |
|
7 begin |
|
8 |
|
9 subsection \<open>Elements in a list\<close> |
|
10 |
|
11 fun elems :: "'a list \<Rightarrow> 'a set" where |
|
12 "elems [] = {}" | |
|
13 "elems (x#xs) = Set.insert x (elems xs)" |
|
14 |
|
15 lemma elems_app: "elems (xs @ ys) = (elems xs \<union> elems ys)" |
|
16 by (induction xs) auto |
|
17 |
|
18 lemma elems_eq_set: "elems xs = set xs" |
|
19 by (induction xs) auto |
|
20 |
|
21 lemma sorted_Cons_iff: |
|
22 "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> elems xs. x < y))" |
|
23 by(simp add: elems_eq_set Sorted_Less.sorted_Cons_iff) |
|
24 |
|
25 lemma sorted_snoc_iff: |
|
26 "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))" |
|
27 by(simp add: elems_eq_set Sorted_Less.sorted_snoc_iff) |
|
28 |
|
29 lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> y < x" |
|
30 by (simp add: sorted_Cons_iff) |
|
31 |
|
32 lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> x < y" |
|
33 by (simp add: sorted_snoc_iff) |
|
34 |
|
35 lemmas elems_simps0 = sorted_lems elems_app |
|
36 lemmas elems_simps = elems_simps0 sorted_Cons_iff sorted_snoc_iff |
|
37 lemmas sortedD = sorted_ConsD sorted_snocD |
|
38 |
|
39 |
|
40 subsection \<open>Inserting into an ordered list without duplicates:\<close> |
|
41 |
|
42 fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
43 "ins_list x [] = [x]" | |
|
44 "ins_list x (y#zs) = |
|
45 (if x < y then x#y#zs else if x=y then x#zs else y # ins_list x zs)" |
|
46 |
|
47 lemma set_ins_list[simp]: "elems (ins_list x xs) = insert x (elems xs)" |
|
48 by(induction xs) auto |
|
49 |
|
50 lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs" |
|
51 apply(induction xs rule: sorted.induct) |
|
52 apply auto |
|
53 by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2) |
|
54 |
|
55 lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)" |
|
56 by(induction xs rule: sorted.induct) auto |
|
57 |
|
58 lemma ins_list_sorted1: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> |
|
59 ins_list x (xs @ y # ys) = xs @ ins_list x (y#ys)" |
|
60 by(induction xs) (auto simp: sorted_lems) |
|
61 |
|
62 lemma ins_list_sorted2: "sorted (xs @ [y]) \<Longrightarrow> x < y \<Longrightarrow> |
|
63 ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)" |
|
64 by(induction xs) (auto simp: sorted_lems) |
|
65 |
|
66 lemmas ins_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 |
|
67 |
|
68 |
|
69 subsection \<open>Delete one occurrence of an element from a list:\<close> |
|
70 |
|
71 fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
72 "del_list a [] = []" | |
|
73 "del_list a (x#xs) = (if a=x then xs else x # del_list a xs)" |
|
74 |
|
75 lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs" |
|
76 by (induct xs) simp_all |
|
77 |
|
78 lemma elems_del_list_eq [simp]: |
|
79 "distinct xs \<Longrightarrow> elems (del_list x xs) = elems xs - {x}" |
|
80 apply(induct xs) |
|
81 apply simp |
|
82 apply (simp add: elems_eq_set) |
|
83 apply blast |
|
84 done |
|
85 |
|
86 lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)" |
|
87 apply(induction xs rule: sorted.induct) |
|
88 apply auto |
|
89 by (meson order.strict_trans sorted_Cons_iff) |
|
90 |
|
91 lemma del_list_sorted1: "sorted (xs @ [x]) \<Longrightarrow> x \<le> y \<Longrightarrow> |
|
92 del_list y (xs @ x # ys) = xs @ del_list y (x # ys)" |
|
93 by (induction xs) (auto simp: sorted_mid_iff2) |
|
94 |
|
95 lemma del_list_sorted2: "sorted (xs @ x # ys) \<Longrightarrow> y < x \<Longrightarrow> |
|
96 del_list y (xs @ x # ys) = del_list y xs @ x # ys" |
|
97 by (induction xs) (auto simp: sorted_Cons_iff intro!: del_list_idem) |
|
98 |
|
99 lemma del_list_sorted3: |
|
100 "sorted (xs @ x # ys @ y # zs) \<Longrightarrow> a < y \<Longrightarrow> |
|
101 del_list a (xs @ x # ys @ y # zs) = del_list a (xs @ x # ys) @ y # zs" |
|
102 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2) |
|
103 |
|
104 lemma del_list_sorted4: |
|
105 "sorted (xs @ x # ys @ y # zs @ z # us) \<Longrightarrow> a < z \<Longrightarrow> |
|
106 del_list a (xs @ x # ys @ y # zs @ z # us) = del_list a (xs @ x # ys @ y # zs) @ z # us" |
|
107 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3) |
|
108 |
|
109 lemma del_list_sorted5: |
|
110 "sorted (xs @ x # ys @ y # zs @ z # us @ u # vs) \<Longrightarrow> a < u \<Longrightarrow> |
|
111 del_list a (xs @ x # ys @ y # zs @ z # us @ u # vs) = |
|
112 del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs" |
|
113 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4) |
|
114 |
|
115 lemmas del_simps = sorted_lems |
|
116 del_list_sorted1 |
|
117 del_list_sorted2 |
|
118 del_list_sorted3 |
|
119 del_list_sorted4 |
|
120 del_list_sorted5 |
|
121 |
|
122 end |