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

src/HOL/Library/Sublist_Order.thy

author | bulwahn |

Tue Apr 05 09:38:28 2011 +0200 (2011-04-05) | |

changeset 42231 | bc1891226d00 |

parent 37765 | 26bdfb7b680b |

child 49084 | e3973567ed4f |

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

removing bounded_forall code equation for characters when loading Code_Char

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

2 Authors: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>

3 Florian Haftmann, Tobias Nipkow, TU Muenchen

4 *)

6 header {* Sublist Ordering *}

8 theory Sublist_Order

9 imports Main

10 begin

12 text {*

13 This theory defines sublist ordering on lists.

14 A list @{text ys} is a sublist of a list @{text xs},

15 iff one obtains @{text ys} by erasing some elements from @{text xs}.

16 *}

18 subsection {* Definitions and basic lemmas *}

20 instantiation list :: (type) ord

21 begin

23 inductive less_eq_list where

24 empty [simp, intro!]: "[] \<le> xs"

25 | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"

26 | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"

28 definition

29 "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"

31 instance proof qed

33 end

35 lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"

36 by (induct rule: less_eq_list.induct) auto

38 lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"

39 by (induct rule: less_eq_list.induct) (auto dest: le_list_length)

41 lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"

42 by (metis le_list_length linorder_not_less)

44 lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"

45 by (auto dest: le_list_length)

47 lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"

48 by (induct zs) (auto intro: drop)

50 lemma [code]: "[] <= xs \<longleftrightarrow> True"

51 by(metis less_eq_list.empty)

53 lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"

54 by simp

56 lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys"

57 proof-

58 { fix xs' ys'

59 assume "xs' <= ys"

60 hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"

61 proof induct

62 case empty thus ?case by simp

63 next

64 case drop thus ?case by (metis less_eq_list.drop)

65 next

66 case take thus ?case by (simp add: drop)

67 qed }

68 from this[OF assms] show ?thesis by simp

69 qed

71 lemma le_list_drop_Cons2:

72 assumes "x#xs <= x#ys" shows "xs <= ys"

73 using assms

74 proof cases

75 case drop thus ?thesis by (metis le_list_drop_Cons list.inject)

76 qed simp_all

78 lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"

79 shows "x ~= y \<Longrightarrow> x # xs <= ys"

80 using assms proof cases qed auto

82 lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>

83 (if x=y then xs <= ys else (x#xs) <= ys)"

84 by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq)

86 lemma le_list_take_many_iff: "zs @ xs \<le> zs @ ys \<longleftrightarrow> xs \<le> ys"

87 by (induct zs) (auto intro: take)

89 lemma le_list_Cons_EX:

90 assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs"

91 proof-

92 { fix xys zs :: "'a list" assume "xys <= zs"

93 hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)"

94 proof induct

95 case empty show ?case by simp

96 next

97 case take thus ?case by (metis list.inject self_append_conv2)

98 next

99 case drop thus ?case by (metis append_eq_Cons_conv)

100 qed

101 } with assms show ?thesis by blast

102 qed

104 instantiation list :: (type) order

105 begin

107 instance proof

108 fix xs ys :: "'a list"

109 show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def ..

110 next

111 fix xs :: "'a list"

112 show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop)

113 next

114 fix xs ys :: "'a list"

115 assume "xs <= ys"

116 hence "ys <= xs \<longrightarrow> xs = ys"

117 proof induct

118 case empty show ?case by simp

119 next

120 case take thus ?case by simp

121 next

122 case drop thus ?case

123 by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n)

124 qed

125 moreover assume "ys <= xs"

126 ultimately show "xs = ys" by blast

127 next

128 fix xs ys zs :: "'a list"

129 assume "xs <= ys"

130 hence "ys <= zs \<longrightarrow> xs <= zs"

131 proof (induct arbitrary:zs)

132 case empty show ?case by simp

133 next

134 case (take xs ys x) show ?case

135 proof

136 assume "x # ys <= zs"

137 with take show "x # xs <= zs"

138 by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2))

139 qed

140 next

141 case drop thus ?case by (metis le_list_drop_Cons)

142 qed

143 moreover assume "ys <= zs"

144 ultimately show "xs <= zs" by blast

145 qed

147 end

149 lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]"

150 by (auto dest: le_list_length)

152 lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"

153 apply (induct rule:less_eq_list.induct)

154 apply (metis eq_Nil_appendI le_list_drop_many)

155 apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)

156 apply simp

157 done

159 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"

160 by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def)

162 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"

163 by (metis empty order_less_le)

165 lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"

166 by (metis empty less_list_def)

168 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"

169 by (unfold less_le) (auto intro: less_eq_list.drop)

171 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"

172 by (metis le_list_Cons2_iff less_list_def)

174 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"

175 by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2)

177 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"

178 by (metis le_list_take_many_iff less_list_def)

181 subsection {* Appending elements *}

183 lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R")

184 proof

185 { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"

186 hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys"

187 proof (induct arbitrary: xs ys zs)

188 case empty show ?case by simp

189 next

190 case (drop xs' ys' x)

191 { assume "ys=[]" hence ?case using drop(1) by auto }

192 moreover

193 { fix us assume "ys = x#us"

194 hence ?case using drop(2) by(simp add: less_eq_list.drop) }

195 ultimately show ?case by (auto simp:Cons_eq_append_conv)

196 next

197 case (take xs' ys' x)

198 { assume "xs=[]" hence ?case using take(1) by auto }

199 moreover

200 { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto}

201 moreover

202 { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }

203 ultimately show ?case by (auto simp:Cons_eq_append_conv)

204 qed }

205 moreover assume ?L

206 ultimately show ?R by blast

207 next

208 assume ?R thus ?L by(metis le_list_append_mono order_refl)

209 qed

211 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"

212 by (unfold less_le) auto

214 lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"

215 by (metis append_Nil2 empty le_list_append_mono)

218 subsection {* Relation to standard list operations *}

220 lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"

221 by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)

223 lemma le_list_filter_left[simp]: "filter f xs \<le> xs"

224 by (induct xs) (auto intro: less_eq_list.drop)

226 lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"

227 by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)

229 lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")

230 proof

231 assume ?L

232 thus ?R

233 proof induct

234 case empty show ?case by (metis sublist_empty)

235 next

236 case (drop xs ys x)

237 then obtain N where "xs = sublist ys N" by blast

238 hence "xs = sublist (x#ys) (Suc ` N)"

239 by (clarsimp simp add:sublist_Cons inj_image_mem_iff)

240 thus ?case by blast

241 next

242 case (take xs ys x)

243 then obtain N where "xs = sublist ys N" by blast

244 hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"

245 by (clarsimp simp add:sublist_Cons inj_image_mem_iff)

246 thus ?case by blast

247 qed

248 next

249 assume ?R

250 then obtain N where "xs = sublist ys N" ..

251 moreover have "sublist ys N <= ys"

252 proof (induct ys arbitrary:N)

253 case Nil show ?case by simp

254 next

255 case Cons thus ?case by (auto simp add:sublist_Cons drop)

256 qed

257 ultimately show ?L by simp

258 qed

260 end