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

src/HOL/Library/List_Prefix.thy

author | haftmann |

Mon Jul 07 08:47:17 2008 +0200 (2008-07-07) | |

changeset 27487 | c8a6ce181805 |

parent 27368 | 9f90ac19e32b |

child 28562 | 4e74209f113e |

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

absolute imports of HOL/*.thy theories

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 Plain "~~/src/HOL/List"

10 begin

12 subsection {* Prefix order on lists *}

14 instantiation list :: (type) order

15 begin

17 definition

18 prefix_def [code func del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"

20 definition

21 strict_prefix_def [code func del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"

23 instance

24 by intro_classes (auto simp add: prefix_def strict_prefix_def)

26 end

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

29 unfolding prefix_def by blast

31 lemma prefixE [elim?]:

32 assumes "xs \<le> ys"

33 obtains zs where "ys = xs @ zs"

34 using assms unfolding prefix_def by blast

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

37 unfolding strict_prefix_def prefix_def by blast

39 lemma strict_prefixE' [elim?]:

40 assumes "xs < ys"

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

42 proof -

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

44 unfolding strict_prefix_def prefix_def by blast

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

46 qed

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

49 unfolding strict_prefix_def by blast

51 lemma strict_prefixE [elim?]:

52 fixes xs ys :: "'a list"

53 assumes "xs < ys"

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

55 using assms unfolding strict_prefix_def by blast

58 subsection {* Basic properties of prefixes *}

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

61 by (simp add: prefix_def)

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

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

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

67 proof

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

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

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

71 by (metis append_Nil2 butlast_append butlast_snoc prefixI zs)

72 next

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

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

75 by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7))

76 qed

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

79 by (auto simp add: prefix_def)

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

82 by (induct xs) simp_all

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

85 by (metis append_Nil2 append_self_conv order_eq_iff prefixI)

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

88 by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI)

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

91 by (auto simp add: prefix_def)

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

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

96 theorem prefix_append:

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

98 apply (induct zs rule: rev_induct)

99 apply force

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

101 apply (metis append_eq_appendI)

102 done

104 lemma append_one_prefix:

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

106 unfolding prefix_def

107 by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj

108 eq_Nil_appendI nth_drop')

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

111 by (auto simp add: prefix_def)

113 lemma prefix_same_cases:

114 "(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"

115 unfolding prefix_def by (metis append_eq_append_conv2)

117 lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"

118 by (auto simp add: prefix_def)

120 lemma take_is_prefix: "take n xs \<le> xs"

121 unfolding prefix_def by (metis append_take_drop_id)

123 lemma map_prefixI: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"

124 by (auto simp: prefix_def)

126 lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys"

127 by (auto simp: strict_prefix_def prefix_def)

129 lemma strict_prefix_simps [simp]:

130 "xs < [] = False"

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

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

133 by (simp_all add: strict_prefix_def cong: conj_cong)

135 lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys"

136 apply (induct n arbitrary: xs ys)

137 apply (case_tac ys, simp_all)[1]

138 apply (metis order_less_trans strict_prefixI take_is_prefix)

139 done

141 lemma not_prefix_cases:

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

143 obtains

144 (c1) "ps \<noteq> []" and "ls = []"

145 | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> as \<le> xs"

146 | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"

147 proof (cases ps)

148 case Nil then show ?thesis using pfx by simp

149 next

150 case (Cons a as)

151 note c = `ps = a#as`

152 show ?thesis

153 proof (cases ls)

154 case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil)

155 next

156 case (Cons x xs)

157 show ?thesis

158 proof (cases "x = a")

159 case True

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

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

162 next

163 case False

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

165 qed

166 qed

167 qed

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

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

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

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

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

174 shows "P ps ls" using np

175 proof (induct ls arbitrary: ps)

176 case Nil then show ?case

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

178 next

179 case (Cons y ys)

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

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

182 by (rule not_prefix_cases) auto

183 show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2)

184 qed

187 subsection {* Parallel lists *}

189 definition

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

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

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

194 unfolding parallel_def by blast

196 lemma parallelE [elim]:

197 assumes "xs \<parallel> ys"

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

199 using assms unfolding parallel_def by blast

201 theorem prefix_cases:

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

203 unfolding parallel_def strict_prefix_def by blast

205 theorem parallel_decomp:

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

207 proof (induct xs rule: rev_induct)

208 case Nil

209 then have False by auto

210 then show ?case ..

211 next

212 case (snoc x xs)

213 show ?case

214 proof (rule prefix_cases)

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

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

217 show ?thesis

218 proof (cases ys')

219 assume "ys' = []"

220 then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)

221 next

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

223 then show ?thesis

224 by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI

225 same_prefix_prefix snoc.prems ys)

226 qed

227 next

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

229 with snoc have False by blast

230 then show ?thesis ..

231 next

232 assume "xs \<parallel> ys"

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

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

235 by blast

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

237 with neq ys show ?thesis by blast

238 qed

239 qed

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

242 apply (rule parallelI)

243 apply (erule parallelE, erule conjE,

244 induct rule: not_prefix_induct, simp+)+

245 done

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

248 by (simp add: parallel_append)

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

251 unfolding parallel_def by auto

254 subsection {* Postfix order on lists *}

256 definition

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

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

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

261 unfolding postfix_def by blast

263 lemma postfixE [elim?]:

264 assumes "xs >>= ys"

265 obtains zs where "xs = zs @ ys"

266 using assms unfolding postfix_def by blast

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

269 by (auto simp add: postfix_def)

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

271 by (auto simp add: postfix_def)

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

273 by (auto simp add: postfix_def)

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

276 by (simp add: postfix_def)

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

278 by (auto simp add: postfix_def)

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

281 by (auto simp add: postfix_def)

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

283 by (auto simp add: postfix_def)

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

286 by (auto simp add: postfix_def)

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

288 by (auto simp add: postfix_def)

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

291 proof -

292 assume "xs >>= ys"

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

294 then show ?thesis by (induct zs) auto

295 qed

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

298 proof -

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

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

301 then show ?thesis

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

303 qed

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

306 proof

307 assume "xs >>= ys"

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

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

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

311 next

312 assume "rev ys <= rev xs"

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

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

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

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

317 qed

319 lemma distinct_postfix: "distinct xs \<Longrightarrow> xs >>= ys \<Longrightarrow> distinct ys"

320 by (clarsimp elim!: postfixE)

322 lemma postfix_map: "xs >>= ys \<Longrightarrow> map f xs >>= map f ys"

323 by (auto elim!: postfixE intro: postfixI)

325 lemma postfix_drop: "as >>= drop n as"

326 unfolding postfix_def

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

328 apply simp

329 done

331 lemma postfix_take: "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"

332 by (clarsimp elim!: postfixE)

334 lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y"

335 by blast

337 lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> y \<le> x"

338 by blast

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

341 unfolding parallel_def by simp

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

344 unfolding parallel_def by simp

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

347 by auto

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

350 by (metis Cons_prefix_Cons parallelE parallelI)

352 lemma not_equal_is_parallel:

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

354 and len: "length xs = length ys"

355 shows "xs \<parallel> ys"

356 using len neq

357 proof (induct rule: list_induct2)

358 case Nil

359 then show ?case by simp

360 next

361 case (Cons a as b bs)

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

363 show ?case

364 proof (cases "a = b")

365 case True

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

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

368 next

369 case False

370 then show ?thesis by (rule Cons_parallelI1)

371 qed

372 qed

375 subsection {* Executable code *}

377 lemma less_eq_code [code func]:

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

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

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

381 by simp_all

383 lemma less_code [code func]:

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

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

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

387 unfolding strict_prefix_def by auto

389 lemmas [code func] = postfix_to_prefix

391 end