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

src/HOL/Library/List_Prefix.thy

author | wenzelm |

Thu Nov 08 20:09:17 2007 +0100 (2007-11-08) | |

changeset 25355 | 69c0a39ba028 |

parent 25322 | e2eac0c30ff5 |

child 25356 | 059c03630d6e |

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

avoid implicit use of prems;

tuned proofs;

tuned proofs;

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

2 ID: $Id$

3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen

4 *)

6 header {* List prefixes and postfixes *}

8 theory List_Prefix

9 imports Main

10 begin

12 subsection {* Prefix order on lists *}

14 instance list :: (type) ord ..

16 defs (overloaded)

17 prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"

18 strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"

20 instance list :: (type) order

21 by intro_classes (auto simp add: prefix_def strict_prefix_def)

23 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"

24 unfolding prefix_def by blast

26 lemma prefixE [elim?]:

27 assumes "xs \<le> ys"

28 obtains zs where "ys = xs @ zs"

29 using assms unfolding prefix_def by blast

31 lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"

32 unfolding strict_prefix_def prefix_def by blast

34 lemma strict_prefixE' [elim?]:

35 assumes "xs < ys"

36 obtains z zs where "ys = xs @ z # zs"

37 proof -

38 from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"

39 unfolding strict_prefix_def prefix_def by blast

40 with that show ?thesis by (auto simp add: neq_Nil_conv)

41 qed

43 lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"

44 unfolding strict_prefix_def by blast

46 lemma strict_prefixE [elim?]:

47 fixes xs ys :: "'a list"

48 assumes "xs < ys"

49 obtains "xs \<le> ys" and "xs \<noteq> ys"

50 using assms unfolding strict_prefix_def by blast

53 subsection {* Basic properties of prefixes *}

55 theorem Nil_prefix [iff]: "[] \<le> xs"

56 by (simp add: prefix_def)

58 theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"

59 by (induct xs) (simp_all add: prefix_def)

61 lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"

62 proof

63 assume "xs \<le> ys @ [y]"

64 then obtain zs where zs: "ys @ [y] = xs @ zs" ..

65 show "xs = ys @ [y] \<or> xs \<le> ys"

66 proof (cases zs rule: rev_cases)

67 assume "zs = []"

68 with zs have "xs = ys @ [y]" by simp

69 then show ?thesis ..

70 next

71 fix z zs' assume "zs = zs' @ [z]"

72 with zs have "ys = xs @ zs'" by simp

73 then have "xs \<le> ys" ..

74 then show ?thesis ..

75 qed

76 next

77 assume "xs = ys @ [y] \<or> xs \<le> ys"

78 then show "xs \<le> ys @ [y]"

79 proof

80 assume "xs = ys @ [y]"

81 then show ?thesis by simp

82 next

83 assume "xs \<le> ys"

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

85 then have "ys @ [y] = xs @ (zs @ [y])" by simp

86 then show ?thesis ..

87 qed

88 qed

90 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"

91 by (auto simp add: prefix_def)

93 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"

94 by (induct xs) simp_all

96 lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"

97 proof -

98 have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix)

99 then show ?thesis by simp

100 qed

102 lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"

103 proof -

104 assume "xs \<le> ys"

105 then obtain us where "ys = xs @ us" ..

106 then have "ys @ zs = xs @ (us @ zs)" by simp

107 then show ?thesis ..

108 qed

110 lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"

111 by (auto simp add: prefix_def)

113 theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"

114 by (cases xs) (auto simp add: prefix_def)

116 theorem prefix_append:

117 "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"

118 apply (induct zs rule: rev_induct)

119 apply force

120 apply (simp del: append_assoc add: append_assoc [symmetric])

121 apply simp

122 apply blast

123 done

125 lemma append_one_prefix:

126 "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"

127 apply (unfold prefix_def)

128 apply (auto simp add: nth_append)

129 apply (case_tac zs)

130 apply auto

131 done

133 theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"

134 by (auto simp add: prefix_def)

136 lemma prefix_same_cases:

137 "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"

138 apply (simp add: prefix_def)

139 apply (erule exE)+

140 apply (simp add: append_eq_append_conv_if split: if_splits)

141 apply (rule disjI2)

142 apply (rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)

143 apply clarify

144 apply (drule sym)

145 apply (insert append_take_drop_id [of "length xs\<^isub>2" xs\<^isub>1])

146 apply simp

147 apply (rule disjI1)

148 apply (rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)

149 apply clarify

150 apply (insert append_take_drop_id [of "length xs\<^isub>1" xs\<^isub>2])

151 apply simp

152 done

154 lemma set_mono_prefix:

155 "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"

156 by (auto simp add: prefix_def)

158 lemma take_is_prefix:

159 "take n xs \<le> xs"

160 apply (simp add: prefix_def)

161 apply (rule_tac x="drop n xs" in exI)

162 apply simp

163 done

165 lemma map_prefixI:

166 "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"

167 by (clarsimp simp: prefix_def)

169 lemma prefix_length_less:

170 "xs < ys \<Longrightarrow> length xs < length ys"

171 apply (clarsimp simp: strict_prefix_def)

172 apply (frule prefix_length_le)

173 apply (rule ccontr, simp)

174 apply (clarsimp simp: prefix_def)

175 done

177 lemma strict_prefix_simps [simp]:

178 "xs < [] = False"

179 "[] < (x # xs) = True"

180 "(x # xs) < (y # ys) = (x = y \<and> xs < ys)"

181 by (simp_all add: strict_prefix_def cong: conj_cong)

183 lemma take_strict_prefix:

184 "xs < ys \<Longrightarrow> take n xs < ys"

185 apply (induct n arbitrary: xs ys)

186 apply (case_tac ys, simp_all)[1]

187 apply (case_tac xs, simp)

188 apply (case_tac ys, simp_all)

189 done

191 lemma not_prefix_cases:

192 assumes pfx: "\<not> ps \<le> ls"

193 and c1: "\<lbrakk> ps \<noteq> []; ls = [] \<rbrakk> \<Longrightarrow> R"

194 and c2: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x = a; \<not> as \<le> xs\<rbrakk> \<Longrightarrow> R"

195 and c3: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x \<noteq> a\<rbrakk> \<Longrightarrow> R"

196 shows "R"

197 proof (cases ps)

198 case Nil then show ?thesis using pfx by simp

199 next

200 case (Cons a as)

201 then have c: "ps = a#as" .

203 show ?thesis

204 proof (cases ls)

205 case Nil

206 have "ps \<noteq> []" by (simp add: Nil Cons)

207 from this and Nil show ?thesis by (rule c1)

208 next

209 case (Cons x xs)

210 show ?thesis

211 proof (cases "x = a")

212 case True

213 have "\<not> as \<le> xs" using pfx c Cons True by simp

214 with c Cons True show ?thesis by (rule c2)

215 next

216 case False

217 with c Cons show ?thesis by (rule c3)

218 qed

219 qed

220 qed

222 lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]:

223 assumes np: "\<not> ps \<le> ls"

224 and base: "\<And>x xs. P (x#xs) []"

225 and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"

226 and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"

227 shows "P ps ls"

228 using np

229 proof (induct ls arbitrary: ps)

230 case Nil then show ?case

231 by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)

232 next

233 case (Cons y ys)

234 then have npfx: "\<not> ps \<le> (y # ys)" by simp

235 then obtain x xs where pv: "ps = x # xs"

236 by (rule not_prefix_cases) auto

238 from Cons

239 have ih: "\<And>ps. \<not>ps \<le> ys \<Longrightarrow> P ps ys" by simp

241 show ?case using npfx

242 by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih)

243 qed

245 subsection {* Parallel lists *}

247 definition

248 parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) where

249 "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"

251 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"

252 unfolding parallel_def by blast

254 lemma parallelE [elim]:

255 assumes "xs \<parallel> ys"

256 obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"

257 using assms unfolding parallel_def by blast

259 theorem prefix_cases:

260 obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"

261 unfolding parallel_def strict_prefix_def by blast

263 theorem parallel_decomp:

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

265 proof (induct xs rule: rev_induct)

266 case Nil

267 then have False by auto

268 then show ?case ..

269 next

270 case (snoc x xs)

271 show ?case

272 proof (rule prefix_cases)

273 assume le: "xs \<le> ys"

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

275 show ?thesis

276 proof (cases ys')

277 assume "ys' = []" with ys have "xs = ys" by simp

278 with snoc have "[x] \<parallel> []" by auto

279 then have False by blast

280 then show ?thesis ..

281 next

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

283 with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)

284 then have "x \<noteq> c" by auto

285 moreover have "xs @ [x] = xs @ x # []" by simp

286 moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)

287 ultimately show ?thesis by blast

288 qed

289 next

290 assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)

291 with snoc have False by blast

292 then show ?thesis ..

293 next

294 assume "xs \<parallel> ys"

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

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

297 by blast

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

299 with neq ys show ?thesis by blast

300 qed

301 qed

303 lemma parallel_append:

304 "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"

305 by (rule parallelI)

306 (erule parallelE, erule conjE,

307 induct rule: not_prefix_induct, simp+)+

309 lemma parallel_appendI:

310 "\<lbrakk> xs \<parallel> ys; x = xs @ xs' ; y = ys @ ys' \<rbrakk> \<Longrightarrow> x \<parallel> y"

311 by simp (rule parallel_append)

313 lemma parallel_commute:

314 "(a \<parallel> b) = (b \<parallel> a)"

315 unfolding parallel_def by auto

317 subsection {* Postfix order on lists *}

319 definition

320 postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where

321 "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"

323 lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys"

324 unfolding postfix_def by blast

326 lemma postfixE [elim?]:

327 assumes "xs >>= ys"

328 obtains zs where "xs = zs @ ys"

329 using assms unfolding postfix_def by blast

331 lemma postfix_refl [iff]: "xs >>= xs"

332 by (auto simp add: postfix_def)

333 lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs"

334 by (auto simp add: postfix_def)

335 lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys"

336 by (auto simp add: postfix_def)

338 lemma Nil_postfix [iff]: "xs >>= []"

339 by (simp add: postfix_def)

340 lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])"

341 by (auto simp add: postfix_def)

343 lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys"

344 by (auto simp add: postfix_def)

345 lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys"

346 by (auto simp add: postfix_def)

348 lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys"

349 by (auto simp add: postfix_def)

350 lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys"

351 by (auto simp add: postfix_def)

353 lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs"

354 proof -

355 assume "xs >>= ys"

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

357 then show ?thesis by (induct zs) auto

358 qed

360 lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys"

361 proof -

362 assume "x#xs >>= y#ys"

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

364 then show ?thesis

365 by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)

366 qed

368 lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"

369 proof

370 assume "xs >>= ys"

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

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

373 then show "rev ys <= rev xs" ..

374 next

375 assume "rev ys <= rev xs"

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

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

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

379 then show "xs >>= ys" ..

380 qed

382 lemma distinct_postfix:

383 assumes dx: "distinct xs"

384 and pf: "xs >>= ys"

385 shows "distinct ys"

386 using dx pf by (clarsimp elim!: postfixE)

388 lemma postfix_map:

389 assumes pf: "xs >>= ys"

390 shows "map f xs >>= map f ys"

391 using pf by (auto elim!: postfixE intro: postfixI)

393 lemma postfix_drop:

394 "as >>= drop n as"

395 unfolding postfix_def

396 by (rule exI [where x = "take n as"]) simp

398 lemma postfix_take:

399 "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"

400 by (clarsimp elim!: postfixE)

402 lemma parallelD1:

403 "x \<parallel> y \<Longrightarrow> \<not> x \<le> y" by blast

405 lemma parallelD2:

406 "x \<parallel> y \<Longrightarrow> \<not> y \<le> x" by blast

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

409 unfolding parallel_def by simp

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

412 unfolding parallel_def by simp

414 lemma Cons_parallelI1:

415 "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" by auto

417 lemma Cons_parallelI2:

418 "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"

419 apply simp

420 apply (rule parallelI)

421 apply simp

422 apply (erule parallelD1)

423 apply simp

424 apply (erule parallelD2)

425 done

427 lemma not_equal_is_parallel:

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

429 and len: "length xs = length ys"

430 shows "xs \<parallel> ys"

431 using len neq

432 proof (induct rule: list_induct2)

433 case 1 then show ?case by simp

434 next

435 case (2 a as b bs)

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

438 show ?case

439 proof (cases "a = b")

440 case True

441 then have "as \<noteq> bs" using 2 by simp

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

443 next

444 case False

445 then show ?thesis by (rule Cons_parallelI1)

446 qed

447 qed

450 subsection {* Exeuctable code *}

452 lemma less_eq_code [code func]:

453 "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"

454 "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"

455 "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"

456 by simp_all

458 lemma less_code [code func]:

459 "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"

460 "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"

461 "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"

462 unfolding strict_prefix_def by auto

464 lemmas [code func] = postfix_to_prefix

466 end