summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Sublist.thy

author | blanchet |

Wed Nov 20 18:58:00 2013 +0100 (2013-11-20) | |

changeset 54538 | ba7392b52a7c |

parent 54483 | 9f24325c2550 |

child 55579 | 207538943038 |

permissions | -rw-r--r-- |

factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)

1 (* Title: HOL/Library/Sublist.thy

2 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen

3 Author: Christian Sternagel, JAIST

4 *)

6 header {* Parallel lists, list suffixes, and homeomorphic embedding *}

8 theory Sublist

9 imports Main

10 begin

12 subsection {* Parallel lists *}

14 definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "\<parallel>" 50)

15 where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"

17 lemma parallelI [intro]: "\<not> prefixeq xs ys \<Longrightarrow> \<not> prefixeq ys xs \<Longrightarrow> xs \<parallel> ys"

18 unfolding parallel_def by blast

20 lemma parallelE [elim]:

21 assumes "xs \<parallel> ys"

22 obtains "\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs"

23 using assms unfolding parallel_def by blast

25 theorem prefixeq_cases:

26 obtains "prefixeq xs ys" | "prefix ys xs" | "xs \<parallel> ys"

27 unfolding parallel_def prefix_def by blast

29 theorem parallel_decomp:

30 "xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"

31 proof (induct xs rule: rev_induct)

32 case Nil

33 then have False by auto

34 then show ?case ..

35 next

36 case (snoc x xs)

37 show ?case

38 proof (rule prefixeq_cases)

39 assume le: "prefixeq xs ys"

40 then obtain ys' where ys: "ys = xs @ ys'" ..

41 show ?thesis

42 proof (cases ys')

43 assume "ys' = []"

44 then show ?thesis by (metis append_Nil2 parallelE prefixeqI snoc.prems ys)

45 next

46 fix c cs assume ys': "ys' = c # cs"

47 have "x \<noteq> c" using snoc.prems ys ys' by fastforce

48 thus "\<exists>as b bs c cs. b \<noteq> c \<and> xs @ [x] = as @ b # bs \<and> ys = as @ c # cs"

49 using ys ys' by blast

50 qed

51 next

52 assume "prefix ys xs"

53 then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def)

54 with snoc have False by blast

55 then show ?thesis ..

56 next

57 assume "xs \<parallel> ys"

58 with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"

59 and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"

60 by blast

61 from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp

62 with neq ys show ?thesis by blast

63 qed

64 qed

66 lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"

67 apply (rule parallelI)

68 apply (erule parallelE, erule conjE,

69 induct rule: not_prefixeq_induct, simp+)+

70 done

72 lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"

73 by (simp add: parallel_append)

75 lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a"

76 unfolding parallel_def by auto

79 subsection {* Suffix order on lists *}

81 definition suffixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

82 where "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)"

84 definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

85 where "suffix xs ys \<longleftrightarrow> (\<exists>us. ys = us @ xs \<and> us \<noteq> [])"

87 lemma suffix_imp_suffixeq:

88 "suffix xs ys \<Longrightarrow> suffixeq xs ys"

89 by (auto simp: suffixeq_def suffix_def)

91 lemma suffixeqI [intro?]: "ys = zs @ xs \<Longrightarrow> suffixeq xs ys"

92 unfolding suffixeq_def by blast

94 lemma suffixeqE [elim?]:

95 assumes "suffixeq xs ys"

96 obtains zs where "ys = zs @ xs"

97 using assms unfolding suffixeq_def by blast

99 lemma suffixeq_refl [iff]: "suffixeq xs xs"

100 by (auto simp add: suffixeq_def)

101 lemma suffix_trans:

102 "suffix xs ys \<Longrightarrow> suffix ys zs \<Longrightarrow> suffix xs zs"

103 by (auto simp: suffix_def)

104 lemma suffixeq_trans: "\<lbrakk>suffixeq xs ys; suffixeq ys zs\<rbrakk> \<Longrightarrow> suffixeq xs zs"

105 by (auto simp add: suffixeq_def)

106 lemma suffixeq_antisym: "\<lbrakk>suffixeq xs ys; suffixeq ys xs\<rbrakk> \<Longrightarrow> xs = ys"

107 by (auto simp add: suffixeq_def)

109 lemma suffixeq_tl [simp]: "suffixeq (tl xs) xs"

110 by (induct xs) (auto simp: suffixeq_def)

112 lemma suffix_tl [simp]: "xs \<noteq> [] \<Longrightarrow> suffix (tl xs) xs"

113 by (induct xs) (auto simp: suffix_def)

115 lemma Nil_suffixeq [iff]: "suffixeq [] xs"

116 by (simp add: suffixeq_def)

117 lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])"

118 by (auto simp add: suffixeq_def)

120 lemma suffixeq_ConsI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (y # ys)"

121 by (auto simp add: suffixeq_def)

122 lemma suffixeq_ConsD: "suffixeq (x # xs) ys \<Longrightarrow> suffixeq xs ys"

123 by (auto simp add: suffixeq_def)

125 lemma suffixeq_appendI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (zs @ ys)"

126 by (auto simp add: suffixeq_def)

127 lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \<Longrightarrow> suffixeq xs ys"

128 by (auto simp add: suffixeq_def)

130 lemma suffix_set_subset:

131 "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffix_def)

133 lemma suffixeq_set_subset:

134 "suffixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffixeq_def)

136 lemma suffixeq_ConsD2: "suffixeq (x # xs) (y # ys) \<Longrightarrow> suffixeq xs ys"

137 proof -

138 assume "suffixeq (x # xs) (y # ys)"

139 then obtain zs where "y # ys = zs @ x # xs" ..

140 then show ?thesis

141 by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI)

142 qed

144 lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \<longleftrightarrow> prefixeq (rev xs) (rev ys)"

145 proof

146 assume "suffixeq xs ys"

147 then obtain zs where "ys = zs @ xs" ..

148 then have "rev ys = rev xs @ rev zs" by simp

149 then show "prefixeq (rev xs) (rev ys)" ..

150 next

151 assume "prefixeq (rev xs) (rev ys)"

152 then obtain zs where "rev ys = rev xs @ zs" ..

153 then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp

154 then have "ys = rev zs @ xs" by simp

155 then show "suffixeq xs ys" ..

156 qed

158 lemma distinct_suffixeq: "distinct ys \<Longrightarrow> suffixeq xs ys \<Longrightarrow> distinct xs"

159 by (clarsimp elim!: suffixeqE)

161 lemma suffixeq_map: "suffixeq xs ys \<Longrightarrow> suffixeq (map f xs) (map f ys)"

162 by (auto elim!: suffixeqE intro: suffixeqI)

164 lemma suffixeq_drop: "suffixeq (drop n as) as"

165 unfolding suffixeq_def

166 apply (rule exI [where x = "take n as"])

167 apply simp

168 done

170 lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs"

171 by (auto elim!: suffixeqE)

173 lemma suffixeq_suffix_reflclp_conv: "suffixeq = suffix\<^sup>=\<^sup>="

174 proof (intro ext iffI)

175 fix xs ys :: "'a list"

176 assume "suffixeq xs ys"

177 show "suffix\<^sup>=\<^sup>= xs ys"

178 proof

179 assume "xs \<noteq> ys"

180 with `suffixeq xs ys` show "suffix xs ys"

181 by (auto simp: suffixeq_def suffix_def)

182 qed

183 next

184 fix xs ys :: "'a list"

185 assume "suffix\<^sup>=\<^sup>= xs ys"

186 then show "suffixeq xs ys"

187 proof

188 assume "suffix xs ys" then show "suffixeq xs ys"

189 by (rule suffix_imp_suffixeq)

190 next

191 assume "xs = ys" then show "suffixeq xs ys"

192 by (auto simp: suffixeq_def)

193 qed

194 qed

196 lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefixeq x y"

197 by blast

199 lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefixeq y x"

200 by blast

202 lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"

203 unfolding parallel_def by simp

205 lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"

206 unfolding parallel_def by simp

208 lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs"

209 by auto

211 lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"

212 by (metis Cons_prefixeq_Cons parallelE parallelI)

214 lemma not_equal_is_parallel:

215 assumes neq: "xs \<noteq> ys"

216 and len: "length xs = length ys"

217 shows "xs \<parallel> ys"

218 using len neq

219 proof (induct rule: list_induct2)

220 case Nil

221 then show ?case by simp

222 next

223 case (Cons a as b bs)

224 have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact

225 show ?case

226 proof (cases "a = b")

227 case True

228 then have "as \<noteq> bs" using Cons by simp

229 then show ?thesis by (rule Cons_parallelI2 [OF True ih])

230 next

231 case False

232 then show ?thesis by (rule Cons_parallelI1)

233 qed

234 qed

236 lemma suffix_reflclp_conv: "suffix\<^sup>=\<^sup>= = suffixeq"

237 by (intro ext) (auto simp: suffixeq_def suffix_def)

239 lemma suffix_lists: "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A"

240 unfolding suffix_def by auto

243 subsection {* Homeomorphic embedding on lists *}

245 inductive list_hembeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"

246 for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"

247 where

248 list_hembeq_Nil [intro, simp]: "list_hembeq P [] ys"

249 | list_hembeq_Cons [intro] : "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (y#ys)"

250 | list_hembeq_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_hembeq P xs ys \<Longrightarrow> list_hembeq P (x#xs) (y#ys)"

252 lemma list_hembeq_Nil2 [simp]:

253 assumes "list_hembeq P xs []" shows "xs = []"

254 using assms by (cases rule: list_hembeq.cases) auto

256 lemma list_hembeq_refl [simp, intro!]:

257 "list_hembeq P xs xs"

258 by (induct xs) auto

260 lemma list_hembeq_Cons_Nil [simp]: "list_hembeq P (x#xs) [] = False"

261 proof -

262 { assume "list_hembeq P (x#xs) []"

263 from list_hembeq_Nil2 [OF this] have False by simp

264 } moreover {

265 assume False

266 then have "list_hembeq P (x#xs) []" by simp

267 } ultimately show ?thesis by blast

268 qed

270 lemma list_hembeq_append2 [intro]: "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (zs @ ys)"

271 by (induct zs) auto

273 lemma list_hembeq_prefix [intro]:

274 assumes "list_hembeq P xs ys" shows "list_hembeq P xs (ys @ zs)"

275 using assms

276 by (induct arbitrary: zs) auto

278 lemma list_hembeq_ConsD:

279 assumes "list_hembeq P (x#xs) ys"

280 shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_hembeq P xs vs"

281 using assms

282 proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)

283 case list_hembeq_Cons

284 then show ?case by (metis append_Cons)

285 next

286 case (list_hembeq_Cons2 x y xs ys)

287 then show ?case by blast

288 qed

290 lemma list_hembeq_appendD:

291 assumes "list_hembeq P (xs @ ys) zs"

292 shows "\<exists>us vs. zs = us @ vs \<and> list_hembeq P xs us \<and> list_hembeq P ys vs"

293 using assms

294 proof (induction xs arbitrary: ys zs)

295 case Nil then show ?case by auto

296 next

297 case (Cons x xs)

298 then obtain us v vs where

299 zs: "zs = us @ v # vs" and p: "P\<^sup>=\<^sup>= x v" and lh: "list_hembeq P (xs @ ys) vs"

300 by (auto dest: list_hembeq_ConsD)

301 obtain sk\<^sub>0 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" and sk\<^sub>1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

302 sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_hembeq P (xs @ x\<^sub>0) x\<^sub>1 \<or> sk\<^sub>0 x\<^sub>0 x\<^sub>1 @ sk\<^sub>1 x\<^sub>0 x\<^sub>1 = x\<^sub>1 \<and> list_hembeq P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_hembeq P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)"

303 using Cons(1) by (metis (no_types))

304 hence "\<forall>x\<^sub>2. list_hembeq P (x # xs) (x\<^sub>2 @ v # sk\<^sub>0 ys vs)" using p lh by auto

305 thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc)

306 qed

308 lemma list_hembeq_suffix:

309 assumes "list_hembeq P xs ys" and "suffix ys zs"

310 shows "list_hembeq P xs zs"

311 using assms(2) and list_hembeq_append2 [OF assms(1)] by (auto simp: suffix_def)

313 lemma list_hembeq_suffixeq:

314 assumes "list_hembeq P xs ys" and "suffixeq ys zs"

315 shows "list_hembeq P xs zs"

316 using assms and list_hembeq_suffix unfolding suffixeq_suffix_reflclp_conv by auto

318 lemma list_hembeq_length: "list_hembeq P xs ys \<Longrightarrow> length xs \<le> length ys"

319 by (induct rule: list_hembeq.induct) auto

321 lemma list_hembeq_trans:

322 assumes "\<And>x y z. \<lbrakk>x \<in> A; y \<in> A; z \<in> A; P x y; P y z\<rbrakk> \<Longrightarrow> P x z"

323 shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A;

324 list_hembeq P xs ys; list_hembeq P ys zs\<rbrakk> \<Longrightarrow> list_hembeq P xs zs"

325 proof -

326 fix xs ys zs

327 assume "list_hembeq P xs ys" and "list_hembeq P ys zs"

328 and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"

329 then show "list_hembeq P xs zs"

330 proof (induction arbitrary: zs)

331 case list_hembeq_Nil show ?case by blast

332 next

333 case (list_hembeq_Cons xs ys y)

334 from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs

335 where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast

336 then have "list_hembeq P ys (v#vs)" by blast

337 then have "list_hembeq P ys zs" unfolding zs by (rule list_hembeq_append2)

338 from list_hembeq_Cons.IH [OF this] and list_hembeq_Cons.prems show ?case by simp

339 next

340 case (list_hembeq_Cons2 x y xs ys)

341 from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs

342 where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast

343 with list_hembeq_Cons2 have "list_hembeq P xs vs" by simp

344 moreover have "P\<^sup>=\<^sup>= x v"

345 proof -

346 from zs and `zs \<in> lists A` have "v \<in> A" by auto

347 moreover have "x \<in> A" and "y \<in> A" using list_hembeq_Cons2 by simp_all

348 ultimately show ?thesis

349 using `P\<^sup>=\<^sup>= x y` and `P\<^sup>=\<^sup>= y v` and assms

350 by blast

351 qed

352 ultimately have "list_hembeq P (x#xs) (v#vs)" by blast

353 then show ?case unfolding zs by (rule list_hembeq_append2)

354 qed

355 qed

358 subsection {* Sublists (special case of homeomorphic embedding) *}

360 abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

361 where "sublisteq xs ys \<equiv> list_hembeq (op =) xs ys"

363 lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto

365 lemma sublisteq_same_length:

366 assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys"

367 using assms by (induct) (auto dest: list_hembeq_length)

369 lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"

370 by (metis list_hembeq_length linorder_not_less)

372 lemma [code]:

373 "list_hembeq P [] ys \<longleftrightarrow> True"

374 "list_hembeq P (x#xs) [] \<longleftrightarrow> False"

375 by (simp_all)

377 lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"

378 by (induct xs, simp, blast dest: list_hembeq_ConsD)

380 lemma sublisteq_Cons2':

381 assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"

382 using assms by (cases) (rule sublisteq_Cons')

384 lemma sublisteq_Cons2_neq:

385 assumes "sublisteq (x#xs) (y#ys)"

386 shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys"

387 using assms by (cases) auto

389 lemma sublisteq_Cons2_iff [simp, code]:

390 "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"

391 by (metis list_hembeq_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)

393 lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"

394 by (induct zs) simp_all

396 lemma sublisteq_refl [simp, intro!]: "sublisteq xs xs" by (induct xs) simp_all

398 lemma sublisteq_antisym:

399 assumes "sublisteq xs ys" and "sublisteq ys xs"

400 shows "xs = ys"

401 using assms

402 proof (induct)

403 case list_hembeq_Nil

404 from list_hembeq_Nil2 [OF this] show ?case by simp

405 next

406 case list_hembeq_Cons2

407 thus ?case by simp

408 next

409 case list_hembeq_Cons

410 hence False using sublisteq_Cons' by fastforce

411 thus ?case ..

412 qed

414 lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"

415 by (rule list_hembeq_trans [of UNIV "op ="]) auto

417 lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"

418 by (auto dest: list_hembeq_length)

420 lemma list_hembeq_append_mono:

421 "\<lbrakk> list_hembeq P xs xs'; list_hembeq P ys ys' \<rbrakk> \<Longrightarrow> list_hembeq P (xs@ys) (xs'@ys')"

422 apply (induct rule: list_hembeq.induct)

423 apply (metis eq_Nil_appendI list_hembeq_append2)

424 apply (metis append_Cons list_hembeq_Cons)

425 apply (metis append_Cons list_hembeq_Cons2)

426 done

429 subsection {* Appending elements *}

431 lemma sublisteq_append [simp]:

432 "sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r")

433 proof

434 { fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'"

435 then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys"

436 proof (induct arbitrary: xs ys zs)

437 case list_hembeq_Nil show ?case by simp

438 next

439 case (list_hembeq_Cons xs' ys' x)

440 { assume "ys=[]" then have ?case using list_hembeq_Cons(1) by auto }

441 moreover

442 { fix us assume "ys = x#us"

443 then have ?case using list_hembeq_Cons(2) by(simp add: list_hembeq.list_hembeq_Cons) }

444 ultimately show ?case by (auto simp:Cons_eq_append_conv)

445 next

446 case (list_hembeq_Cons2 x y xs' ys')

447 { assume "xs=[]" then have ?case using list_hembeq_Cons2(1) by auto }

448 moreover

449 { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_hembeq_Cons2 by auto}

450 moreover

451 { fix us assume "xs=x#us" "ys=[]" then have ?case using list_hembeq_Cons2(2) by bestsimp }

452 ultimately show ?case using `op =\<^sup>=\<^sup>= x y` by (auto simp: Cons_eq_append_conv)

453 qed }

454 moreover assume ?l

455 ultimately show ?r by blast

456 next

457 assume ?r then show ?l by (metis list_hembeq_append_mono sublisteq_refl)

458 qed

460 lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"

461 by (induct zs) auto

463 lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"

464 by (metis append_Nil2 list_hembeq_Nil list_hembeq_append_mono)

467 subsection {* Relation to standard list operations *}

469 lemma sublisteq_map:

470 assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)"

471 using assms by (induct) auto

473 lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs"

474 by (induct xs) auto

476 lemma sublisteq_filter [simp]:

477 assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)"

478 using assms by induct auto

480 lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")

481 proof

482 assume ?L

483 then show ?R

484 proof (induct)

485 case list_hembeq_Nil show ?case by (metis sublist_empty)

486 next

487 case (list_hembeq_Cons xs ys x)

488 then obtain N where "xs = sublist ys N" by blast

489 then have "xs = sublist (x#ys) (Suc ` N)"

490 by (clarsimp simp add:sublist_Cons inj_image_mem_iff)

491 then show ?case by blast

492 next

493 case (list_hembeq_Cons2 x y xs ys)

494 then obtain N where "xs = sublist ys N" by blast

495 then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"

496 by (clarsimp simp add:sublist_Cons inj_image_mem_iff)

497 moreover from list_hembeq_Cons2 have "x = y" by simp

498 ultimately show ?case by blast

499 qed

500 next

501 assume ?R

502 then obtain N where "xs = sublist ys N" ..

503 moreover have "sublisteq (sublist ys N) ys"

504 proof (induct ys arbitrary: N)

505 case Nil show ?case by simp

506 next

507 case Cons then show ?case by (auto simp: sublist_Cons)

508 qed

509 ultimately show ?L by simp

510 qed

512 end