19 |
21 |
20 instantiation list :: (type) ord |
22 instantiation list :: (type) ord |
21 begin |
23 begin |
22 |
24 |
23 definition |
25 definition |
24 "(xs :: 'a list) \<le> ys \<longleftrightarrow> emb (op =) xs ys" |
26 "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys" |
25 |
27 |
26 definition |
28 definition |
27 "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" |
29 "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" |
28 |
30 |
29 instance proof qed |
31 instance .. |
30 |
32 |
31 end |
33 end |
32 |
34 |
33 lemma empty [simp, intro!]: "[] \<le> xs" by (auto simp: less_eq_list_def) |
35 instance list :: (type) order |
34 |
36 proof |
35 lemma drop: "xs \<le> ys \<Longrightarrow> xs \<le> (y # ys)" |
|
36 by (unfold less_eq_list_def) blast |
|
37 |
|
38 lemma take: "xs \<le> ys \<Longrightarrow> (x#xs) \<le> (x#ys)" |
|
39 by (unfold less_eq_list_def) blast |
|
40 |
|
41 lemmas le_list_induct [consumes 1, case_names empty drop take] = |
|
42 emb.induct [of "op =", folded less_eq_list_def] |
|
43 |
|
44 lemmas le_list_cases [consumes 1, case_names empty drop take] = |
|
45 emb.cases [of "op =", folded less_eq_list_def] |
|
46 |
|
47 lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys" |
|
48 by (induct rule: le_list_induct) auto |
|
49 |
|
50 lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys" |
|
51 by (induct rule: le_list_induct) (auto dest: le_list_length) |
|
52 |
|
53 lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys" |
|
54 by (metis le_list_length linorder_not_less) |
|
55 |
|
56 lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []" |
|
57 by (auto dest: le_list_length) |
|
58 |
|
59 lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys" |
|
60 by (induct zs) (auto simp: less_eq_list_def) |
|
61 |
|
62 lemma [code]: "[] <= xs \<longleftrightarrow> True" |
|
63 by (simp add: less_eq_list_def) |
|
64 |
|
65 lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False" |
|
66 by simp |
|
67 |
|
68 lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys" |
|
69 proof- |
|
70 { fix xs' ys' |
|
71 assume "xs' <= ys" |
|
72 hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys" |
|
73 proof (induct rule: le_list_induct) |
|
74 case empty thus ?case by simp |
|
75 next |
|
76 note drop' = drop |
|
77 case drop thus ?case by (metis drop') |
|
78 next |
|
79 note t = take |
|
80 case take thus ?case by (simp add: drop) |
|
81 qed } |
|
82 from this[OF assms] show ?thesis by simp |
|
83 qed |
|
84 |
|
85 lemma le_list_drop_Cons2: |
|
86 assumes "x#xs <= x#ys" shows "xs <= ys" |
|
87 using assms |
|
88 proof (cases rule: le_list_cases) |
|
89 case drop thus ?thesis by (metis le_list_drop_Cons list.inject) |
|
90 qed simp_all |
|
91 |
|
92 lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys" |
|
93 shows "x ~= y \<Longrightarrow> x # xs <= ys" |
|
94 using assms by (cases rule: le_list_cases) auto |
|
95 |
|
96 lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow> |
|
97 (if x=y then xs <= ys else (x#xs) <= ys)" |
|
98 by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq) |
|
99 |
|
100 lemma le_list_take_many_iff: "zs @ xs \<le> zs @ ys \<longleftrightarrow> xs \<le> ys" |
|
101 by (induct zs) (auto intro: take) |
|
102 |
|
103 lemma le_list_Cons_EX: |
|
104 assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs" |
|
105 proof- |
|
106 { fix xys zs :: "'a list" assume "xys <= zs" |
|
107 hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)" |
|
108 proof (induct rule: le_list_induct) |
|
109 case empty show ?case by simp |
|
110 next |
|
111 case take thus ?case by (metis list.inject self_append_conv2) |
|
112 next |
|
113 case drop thus ?case by (metis append_eq_Cons_conv) |
|
114 qed |
|
115 } with assms show ?thesis by blast |
|
116 qed |
|
117 |
|
118 instantiation list :: (type) order |
|
119 begin |
|
120 |
|
121 instance proof |
|
122 fix xs ys :: "'a list" |
37 fix xs ys :: "'a list" |
123 show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. |
38 show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. |
124 next |
39 next |
125 fix xs :: "'a list" |
40 fix xs :: "'a list" |
126 show "xs \<le> xs" by (induct xs) (auto intro!: drop) |
41 show "xs \<le> xs" by (simp add: less_eq_list_def) |
127 next |
42 next |
128 fix xs ys :: "'a list" |
43 fix xs ys :: "'a list" |
129 assume "xs <= ys" |
44 assume "xs <= ys" and "ys <= xs" |
130 hence "ys <= xs \<longrightarrow> xs = ys" |
45 thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym) |
131 proof (induct rule: le_list_induct) |
|
132 case empty show ?case by simp |
|
133 next |
|
134 case take thus ?case by simp |
|
135 next |
|
136 case drop thus ?case |
|
137 by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n) |
|
138 qed |
|
139 moreover assume "ys <= xs" |
|
140 ultimately show "xs = ys" by blast |
|
141 next |
46 next |
142 fix xs ys zs :: "'a list" |
47 fix xs ys zs :: "'a list" |
143 assume "xs <= ys" |
48 assume "xs <= ys" and "ys <= zs" |
144 hence "ys <= zs \<longrightarrow> xs <= zs" |
49 thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans) |
145 proof (induct arbitrary:zs rule: le_list_induct) |
|
146 case empty show ?case by simp |
|
147 next |
|
148 note take' = take |
|
149 case (take x y xs ys) show ?case |
|
150 proof |
|
151 assume "y # ys <= zs" |
|
152 with take show "x # xs <= zs" |
|
153 by(metis le_list_Cons_EX le_list_drop_many take') |
|
154 qed |
|
155 next |
|
156 case drop thus ?case by (metis le_list_drop_Cons) |
|
157 qed |
|
158 moreover assume "ys <= zs" |
|
159 ultimately show "xs <= zs" by blast |
|
160 qed |
50 qed |
161 |
51 |
162 end |
|
163 |
|
164 lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]" |
|
165 by (auto dest: le_list_length) |
|
166 |
|
167 lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'" |
|
168 apply (induct rule: le_list_induct) |
|
169 apply (metis eq_Nil_appendI le_list_drop_many) |
|
170 apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans) |
|
171 apply simp |
|
172 done |
|
173 |
|
174 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
52 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" |
175 by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def) |
53 by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def) |
176 |
54 |
177 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" |
55 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" |
178 by (metis empty order_less_le) |
56 by (metis less_eq_list_def emb_Nil order_less_le) |
179 |
57 |
180 lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False" |
58 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False" |
181 by (metis empty less_list_def) |
59 by (metis emb_Nil less_eq_list_def less_list_def) |
182 |
60 |
183 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys" |
61 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys" |
184 by (unfold less_le) (auto intro: drop) |
62 by (unfold less_le less_eq_list_def) (auto) |
185 |
63 |
186 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys" |
64 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys" |
187 by (metis le_list_Cons2_iff less_list_def) |
65 by (metis sub_Cons2_iff less_list_def less_eq_list_def) |
188 |
66 |
189 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" |
67 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" |
190 by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2) |
68 by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def) |
191 |
69 |
192 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys" |
70 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys" |
193 by (metis le_list_take_many_iff less_list_def) |
71 by (metis less_list_def less_eq_list_def sub_append') |
194 |
|
195 |
|
196 subsection {* Appending elements *} |
|
197 |
|
198 lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R") |
|
199 proof |
|
200 { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'" |
|
201 hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys" |
|
202 proof (induct arbitrary: xs ys zs rule: le_list_induct) |
|
203 case empty show ?case by simp |
|
204 next |
|
205 note drop' = drop |
|
206 case (drop xs' ys' x) |
|
207 { assume "ys=[]" hence ?case using drop(1) by auto } |
|
208 moreover |
|
209 { fix us assume "ys = x#us" |
|
210 hence ?case using drop(2) by(simp add: drop') } |
|
211 ultimately show ?case by (auto simp:Cons_eq_append_conv) |
|
212 next |
|
213 case (take x y xs' ys') |
|
214 { assume "xs=[]" hence ?case using take(1) by auto } |
|
215 moreover |
|
216 { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take by auto} |
|
217 moreover |
|
218 { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp } |
|
219 ultimately show ?case using `x = y` by (auto simp:Cons_eq_append_conv) |
|
220 qed } |
|
221 moreover assume ?L |
|
222 ultimately show ?R by blast |
|
223 next |
|
224 assume ?R thus ?L by(metis le_list_append_mono order_refl) |
|
225 qed |
|
226 |
72 |
227 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys" |
73 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys" |
228 by (unfold less_le) auto |
74 by (unfold less_le less_eq_list_def) auto |
229 |
|
230 lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs" |
|
231 by (metis append_Nil2 empty le_list_append_mono) |
|
232 |
|
233 |
|
234 subsection {* Relation to standard list operations *} |
|
235 |
|
236 lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys" |
|
237 by (induct rule: le_list_induct) (auto intro: drop) |
|
238 |
|
239 lemma le_list_filter_left[simp]: "filter f xs \<le> xs" |
|
240 by (induct xs) (auto intro: drop) |
|
241 |
|
242 lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys" |
|
243 by (induct rule: le_list_induct) (auto intro: drop) |
|
244 |
|
245 lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R") |
|
246 proof |
|
247 assume ?L |
|
248 thus ?R |
|
249 proof (induct rule: le_list_induct) |
|
250 case empty show ?case by (metis sublist_empty) |
|
251 next |
|
252 case (drop xs ys x) |
|
253 then obtain N where "xs = sublist ys N" by blast |
|
254 hence "xs = sublist (x#ys) (Suc ` N)" |
|
255 by (clarsimp simp add:sublist_Cons inj_image_mem_iff) |
|
256 thus ?case by blast |
|
257 next |
|
258 case (take x y xs ys) |
|
259 then obtain N where "xs = sublist ys N" by blast |
|
260 hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))" |
|
261 by (clarsimp simp add:sublist_Cons inj_image_mem_iff) |
|
262 thus ?case unfolding `x = y` by blast |
|
263 qed |
|
264 next |
|
265 assume ?R |
|
266 then obtain N where "xs = sublist ys N" .. |
|
267 moreover have "sublist ys N <= ys" |
|
268 proof (induct ys arbitrary:N) |
|
269 case Nil show ?case by simp |
|
270 next |
|
271 case Cons thus ?case by (auto simp add:sublist_Cons drop) |
|
272 qed |
|
273 ultimately show ?L by simp |
|
274 qed |
|
275 |
75 |
276 end |
76 end |