author  eberlm <eberlm@in.tum.de> 
Thu, 18 May 2017 12:02:21 +0200  
changeset 65869  a6ed757b8585 
parent 64886  cea327ecb8e3 
child 65954  431024edc9cf 
permissions  rwrr 
49087  1 
(* Title: HOL/Library/Sublist.thy 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

2 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen 
49087  3 
Author: Christian Sternagel, JAIST 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

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

5 

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

7 

49087  8 
theory Sublist 
9 
imports Main 

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

11 

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

13 

63117  14 
definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
15 
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

16 

63117  17 
definition strict_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
18 
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

19 

63117  20 
interpretation prefix_order: order prefix strict_prefix 
21 
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

22 

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

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

25 

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

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

28 

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

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

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

33 

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

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

36 

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

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

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

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

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

43 
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

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

45 

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

49 

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

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

54 
using assms unfolding strict_prefix_def by blast 

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

55 

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

56 

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

58 

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

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

62 

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

66 

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

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

70 
then obtain zs where zs: "ys @ [y] = xs @ zs" .. 
63117  71 
show "xs = ys @ [y] \<or> prefix xs ys" 
72 
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

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

76 
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

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

78 

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

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

81 

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

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

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

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

87 

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

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

90 

65869  91 
lemma same_prefix_nil [simp]: "prefix (xs @ ys) xs = (ys = [])" 
63117  92 
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

93 

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

96 

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

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

99 

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

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

102 

63117  103 
theorem prefix_append: 
104 
"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

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

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

107 
apply (simp del: append_assoc add: append_assoc [symmetric]) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

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

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

110 

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

113 
proof (unfold prefix_def) 

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

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

115 
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

116 
assume a2: "length xs < length ys" 
61076  117 
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

118 
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

119 
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

120 
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

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

122 

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

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

125 

63117  126 
lemma prefix_same_cases: 
127 
"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" 

128 
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

129 

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

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

133 

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

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

136 

63117  137 
lemma take_is_prefix: "prefix (take n xs) xs" 
138 
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

139 

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

142 

63117  143 
lemma map_prefixI: "prefix xs ys \<Longrightarrow> prefix (map f xs) (map f ys)" 
144 
by (auto simp: prefix_def) 

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

145 

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

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

148 

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

151 

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

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

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

156 
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

157 

63117  158 
lemma take_strict_prefix: "strict_prefix xs ys \<Longrightarrow> strict_prefix (take n xs) ys" 
63649  159 
proof (induct n arbitrary: xs ys) 
160 
case 0 

161 
then show ?case by (cases ys) simp_all 

162 
next 

163 
case (Suc n) 

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

165 
qed 

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

166 

63117  167 
lemma not_prefix_cases: 
168 
assumes pfx: "\<not> prefix ps ls" 

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

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

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

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

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

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

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

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

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

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

180 
proof (cases ls) 
63117  181 
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

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

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

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

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

186 
case True 
63117  187 
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

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

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

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

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

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

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

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

195 

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

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

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

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

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

202 
proof (induct ls arbitrary: ps) 
63649  203 
case Nil 
204 
then show ?case 

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

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

207 
case (Cons y ys) 
63117  208 
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

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

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

213 

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

214 

63155  215 
subsection \<open>Prefixes\<close> 
216 

217 
fun prefixes where 

218 
"prefixes [] = [[]]"  

219 
"prefixes (x#xs) = [] # map (op # x) (prefixes xs)" 

220 

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

63649  222 
proof (induct xs arbitrary: ys) 
223 
case Nil 

224 
then show ?case by (cases ys) auto 

225 
next 

226 
case (Cons a xs) 

227 
then show ?case by (cases ys) auto 

228 
qed 

63155  229 

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

65869  231 
by (induction xs) auto 
232 

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

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

235 

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

237 
by (induction xs) auto 

238 

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

240 
by (cases xs) auto 

63155  241 

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

63155  244 

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

247 

248 
lemma prefixes_append: 

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

250 
proof (induction xs) 

251 
case Nil 

252 
thus ?case by (cases ys) auto 

253 
qed simp_all 

254 

255 
lemma prefixes_eq_snoc: 

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

65869  258 
by (cases ys rule: rev_cases) auto 
259 

260 
lemma prefixes_tailrec [code]: 

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

262 
proof  

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

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

265 
proof (induction xs arbitrary: ys zs) 

266 
case (Cons x xs ys zs) 

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

268 
show ?case by (simp add: o_def) 

269 
qed simp_all 

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

271 
qed 

272 

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

274 
by auto 

275 

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

277 
by (subst distinct_card) auto 

278 

279 
lemma set_prefixes_append: 

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

281 
by (subst prefixes_append, cases ys) auto 

63155  282 

283 

63173  284 
subsection \<open>Longest Common Prefix\<close> 
285 

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

287 
"Longest_common_prefix L = (GREATEST ps WRT length. \<forall>xs \<in> L. prefix ps xs)" 

288 

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

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

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

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

293 
case 0 

294 
have "[] : L" using "0.hyps" LeastI[of "\<lambda>n. \<exists>xs\<in>L. n = length xs"] \<open>L \<noteq> {}\<close> 

295 
by auto 

296 
hence "?P L []" by(auto) 

297 
thus ?case .. 

298 
next 

299 
case (Suc n) 

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

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

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

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

304 
show ?case 

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

306 
case True 

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

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

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

310 
by  (rule Least_equality, fastforce+) 

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

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

313 
{ fix qs 

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

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

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

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

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

319 
} 

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

321 
thus ?thesis .. 

322 
next 

323 
case False 

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

325 
by (auto) (metis list.exhaust) 

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

327 
by auto (metis Cons_prefix_Cons prefix_Cons) 

328 
hence "?P L []" by auto 

329 
thus ?thesis .. 

330 
qed 

331 
qed 

332 

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

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

335 
by(rule ex_ex1I[OF Longest_common_prefix_ex]; 

336 
meson equals0I prefix_length_prefix prefix_order.antisym) 

337 

338 
lemma Longest_common_prefix_eq: 

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

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

341 
\<Longrightarrow> Longest_common_prefix L = ps" 

342 
unfolding Longest_common_prefix_def GreatestM_def 

343 
by(rule some1_equality[OF Longest_common_prefix_unique]) auto 

344 

345 
lemma Longest_common_prefix_prefix: 

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

347 
unfolding Longest_common_prefix_def GreatestM_def 

348 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 

349 

350 
lemma Longest_common_prefix_longest: 

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

352 
unfolding Longest_common_prefix_def GreatestM_def 

353 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 

354 

355 
lemma Longest_common_prefix_max_prefix: 

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

357 
by(metis Longest_common_prefix_prefix Longest_common_prefix_longest 

358 
prefix_length_prefix ex_in_conv) 

359 

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

361 
using Longest_common_prefix_prefix prefix_Nil by blast 

362 

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

364 
Longest_common_prefix (op # x ` L) = x # Longest_common_prefix L" 

365 
apply(rule Longest_common_prefix_eq) 

366 
apply(simp) 

367 
apply (simp add: Longest_common_prefix_prefix) 

368 
apply simp 

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

370 
Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc) 

371 

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

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

374 
proof  

375 
have "L = op # x ` {ys. x#ys \<in> L}" using assms(2,3) 

376 
by (auto simp: image_def)(metis hd_Cons_tl) 

377 
thus ?thesis 

378 
by (metis Longest_common_prefix_image_Cons image_is_empty assms(1)) 

379 
qed 

380 

381 
lemma Longest_common_prefix_eq_Nil: 

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

383 
by (metis Longest_common_prefix_prefix list.inject prefix_Cons) 

384 

385 

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

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

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

389 
"longest_common_prefix _ _ = []" 

390 

391 
lemma longest_common_prefix_prefix1: 

392 
"prefix (longest_common_prefix xs ys) xs" 

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

394 

395 
lemma longest_common_prefix_prefix2: 

396 
"prefix (longest_common_prefix xs ys) ys" 

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

398 

399 
lemma longest_common_prefix_max_prefix: 

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

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

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

403 
(auto simp: prefix_Cons) 

404 

405 

60500  406 
subsection \<open>Parallel lists\<close> 
10389  407 

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

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

413 

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

418 

63117  419 
theorem prefix_cases: 
420 
obtains "prefix xs ys"  "strict_prefix ys xs"  "xs \<parallel> ys" 

421 
unfolding parallel_def strict_prefix_def by blast 

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

422 

10389  423 
theorem parallel_decomp: 
50516  424 
"xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 
10408  425 
proof (induct xs rule: rev_induct) 
11987  426 
case Nil 
23254  427 
then have False by auto 
428 
then show ?case .. 

10408  429 
next 
11987  430 
case (snoc x xs) 
431 
show ?case 

63117  432 
proof (rule prefix_cases) 
433 
assume le: "prefix xs ys" 

10408  434 
then obtain ys' where ys: "ys = xs @ ys'" .. 
435 
show ?thesis 

436 
proof (cases ys') 

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

443 
using ys ys' by blast 

10389  444 
qed 
10408  445 
next 
63117  446 
assume "strict_prefix ys xs" 
447 
then have "prefix ys (xs @ [x])" by (simp add: strict_prefix_def) 

11987  448 
with snoc have False by blast 
23254  449 
then show ?thesis .. 
10408  450 
next 
451 
assume "xs \<parallel> ys" 

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

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

456 
with neq ys show ?thesis by blast 

10389  457 
qed 
458 
qed 

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

459 

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

63117  463 
induct rule: not_prefix_induct, simp+)+ 
25692  464 
done 
25299  465 

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

25299  468 

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

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

471 

25356  472 

60500  473 
subsection \<open>Suffix order on lists\<close> 
17201  474 

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

49087  477 

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

480 

65869  481 
interpretation suffix_order: order suffix strict_suffix 
482 
by standard (auto simp: suffix_def strict_suffix_def) 

483 

484 
interpretation suffix_bot: order_bot Nil suffix strict_suffix 

485 
by standard (simp add: suffix_def) 

49087  486 

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

21305  489 

63149  490 
lemma suffixE [elim?]: 
491 
assumes "suffix xs ys" 

49087  492 
obtains zs where "ys = zs @ xs" 
63149  493 
using assms unfolding suffix_def by blast 
21305  494 

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

497 

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

65869  501 
lemma Nil_suffix [simp]: "suffix [] xs" 
63149  502 
by (simp add: suffix_def) 
49087  503 

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

506 

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

508 
by (auto simp add: suffix_def) 

509 

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

511 
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

512 

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

515 

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

517 
by (auto simp add: suffix_def) 

49087  518 

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

521 

63149  522 
lemma suffix_set_subset: "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" 
65869  523 
by (auto simp: suffix_def) 
49087  524 

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

532 

63149  533 
lemma suffix_to_prefix [code]: "suffix xs ys \<longleftrightarrow> prefix (rev xs) (rev ys)" 
49087  534 
proof 
63149  535 
assume "suffix xs ys" 
49087  536 
then obtain zs where "ys = zs @ xs" .. 
537 
then have "rev ys = rev xs @ rev zs" by simp 

63117  538 
then show "prefix (rev xs) (rev ys)" .. 
49087  539 
next 
63117  540 
assume "prefix (rev xs) (rev ys)" 
49087  541 
then obtain zs where "rev ys = rev xs @ zs" .. 
542 
then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp 

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

63149  544 
then show "suffix xs ys" .. 
21305  545 
qed 
65869  546 

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

548 
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

549 

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

17201  552 

63149  553 
lemma suffix_map: "suffix xs ys \<Longrightarrow> suffix (map f xs) (map f ys)" 
554 
by (auto elim!: suffixE intro: suffixI) 

25299  555 

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

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

25299  561 

63149  562 
lemma strict_suffix_reflclp_conv: "strict_suffix\<^sup>=\<^sup>= = suffix" 
65869  563 
by (intro ext) (auto simp: suffix_def strict_suffix_def) 
63149  564 

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

566 
unfolding suffix_def by auto 

49087  567 

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

570 

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

572 
by (auto simp add: suffix_def) 

573 

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

575 
by (simp add: suffix_to_prefix) 

576 

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

578 
by (simp add: suffix_to_prefix) 

579 

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

581 
unfolding suffix_def by (auto simp: Cons_eq_append_conv) 

582 

583 
theorem suffix_append: 

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

585 
by (auto simp: suffix_def append_eq_append_conv2) 

586 

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

588 
by (auto simp add: suffix_def) 

589 

590 
lemma suffix_same_cases: 

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

592 
unfolding suffix_def by (force simp: append_eq_append_conv2) 

593 

594 
lemma suffix_length_suffix: 

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

596 
by (auto simp: suffix_to_prefix intro: prefix_length_prefix) 

597 

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

599 
by (auto simp: strict_suffix_def suffix_def) 

600 

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

602 
by (auto simp: strict_suffix_def suffix_def) 

603 

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

605 
proof (induct n arbitrary: xs ys) 

606 
case 0 

607 
then show ?case by (cases ys) simp_all 

608 
next 

609 
case (Suc n) 

610 
then show ?case 

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

612 
qed 

613 

614 
lemma not_suffix_cases: 

615 
assumes pfx: "\<not> suffix ps ls" 

616 
obtains 

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

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

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

620 
proof (cases ps rule: rev_cases) 

621 
case Nil 

622 
then show ?thesis using pfx by simp 

623 
next 

624 
case (snoc as a) 

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

626 
show ?thesis 

627 
proof (cases ls rule: rev_cases) 

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

629 
next 

630 
case (snoc xs x) 

631 
show ?thesis 

632 
proof (cases "x = a") 

633 
case True 

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

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

636 
next 

637 
case False 

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

639 
qed 

640 
qed 

641 
qed 

642 

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

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

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

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

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

648 
shows "P ps ls" using np 

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

650 
case Nil 

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

652 
next 

653 
case (snoc y ys ps) 

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

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

656 
by (rule not_suffix_cases) auto 

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

658 
qed 

659 

660 

63117  661 
lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefix x y" 
25692  662 
by blast 
25299  663 

63117  664 
lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefix y x" 
25692  665 
by blast 
25355  666 

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

25692  668 
unfolding parallel_def by simp 
25355  669 

25299  670 
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x" 
25692  671 
unfolding parallel_def by simp 
25299  672 

25564  673 
lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" 
25692  674 
by auto 
25299  675 

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

25299  679 
lemma not_equal_is_parallel: 
680 
assumes neq: "xs \<noteq> ys" 

25356  681 
and len: "length xs = length ys" 
682 
shows "xs \<parallel> ys" 

25299  683 
using len neq 
25355  684 
proof (induct rule: list_induct2) 
26445  685 
case Nil 
25356  686 
then show ?case by simp 
25299  687 
next 
26445  688 
case (Cons a as b bs) 
25355  689 
have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact 
25299  690 
show ?case 
691 
proof (cases "a = b") 

25355  692 
case True 
26445  693 
then have "as \<noteq> bs" using Cons by simp 
25355  694 
then show ?thesis by (rule Cons_parallelI2 [OF True ih]) 
25299  695 
next 
696 
case False 

25355  697 
then show ?thesis by (rule Cons_parallelI1) 
25299  698 
qed 
699 
qed 

22178  700 

65869  701 
subsection \<open>Suffixes\<close> 
702 

703 
fun suffixes where 

704 
"suffixes [] = [[]]" 

705 
 "suffixes (x#xs) = suffixes xs @ [x # xs]" 

706 

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

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

709 

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

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

712 

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

714 
by (induction xs) auto 

715 

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

717 
by (induction xs) auto 

718 

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

720 
by (cases xs) auto 

721 

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

723 
by (induction xs) simp_all 

724 

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

726 
by (cases xs) simp_all 

727 

728 
lemma suffixes_append: 

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

730 
proof (induction ys rule: rev_induct) 

731 
case Nil 

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

733 
next 

734 
case (snoc y ys) 

735 
show ?case 

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

737 
qed 

738 

739 
lemma suffixes_eq_snoc: 

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

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

742 
by (cases ys) auto 

743 

744 
lemma suffixes_tailrec [code]: 

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

746 
proof  

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

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

749 
proof (induction xs arbitrary: ys zs) 

750 
case (Cons x xs ys zs) 

751 
from Cons.IH[of ys zs] 

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

753 
qed simp_all 

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

755 
qed 

756 

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

758 
by auto 

759 

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

761 
by (subst distinct_card) auto 

762 

763 
lemma set_suffixes_append: 

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

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

766 

767 

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

769 
by (induction xs) auto 

770 

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

772 
by (induction xs) auto 

773 

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

775 
by (induction xs) auto 

776 

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

778 
by (induction xs) auto 

779 

49087  780 

60500  781 
subsection \<open>Homeomorphic embedding on lists\<close> 
49087  782 

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

783 
inductive list_emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
49087  784 
for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" 
785 
where 

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

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

787 
 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

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

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

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

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

792 
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

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

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

795 
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

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

797 

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

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

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

800 
using assms by (cases rule: list_emb.cases) auto 
49087  801 

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

802 
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

803 
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

804 
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

805 
using assms by (induct xs) auto 
49087  806 

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

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

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

810 
from list_emb_Nil2 [OF this] have False by simp 
49087  811 
} moreover { 
812 
assume False 

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

813 
then have "list_emb P (x#xs) []" by simp 
49087  814 
} ultimately show ?thesis by blast 
815 
qed 

816 

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

817 
lemma list_emb_append2 [intro]: "list_emb P xs ys \<Longrightarrow> list_emb P xs (zs @ ys)" 
49087  818 
by (induct zs) auto 
819 

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

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

821 
assumes "list_emb P xs ys" shows "list_emb P xs (ys @ zs)" 
49087  822 
using assms 
823 
by (induct arbitrary: zs) auto 

824 

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

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

826 
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

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

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

833 
case (list_emb_Cons2 x y xs ys) 
54483  834 
then show ?case by blast 
49087  835 
qed 
836 

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

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

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

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

49107  842 
case Nil then show ?case by auto 
49087  843 
next 
844 
case (Cons x xs) 

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

846 
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

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

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

851 
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  852 
thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc) 
49087  853 
qed 
854 

63149  855 
lemma list_emb_strict_suffix: 
856 
assumes "list_emb P xs ys" and "strict_suffix ys zs" 

857 
shows "list_emb P xs zs" 

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

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

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

861 
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

862 
shows "list_emb P xs zs" 
63149  863 
using assms and list_emb_strict_suffix 
864 
unfolding strict_suffix_reflclp_conv[symmetric] by auto 

49087  865 

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

866 
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

867 
by (induct rule: list_emb.induct) auto 
49087  868 

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

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

870 
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

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

873 
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

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

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

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

880 
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

881 
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

882 
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

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

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

887 
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

888 
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

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

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

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

897 
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

898 
then show ?case unfolding zs by (rule list_emb_append2) 
49087  899 
qed 
900 
qed 

901 

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

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

903 
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

904 
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

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

906 

65869  907 
lemma list_emb_Cons_iff1 [simp]: 
908 
assumes "P x y" 

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

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

911 

912 
lemma list_emb_Cons_iff2 [simp]: 

913 
assumes "\<not>P x y" 

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

915 
using assms by (subst list_emb.simps) auto 

916 

917 
lemma list_emb_code [code]: 

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

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

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

921 
by simp_all 

922 

923 

49087  924 

60500  925 
subsection \<open>Sublists (special case of homeomorphic embedding)\<close> 
49087  926 

50516  927 
abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

928 
where "sublisteq xs ys \<equiv> list_emb (op =) xs ys" 
65869  929 

930 
definition strict_sublist where "strict_sublist xs ys \<longleftrightarrow> xs \<noteq> ys \<and> sublisteq xs ys" 

49087  931 

50516  932 
lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto 
49087  933 

50516  934 
lemma sublisteq_same_length: 
935 
assumes "sublisteq 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

936 
using assms by (induct) (auto dest: list_emb_length) 
49087  937 

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

939 
by (metis list_emb_length linorder_not_less) 
49087  940 

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

942 
by (induct xs, simp, blast dest: list_emb_ConsD) 
49087  943 

50516  944 
lemma sublisteq_Cons2': 
945 
assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys" 

946 
using assms by (cases) (rule sublisteq_Cons') 

49087  947 

50516  948 
lemma sublisteq_Cons2_neq: 
949 
assumes "sublisteq (x#xs) (y#ys)" 

950 
shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys" 

49087  951 
using assms by (cases) auto 
952 

65869  953 
lemma sublisteq_Cons2_iff [simp]: 
50516  954 
"sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)" 
65869  955 
by simp 
49087  956 

50516  957 
lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys" 
49087  958 
by (induct zs) simp_all 
65869  959 

960 
interpretation sublist_order: order sublisteq strict_sublist 

961 
proof 

962 
fix xs ys :: "'a list" 

963 
{ 

964 
assume "sublisteq xs ys" and "sublisteq ys xs" 

965 
thus "xs = ys" 

966 
proof (induct) 

967 
case list_emb_Nil 

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

969 
next 

970 
case list_emb_Cons2 

971 
thus ?case by simp 

972 
next 

973 
case list_emb_Cons 

974 
hence False using sublisteq_Cons' by fastforce 

975 
thus ?case .. 

976 
qed 

977 
} 

978 
thus "strict_sublist xs ys \<longleftrightarrow> (sublisteq xs ys \<and> \<not>sublisteq ys xs)" 

979 
by (auto simp: strict_sublist_def) 

980 
qed (auto simp: list_emb_refl intro: list_emb_trans) 

49087  981 

65869  982 
lemma in_set_sublists [simp]: "xs \<in> set (sublists ys) \<longleftrightarrow> sublisteq xs ys" 
983 
proof 

984 
assume "xs \<in> set (sublists ys)" 

985 
thus "sublisteq xs ys" 

986 
by (induction ys arbitrary: xs) (auto simp: Let_def) 

49087  987 
next 
65869  988 
have [simp]: "[] \<in> set (sublists ys)" for ys :: "'a list" 
989 
by (induction ys) (auto simp: Let_def) 

990 
assume "sublisteq xs ys" 

991 
thus "xs \<in> set (sublists ys)" 

992 
by (induction xs ys rule: list_emb.induct) (auto simp: Let_def) 

49087  993 
qed 
994 

65869  995 
lemma set_sublists_eq: "set (sublists ys) = {xs. sublisteq xs ys}" 
996 
by auto 

49087  997 

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

999 
by (auto dest: list_emb_length) 
49087  1000 

64886  1001 
lemma sublisteq_singleton_left: "sublisteq [x] ys \<longleftrightarrow> x \<in> set ys" 
1002 
by (fastforce dest: list_emb_ConsD split_list_last) 

1003 

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

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

1005 
"\<lbrakk> list_emb P xs xs'; list_emb P ys ys' \<rbrakk> \<Longrightarrow> list_emb P (xs@ys) (xs'@ys')" 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1006 
apply (induct rule: list_emb.induct) 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1007 
apply (metis eq_Nil_appendI list_emb_append2) 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1008 
apply (metis append_Cons list_emb_Cons) 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1009 
apply (metis append_Cons list_emb_Cons2) 
49107  1010 
done 
49087  1011 

1012 

60500  1013 
subsection \<open>Appending elements\<close> 
49087  1014 

50516  1015 
lemma sublisteq_append [simp]: 
1016 
"sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r") 

49087  1017 
proof 
50516  1018 
{ fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'" 
1019 
then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys" 

49087  1020 
proof (induct arbitrary: xs ys zs) 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

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

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

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

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

1027 
then have ?case using list_emb_Cons(2) by(simp add: list_emb.list_emb_Cons) } 
49087  1028 
ultimately show ?case by (auto simp:Cons_eq_append_conv) 
1029 
next 

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

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

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

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

1035 
{ fix us assume "xs=x#us" "ys=[]" then have ?case using list_emb_Cons2(2) by bestsimp } 
60500  1036 
ultimately show ?case using \<open>op = x y\<close> by (auto simp: Cons_eq_append_conv) 
49087  1037 
qed } 
1038 
moreover assume ?l 

1039 
ultimately show ?r by blast 

1040 
next 

65869  1041 
assume ?r then show ?l by (metis list_emb_append_mono sublist_order.order_refl) 
49087  1042 
qed 
1043 

65869  1044 
lemma sublisteq_append_iff: 
1045 
"sublisteq xs (ys @ zs) \<longleftrightarrow> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> sublisteq xs1 ys \<and> sublisteq xs2 zs)" 

1046 
(is "?lhs = ?rhs") 

1047 
proof 

1048 
assume ?lhs thus ?rhs 

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

1050 
case (list_emb_Cons xs ws y ys zs) 

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

1052 
show ?case by (cases ys) auto 

1053 
next 

1054 
case (list_emb_Cons2 x y xs ws ys zs) 

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

1056 
and list_emb_Cons2(1,2,4) 

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

1058 
qed auto 

1059 
qed (auto intro: list_emb_append_mono) 

1060 

1061 
lemma sublisteq_appendE [case_names append]: 

1062 
assumes "sublisteq xs (ys @ zs)" 

1063 
obtains xs1 xs2 where "xs = xs1 @ xs2" "sublisteq xs1 ys" "sublisteq xs2 zs" 

1064 
using assms by (subst (asm) sublisteq_append_iff) auto 

1065 

50516  1066 
lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)" 
49087  1067 
by (induct zs) auto 
1068 

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

1070 
by (metis append_Nil2 list_emb_Nil list_emb_append_mono) 
49087  1071 

1072 

60500  1073 
subsection \<open>Relation to standard list operations\<close> 
49087  1074 

50516  1075 
lemma sublisteq_map: 
1076 
assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)" 

49087  1077 
using assms by (induct) auto 
1078 

50516  1079 
lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs" 
49087  1080 
by (induct xs) auto 
1081 

50516  1082 
lemma sublisteq_filter [simp]: 
1083 
assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)" 

54483  1084 
using assms by induct auto 
49087  1085 

50516  1086 
lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R") 
49087  1087 
proof 
1088 
assume ?L 

49107  1089 
then show ?R 
49087  1090 
proof (induct) 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

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

1093 
case (list_emb_Cons xs ys x) 
49087  1094 
then obtain N where "xs = sublist ys N" by blast 
49107  1095 
then have "xs = sublist (x#ys) (Suc ` N)" 
49087  1096 
by (clarsimp simp add:sublist_Cons inj_image_mem_iff) 
49107  1097 
then show ?case by blast 
49087  1098 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1099 
case (list_emb_Cons2 x y xs ys) 
49087  1100 
then obtain N where "xs = sublist ys N" by blast 
49107  1101 
then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))" 
49087  1102 
by (clarsimp simp add:sublist_Cons inj_image_mem_iff) 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

1103 
moreover from list_emb_Cons2 have "x = y" by simp 
50516  1104 
ultimately show ?case by blast 
49087  1105 
qed 
1106 
next 

1107 
assume ?R 

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

50516  1109 
moreover have "sublisteq (sublist ys N) ys" 
49107  1110 
proof (induct ys arbitrary: N) 
49087  1111 
case Nil show ?case by simp 
1112 
next 

49107  1113 
case Cons then show ?case by (auto simp: sublist_Cons) 
49087  1114 
qed 
1115 
ultimately show ?L by simp 

1116 
qed 

1117 

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

1118 
end 