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

src/HOL/Library/List_Prefix.thy

author | wenzelm |

Sat Jan 21 23:02:21 2006 +0100 (2006-01-21) | |

changeset 18730 | 843da46f89ac |

parent 18258 | 836491e9b7d5 |

child 19086 | 1b3780be6cc2 |

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

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?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"

27 unfolding prefix_def by blast

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

30 unfolding strict_prefix_def prefix_def by blast

32 lemma strict_prefixE' [elim?]:

33 assumes lt: "xs < ys"

34 and r: "!!z zs. ys = xs @ z # zs ==> C"

35 shows C

36 proof -

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

38 unfolding strict_prefix_def prefix_def by 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 unfolding strict_prefix_def by blast

45 lemma strict_prefixE [elim?]:

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

47 unfolding strict_prefix_def by 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 (auto simp add: prefix_def)

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)

133 lemma prefix_same_cases:

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

135 apply (simp add: prefix_def)

136 apply (erule exE)+

137 apply (simp add: append_eq_append_conv_if split: if_splits)

138 apply (rule disjI2)

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

140 apply clarify

141 apply (drule sym)

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

143 apply simp

144 apply (rule disjI1)

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

146 apply clarify

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

148 apply simp

149 done

151 lemma set_mono_prefix:

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

153 by (auto simp add: prefix_def)

156 subsection {* Parallel lists *}

158 constdefs

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

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

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

163 unfolding parallel_def by blast

165 lemma parallelE [elim]:

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

167 unfolding parallel_def by blast

169 theorem prefix_cases:

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

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

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

173 unfolding parallel_def strict_prefix_def by blast

175 theorem parallel_decomp:

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

177 proof (induct xs rule: rev_induct)

178 case Nil

179 hence False by auto

180 thus ?case ..

181 next

182 case (snoc x xs)

183 show ?case

184 proof (rule prefix_cases)

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

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

187 show ?thesis

188 proof (cases ys')

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

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

191 hence False by blast

192 thus ?thesis ..

193 next

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

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

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

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

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

199 ultimately show ?thesis by blast

200 qed

201 next

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

203 with snoc have False by blast

204 thus ?thesis ..

205 next

206 assume "xs \<parallel> ys"

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

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

209 by blast

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

211 with neq ys show ?thesis by blast

212 qed

213 qed

216 subsection {* Postfix order on lists *}

218 constdefs

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

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

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

223 by (auto simp add: postfix_def)

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

225 by (auto simp add: postfix_def)

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

227 by (auto simp add: postfix_def)

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

230 by (simp add: postfix_def)

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

232 by (auto simp add:postfix_def)

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

235 by (auto simp add: postfix_def)

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

237 by (auto simp add: postfix_def)

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

240 by (auto simp add: postfix_def)

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

242 by(auto simp add: postfix_def)

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

245 by (induct zs) auto

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

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

249 lemma postfix_ConsD2_lemma: "x#xs = zs @ y#ys \<Longrightarrow> xs >>= ys"

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

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

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

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

255 apply (unfold prefix_def postfix_def, safe)

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

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

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

259 done

261 end