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

src/HOL/Library/List_Prefix.thy

author | chaieb |

Mon Jun 11 11:06:04 2007 +0200 (2007-06-11) | |

changeset 23315 | df3a7e9ebadb |

parent 23254 | 99644a53f16d |

child 23394 | 474ff28210c0 |

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

tuned Proof

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 prems 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 prems 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)

159 subsection {* Parallel lists *}

161 definition

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

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

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

166 unfolding parallel_def by blast

168 lemma parallelE [elim]:

169 assumes "xs \<parallel> ys"

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

171 using prems unfolding parallel_def by blast

173 theorem prefix_cases:

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

175 unfolding parallel_def strict_prefix_def by blast

177 theorem parallel_decomp:

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

179 proof (induct xs rule: rev_induct)

180 case Nil

181 then have False by auto

182 then show ?case ..

183 next

184 case (snoc x xs)

185 show ?case

186 proof (rule prefix_cases)

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

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

189 show ?thesis

190 proof (cases ys')

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

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

193 then have False by blast

194 then show ?thesis ..

195 next

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

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

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

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

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

201 ultimately show ?thesis by blast

202 qed

203 next

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

205 with snoc have False by blast

206 then show ?thesis ..

207 next

208 assume "xs \<parallel> ys"

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

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

211 by blast

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

213 with neq ys show ?thesis by blast

214 qed

215 qed

218 subsection {* Postfix order on lists *}

220 definition

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

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

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

225 unfolding postfix_def by blast

227 lemma postfixE [elim?]:

228 assumes "xs >>= ys"

229 obtains zs where "xs = zs @ ys"

230 using prems unfolding postfix_def by blast

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

233 by (auto simp add: postfix_def)

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

235 by (auto simp add: postfix_def)

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

237 by (auto simp add: postfix_def)

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

240 by (simp add: postfix_def)

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

242 by (auto simp add: postfix_def)

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

245 by (auto simp add: postfix_def)

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

247 by (auto simp add: postfix_def)

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

250 by (auto simp add: postfix_def)

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

252 by (auto simp add: postfix_def)

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

255 proof -

256 assume "xs >>= ys"

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

258 then show ?thesis by (induct zs) auto

259 qed

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

262 proof -

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

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

265 then show ?thesis

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

267 qed

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

270 proof

271 assume "xs >>= ys"

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

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

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

275 next

276 assume "rev ys <= rev xs"

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

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

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

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

281 qed

284 subsection {* Exeuctable code *}

286 lemma less_eq_code [code func]:

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

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

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

290 by simp_all

292 lemma less_code [code func]:

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

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

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

296 unfolding strict_prefix_def by auto

298 lemmas [code func] = postfix_to_prefix

300 end