64 by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2) |
64 by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2) |
65 |
65 |
66 lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)" |
66 lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)" |
67 by(induction xs rule: sorted.induct) auto |
67 by(induction xs rule: sorted.induct) auto |
68 |
68 |
69 lemma ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> |
69 lemma ins_list_sorted: "sorted (xs @ [a]) \<Longrightarrow> |
70 ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)" |
70 ins_list x (xs @ a # ys) = |
|
71 (if a \<le> x then xs @ ins_list x (a#ys) else ins_list x xs @ (a#ys))" |
71 by(induction xs) (auto simp: sorted_lems) |
72 by(induction xs) (auto simp: sorted_lems) |
72 |
73 |
73 lemma ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow> |
74 text\<open>In principle, @{thm ins_list_sorted} suffices, but the following two |
|
75 corollaries speed up proofs.\<close> |
|
76 |
|
77 corollary ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> |
|
78 ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)" |
|
79 by(simp add: ins_list_sorted) |
|
80 |
|
81 corollary ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow> |
74 ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)" |
82 ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)" |
75 by(induction xs) (auto simp: sorted_lems) |
83 by(auto simp: ins_list_sorted) |
76 |
84 |
77 lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 |
85 lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 |
78 |
86 |
79 |
87 |
80 subsection \<open>Delete one occurrence of an element from a list:\<close> |
88 subsection \<open>Delete one occurrence of an element from a list:\<close> |
97 lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)" |
105 lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)" |
98 apply(induction xs rule: sorted.induct) |
106 apply(induction xs rule: sorted.induct) |
99 apply auto |
107 apply auto |
100 by (meson order.strict_trans sorted_Cons_iff) |
108 by (meson order.strict_trans sorted_Cons_iff) |
101 |
109 |
102 lemma del_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> |
110 lemma del_list_sorted: "sorted (xs @ a # ys) \<Longrightarrow> |
|
111 del_list x (xs @ a # ys) = (if x < a then del_list x xs @ a # ys else xs @ del_list x (a # ys))" |
|
112 by(induction xs) |
|
113 (fastforce simp: sorted_lems sorted_Cons_iff elems_eq_set intro!: del_list_idem)+ |
|
114 |
|
115 text\<open>In principle, @{thm del_list_sorted} suffices, but the following |
|
116 corollaries speed up proofs.\<close> |
|
117 |
|
118 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)" |
119 del_list x (xs @ a # ys) = xs @ del_list x (a # ys)" |
104 by (induction xs) (auto simp: sorted_mid_iff2) |
120 by (auto simp: del_list_sorted) |
105 |
121 |
106 lemma del_list_sorted2: "sorted (xs @ a # ys) \<Longrightarrow> x < a \<Longrightarrow> |
122 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" |
123 del_list x (xs @ a # ys) = del_list x xs @ a # ys" |
108 by (induction xs) (auto simp: sorted_Cons_iff intro!: del_list_idem) |
124 by (auto simp: del_list_sorted) |
109 |
125 |
110 lemma del_list_sorted3: |
126 corollary del_list_sorted3: |
111 "sorted (xs @ a # ys @ b # zs) \<Longrightarrow> x < b \<Longrightarrow> |
127 "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" |
128 del_list x (xs @ a # ys @ b # zs) = del_list x (xs @ a # ys) @ b # zs" |
113 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2) |
129 by (auto simp: del_list_sorted sorted_lems) |
114 |
130 |
115 lemma del_list_sorted4: |
131 corollary del_list_sorted4: |
116 "sorted (xs @ a # ys @ b # zs @ c # us) \<Longrightarrow> x < c \<Longrightarrow> |
132 "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" |
133 del_list x (xs @ a # ys @ b # zs @ c # us) = del_list x (xs @ a # ys @ b # zs) @ c # us" |
118 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3) |
134 by (auto simp: del_list_sorted sorted_lems) |
119 |
135 |
120 lemma del_list_sorted5: |
136 corollary del_list_sorted5: |
121 "sorted (xs @ a # ys @ b # zs @ c # us @ d # vs) \<Longrightarrow> x < d \<Longrightarrow> |
137 "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) = |
138 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" |
139 del_list x (xs @ a # ys @ b # zs @ c # us) @ d # vs" |
124 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4) |
140 by (auto simp: del_list_sorted sorted_lems) |
125 |
141 |
126 lemmas del_list_simps = sorted_lems |
142 lemmas del_list_simps = sorted_lems |
127 del_list_sorted1 |
143 del_list_sorted1 |
128 del_list_sorted2 |
144 del_list_sorted2 |
129 del_list_sorted3 |
145 del_list_sorted3 |