author  desharna 
Fri, 05 Mar 2021 15:01:59 +0100  
changeset 73381  3fdb94d87e0e 
parent 73380  99c1c4f89605 
child 73397  d47c8a89c6a5 
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 

73380
99c1c4f89605
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(takedrop)While
desharna
parents:
73186
diff
changeset

141 
lemma takeWhile_is_prefix: "prefix (takeWhile P xs) xs" 
99c1c4f89605
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(takedrop)While
desharna
parents:
73186
diff
changeset

142 
unfolding prefix_def by (metis takeWhile_dropWhile_id) 
99c1c4f89605
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(takedrop)While
desharna
parents:
73186
diff
changeset

143 

63155  144 
lemma prefixeq_butlast: "prefix (butlast xs) xs" 
145 
by (simp add: butlast_conv_take take_is_prefix) 

146 

71789  147 
lemma prefix_map_rightE: 
148 
assumes "prefix xs (map f ys)" 

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

150 
proof  

151 
define n where "n = length xs" 

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

153 
using assms by (auto simp: prefix_def n_def) 

154 
thus ?thesis 

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

156 
qed 

157 

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

160 

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

162 
by (auto simp: prefix_def) 

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

163 

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

166 

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

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

169 

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

172 

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

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

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

177 
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

178 

63117  179 
lemma take_strict_prefix: "strict_prefix xs ys \<Longrightarrow> strict_prefix (take n xs) ys" 
63649  180 
proof (induct n arbitrary: xs ys) 
181 
case 0 

182 
then show ?case by (cases ys) simp_all 

183 
next 

184 
case (Suc n) 

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

186 
qed 

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

187 

71789  188 
lemma prefix_takeWhile: 
189 
assumes "prefix xs ys" 

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

191 
proof  

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

193 
by (auto simp: prefix_def) 

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

195 
by (induction xs) auto 

196 
thus ?thesis by (simp add: ys) 

197 
qed 

198 

199 
lemma prefix_dropWhile: 

200 
assumes "prefix xs ys" 

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

202 
proof  

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

204 
by (auto simp: prefix_def) 

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

206 
by (induction xs) auto 

207 
thus ?thesis by (simp add: ys) 

208 
qed 

209 

210 
lemma prefix_remdups_adj: 

211 
assumes "prefix xs ys" 

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

213 
using assms 

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

215 
case (less xs) 

216 
show ?case 

217 
proof (cases xs) 

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

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

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

221 
from less show ?thesis 

222 
by (auto simp: remdups_adj_Cons' less_Suc_eq_le length_dropWhile_le 

223 
intro!: less prefix_dropWhile) 

224 
qed auto 

225 
qed 

226 

63117  227 
lemma not_prefix_cases: 
228 
assumes pfx: "\<not> prefix ps ls" 

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

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

230 
(c1) "ps \<noteq> []" and "ls = []" 
63117  231 
 (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

232 
 (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

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

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

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

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

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

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

240 
proof (cases ls) 
63117  241 
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

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

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

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

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

246 
case True 
63117  247 
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

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

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

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

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

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

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

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

255 

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

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

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

259 
and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)" 
63117  260 
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

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

262 
proof (induct ls arbitrary: ps) 
63649  263 
case Nil 
264 
then show ?case 

63117  265 
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

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

267 
case (Cons y ys) 
63117  268 
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

269 
then obtain x xs where pv: "ps = x # xs" 
63117  270 
by (rule not_prefix_cases) auto 
271 
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

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

273 

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

274 

63155  275 
subsection \<open>Prefixes\<close> 
276 

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

277 
primrec prefixes where 
63155  278 
"prefixes [] = [[]]"  
67399  279 
"prefixes (x#xs) = [] # map ((#) x) (prefixes xs)" 
63155  280 

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

63649  282 
proof (induct xs arbitrary: ys) 
283 
case Nil 

284 
then show ?case by (cases ys) auto 

285 
next 

286 
case (Cons a xs) 

287 
then show ?case by (cases ys) auto 

288 
qed 

63155  289 

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

65869  291 
by (induction xs) auto 
292 

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

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

295 

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

297 
by (induction xs) auto 

298 

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

300 
by (cases xs) auto 

63155  301 

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

63155  304 

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

307 

308 
lemma prefixes_append: 

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

310 
proof (induction xs) 

311 
case Nil 

312 
thus ?case by (cases ys) auto 

313 
qed simp_all 

314 

315 
lemma prefixes_eq_snoc: 

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

65869  318 
by (cases ys rule: rev_cases) auto 
319 

320 
lemma prefixes_tailrec [code]: 

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

322 
proof  

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

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

325 
proof (induction xs arbitrary: ys zs) 

326 
case (Cons x xs ys zs) 

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

328 
show ?case by (simp add: o_def) 

329 
qed simp_all 

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

331 
qed 

332 

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

334 
by auto 

335 

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

337 
by (subst distinct_card) auto 

338 

339 
lemma set_prefixes_append: 

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

341 
by (subst prefixes_append, cases ys) auto 

63155  342 

343 

63173  344 
subsection \<open>Longest Common Prefix\<close> 
345 

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

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

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

350 
\<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)" 

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

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

353 
case 0 

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

357 
thus ?case .. 

358 
next 

359 
case (Suc n) 

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

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

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

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

364 
show ?case 

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

366 
case True 

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

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

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

370 
by  (rule Least_equality, fastforce+) 

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

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

373 
{ fix qs 

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

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

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

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

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

379 
} 

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

381 
thus ?thesis .. 

382 
next 

383 
case False 

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

385 
by (auto) (metis list.exhaust) 

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

387 
by auto (metis Cons_prefix_Cons prefix_Cons) 

388 
hence "?P L []" by auto 

389 
thus ?thesis .. 

390 
qed 

391 
qed 

392 

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

394 
\<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)" 

395 
by(rule ex_ex1I[OF Longest_common_prefix_ex]; 

396 
meson equals0I prefix_length_prefix prefix_order.antisym) 

397 

398 
lemma Longest_common_prefix_eq: 

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

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

401 
\<Longrightarrow> Longest_common_prefix L = ps" 

65954  402 
unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder 
63173  403 
by(rule some1_equality[OF Longest_common_prefix_unique]) auto 
404 

405 
lemma Longest_common_prefix_prefix: 

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

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

410 
lemma Longest_common_prefix_longest: 

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

65954  412 
unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder 
63173  413 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 
414 

415 
lemma Longest_common_prefix_max_prefix: 

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

417 
by(metis Longest_common_prefix_prefix Longest_common_prefix_longest 

418 
prefix_length_prefix ex_in_conv) 

419 

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

421 
using Longest_common_prefix_prefix prefix_Nil by blast 

422 

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

67399  424 
Longest_common_prefix ((#) x ` L) = x # Longest_common_prefix L" 
63173  425 
apply(rule Longest_common_prefix_eq) 
426 
apply(simp) 

427 
apply (simp add: Longest_common_prefix_prefix) 

428 
apply simp 

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

430 
Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc) 

431 

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

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

434 
proof  

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

438 
by (metis Longest_common_prefix_image_Cons image_is_empty assms(1)) 

439 
qed 

440 

441 
lemma Longest_common_prefix_eq_Nil: 

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

443 
by (metis Longest_common_prefix_prefix list.inject prefix_Cons) 

444 

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

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

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

448 
"longest_common_prefix _ _ = []" 

449 

450 
lemma longest_common_prefix_prefix1: 

451 
"prefix (longest_common_prefix xs ys) xs" 

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

453 

454 
lemma longest_common_prefix_prefix2: 

455 
"prefix (longest_common_prefix xs ys) ys" 

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

457 

458 
lemma longest_common_prefix_max_prefix: 

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

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

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

462 
(auto simp: prefix_Cons) 

463 

464 

60500  465 
subsection \<open>Parallel lists\<close> 
10389  466 

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

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

472 

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

477 

63117  478 
theorem prefix_cases: 
479 
obtains "prefix xs ys"  "strict_prefix ys xs"  "xs \<parallel> ys" 

480 
unfolding parallel_def strict_prefix_def by blast 

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

481 

73186  482 
lemma parallel_cancel: "a#xs \<parallel> a#ys \<Longrightarrow> xs \<parallel> ys" 
483 
by (simp add: parallel_def) 

484 

10389  485 
theorem parallel_decomp: 
50516  486 
"xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 
73186  487 
proof (induct rule: list_induct2', blast, force, force) 
488 
case (4 x xs y ys) 

489 
then show ?case 

490 
proof (cases "x \<noteq> y", blast) 

491 
assume "\<not> x \<noteq> y" hence "x = y" by blast 

492 
then show ?thesis 

493 
using "4.hyps"[OF parallel_cancel[OF "4.prems"[folded \<open>x = y\<close>]]] 

494 
by (meson Cons_eq_appendI) 

10389  495 
qed 
496 
qed 

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

497 

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

63117  501 
induct rule: not_prefix_induct, simp+)+ 
25692  502 
done 
25299  503 

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

25299  506 

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

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

509 

25356  510 

60500  511 
subsection \<open>Suffix order on lists\<close> 
17201  512 

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

49087  515 

63149  516 
definition strict_suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
65869  517 
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

518 

65869  519 
interpretation suffix_order: order suffix strict_suffix 
520 
by standard (auto simp: suffix_def strict_suffix_def) 

521 

522 
interpretation suffix_bot: order_bot Nil suffix strict_suffix 

523 
by standard (simp add: suffix_def) 

49087  524 

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

21305  527 

63149  528 
lemma suffixE [elim?]: 
529 
assumes "suffix xs ys" 

49087  530 
obtains zs where "ys = zs @ xs" 
63149  531 
using assms unfolding suffix_def by blast 
65957  532 

63149  533 
lemma suffix_tl [simp]: "suffix (tl xs) xs" 
49087  534 
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

535 

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

65869  539 
lemma Nil_suffix [simp]: "suffix [] xs" 
63149  540 
by (simp add: suffix_def) 
49087  541 

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

544 

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

546 
by (auto simp add: suffix_def) 

547 

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

549 
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

550 

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

553 

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

555 
by (auto simp add: suffix_def) 

49087  556 

63149  557 
lemma strict_suffix_set_subset: "strict_suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" 
65869  558 
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

559 

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

49087  562 

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

565 

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

573 

63149  574 
lemma suffix_to_prefix [code]: "suffix xs ys \<longleftrightarrow> prefix (rev xs) (rev ys)" 
49087  575 
proof 
63149  576 
assume "suffix xs ys" 
49087  577 
then obtain zs where "ys = zs @ xs" .. 
578 
then have "rev ys = rev xs @ rev zs" by simp 

63117  579 
then show "prefix (rev xs) (rev ys)" .. 
49087  580 
next 
63117  581 
assume "prefix (rev xs) (rev ys)" 
49087  582 
then obtain zs where "rev ys = rev xs @ zs" .. 
583 
then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp 

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

63149  585 
then show "suffix xs ys" .. 
21305  586 
qed 
65869  587 

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

589 
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

590 

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

17201  593 

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

596 

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

598 
by (auto simp: suffix_def) 

25299  599 

63149  600 
lemma suffix_drop: "suffix (drop n as) as" 
73380
99c1c4f89605
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(takedrop)While
desharna
parents:
73186
diff
changeset

601 
unfolding suffix_def by (metis append_take_drop_id) 
99c1c4f89605
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(takedrop)While
desharna
parents:
73186
diff
changeset

602 

99c1c4f89605
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(takedrop)While
desharna
parents:
73186
diff
changeset

603 
lemma suffix_dropWhile: "suffix (dropWhile P xs) xs" 
99c1c4f89605
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(takedrop)While
desharna
parents:
73186
diff
changeset

604 
unfolding suffix_def by (metis takeWhile_dropWhile_id) 
25299  605 

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

25299  608 

63149  609 
lemma strict_suffix_reflclp_conv: "strict_suffix\<^sup>=\<^sup>= = suffix" 
65869  610 
by (intro ext) (auto simp: suffix_def strict_suffix_def) 
63149  611 

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

613 
unfolding suffix_def by auto 

49087  614 

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

617 

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

619 
by (auto simp add: suffix_def) 

620 

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

622 
by (simp add: suffix_to_prefix) 

623 

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

625 
by (simp add: suffix_to_prefix) 

626 

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

628 
unfolding suffix_def by (auto simp: Cons_eq_append_conv) 

629 

630 
theorem suffix_append: 

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

632 
by (auto simp: suffix_def append_eq_append_conv2) 

633 

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

635 
by (auto simp add: suffix_def) 

636 

637 
lemma suffix_same_cases: 

638 
"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" 

639 
unfolding suffix_def by (force simp: append_eq_append_conv2) 

640 

641 
lemma suffix_length_suffix: 

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

643 
by (auto simp: suffix_to_prefix intro: prefix_length_prefix) 

644 

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

646 
by (auto simp: strict_suffix_def suffix_def) 

647 

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

649 
by (auto simp: strict_suffix_def suffix_def) 

650 

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

652 
proof (induct n arbitrary: xs ys) 

653 
case 0 

654 
then show ?case by (cases ys) simp_all 

655 
next 

656 
case (Suc n) 

657 
then show ?case 

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

659 
qed 

660 

71789  661 
lemma suffix_map_rightE: 
662 
assumes "suffix xs (map f ys)" 

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

664 
proof  

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

666 
by (auto simp: suffix_def) 

667 
define n where "n = length xs'" 

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

669 
by (simp add: xs' n_def) 

670 
thus ?thesis 

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

672 
qed 

673 

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

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

676 
by (simp add: suffix_to_prefix) 

677 

65869  678 
lemma not_suffix_cases: 
679 
assumes pfx: "\<not> suffix ps ls" 

680 
obtains 

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

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

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

684 
proof (cases ps rule: rev_cases) 

685 
case Nil 

686 
then show ?thesis using pfx by simp 

687 
next 

688 
case (snoc as a) 

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

690 
show ?thesis 

691 
proof (cases ls rule: rev_cases) 

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

693 
next 

694 
case (snoc xs x) 

695 
show ?thesis 

696 
proof (cases "x = a") 

697 
case True 

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

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

700 
next 

701 
case False 

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

703 
qed 

704 
qed 

705 
qed 

706 

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

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

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

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

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

712 
shows "P ps ls" using np 

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

714 
case Nil 

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

716 
next 

717 
case (snoc y ys ps) 

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

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

720 
by (rule not_suffix_cases) auto 

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

722 
qed 

723 

724 

63117  725 
lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefix x y" 
25692  726 
by blast 
25299  727 

63117  728 
lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefix y x" 
25692  729 
by blast 
25355  730 

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

25692  732 
unfolding parallel_def by simp 
25355  733 

25299  734 
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x" 
25692  735 
unfolding parallel_def by simp 
25299  736 

25564  737 
lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" 
25692  738 
by auto 
25299  739 

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

25299  743 
lemma not_equal_is_parallel: 
744 
assumes neq: "xs \<noteq> ys" 

25356  745 
and len: "length xs = length ys" 
746 
shows "xs \<parallel> ys" 

25299  747 
using len neq 
25355  748 
proof (induct rule: list_induct2) 
26445  749 
case Nil 
25356  750 
then show ?case by simp 
25299  751 
next 
26445  752 
case (Cons a as b bs) 
25355  753 
have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact 
25299  754 
show ?case 
755 
proof (cases "a = b") 

25355  756 
case True 
26445  757 
then have "as \<noteq> bs" using Cons by simp 
25355  758 
then show ?thesis by (rule Cons_parallelI2 [OF True ih]) 
25299  759 
next 
760 
case False 

25355  761 
then show ?thesis by (rule Cons_parallelI1) 
25299  762 
qed 
763 
qed 

22178  764 

71789  765 

65869  766 
subsection \<open>Suffixes\<close> 
767 

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

768 
primrec suffixes where 
65869  769 
"suffixes [] = [[]]" 
770 
 "suffixes (x#xs) = suffixes xs @ [x # xs]" 

771 

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

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

774 

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

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

777 

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

779 
by (induction xs) auto 

780 

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

782 
by (induction xs) auto 

783 

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

785 
by (cases xs) auto 

786 

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

788 
by (induction xs) simp_all 

789 

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

791 
by (cases xs) simp_all 

792 

793 
lemma suffixes_append: 

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

795 
proof (induction ys rule: rev_induct) 

796 
case Nil 

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

798 
next 

799 
case (snoc y ys) 

800 
show ?case 

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

802 
qed 

803 

804 
lemma suffixes_eq_snoc: 

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

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

807 
by (cases ys) auto 

808 

809 
lemma suffixes_tailrec [code]: 

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

811 
proof  

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

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

814 
proof (induction xs arbitrary: ys zs) 

815 
case (Cons x xs ys zs) 

816 
from Cons.IH[of ys zs] 

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

818 
qed simp_all 

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

820 
qed 

821 

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

823 
by auto 

824 

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

826 
by (subst distinct_card) auto 

827 

828 
lemma set_suffixes_append: 

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

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

831 

832 

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

834 
by (induction xs) auto 

835 

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

837 
by (induction xs) auto 

838 

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

840 
by (induction xs) auto 

841 

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

843 
by (induction xs) auto 

844 

49087  845 

60500  846 
subsection \<open>Homeomorphic embedding on lists\<close> 
49087  847 

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

848 
inductive list_emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
49087  849 
for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" 
850 
where 

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

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

852 
 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

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

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

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

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

857 
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

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

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

860 
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

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

862 

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

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

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

865 
using assms by (cases rule: list_emb.cases) auto 
49087  866 

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

867 
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

868 
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

869 
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

870 
using assms by (induct xs) auto 
49087  871 

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

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

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

875 
from list_emb_Nil2 [OF this] have False by simp 
49087  876 
} moreover { 
877 
assume False 

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

878 
then have "list_emb P (x#xs) []" by simp 
49087  879 
} ultimately show ?thesis by blast 
880 
qed 

881 

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

882 
lemma list_emb_append2 [intro]: "list_emb P xs ys \<Longrightarrow> list_emb P xs (zs @ ys)" 
49087  883 
by (induct zs) auto 
884 

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

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

886 
assumes "list_emb P xs ys" shows "list_emb P xs (ys @ zs)" 
49087  887 
using assms 
888 
by (induct arbitrary: zs) auto 

889 

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

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

891 
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

892 
shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> list_emb P xs vs" 
49087  893 
using assms 
49107  894 
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

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

898 
case (list_emb_Cons2 x y xs ys) 
54483  899 
then show ?case by blast 
49087  900 
qed 
901 

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

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

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

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

49107  907 
case Nil then show ?case by auto 
49087  908 
next 
909 
case (Cons x xs) 

54483  910 
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

911 
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

912 
by (auto dest: list_emb_ConsD) 
54483  913 
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

914 
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  915 
using Cons(1) by (metis (no_types)) 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

916 
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  917 
thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc) 
49087  918 
qed 
919 

63149  920 
lemma list_emb_strict_suffix: 
921 
assumes "list_emb P xs ys" and "strict_suffix ys zs" 

922 
shows "list_emb P xs zs" 

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

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

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

926 
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

927 
shows "list_emb P xs zs" 
63149  928 
using assms and list_emb_strict_suffix 
929 
unfolding strict_suffix_reflclp_conv[symmetric] by auto 

49087  930 

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

931 
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

932 
by (induct rule: list_emb.induct) auto 
49087  933 

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

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

935 
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

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

938 
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

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

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

943 
case (list_emb_Cons xs ys y) 
60500  944 
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

945 
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

946 
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

947 
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

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

950 
case (list_emb_Cons2 x y xs ys) 
60500  951 
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

952 
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

953 
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

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

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

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

962 
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

963 
then show ?case unfolding zs by (rule list_emb_append2) 
49087  964 
qed 
965 
qed 

966 

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

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

968 
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

969 
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

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

971 

65869  972 
lemma list_emb_Cons_iff1 [simp]: 
973 
assumes "P x y" 

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

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

976 

977 
lemma list_emb_Cons_iff2 [simp]: 

978 
assumes "\<not>P x y" 

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

980 
using assms by (subst list_emb.simps) auto 

981 

982 
lemma list_emb_code [code]: 

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

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

985 
"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)" 

986 
by simp_all 

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

987 

65869  988 

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

989 
subsection \<open>Subsequences (special case of homeomorphic embedding)\<close> 
49087  990 

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

991 
abbreviation subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
67399  992 
where "subseq xs ys \<equiv> list_emb (=) xs ys" 
65869  993 

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

994 
definition strict_subseq where "strict_subseq xs ys \<longleftrightarrow> xs \<noteq> ys \<and> subseq xs ys" 
49087  995 

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

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

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

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

999 
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

1000 
using assms by (induct) (auto dest: list_emb_length) 
49087  1001 

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

1002 
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

1003 
by (metis list_emb_length linorder_not_less) 
49087  1004 

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

1005 
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

1006 
by (induct xs, simp, blast dest: list_emb_ConsD) 
49087  1007 

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

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

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

1010 
using assms by (cases) (rule subseq_Cons') 
49087  1011 

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

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

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

1014 
shows "x \<noteq> y \<Longrightarrow> subseq (x#xs) ys" 
49087  1015 
using assms by (cases) auto 
1016 

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

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

1018 
"subseq (x#xs) (y#ys) = (if x = y then subseq xs ys else subseq (x#xs) ys)" 
65869  1019 
by simp 
49087  1020 

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

1021 
lemma subseq_append': "subseq (zs @ xs) (zs @ ys) \<longleftrightarrow> subseq xs ys" 
49087  1022 
by (induct zs) simp_all 
65869  1023 

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

1024 
interpretation subseq_order: order subseq strict_subseq 
65869  1025 
proof 
1026 
fix xs ys :: "'a list" 

1027 
{ 

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

1028 
assume "subseq xs ys" and "subseq ys xs" 
65869  1029 
thus "xs = ys" 
1030 
proof (induct) 

1031 
case list_emb_Nil 

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

1033 
next 

1034 
case list_emb_Cons2 

1035 
thus ?case by simp 

1036 
next 

1037 
case list_emb_Cons 

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

1038 
hence False using subseq_Cons' by fastforce 
65869  1039 
thus ?case .. 
1040 
qed 

1041 
} 

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

1042 
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

1043 
by (auto simp: strict_subseq_def) 
65869  1044 
qed (auto simp: list_emb_refl intro: list_emb_trans) 
49087  1045 

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

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

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

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

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

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

1055 
thus "xs \<in> set (subseqs ys)" 
65869  1056 
by (induction xs ys rule: list_emb.induct) (auto simp: Let_def) 
49087  1057 
qed 
1058 

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

1059 
lemma set_subseqs_eq: "set (subseqs ys) = {xs. subseq xs ys}" 
65869  1060 
by auto 
49087  1061 

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

1062 
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

1063 
by (auto dest: list_emb_length) 
49087  1064 

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

1065 
lemma subseq_singleton_left: "subseq [x] ys \<longleftrightarrow> x \<in> set ys" 
64886  1066 
by (fastforce dest: list_emb_ConsD split_list_last) 
1067 

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

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

1069 
"\<lbrakk> list_emb P xs xs'; list_emb P ys ys' \<rbrakk> \<Longrightarrow> list_emb P (xs@ys) (xs'@ys')" 
65957  1070 
by (induct rule: list_emb.induct) auto 
1071 

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

1073 
by (auto simp: prefix_def) 

1074 

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

1076 
by (auto simp: suffix_def) 

49087  1077 

1078 

60500  1079 
subsection \<open>Appending elements\<close> 
49087  1080 

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

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

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

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

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

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

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

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

1093 
then have ?case using list_emb_Cons(2) by(simp add: list_emb.list_emb_Cons) } 
49087  1094 
ultimately show ?case by (auto simp:Cons_eq_append_conv) 
1095 
next 

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

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

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

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

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

1105 
ultimately show ?r by blast 

1106 
next 

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

1107 
assume ?r then show ?l by (metis list_emb_append_mono subseq_order.order_refl) 
49087  1108 
qed 
1109 

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

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

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

1114 
assume ?lhs thus ?rhs 

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

1116 
case (list_emb_Cons xs ws y ys zs) 

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

1118 
show ?case by (cases ys) auto 

1119 
next 

1120 
case (list_emb_Cons2 x y xs ws ys zs) 

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

1122 
and list_emb_Cons2(1,2,4) 

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

1124 
qed auto 

1125 
qed (auto intro: list_emb_append_mono) 

1126 

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

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

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

1129 
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

1130 
using assms by (subst (asm) subseq_append_iff) auto 
65869  1131 

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

1132 
lemma subseq_drop_many: "subseq xs ys \<Longrightarrow> subseq xs (zs @ ys)" 
49087  1133 
by (induct zs) auto 
1134 

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

1135 
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

1136 
by (metis append_Nil2 list_emb_Nil list_emb_append_mono) 
49087  1137 

1138 

60500  1139 
subsection \<open>Relation to standard list operations\<close> 
49087  1140 

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

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

1142 
assumes "subseq xs ys" shows "subseq (map f xs) (map f ys)" 
49087  1143 
using assms by (induct) auto 
1144 

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

1145 
lemma subseq_filter_left [simp]: "subseq (filter P xs) xs" 
49087  1146 
by (induct xs) auto 
1147 

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

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

1149 
assumes "subseq xs ys" shows "subseq (filter P xs) (filter P ys)" 
54483  1150 
using assms by induct auto 
49087  1151 

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

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

1153 
"subseq xs ys \<longleftrightarrow> (\<exists>N. xs = nths ys N)" (is "?L = ?R") 
49087  1154 
proof 
1155 
assume ?L 

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

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

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

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

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

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

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

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

1168 
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

1169 
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

1170 
moreover from list_emb_Cons2 have "x = y" by simp 
50516  1171 
ultimately show ?case by blast 
49087  1172 
qed 
1173 
next 

1174 
assume ?R 

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

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

1176 
moreover have "subseq (nths ys N) ys" 
49107  1177 
proof (induct ys arbitrary: N) 
49087  1178 
case Nil show ?case by simp 
1179 
next 

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

1180 
case Cons then show ?case by (auto simp: nths_Cons) 
49087  1181 
qed 
1182 
ultimately show ?L by simp 

1183 
qed 

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

1184 

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

1185 

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

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

1187 

71789  1188 
subsubsection \<open>\<open>sublist\<close>\<close> 
1189 

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

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

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

1192 

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

1193 
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

1194 
"strict_sublist xs ys \<longleftrightarrow> sublist xs ys \<and> xs \<noteq> ys" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1195 

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

1196 
interpretation sublist_order: order sublist strict_sublist 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1198 
fix xs ys zs :: "'a list" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1200 
then obtain xs1 xs2 ys1 ys2 where "ys = xs1 @ xs @ xs2" "zs = ys1 @ ys @ ys2" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1201 
by (auto simp: sublist_def) 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1202 
hence "zs = (ys1 @ xs1) @ xs @ (xs2 @ ys2)" by simp 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1203 
thus "sublist xs zs" unfolding sublist_def by blast 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1205 
fix xs ys :: "'a list" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

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

1208 
then obtain as bs cs ds 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1209 
where xs: "xs = as @ ys @ bs" and ys: "ys = cs @ xs @ ds" 