author  nipkow 
Thu, 23 Apr 2020 09:57:41 +0200  
changeset 71789  3b6547bdf6e2 
parent 68406  6beb45f6cf67 
child 73186  ce90865dbaeb 
permissions  rwrr 
49087  1 
(* Title: HOL/Library/Sublist.thy 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

2 
Author: Tobias Nipkow and Markus Wenzel, TU München 
49087  3 
Author: Christian Sternagel, JAIST 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

4 
Author: Manuel Eberl, TU München 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

5 
*) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

6 

60500  7 
section \<open>List prefixes, suffixes, and homeomorphic embedding\<close> 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

8 

49087  9 
theory Sublist 
10 
imports Main 

15131  11 
begin 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

12 

60500  13 
subsection \<open>Prefix order on lists\<close> 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

14 

63117  15 
definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
16 
where "prefix xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)" 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

17 

63117  18 
definition strict_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
19 
where "strict_prefix xs ys \<longleftrightarrow> prefix xs ys \<and> xs \<noteq> ys" 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

20 

63117  21 
interpretation prefix_order: order prefix strict_prefix 
22 
by standard (auto simp: prefix_def strict_prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

23 

63117  24 
interpretation prefix_bot: order_bot Nil prefix strict_prefix 
25 
by standard (simp add: prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

26 

63117  27 
lemma prefixI [intro?]: "ys = xs @ zs \<Longrightarrow> prefix xs ys" 
28 
unfolding prefix_def by blast 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

29 

63117  30 
lemma prefixE [elim?]: 
31 
assumes "prefix xs ys" 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

32 
obtains zs where "ys = xs @ zs" 
63117  33 
using assms unfolding prefix_def by blast 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

34 

63117  35 
lemma strict_prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> strict_prefix xs ys" 
36 
unfolding strict_prefix_def prefix_def by blast 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

37 

63117  38 
lemma strict_prefixE' [elim?]: 
39 
assumes "strict_prefix xs ys" 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

40 
obtains z zs where "ys = xs @ z # zs" 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

41 
proof  
63117  42 
from \<open>strict_prefix xs ys\<close> obtain us where "ys = xs @ us" and "xs \<noteq> ys" 
43 
unfolding strict_prefix_def prefix_def by blast 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

44 
with that show ?thesis by (auto simp add: neq_Nil_conv) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

45 
qed 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

46 

63155  47 
(* FIXME rm *) 
63117  48 
lemma strict_prefixI [intro?]: "prefix xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> strict_prefix xs ys" 
63155  49 
by(fact prefix_order.le_neq_trans) 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

50 

63117  51 
lemma strict_prefixE [elim?]: 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

52 
fixes xs ys :: "'a list" 
63117  53 
assumes "strict_prefix xs ys" 
54 
obtains "prefix xs ys" and "xs \<noteq> ys" 

55 
using assms unfolding strict_prefix_def by blast 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

56 

207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

57 

60500  58 
subsection \<open>Basic properties of prefixes\<close> 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

59 

63155  60 
(* FIXME rm *) 
65869  61 
theorem Nil_prefix [simp]: "prefix [] xs" 
62 
by (fact prefix_bot.bot_least) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

63 

63155  64 
(* FIXME rm *) 
63117  65 
theorem prefix_Nil [simp]: "(prefix xs []) = (xs = [])" 
65869  66 
by (fact prefix_bot.bot_unique) 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

67 

63117  68 
lemma prefix_snoc [simp]: "prefix xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefix xs ys" 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

69 
proof 
63117  70 
assume "prefix xs (ys @ [y])" 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

71 
then obtain zs where zs: "ys @ [y] = xs @ zs" .. 
63117  72 
show "xs = ys @ [y] \<or> prefix xs ys" 
73 
by (metis append_Nil2 butlast_append butlast_snoc prefixI zs) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

74 
next 
63117  75 
assume "xs = ys @ [y] \<or> prefix xs ys" 
76 
then show "prefix xs (ys @ [y])" 

77 
by (metis prefix_order.eq_iff prefix_order.order_trans prefixI) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

78 
qed 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

79 

63117  80 
lemma Cons_prefix_Cons [simp]: "prefix (x # xs) (y # ys) = (x = y \<and> prefix xs ys)" 
81 
by (auto simp add: prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

82 

63117  83 
lemma prefix_code [code]: 
84 
"prefix [] xs \<longleftrightarrow> True" 

85 
"prefix (x # xs) [] \<longleftrightarrow> False" 

86 
"prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys" 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

87 
by simp_all 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

88 

63117  89 
lemma same_prefix_prefix [simp]: "prefix (xs @ ys) (xs @ zs) = prefix ys zs" 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

90 
by (induct xs) simp_all 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

91 

65869  92 
lemma same_prefix_nil [simp]: "prefix (xs @ ys) xs = (ys = [])" 
63117  93 
by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixI) 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

94 

63117  95 
lemma prefix_prefix [simp]: "prefix xs ys \<Longrightarrow> prefix xs (ys @ zs)" 
64886  96 
unfolding prefix_def by fastforce 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

97 

63117  98 
lemma append_prefixD: "prefix (xs @ ys) zs \<Longrightarrow> prefix xs zs" 
99 
by (auto simp add: prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

100 

63117  101 
theorem prefix_Cons: "prefix xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefix zs ys))" 
102 
by (cases xs) (auto simp add: prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

103 

63117  104 
theorem prefix_append: 
105 
"prefix xs (ys @ zs) = (prefix xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefix us zs))" 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

106 
apply (induct zs rule: rev_induct) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

107 
apply force 
68406  108 
apply (simp flip: append_assoc) 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

109 
apply (metis append_eq_appendI) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

110 
done 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

111 

63117  112 
lemma append_one_prefix: 
113 
"prefix xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefix (xs @ [ys ! length xs]) ys" 

114 
proof (unfold prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

115 
assume a1: "\<exists>zs. ys = xs @ zs" 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

116 
then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

117 
assume a2: "length xs < length ys" 
61076  118 
have f1: "\<And>v. ([]::'a list) @ v = v" using append_Nil2 by simp 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

119 
have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

120 
hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

121 
thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

122 
qed 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

123 

63117  124 
theorem prefix_length_le: "prefix xs ys \<Longrightarrow> length xs \<le> length ys" 
125 
by (auto simp add: prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

126 

63117  127 
lemma prefix_same_cases: 
128 
"prefix (xs\<^sub>1::'a list) ys \<Longrightarrow> prefix xs\<^sub>2 ys \<Longrightarrow> prefix xs\<^sub>1 xs\<^sub>2 \<or> prefix xs\<^sub>2 xs\<^sub>1" 

129 
unfolding prefix_def by (force simp: append_eq_append_conv2) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

130 

63173  131 
lemma prefix_length_prefix: 
132 
"prefix ps xs \<Longrightarrow> prefix qs xs \<Longrightarrow> length ps \<le> length qs \<Longrightarrow> prefix ps qs" 

133 
by (auto simp: prefix_def) (metis append_Nil2 append_eq_append_conv_if) 

134 

63117  135 
lemma set_mono_prefix: "prefix xs ys \<Longrightarrow> set xs \<subseteq> set ys" 
136 
by (auto simp add: prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

137 

63117  138 
lemma take_is_prefix: "prefix (take n xs) xs" 
139 
unfolding prefix_def by (metis append_take_drop_id) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

140 

63155  141 
lemma prefixeq_butlast: "prefix (butlast xs) xs" 
142 
by (simp add: butlast_conv_take take_is_prefix) 

143 

71789  144 
lemma prefix_map_rightE: 
145 
assumes "prefix xs (map f ys)" 

146 
shows "\<exists>xs'. prefix xs' ys \<and> xs = map f xs'" 

147 
proof  

148 
define n where "n = length xs" 

149 
have "xs = take n (map f ys)" 

150 
using assms by (auto simp: prefix_def n_def) 

151 
thus ?thesis 

152 
by (intro exI[of _ "take n ys"]) (auto simp: take_map take_is_prefix) 

153 
qed 

154 

67606  155 
lemma map_mono_prefix: "prefix xs ys \<Longrightarrow> prefix (map f xs) (map f ys)" 
156 
by (auto simp: prefix_def) 

157 

158 
lemma filter_mono_prefix: "prefix xs ys \<Longrightarrow> prefix (filter P xs) (filter P ys)" 

159 
by (auto simp: prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

160 

67612  161 
lemma sorted_antimono_prefix: "prefix xs ys \<Longrightarrow> sorted ys \<Longrightarrow> sorted xs" 
162 
by (metis sorted_append prefix_def) 

163 

63117  164 
lemma prefix_length_less: "strict_prefix xs ys \<Longrightarrow> length xs < length ys" 
165 
by (auto simp: strict_prefix_def prefix_def) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

166 

63155  167 
lemma prefix_snocD: "prefix (xs@[x]) ys \<Longrightarrow> strict_prefix xs ys" 
168 
by (simp add: strict_prefixI' prefix_order.dual_order.strict_trans1) 

169 

63117  170 
lemma strict_prefix_simps [simp, code]: 
171 
"strict_prefix xs [] \<longleftrightarrow> False" 

172 
"strict_prefix [] (x # xs) \<longleftrightarrow> True" 

173 
"strict_prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> strict_prefix xs ys" 

174 
by (simp_all add: strict_prefix_def cong: conj_cong) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

175 

63117  176 
lemma take_strict_prefix: "strict_prefix xs ys \<Longrightarrow> strict_prefix (take n xs) ys" 
63649  177 
proof (induct n arbitrary: xs ys) 
178 
case 0 

179 
then show ?case by (cases ys) simp_all 

180 
next 

181 
case (Suc n) 

182 
then show ?case by (metis prefix_order.less_trans strict_prefixI take_is_prefix) 

183 
qed 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

184 

71789  185 
lemma prefix_takeWhile: 
186 
assumes "prefix xs ys" 

187 
shows "prefix (takeWhile P xs) (takeWhile P ys)" 

188 
proof  

189 
from assms obtain zs where ys: "ys = xs @ zs" 

190 
by (auto simp: prefix_def) 

191 
have "prefix (takeWhile P xs) (takeWhile P (xs @ zs))" 

192 
by (induction xs) auto 

193 
thus ?thesis by (simp add: ys) 

194 
qed 

195 

196 
lemma prefix_dropWhile: 

197 
assumes "prefix xs ys" 

198 
shows "prefix (dropWhile P xs) (dropWhile P ys)" 

199 
proof  

200 
from assms obtain zs where ys: "ys = xs @ zs" 

201 
by (auto simp: prefix_def) 

202 
have "prefix (dropWhile P xs) (dropWhile P (xs @ zs))" 

203 
by (induction xs) auto 

204 
thus ?thesis by (simp add: ys) 

205 
qed 

206 

207 
lemma prefix_remdups_adj: 

208 
assumes "prefix xs ys" 

209 
shows "prefix (remdups_adj xs) (remdups_adj ys)" 

210 
using assms 

211 
proof (induction "length xs" arbitrary: xs ys rule: less_induct) 

212 
case (less xs) 

213 
show ?case 

214 
proof (cases xs) 

215 
case [simp]: (Cons x xs') 

216 
then obtain y ys' where [simp]: "ys = y # ys'" 

217 
using \<open>prefix xs ys\<close> by (cases ys) auto 

218 
from less show ?thesis 

219 
by (auto simp: remdups_adj_Cons' less_Suc_eq_le length_dropWhile_le 

220 
intro!: less prefix_dropWhile) 

221 
qed auto 

222 
qed 

223 

63117  224 
lemma not_prefix_cases: 
225 
assumes pfx: "\<not> prefix ps ls" 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

226 
obtains 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

227 
(c1) "ps \<noteq> []" and "ls = []" 
63117  228 
 (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefix as xs" 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

229 
 (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a" 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

230 
proof (cases ps) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

231 
case Nil 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

232 
then show ?thesis using pfx by simp 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

233 
next 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

234 
case (Cons a as) 
60500  235 
note c = \<open>ps = a#as\<close> 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

236 
show ?thesis 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

237 
proof (cases ls) 
63117  238 
case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil) 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

239 
next 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

240 
case (Cons x xs) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

241 
show ?thesis 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

242 
proof (cases "x = a") 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

243 
case True 
63117  244 
have "\<not> prefix as xs" using pfx c Cons True by simp 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

245 
with c Cons True show ?thesis by (rule c2) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

246 
next 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

247 
case False 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

248 
with c Cons show ?thesis by (rule c3) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

249 
qed 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

250 
qed 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

251 
qed 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

252 

63117  253 
lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: 
254 
assumes np: "\<not> prefix ps ls" 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

255 
and base: "\<And>x xs. P (x#xs) []" 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

256 
and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)" 
63117  257 
and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefix xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)" 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

258 
shows "P ps ls" using np 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

259 
proof (induct ls arbitrary: ps) 
63649  260 
case Nil 
261 
then show ?case 

63117  262 
by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

263 
next 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

264 
case (Cons y ys) 
63117  265 
then have npfx: "\<not> prefix ps (y # ys)" by simp 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

266 
then obtain x xs where pv: "ps = x # xs" 
63117  267 
by (rule not_prefix_cases) auto 
268 
show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2) 

55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

269 
qed 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

270 

207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

271 

63155  272 
subsection \<open>Prefixes\<close> 
273 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

274 
primrec prefixes where 
63155  275 
"prefixes [] = [[]]"  
67399  276 
"prefixes (x#xs) = [] # map ((#) x) (prefixes xs)" 
63155  277 

278 
lemma in_set_prefixes[simp]: "xs \<in> set (prefixes ys) \<longleftrightarrow> prefix xs ys" 

63649  279 
proof (induct xs arbitrary: ys) 
280 
case Nil 

281 
then show ?case by (cases ys) auto 

282 
next 

283 
case (Cons a xs) 

284 
then show ?case by (cases ys) auto 

285 
qed 

63155  286 

287 
lemma length_prefixes[simp]: "length (prefixes xs) = length xs+1" 

65869  288 
by (induction xs) auto 
289 

290 
lemma distinct_prefixes [intro]: "distinct (prefixes xs)" 

291 
by (induction xs) (auto simp: distinct_map) 

292 

293 
lemma prefixes_snoc [simp]: "prefixes (xs@[x]) = prefixes xs @ [xs@[x]]" 

294 
by (induction xs) auto 

295 

296 
lemma prefixes_not_Nil [simp]: "prefixes xs \<noteq> []" 

297 
by (cases xs) auto 

63155  298 

65869  299 
lemma hd_prefixes [simp]: "hd (prefixes xs) = []" 
300 
by (cases xs) simp_all 

63155  301 

65869  302 
lemma last_prefixes [simp]: "last (prefixes xs) = xs" 
303 
by (induction xs) (simp_all add: last_map) 

304 

305 
lemma prefixes_append: 

306 
"prefixes (xs @ ys) = prefixes xs @ map (\<lambda>ys'. xs @ ys') (tl (prefixes ys))" 

307 
proof (induction xs) 

308 
case Nil 

309 
thus ?case by (cases ys) auto 

310 
qed simp_all 

311 

312 
lemma prefixes_eq_snoc: 

63155  313 
"prefixes ys = xs @ [x] \<longleftrightarrow> 
314 
(ys = [] \<and> xs = [] \<or> (\<exists>z zs. ys = zs@[z] \<and> xs = prefixes zs)) \<and> x = ys" 

65869  315 
by (cases ys rule: rev_cases) auto 
316 

317 
lemma prefixes_tailrec [code]: 

318 
"prefixes xs = rev (snd (foldl (\<lambda>(acc1, acc2) x. (x#acc1, rev (x#acc1)#acc2)) ([],[[]]) xs))" 

319 
proof  

320 
have "foldl (\<lambda>(acc1, acc2) x. (x#acc1, rev (x#acc1)#acc2)) (ys, rev ys # zs) xs = 

321 
(rev xs @ ys, rev (map (\<lambda>as. rev ys @ as) (prefixes xs)) @ zs)" for ys zs 

322 
proof (induction xs arbitrary: ys zs) 

323 
case (Cons x xs ys zs) 

324 
from Cons.IH[of "x # ys" "rev ys # zs"] 

325 
show ?case by (simp add: o_def) 

326 
qed simp_all 

327 
from this [of "[]" "[]"] show ?thesis by simp 

328 
qed 

329 

330 
lemma set_prefixes_eq: "set (prefixes xs) = {ys. prefix ys xs}" 

331 
by auto 

332 

333 
lemma card_set_prefixes [simp]: "card (set (prefixes xs)) = Suc (length xs)" 

334 
by (subst distinct_card) auto 

335 

336 
lemma set_prefixes_append: 

337 
"set (prefixes (xs @ ys)) = set (prefixes xs) \<union> {xs @ ys' ys'. ys' \<in> set (prefixes ys)}" 

338 
by (subst prefixes_append, cases ys) auto 

63155  339 

340 

63173  341 
subsection \<open>Longest Common Prefix\<close> 
342 

343 
definition Longest_common_prefix :: "'a list set \<Rightarrow> 'a list" where 

65954  344 
"Longest_common_prefix L = (ARG_MAX length ps. \<forall>xs \<in> L. prefix ps xs)" 
63173  345 

346 
lemma Longest_common_prefix_ex: "L \<noteq> {} \<Longrightarrow> 

347 
\<exists>ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)" 

348 
(is "_ \<Longrightarrow> \<exists>ps. ?P L ps") 

349 
proof(induction "LEAST n. \<exists>xs \<in>L. n = length xs" arbitrary: L) 

350 
case 0 

67613  351 
have "[] \<in> L" using "0.hyps" LeastI[of "\<lambda>n. \<exists>xs\<in>L. n = length xs"] \<open>L \<noteq> {}\<close> 
63173  352 
by auto 
353 
hence "?P L []" by(auto) 

354 
thus ?case .. 

355 
next 

356 
case (Suc n) 

357 
let ?EX = "\<lambda>n. \<exists>xs\<in>L. n = length xs" 

358 
obtain x xs where xxs: "x#xs \<in> L" "size xs = n" using Suc.prems Suc.hyps(2) 

359 
by(metis LeastI_ex[of ?EX] Suc_length_conv ex_in_conv) 

360 
hence "[] \<notin> L" using Suc.hyps(2) by auto 

361 
show ?case 

362 
proof (cases "\<forall>xs \<in> L. \<exists>ys. xs = x#ys") 

363 
case True 

364 
let ?L = "{ys. x#ys \<in> L}" 

365 
have 1: "(LEAST n. \<exists>xs \<in> ?L. n = length xs) = n" 

366 
using xxs Suc.prems Suc.hyps(2) Least_le[of "?EX"] 

367 
by  (rule Least_equality, fastforce+) 

368 
have 2: "?L \<noteq> {}" using \<open>x # xs \<in> L\<close> by auto 

369 
from Suc.hyps(1)[OF 1[symmetric] 2] obtain ps where IH: "?P ?L ps" .. 

370 
{ fix qs 

371 
assume "\<forall>qs. (\<forall>xa. x # xa \<in> L \<longrightarrow> prefix qs xa) \<longrightarrow> length qs \<le> length ps" 

372 
and "\<forall>xs\<in>L. prefix qs xs" 

373 
hence "length (tl qs) \<le> length ps" 

374 
by (metis Cons_prefix_Cons hd_Cons_tl list.sel(2) Nil_prefix) 

375 
hence "length qs \<le> Suc (length ps)" by auto 

376 
} 

377 
hence "?P L (x#ps)" using True IH by auto 

378 
thus ?thesis .. 

379 
next 

380 
case False 

381 
then obtain y ys where yys: "x\<noteq>y" "y#ys \<in> L" using \<open>[] \<notin> L\<close> 

382 
by (auto) (metis list.exhaust) 

383 
have "\<forall>qs. (\<forall>xs\<in>L. prefix qs xs) \<longrightarrow> qs = []" using yys \<open>x#xs \<in> L\<close> 

384 
by auto (metis Cons_prefix_Cons prefix_Cons) 

385 
hence "?P L []" by auto 

386 
thus ?thesis .. 

387 
qed 

388 
qed 

389 

390 
lemma Longest_common_prefix_unique: "L \<noteq> {} \<Longrightarrow> 

391 
\<exists>! ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)" 

392 
by(rule ex_ex1I[OF Longest_common_prefix_ex]; 

393 
meson equals0I prefix_length_prefix prefix_order.antisym) 

394 

395 
lemma Longest_common_prefix_eq: 

396 
"\<lbrakk> L \<noteq> {}; \<forall>xs \<in> L. prefix ps xs; 

397 
\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps \<rbrakk> 

398 
\<Longrightarrow> Longest_common_prefix L = ps" 

65954  399 
unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder 
63173  400 
by(rule some1_equality[OF Longest_common_prefix_unique]) auto 
401 

402 
lemma Longest_common_prefix_prefix: 

403 
"xs \<in> L \<Longrightarrow> prefix (Longest_common_prefix L) xs" 

65954  404 
unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder 
63173  405 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 
406 

407 
lemma Longest_common_prefix_longest: 

408 
"L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> length ps \<le> length(Longest_common_prefix L)" 

65954  409 
unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder 
63173  410 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 
411 

412 
lemma Longest_common_prefix_max_prefix: 

413 
"L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> prefix ps (Longest_common_prefix L)" 

414 
by(metis Longest_common_prefix_prefix Longest_common_prefix_longest 

415 
prefix_length_prefix ex_in_conv) 

416 

417 
lemma Longest_common_prefix_Nil: "[] \<in> L \<Longrightarrow> Longest_common_prefix L = []" 

418 
using Longest_common_prefix_prefix prefix_Nil by blast 

419 

420 
lemma Longest_common_prefix_image_Cons: "L \<noteq> {} \<Longrightarrow> 

67399  421 
Longest_common_prefix ((#) x ` L) = x # Longest_common_prefix L" 
63173  422 
apply(rule Longest_common_prefix_eq) 
423 
apply(simp) 

424 
apply (simp add: Longest_common_prefix_prefix) 

425 
apply simp 

426 
by(metis Longest_common_prefix_longest[of L] Cons_prefix_Cons Nitpick.size_list_simp(2) 

427 
Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc) 

428 

429 
lemma Longest_common_prefix_eq_Cons: assumes "L \<noteq> {}" "[] \<notin> L" "\<forall>xs\<in>L. hd xs = x" 

430 
shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \<in> L}" 

431 
proof  

67399  432 
have "L = (#) x ` {ys. x#ys \<in> L}" using assms(2,3) 
63173  433 
by (auto simp: image_def)(metis hd_Cons_tl) 
434 
thus ?thesis 

435 
by (metis Longest_common_prefix_image_Cons image_is_empty assms(1)) 

436 
qed 

437 

438 
lemma Longest_common_prefix_eq_Nil: 

439 
"\<lbrakk>x#ys \<in> L; y#zs \<in> L; x \<noteq> y \<rbrakk> \<Longrightarrow> Longest_common_prefix L = []" 

440 
by (metis Longest_common_prefix_prefix list.inject prefix_Cons) 

441 

442 
fun longest_common_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

443 
"longest_common_prefix (x#xs) (y#ys) = 

444 
(if x=y then x # longest_common_prefix xs ys else [])"  

445 
"longest_common_prefix _ _ = []" 

446 

447 
lemma longest_common_prefix_prefix1: 

448 
"prefix (longest_common_prefix xs ys) xs" 

449 
by(induction xs ys rule: longest_common_prefix.induct) auto 

450 

451 
lemma longest_common_prefix_prefix2: 

452 
"prefix (longest_common_prefix xs ys) ys" 

453 
by(induction xs ys rule: longest_common_prefix.induct) auto 

454 

455 
lemma longest_common_prefix_max_prefix: 

456 
"\<lbrakk> prefix ps xs; prefix ps ys \<rbrakk> 

457 
\<Longrightarrow> prefix ps (longest_common_prefix xs ys)" 

458 
by(induction xs ys arbitrary: ps rule: longest_common_prefix.induct) 

459 
(auto simp: prefix_Cons) 

460 

461 

60500  462 
subsection \<open>Parallel lists\<close> 
10389  463 

50516  464 
definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "\<parallel>" 50) 
63117  465 
where "(xs \<parallel> ys) = (\<not> prefix xs ys \<and> \<not> prefix ys xs)" 
10389  466 

63117  467 
lemma parallelI [intro]: "\<not> prefix xs ys \<Longrightarrow> \<not> prefix ys xs \<Longrightarrow> xs \<parallel> ys" 
25692  468 
unfolding parallel_def by blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

469 

10389  470 
lemma parallelE [elim]: 
25692  471 
assumes "xs \<parallel> ys" 
63117  472 
obtains "\<not> prefix xs ys \<and> \<not> prefix ys xs" 
25692  473 
using assms unfolding parallel_def by blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

474 

63117  475 
theorem prefix_cases: 
476 
obtains "prefix xs ys"  "strict_prefix ys xs"  "xs \<parallel> ys" 

477 
unfolding parallel_def strict_prefix_def by blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

478 

10389  479 
theorem parallel_decomp: 
50516  480 
"xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 
10408  481 
proof (induct xs rule: rev_induct) 
11987  482 
case Nil 
23254  483 
then have False by auto 
484 
then show ?case .. 

10408  485 
next 
11987  486 
case (snoc x xs) 
487 
show ?case 

63117  488 
proof (rule prefix_cases) 
489 
assume le: "prefix xs ys" 

10408  490 
then obtain ys' where ys: "ys = xs @ ys'" .. 
491 
show ?thesis 

492 
proof (cases ys') 

25564  493 
assume "ys' = []" 
63117  494 
then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys) 
10389  495 
next 
10408  496 
fix c cs assume ys': "ys' = c # cs" 
54483  497 
have "x \<noteq> c" using snoc.prems ys ys' by fastforce 
498 
thus "\<exists>as b bs c cs. b \<noteq> c \<and> xs @ [x] = as @ b # bs \<and> ys = as @ c # cs" 

499 
using ys ys' by blast 

10389  500 
qed 
10408  501 
next 
63117  502 
assume "strict_prefix ys xs" 
503 
then have "prefix ys (xs @ [x])" by (simp add: strict_prefix_def) 

11987  504 
with snoc have False by blast 
23254  505 
then show ?thesis .. 
10408  506 
next 
507 
assume "xs \<parallel> ys" 

11987  508 
with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" 
10408  509 
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" 
510 
by blast 

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

512 
with neq ys show ?thesis by blast 

10389  513 
qed 
514 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

515 

25564  516 
lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d" 
25692  517 
apply (rule parallelI) 
518 
apply (erule parallelE, erule conjE, 

63117  519 
induct rule: not_prefix_induct, simp+)+ 
25692  520 
done 
25299  521 

25692  522 
lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y" 
523 
by (simp add: parallel_append) 

25299  524 

25692  525 
lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a" 
526 
unfolding parallel_def by auto 

14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

527 

25356  528 

60500  529 
subsection \<open>Suffix order on lists\<close> 
17201  530 

63149  531 
definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
532 
where "suffix xs ys = (\<exists>zs. ys = zs @ xs)" 

49087  533 

63149  534 
definition strict_suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
65869  535 
where "strict_suffix xs ys \<longleftrightarrow> suffix xs ys \<and> xs \<noteq> ys" 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

536 

65869  537 
interpretation suffix_order: order suffix strict_suffix 
538 
by standard (auto simp: suffix_def strict_suffix_def) 

539 

540 
interpretation suffix_bot: order_bot Nil suffix strict_suffix 

541 
by standard (simp add: suffix_def) 

49087  542 

63149  543 
lemma suffixI [intro?]: "ys = zs @ xs \<Longrightarrow> suffix xs ys" 
544 
unfolding suffix_def by blast 

21305  545 

63149  546 
lemma suffixE [elim?]: 
547 
assumes "suffix xs ys" 

49087  548 
obtains zs where "ys = zs @ xs" 
63149  549 
using assms unfolding suffix_def by blast 
65957  550 

63149  551 
lemma suffix_tl [simp]: "suffix (tl xs) xs" 
49087  552 
by (induct xs) (auto simp: suffix_def) 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

553 

63149  554 
lemma strict_suffix_tl [simp]: "xs \<noteq> [] \<Longrightarrow> strict_suffix (tl xs) xs" 
65869  555 
by (induct xs) (auto simp: strict_suffix_def suffix_def) 
63149  556 

65869  557 
lemma Nil_suffix [simp]: "suffix [] xs" 
63149  558 
by (simp add: suffix_def) 
49087  559 

63149  560 
lemma suffix_Nil [simp]: "(suffix xs []) = (xs = [])" 
561 
by (auto simp add: suffix_def) 

562 

563 
lemma suffix_ConsI: "suffix xs ys \<Longrightarrow> suffix xs (y # ys)" 

564 
by (auto simp add: suffix_def) 

565 

566 
lemma suffix_ConsD: "suffix (x # xs) ys \<Longrightarrow> suffix xs ys" 

567 
by (auto simp add: suffix_def) 

14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

568 

63149  569 
lemma suffix_appendI: "suffix xs ys \<Longrightarrow> suffix xs (zs @ ys)" 
570 
by (auto simp add: suffix_def) 

571 

572 
lemma suffix_appendD: "suffix (zs @ xs) ys \<Longrightarrow> suffix xs ys" 

573 
by (auto simp add: suffix_def) 

49087  574 

63149  575 
lemma strict_suffix_set_subset: "strict_suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" 
65869  576 
by (auto simp: strict_suffix_def suffix_def) 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

577 

67606  578 
lemma set_mono_suffix: "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" 
579 
by (auto simp: suffix_def) 

49087  580 

67612  581 
lemma sorted_antimono_suffix: "suffix xs ys \<Longrightarrow> sorted ys \<Longrightarrow> sorted xs" 
582 
by (metis sorted_append suffix_def) 

583 

63149  584 
lemma suffix_ConsD2: "suffix (x # xs) (y # ys) \<Longrightarrow> suffix xs ys" 
21305  585 
proof  
63149  586 
assume "suffix (x # xs) (y # ys)" 
49107  587 
then obtain zs where "y # ys = zs @ x # xs" .. 
49087  588 
then show ?thesis 
63149  589 
by (induct zs) (auto intro!: suffix_appendI suffix_ConsI) 
21305  590 
qed 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

591 

63149  592 
lemma suffix_to_prefix [code]: "suffix xs ys \<longleftrightarrow> prefix (rev xs) (rev ys)" 
49087  593 
proof 
63149  594 
assume "suffix xs ys" 
49087  595 
then obtain zs where "ys = zs @ xs" .. 
596 
then have "rev ys = rev xs @ rev zs" by simp 

63117  597 
then show "prefix (rev xs) (rev ys)" .. 
49087  598 
next 
63117  599 
assume "prefix (rev xs) (rev ys)" 
49087  600 
then obtain zs where "rev ys = rev xs @ zs" .. 
601 
then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp 

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

63149  603 
then show "suffix xs ys" .. 
21305  604 
qed 
65869  605 

606 
lemma strict_suffix_to_prefix [code]: "strict_suffix xs ys \<longleftrightarrow> strict_prefix (rev xs) (rev ys)" 

607 
by (auto simp: suffix_to_prefix strict_suffix_def strict_prefix_def) 

14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

608 

63149  609 
lemma distinct_suffix: "distinct ys \<Longrightarrow> suffix xs ys \<Longrightarrow> distinct xs" 
610 
by (clarsimp elim!: suffixE) 

17201  611 

67606  612 
lemma map_mono_suffix: "suffix xs ys \<Longrightarrow> suffix (map f xs) (map f ys)" 
613 
by (auto elim!: suffixE intro: suffixI) 

614 

615 
lemma filter_mono_suffix: "suffix xs ys \<Longrightarrow> suffix (filter P xs) (filter P ys)" 

616 
by (auto simp: suffix_def) 

25299  617 

63149  618 
lemma suffix_drop: "suffix (drop n as) as" 
65869  619 
unfolding suffix_def by (rule exI [where x = "take n as"]) simp 
25299  620 

63149  621 
lemma suffix_take: "suffix xs ys \<Longrightarrow> ys = take (length ys  length xs) ys @ xs" 
622 
by (auto elim!: suffixE) 

25299  623 

63149  624 
lemma strict_suffix_reflclp_conv: "strict_suffix\<^sup>=\<^sup>= = suffix" 
65869  625 
by (intro ext) (auto simp: suffix_def strict_suffix_def) 
63149  626 

627 
lemma suffix_lists: "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A" 

628 
unfolding suffix_def by auto 

49087  629 

65869  630 
lemma suffix_snoc [simp]: "suffix xs (ys @ [y]) \<longleftrightarrow> xs = [] \<or> (\<exists>zs. xs = zs @ [y] \<and> suffix zs ys)" 
631 
by (cases xs rule: rev_cases) (auto simp: suffix_def) 

632 

633 
lemma snoc_suffix_snoc [simp]: "suffix (xs @ [x]) (ys @ [y]) = (x = y \<and> suffix xs ys)" 

634 
by (auto simp add: suffix_def) 

635 

636 
lemma same_suffix_suffix [simp]: "suffix (ys @ xs) (zs @ xs) = suffix ys zs" 

637 
by (simp add: suffix_to_prefix) 

638 

639 
lemma same_suffix_nil [simp]: "suffix (ys @ xs) xs = (ys = [])" 

640 
by (simp add: suffix_to_prefix) 

641 

642 
theorem suffix_Cons: "suffix xs (y # ys) \<longleftrightarrow> xs = y # ys \<or> suffix xs ys" 

643 
unfolding suffix_def by (auto simp: Cons_eq_append_conv) 

644 

645 
theorem suffix_append: 

646 
"suffix xs (ys @ zs) \<longleftrightarrow> suffix xs zs \<or> (\<exists>xs'. xs = xs' @ zs \<and> suffix xs' ys)" 

647 
by (auto simp: suffix_def append_eq_append_conv2) 

648 

649 
theorem suffix_length_le: "suffix xs ys \<Longrightarrow> length xs \<le> length ys" 

650 
by (auto simp add: suffix_def) 

651 

652 
lemma suffix_same_cases: 

653 
"suffix (xs\<^sub>1::'a list) ys \<Longrightarrow> suffix xs\<^sub>2 ys \<Longrightarrow> suffix xs\<^sub>1 xs\<^sub>2 \<or> suffix xs\<^sub>2 xs\<^sub>1" 

654 
unfolding suffix_def by (force simp: append_eq_append_conv2) 

655 

656 
lemma suffix_length_suffix: 

657 
"suffix ps xs \<Longrightarrow> suffix qs xs \<Longrightarrow> length ps \<le> length qs \<Longrightarrow> suffix ps qs" 

658 
by (auto simp: suffix_to_prefix intro: prefix_length_prefix) 

659 

660 
lemma suffix_length_less: "strict_suffix xs ys \<Longrightarrow> length xs < length ys" 

661 
by (auto simp: strict_suffix_def suffix_def) 

662 

663 
lemma suffix_ConsD': "suffix (x#xs) ys \<Longrightarrow> strict_suffix xs ys" 

664 
by (auto simp: strict_suffix_def suffix_def) 

665 

666 
lemma drop_strict_suffix: "strict_suffix xs ys \<Longrightarrow> strict_suffix (drop n xs) ys" 

667 
proof (induct n arbitrary: xs ys) 

668 
case 0 

669 
then show ?case by (cases ys) simp_all 

670 
next 

671 
case (Suc n) 

672 
then show ?case 

673 
by (cases xs) (auto intro: Suc dest: suffix_ConsD' suffix_order.less_imp_le) 

674 
qed 

675 

71789  676 
lemma suffix_map_rightE: 
677 
assumes "suffix xs (map f ys)" 

678 
shows "\<exists>xs'. suffix xs' ys \<and> xs = map f xs'" 

679 
proof  

680 
from assms obtain xs' where xs': "map f ys = xs' @ xs" 

681 
by (auto simp: suffix_def) 

682 
define n where "n = length xs'" 

683 
have "xs = drop n (map f ys)" 

684 
by (simp add: xs' n_def) 

685 
thus ?thesis 

686 
by (intro exI[of _ "drop n ys"]) (auto simp: drop_map suffix_drop) 

687 
qed 

688 

689 
lemma suffix_remdups_adj: "suffix xs ys \<Longrightarrow> suffix (remdups_adj xs) (remdups_adj ys)" 

690 
using prefix_remdups_adj[of "rev xs" "rev ys"] 

691 
by (simp add: suffix_to_prefix) 

692 

65869  693 
lemma not_suffix_cases: 
694 
assumes pfx: "\<not> suffix ps ls" 

695 
obtains 

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

697 
 (c2) a as x xs where "ps = as@[a]" and "ls = xs@[x]" and "x = a" and "\<not> suffix as xs" 

698 
 (c3) a as x xs where "ps = as@[a]" and "ls = xs@[x]" and "x \<noteq> a" 

699 
proof (cases ps rule: rev_cases) 

700 
case Nil 

701 
then show ?thesis using pfx by simp 

702 
next 

703 
case (snoc as a) 

704 
note c = \<open>ps = as@[a]\<close> 

705 
show ?thesis 

706 
proof (cases ls rule: rev_cases) 

707 
case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_suffix_nil) 

708 
next 

709 
case (snoc xs x) 

710 
show ?thesis 

711 
proof (cases "x = a") 

712 
case True 

713 
have "\<not> suffix as xs" using pfx c snoc True by simp 

714 
with c snoc True show ?thesis by (rule c2) 

715 
next 

716 
case False 

717 
with c snoc show ?thesis by (rule c3) 

718 
qed 

719 
qed 

720 
qed 

721 

722 
lemma not_suffix_induct [consumes 1, case_names Nil Neq Eq]: 

723 
assumes np: "\<not> suffix ps ls" 

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

725 
and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (xs@[x]) (ys@[y])" 

726 
and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> suffix xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (xs@[x]) (ys@[y])" 

727 
shows "P ps ls" using np 

728 
proof (induct ls arbitrary: ps rule: rev_induct) 

729 
case Nil 

730 
then show ?case by (cases ps rule: rev_cases) (auto intro: base) 

731 
next 

732 
case (snoc y ys ps) 

733 
then have npfx: "\<not> suffix ps (ys @ [y])" by simp 

734 
then obtain x xs where pv: "ps = xs @ [x]" 

735 
by (rule not_suffix_cases) auto 

736 
show ?case by (metis snoc.hyps snoc_suffix_snoc npfx pv r1 r2) 

737 
qed 

738 

739 

63117  740 
lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefix x y" 
25692  741 
by blast 
25299  742 

63117  743 
lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefix y x" 
25692  744 
by blast 
25355  745 

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

25692  747 
unfolding parallel_def by simp 
25355  748 

25299  749 
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x" 
25692  750 
unfolding parallel_def by simp 
25299  751 

25564  752 
lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" 
25692  753 
by auto 
25299  754 

25564  755 
lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs" 
63117  756 
by (metis Cons_prefix_Cons parallelE parallelI) 
25665  757 

25299  758 
lemma not_equal_is_parallel: 
759 
assumes neq: "xs \<noteq> ys" 

25356  760 
and len: "length xs = length ys" 
761 
shows "xs \<parallel> ys" 

25299  762 
using len neq 
25355  763 
proof (induct rule: list_induct2) 
26445  764 
case Nil 
25356  765 
then show ?case by simp 
25299  766 
next 
26445  767 
case (Cons a as b bs) 
25355  768 
have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact 
25299  769 
show ?case 
770 
proof (cases "a = b") 

25355  771 
case True 
26445  772 
then have "as \<noteq> bs" using Cons by simp 
25355  773 
then show ?thesis by (rule Cons_parallelI2 [OF True ih]) 
25299  774 
next 
775 
case False 

25355  776 
then show ?thesis by (rule Cons_parallelI1) 
25299  777 
qed 
778 
qed 

22178  779 

71789  780 

65869  781 
subsection \<open>Suffixes\<close> 
782 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

783 
primrec suffixes where 
65869  784 
"suffixes [] = [[]]" 
785 
 "suffixes (x#xs) = suffixes xs @ [x # xs]" 

786 

787 
lemma in_set_suffixes [simp]: "xs \<in> set (suffixes ys) \<longleftrightarrow> suffix xs ys" 

788 
by (induction ys) (auto simp: suffix_def Cons_eq_append_conv) 

789 

790 
lemma distinct_suffixes [intro]: "distinct (suffixes xs)" 

791 
by (induction xs) (auto simp: suffix_def) 

792 

793 
lemma length_suffixes [simp]: "length (suffixes xs) = Suc (length xs)" 

794 
by (induction xs) auto 

795 

796 
lemma suffixes_snoc [simp]: "suffixes (xs @ [x]) = [] # map (\<lambda>ys. ys @ [x]) (suffixes xs)" 

797 
by (induction xs) auto 

798 

799 
lemma suffixes_not_Nil [simp]: "suffixes xs \<noteq> []" 

800 
by (cases xs) auto 

801 

802 
lemma hd_suffixes [simp]: "hd (suffixes xs) = []" 

803 
by (induction xs) simp_all 

804 

805 
lemma last_suffixes [simp]: "last (suffixes xs) = xs" 

806 
by (cases xs) simp_all 

807 

808 
lemma suffixes_append: 

809 
"suffixes (xs @ ys) = suffixes ys @ map (\<lambda>xs'. xs' @ ys) (tl (suffixes xs))" 

810 
proof (induction ys rule: rev_induct) 

811 
case Nil 

812 
thus ?case by (cases xs rule: rev_cases) auto 

813 
next 

814 
case (snoc y ys) 

815 
show ?case 

816 
by (simp only: append.assoc [symmetric] suffixes_snoc snoc.IH) simp 

817 
qed 

818 

819 
lemma suffixes_eq_snoc: 

820 
"suffixes ys = xs @ [x] \<longleftrightarrow> 

821 
(ys = [] \<and> xs = [] \<or> (\<exists>z zs. ys = z#zs \<and> xs = suffixes zs)) \<and> x = ys" 

822 
by (cases ys) auto 

823 

824 
lemma suffixes_tailrec [code]: 

825 
"suffixes xs = rev (snd (foldl (\<lambda>(acc1, acc2) x. (x#acc1, (x#acc1)#acc2)) ([],[[]]) (rev xs)))" 

826 
proof  

827 
have "foldl (\<lambda>(acc1, acc2) x. (x#acc1, (x#acc1)#acc2)) (ys, ys # zs) (rev xs) = 

828 
(xs @ ys, rev (map (\<lambda>as. as @ ys) (suffixes xs)) @ zs)" for ys zs 

829 
proof (induction xs arbitrary: ys zs) 

830 
case (Cons x xs ys zs) 

831 
from Cons.IH[of ys zs] 

832 
show ?case by (simp add: o_def case_prod_unfold) 

833 
qed simp_all 

834 
from this [of "[]" "[]"] show ?thesis by simp 

835 
qed 

836 

837 
lemma set_suffixes_eq: "set (suffixes xs) = {ys. suffix ys xs}" 

838 
by auto 

839 

840 
lemma card_set_suffixes [simp]: "card (set (suffixes xs)) = Suc (length xs)" 

841 
by (subst distinct_card) auto 

842 

843 
lemma set_suffixes_append: 

844 
"set (suffixes (xs @ ys)) = set (suffixes ys) \<union> {xs' @ ys xs'. xs' \<in> set (suffixes xs)}" 

845 
by (subst suffixes_append, cases xs rule: rev_cases) auto 

846 

847 

848 
lemma suffixes_conv_prefixes: "suffixes xs = map rev (prefixes (rev xs))" 

849 
by (induction xs) auto 

850 

851 
lemma prefixes_conv_suffixes: "prefixes xs = map rev (suffixes (rev xs))" 

852 
by (induction xs) auto 

853 

854 
lemma prefixes_rev: "prefixes (rev xs) = map rev (suffixes xs)" 

855 
by (induction xs) auto 

856 

857 
lemma suffixes_rev: "suffixes (rev xs) = map rev (prefixes xs)" 

858 
by (induction xs) auto 

859 

49087  860 

60500  861 
subsection \<open>Homeomorphic embedding on lists\<close> 
49087  862 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

863 
inductive list_emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
49087  864 
for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" 
865 
where 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

866 
list_emb_Nil [intro, simp]: "list_emb P [] ys" 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

867 
 list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)" 
57498
ea44ec62a574
no builtin reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the baseorder is)
Christian Sternagel
parents:
57497
diff
changeset

868 
 list_emb_Cons2 [intro]: "P x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)" 
50516  869 

57499
7e22776f2d32
added monotonicity lemma for list embedding
Christian Sternagel
parents:
57498
diff
changeset

870 
lemma list_emb_mono: 
7e22776f2d32
added monotonicity lemma for list embedding
Christian Sternagel
parents:
57498
diff
changeset

871 
assumes "\<And>x y. P x y \<longrightarrow> Q x y" 
7e22776f2d32
added monotonicity lemma for list embedding
Christian Sternagel
parents:
57498
diff
changeset

872 
shows "list_emb P xs ys \<longrightarrow> list_emb Q xs ys" 
7e22776f2d32
added monotonicity lemma for list embedding
Christian Sternagel
parents:
57498
diff
changeset

873 
proof 
7e22776f2d32
added monotonicity lemma for list embedding
Christian Sternagel
parents:
57498
diff
changeset

874 
assume "list_emb P xs ys" 
7e22776f2d32
added monotonicity lemma for list embedding
Christian Sternagel
parents:
57498
diff
changeset

875 
then show "list_emb Q xs ys" by (induct) (auto simp: assms) 
7e22776f2d32
added monotonicity lemma for list embedding
Christian Sternagel
parents:
57498
diff
changeset

876 
qed 
7e22776f2d32
added monotonicity lemma for list embedding
Christian Sternagel
parents:
57498
diff
changeset

877 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

878 
lemma list_emb_Nil2 [simp]: 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

879 
assumes "list_emb P xs []" shows "xs = []" 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

880 
using assms by (cases rule: list_emb.cases) auto 
49087  881 

57498
ea44ec62a574
no builtin reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the baseorder is)
Christian Sternagel
parents:
57497
diff
changeset

882 
lemma list_emb_refl: 
ea44ec62a574
no builtin reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the baseorder is)
Christian Sternagel
parents:
57497
diff
changeset

883 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> P x x" 
ea44ec62a574
no builtin reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the baseorder is)
Christian Sternagel
parents:
57497
diff
changeset

884 
shows "list_emb P xs xs" 
ea44ec62a574
no builtin reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the baseorder is)
Christian Sternagel
parents:
57497
diff
changeset

885 
using assms by (induct xs) auto 
49087  886 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

887 
lemma list_emb_Cons_Nil [simp]: "list_emb P (x#xs) [] = False" 
49087  888 
proof  
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

889 
{ assume "list_emb P (x#xs) []" 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

890 
from list_emb_Nil2 [OF this] have False by simp 
49087  891 
} moreover { 
892 
assume False 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

893 
then have "list_emb P (x#xs) []" by simp 
49087  894 
} ultimately show ?thesis by blast 
895 
qed 

896 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

897 
lemma list_emb_append2 [intro]: "list_emb P xs ys \<Longrightarrow> list_emb P xs (zs @ ys)" 
49087  898 
by (induct zs) auto 
899 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

900 
lemma list_emb_prefix [intro]: 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

901 
assumes "list_emb P xs ys" shows "list_emb P xs (ys @ zs)" 
49087  902 
using assms 
903 
by (induct arbitrary: zs) auto 

904 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

905 
lemma list_emb_ConsD: 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

906 
assumes "list_emb P (x#xs) ys" 
57498
ea44ec62a574
no builtin reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the baseorder is)
Christian Sternagel
parents:
57497
diff
changeset

907 
shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> list_emb P xs vs" 
49087  908 
using assms 
49107  909 
proof (induct x \<equiv> "x # xs" ys arbitrary: x xs) 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

910 
case list_emb_Cons 
49107  911 
then show ?case by (metis append_Cons) 
49087  912 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

913 
case (list_emb_Cons2 x y xs ys) 
54483  914 
then show ?case by blast 
49087  915 
qed 
916 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

917 
lemma list_emb_appendD: 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

918 
assumes "list_emb P (xs @ ys) zs" 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

919 
shows "\<exists>us vs. zs = us @ vs \<and> list_emb P xs us \<and> list_emb P ys vs" 
49087  920 
using assms 
921 
proof (induction xs arbitrary: ys zs) 

49107  922 
case Nil then show ?case by auto 
49087  923 
next 
924 
case (Cons x xs) 

54483  925 
then obtain us v vs where 
57498
ea44ec62a574
no builtin reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the baseorder is)
Christian Sternagel
parents:
57497
diff
changeset

926 
zs: "zs = us @ v # vs" and p: "P x v" and lh: "list_emb P (xs @ ys) vs" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

927 
by (auto dest: list_emb_ConsD) 
54483  928 
obtain sk\<^sub>0 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" and sk\<^sub>1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

929 
sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_emb P (xs @ x\<^sub>0) x\<^sub>1 \<or> sk\<^sub>0 x\<^sub>0 x\<^sub>1 @ sk\<^sub>1 x\<^sub>0 x\<^sub>1 = x\<^sub>1 \<and> list_emb P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_emb P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)" 
54483  930 
using Cons(1) by (metis (no_types)) 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

931 
hence "\<forall>x\<^sub>2. list_emb P (x # xs) (x\<^sub>2 @ v # sk\<^sub>0 ys vs)" using p lh by auto 
54483  932 
thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc) 
49087  933 
qed 
934 

63149  935 
lemma list_emb_strict_suffix: 
936 
assumes "list_emb P xs ys" and "strict_suffix ys zs" 

937 
shows "list_emb P xs zs" 

65869  938 
using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: strict_suffix_def suffix_def) 
63149  939 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

940 
lemma list_emb_suffix: 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

941 
assumes "list_emb P xs ys" and "suffix ys zs" 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

942 
shows "list_emb P xs zs" 
63149  943 
using assms and list_emb_strict_suffix 
944 
unfolding strict_suffix_reflclp_conv[symmetric] by auto 

49087  945 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

946 
lemma list_emb_length: "list_emb P xs ys \<Longrightarrow> length xs \<le> length ys" 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

947 
by (induct rule: list_emb.induct) auto 
49087  948 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

949 
lemma list_emb_trans: 
57500
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

950 
assumes "\<And>x y z. \<lbrakk>x \<in> set xs; y \<in> set ys; z \<in> set zs; P x y; P y z\<rbrakk> \<Longrightarrow> P x z" 
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

951 
shows "\<lbrakk>list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs" 
50516  952 
proof  
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

953 
assume "list_emb P xs ys" and "list_emb P ys zs" 
57500
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

954 
then show "list_emb P xs zs" using assms 
49087  955 
proof (induction arbitrary: zs) 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

956 
case list_emb_Nil show ?case by blast 
49087  957 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

958 
case (list_emb_Cons xs ys y) 
60500  959 
from list_emb_ConsD [OF \<open>list_emb P (y#ys) zs\<close>] obtain us v vs 
57500
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

960 
where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

961 
then have "list_emb P ys (v#vs)" by blast 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

962 
then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2) 
57500
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

963 
from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by auto 
49087  964 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

965 
case (list_emb_Cons2 x y xs ys) 
60500  966 
from list_emb_ConsD [OF \<open>list_emb P (y#ys) zs\<close>] obtain us v vs 
57498
ea44ec62a574
no builtin reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the baseorder is)
Christian Sternagel
parents:
57497
diff
changeset

967 
where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast 
57500
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

968 
with list_emb_Cons2 have "list_emb P xs vs" by auto 
57498
ea44ec62a574
no builtin reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the baseorder is)
Christian Sternagel
parents:
57497
diff
changeset

969 
moreover have "P x v" 
49087  970 
proof  
57500
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

971 
from zs have "v \<in> set zs" by auto 
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

972 
moreover have "x \<in> set (x#xs)" and "y \<in> set (y#ys)" by simp_all 
50516  973 
ultimately show ?thesis 
60500  974 
using \<open>P x y\<close> and \<open>P y v\<close> and list_emb_Cons2 
50516  975 
by blast 
49087  976 
qed 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

977 
ultimately have "list_emb P (x#xs) (v#vs)" by blast 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

978 
then show ?case unfolding zs by (rule list_emb_append2) 
49087  979 
qed 
980 
qed 

981 

57500
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

982 
lemma list_emb_set: 
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

983 
assumes "list_emb P xs ys" and "x \<in> set xs" 
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

984 
obtains y where "y \<in> set ys" and "P x y" 
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

985 
using assms by (induct) auto 
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

986 

65869  987 
lemma list_emb_Cons_iff1 [simp]: 
988 
assumes "P x y" 

989 
shows "list_emb P (x#xs) (y#ys) \<longleftrightarrow> list_emb P xs ys" 

990 
using assms by (subst list_emb.simps) (auto dest: list_emb_ConsD) 

991 

992 
lemma list_emb_Cons_iff2 [simp]: 

993 
assumes "\<not>P x y" 

994 
shows "list_emb P (x#xs) (y#ys) \<longleftrightarrow> list_emb P (x#xs) ys" 

995 
using assms by (subst list_emb.simps) auto 

996 

997 
lemma list_emb_code [code]: 

998 
"list_emb P [] ys \<longleftrightarrow> True" 

999 
"list_emb P (x#xs) [] \<longleftrightarrow> False" 

1000 
"list_emb P (x#xs) (y#ys) \<longleftrightarrow> (if P x y then list_emb P xs ys else list_emb P (x#xs) ys)" 

1001 
by simp_all 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1002 

65869  1003 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1004 
subsection \<open>Subsequences (special case of homeomorphic embedding)\<close> 
49087  1005 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1006 
abbreviation subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
67399  1007 
where "subseq xs ys \<equiv> list_emb (=) xs ys" 
65869  1008 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1009 
definition strict_subseq where "strict_subseq xs ys \<longleftrightarrow> xs \<noteq> ys \<and> subseq xs ys" 
49087  1010 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1011 
lemma subseq_Cons2: "subseq xs ys \<Longrightarrow> subseq (x#xs) (x#ys)" by auto 
49087  1012 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1013 
lemma subseq_same_length: 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1014 
assumes "subseq xs ys" and "length xs = length ys" shows "xs = ys" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1015 
using assms by (induct) (auto dest: list_emb_length) 
49087  1016 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1017 
lemma not_subseq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> subseq xs ys" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1018 
by (metis list_emb_length linorder_not_less) 
49087  1019 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1020 
lemma subseq_Cons': "subseq (x#xs) ys \<Longrightarrow> subseq xs ys" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1021 
by (induct xs, simp, blast dest: list_emb_ConsD) 
49087  1022 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1023 
lemma subseq_Cons2': 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1024 
assumes "subseq (x#xs) (x#ys)" shows "subseq xs ys" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1025 
using assms by (cases) (rule subseq_Cons') 
49087  1026 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1027 
lemma subseq_Cons2_neq: 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1028 
assumes "subseq (x#xs) (y#ys)" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1029 
shows "x \<noteq> y \<Longrightarrow> subseq (x#xs) ys" 
49087  1030 
using assms by (cases) auto 
1031 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1032 
lemma subseq_Cons2_iff [simp]: 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1033 
"subseq (x#xs) (y#ys) = (if x = y then subseq xs ys else subseq (x#xs) ys)" 
65869  1034 
by simp 
49087  1035 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1036 
lemma subseq_append': "subseq (zs @ xs) (zs @ ys) \<longleftrightarrow> subseq xs ys" 
49087  1037 
by (induct zs) simp_all 
65869  1038 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1039 
interpretation subseq_order: order subseq strict_subseq 
65869  1040 
proof 
1041 
fix xs ys :: "'a list" 

1042 
{ 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1043 
assume "subseq xs ys" and "subseq ys xs" 
65869  1044 
thus "xs = ys" 
1045 
proof (induct) 

1046 
case list_emb_Nil 

1047 
from list_emb_Nil2 [OF this] show ?case by simp 

1048 
next 

1049 
case list_emb_Cons2 

1050 
thus ?case by simp 

1051 
next 

1052 
case list_emb_Cons 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1053 
hence False using subseq_Cons' by fastforce 
65869  1054 
thus ?case .. 
1055 
qed 

1056 
} 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1057 
thus "strict_subseq xs ys \<longleftrightarrow> (subseq xs ys \<and> \<not>subseq ys xs)" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1058 
by (auto simp: strict_subseq_def) 
65869  1059 
qed (auto simp: list_emb_refl intro: list_emb_trans) 
49087  1060 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1061 
lemma in_set_subseqs [simp]: "xs \<in> set (subseqs ys) \<longleftrightarrow> subseq xs ys" 
65869  1062 
proof 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1063 
assume "xs \<in> set (subseqs ys)" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1064 
thus "subseq xs ys" 
65869  1065 
by (induction ys arbitrary: xs) (auto simp: Let_def) 
49087  1066 
next 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1067 
have [simp]: "[] \<in> set (subseqs ys)" for ys :: "'a list" 
65869  1068 
by (induction ys) (auto simp: Let_def) 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1069 
assume "subseq xs ys" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1070 
thus "xs \<in> set (subseqs ys)" 
65869  1071 
by (induction xs ys rule: list_emb.induct) (auto simp: Let_def) 
49087  1072 
qed 
1073 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1074 
lemma set_subseqs_eq: "set (subseqs ys) = {xs. subseq xs ys}" 
65869  1075 
by auto 
49087  1076 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1077 
lemma subseq_append_le_same_iff: "subseq (xs @ ys) ys \<longleftrightarrow> xs = []" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1078 
by (auto dest: list_emb_length) 
49087  1079 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1080 
lemma subseq_singleton_left: "subseq [x] ys \<longleftrightarrow> x \<in> set ys" 
64886  1081 
by (fastforce dest: list_emb_ConsD split_list_last) 
1082 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1083 
lemma list_emb_append_mono: 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1084 
"\<lbrakk> list_emb P xs xs'; list_emb P ys ys' \<rbrakk> \<Longrightarrow> list_emb P (xs@ys) (xs'@ys')" 
65957  1085 
by (induct rule: list_emb.induct) auto 
1086 

1087 
lemma prefix_imp_subseq [intro]: "prefix xs ys \<Longrightarrow> subseq xs ys" 

1088 
by (auto simp: prefix_def) 

1089 

1090 
lemma suffix_imp_subseq [intro]: "suffix xs ys \<Longrightarrow> subseq xs ys" 

1091 
by (auto simp: suffix_def) 

49087  1092 

1093 

60500  1094 
subsection \<open>Appending elements\<close> 
49087  1095 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1096 
lemma subseq_append [simp]: 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1097 
"subseq (xs @ zs) (ys @ zs) \<longleftrightarrow> subseq xs ys" (is "?l = ?r") 
49087  1098 
proof 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1099 
{ fix xs' ys' xs ys zs :: "'a list" assume "subseq xs' ys'" 
67091  1100 
then have "xs' = xs @ zs \<and> ys' = ys @ zs \<longrightarrow> subseq xs ys" 
49087  1101 
proof (induct arbitrary: xs ys zs) 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1102 
case list_emb_Nil show ?case by simp 
49087  1103 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1104 
case (list_emb_Cons xs' ys' x) 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1105 
{ assume "ys=[]" then have ?case using list_emb_Cons(1) by auto } 
49087  1106 
moreover 
1107 
{ fix us assume "ys = x#us" 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1108 
then have ?case using list_emb_Cons(2) by(simp add: list_emb.list_emb_Cons) } 
49087  1109 
ultimately show ?case by (auto simp:Cons_eq_append_conv) 
1110 
next 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1111 
case (list_emb_Cons2 x y xs' ys') 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1112 
{ assume "xs=[]" then have ?case using list_emb_Cons2(1) by auto } 
49087  1113 
moreover 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1114 
{ fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_emb_Cons2 by auto} 
49087  1115 
moreover 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1116 
{ fix us assume "xs=x#us" "ys=[]" then have ?case using list_emb_Cons2(2) by bestsimp } 
67399  1117 
ultimately show ?case using \<open>(=) x y\<close> by (auto simp: Cons_eq_append_conv) 
49087  1118 
qed } 
1119 
moreover assume ?l 

1120 
ultimately show ?r by blast 

1121 
next 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1122 
assume ?r then show ?l by (metis list_emb_append_mono subseq_order.order_refl) 
49087  1123 
qed 
1124 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1125 
lemma subseq_append_iff: 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1126 
"subseq xs (ys @ zs) \<longleftrightarrow> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> subseq xs1 ys \<and> subseq xs2 zs)" 
65869  1127 
(is "?lhs = ?rhs") 
1128 
proof 

1129 
assume ?lhs thus ?rhs 

1130 
proof (induction xs "ys @ zs" arbitrary: ys zs rule: list_emb.induct) 

1131 
case (list_emb_Cons xs ws y ys zs) 

1132 
from list_emb_Cons(2)[of "tl ys" zs] and list_emb_Cons(2)[of "[]" "tl zs"] and list_emb_Cons(1,3) 

1133 
show ?case by (cases ys) auto 

1134 
next 

1135 
case (list_emb_Cons2 x y xs ws ys zs) 

1136 
from list_emb_Cons2(3)[of "tl ys" zs] and list_emb_Cons2(3)[of "[]" "tl zs"] 

1137 
and list_emb_Cons2(1,2,4) 

1138 
show ?case by (cases ys) (auto simp: Cons_eq_append_conv) 

1139 
qed auto 

1140 
qed (auto intro: list_emb_append_mono) 

1141 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1142 
lemma subseq_appendE [case_names append]: 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1143 
assumes "subseq xs (ys @ zs)" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1144 
obtains xs1 xs2 where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1145 
using assms by (subst (asm) subseq_append_iff) auto 
65869  1146 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1147 
lemma subseq_drop_many: "subseq xs ys \<Longrightarrow> subseq xs (zs @ ys)" 
49087  1148 
by (induct zs) auto 
1149 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1150 
lemma subseq_rev_drop_many: "subseq xs ys \<Longrightarrow> subseq xs (ys @ zs)" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1151 
by (metis append_Nil2 list_emb_Nil list_emb_append_mono) 
49087  1152 

1153 

60500  1154 
subsection \<open>Relation to standard list operations\<close> 
49087  1155 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1156 
lemma subseq_map: 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1157 
assumes "subseq xs ys" shows "subseq (map f xs) (map f ys)" 
49087  1158 
using assms by (induct) auto 
1159 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1160 
lemma subseq_filter_left [simp]: "subseq (filter P xs) xs" 
49087  1161 
by (induct xs) auto 
1162 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1163 
lemma subseq_filter [simp]: 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1164 
assumes "subseq xs ys" shows "subseq (filter P xs) (filter P ys)" 
54483  1165 
using assms by induct auto 
49087  1166 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1167 
lemma subseq_conv_nths: 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1168 
"subseq xs ys \<longleftrightarrow> (\<exists>N. xs = nths ys N)" (is "?L = ?R") 
49087  1169 
proof 
1170 
assume ?L 

49107  1171 
then show ?R 
49087  1172 
proof (induct) 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1173 
case list_emb_Nil show ?case by (metis nths_empty) 
49087  1174 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1175 
case (list_emb_Cons xs ys x) 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1176 
then obtain N where "xs = nths ys N" by blast 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1177 
then have "xs = nths (x#ys) (Suc ` N)" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1178 
by (clarsimp simp add: nths_Cons inj_image_mem_iff) 
49107  1179 
then show ?case by blast 
49087  1180 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1181 
case (list_emb_Cons2 x y xs ys) 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1182 
then obtain N where "xs = nths ys N" by blast 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1183 
then have "x#xs = nths (x#ys) (insert 0 (Suc ` N))" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1184 
by (clarsimp simp add: nths_Cons inj_image_mem_iff) 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1185 
moreover from list_emb_Cons2 have "x = y" by simp 
50516  1186 
ultimately show ?case by blast 
49087  1187 
qed 
1188 
next 

1189 
assume ?R 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1190 
then obtain N where "xs = nths ys N" .. 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1191 
moreover have "subseq (nths ys N) ys" 
49107  1192 
proof (induct ys arbitrary: N) 
49087  1193 
case Nil show ?case by simp 
1194 
next 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1195 
case Cons then show ?case by (auto simp: nths_Cons) 
49087  1196 
qed 
1197 
ultimately show ?L by simp 

1198 
qed 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1199 

639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1200 

639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1201 
subsection \<open>Contiguous sublists\<close> 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1202 

71789  1203 
subsubsection \<open>\<open>sublist\<close>\<close> 
1204 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1205 
definition sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1206 
"sublist xs ys = (\<exists>ps ss. ys = ps @ xs @ ss)" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1207 

639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1208 
definition strict_sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1209 
"strict_sublist xs ys \<longleftrightarrow> sublist xs ys \<and> xs \<noteq 