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

src/HOL/Library/List_Prefix.thy

author | nipkow |

Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) | |

changeset 15140 | 322485b816ac |

parent 15131 | c69542757a4d |

child 15355 | 0de05d104060 |

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

import -> imports

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 by (unfold prefix_def) blast

26 lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"

27 by (unfold prefix_def) blast

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

30 by (unfold strict_prefix_def prefix_def) blast

32 lemma strict_prefixE' [elim?]:

33 "xs < ys ==> (!!z zs. ys = xs @ z # zs ==> C) ==> C"

34 proof -

35 assume r: "!!z zs. ys = xs @ z # zs ==> C"

36 assume "xs < ys"

37 then obtain us where "ys = xs @ us" and "xs \<noteq> ys"

38 by (unfold strict_prefix_def prefix_def) blast

39 with r show ?thesis by (auto simp add: neq_Nil_conv)

40 qed

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

43 by (unfold strict_prefix_def) blast

45 lemma strict_prefixE [elim?]:

46 "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C"

47 by (unfold strict_prefix_def) blast

50 subsection {* Basic properties of prefixes *}

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

53 by (simp add: prefix_def)

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

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

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

59 proof

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

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

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

63 proof (cases zs rule: rev_cases)

64 assume "zs = []"

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

66 thus ?thesis ..

67 next

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

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

70 hence "xs \<le> ys" ..

71 thus ?thesis ..

72 qed

73 next

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

75 thus "xs \<le> ys @ [y]"

76 proof

77 assume "xs = ys @ [y]"

78 thus ?thesis by simp

79 next

80 assume "xs \<le> ys"

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

82 hence "ys @ [y] = xs @ (zs @ [y])" by simp

83 thus ?thesis ..

84 qed

85 qed

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

88 by (auto simp add: prefix_def)

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

91 by (induct xs) simp_all

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

94 proof -

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

96 thus ?thesis by simp

97 qed

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

100 proof -

101 assume "xs \<le> ys"

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

103 hence "ys @ zs = xs @ (us @ zs)" by simp

104 thus ?thesis ..

105 qed

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

108 by(simp add:prefix_def) blast

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

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

113 theorem prefix_append:

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

115 apply (induct zs rule: rev_induct)

116 apply force

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

118 apply simp

119 apply blast

120 done

122 lemma append_one_prefix:

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

124 apply (unfold prefix_def)

125 apply (auto simp add: nth_append)

126 apply (case_tac zs)

127 apply auto

128 done

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

131 by (auto simp add: prefix_def)

134 lemma prefix_same_cases:

135 "\<lbrakk> (xs\<^isub>1::'a list) \<le> ys; xs\<^isub>2 \<le> ys \<rbrakk> \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"

136 apply(simp add:prefix_def)

137 apply(erule exE)+

138 apply(simp add: append_eq_append_conv_if split:if_splits)

139 apply(rule disjI2)

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

141 apply clarify

142 apply(drule sym)

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

144 apply simp

145 apply(rule disjI1)

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

147 apply clarify

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

149 apply simp

150 done

152 lemma set_mono_prefix:

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

154 by(fastsimp simp add:prefix_def)

157 subsection {* Parallel lists *}

159 constdefs

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

161 "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"

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

164 by (unfold parallel_def) blast

166 lemma parallelE [elim]:

167 "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C"

168 by (unfold parallel_def) blast

170 theorem prefix_cases:

171 "(xs \<le> ys ==> C) ==>

172 (ys < xs ==> C) ==>

173 (xs \<parallel> ys ==> C) ==> C"

174 by (unfold parallel_def strict_prefix_def) blast

176 theorem parallel_decomp:

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

178 proof (induct xs rule: rev_induct)

179 case Nil

180 hence False by auto

181 thus ?case ..

182 next

183 case (snoc x xs)

184 show ?case

185 proof (rule prefix_cases)

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

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

188 show ?thesis

189 proof (cases ys')

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

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

192 hence False by blast

193 thus ?thesis ..

194 next

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

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

197 hence "x \<noteq> c" by auto

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

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

200 ultimately show ?thesis by blast

201 qed

202 next

203 assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)

204 with snoc have False by blast

205 thus ?thesis ..

206 next

207 assume "xs \<parallel> ys"

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

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

210 by blast

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

212 with neq ys show ?thesis by blast

213 qed

214 qed

217 subsection {* Postfix order on lists *}

219 constdefs

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

221 "xs >= ys == \<exists>zs. xs = zs @ ys"

223 lemma postfix_refl [simp, intro!]: "xs >= xs"

224 by (auto simp add: postfix_def)

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

226 by (auto simp add: postfix_def)

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

228 by (auto simp add: postfix_def)

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

231 by (simp add: postfix_def)

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

233 by (auto simp add:postfix_def)

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

236 by (auto simp add: postfix_def)

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

238 by (auto simp add: postfix_def)

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

241 by (auto simp add: postfix_def)

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

243 by(auto simp add: postfix_def)

245 lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"

246 by (induct zs, auto)

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

248 by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)

250 lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >= ys"

251 by (induct zs, auto intro!: postfix_appendI postfix_ConsI)

252 lemma postfix_ConsD2: "x#xs >= y#ys \<Longrightarrow> xs >= ys"

253 by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)

255 lemma postfix2prefix: "(xs >= ys) = (rev ys <= rev xs)"

256 apply (unfold prefix_def postfix_def, safe)

257 apply (rule_tac x = "rev zs" in exI, simp)

258 apply (rule_tac x = "rev zs" in exI)

259 apply (rule rev_is_rev_conv [THEN iffD1], simp)

260 done

262 end