author  eberlm <eberlm@in.tum.de> 
Mon, 29 May 2017 09:14:15 +0200  
changeset 65956  639eb3617a86 
parent 65954  431024edc9cf 
child 65957  558ba6b37f5c 
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 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

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

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

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

111 

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

114 
proof (unfold prefix_def) 

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

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

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

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

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

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

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

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

123 

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

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

126 

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

129 
unfolding prefix_def by (force simp: append_eq_append_conv2) 

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

130 

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

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

134 

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

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

137 

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

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

140 

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

143 

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

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

146 

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

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

149 

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

152 

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

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

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

157 
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

158 

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

162 
then show ?case by (cases ys) simp_all 

163 
next 

164 
case (Suc n) 

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

166 
qed 

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

167 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

192 
with c Cons show ?thesis by (rule c3) 
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 
qed 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

196 

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

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

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

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

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

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

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

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

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

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

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

214 

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

215 

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

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

218 
primrec prefixes where 
63155  219 
"prefixes [] = [[]]"  
220 
"prefixes (x#xs) = [] # map (op # x) (prefixes xs)" 

221 

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

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

225 
then show ?case by (cases ys) auto 

226 
next 

227 
case (Cons a xs) 

228 
then show ?case by (cases ys) auto 

229 
qed 

63155  230 

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

65869  232 
by (induction xs) auto 
233 

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

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

236 

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

238 
by (induction xs) auto 

239 

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

241 
by (cases xs) auto 

63155  242 

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

63155  245 

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

248 

249 
lemma prefixes_append: 

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

251 
proof (induction xs) 

252 
case Nil 

253 
thus ?case by (cases ys) auto 

254 
qed simp_all 

255 

256 
lemma prefixes_eq_snoc: 

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

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

261 
lemma prefixes_tailrec [code]: 

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

263 
proof  

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

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

266 
proof (induction xs arbitrary: ys zs) 

267 
case (Cons x xs ys zs) 

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

269 
show ?case by (simp add: o_def) 

270 
qed simp_all 

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

272 
qed 

273 

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

275 
by auto 

276 

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

278 
by (subst distinct_card) auto 

279 

280 
lemma set_prefixes_append: 

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

282 
by (subst prefixes_append, cases ys) auto 

63155  283 

284 

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

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

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

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

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

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

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

294 
case 0 

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

296 
by auto 

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

298 
thus ?case .. 

299 
next 

300 
case (Suc n) 

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

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

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

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

305 
show ?case 

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

307 
case True 

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

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

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

311 
by  (rule Least_equality, fastforce+) 

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

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

314 
{ fix qs 

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

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

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

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

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

320 
} 

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

322 
thus ?thesis .. 

323 
next 

324 
case False 

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

326 
by (auto) (metis list.exhaust) 

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

328 
by auto (metis Cons_prefix_Cons prefix_Cons) 

329 
hence "?P L []" by auto 

330 
thus ?thesis .. 

331 
qed 

332 
qed 

333 

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

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

336 
by(rule ex_ex1I[OF Longest_common_prefix_ex]; 

337 
meson equals0I prefix_length_prefix prefix_order.antisym) 

338 

339 
lemma Longest_common_prefix_eq: 

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

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

342 
\<Longrightarrow> Longest_common_prefix L = ps" 

65954  343 
unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder 
63173  344 
by(rule some1_equality[OF Longest_common_prefix_unique]) auto 
345 

346 
lemma Longest_common_prefix_prefix: 

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

65954  348 
unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder 
63173  349 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 
350 

351 
lemma Longest_common_prefix_longest: 

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

65954  353 
unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder 
63173  354 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 
355 

356 
lemma Longest_common_prefix_max_prefix: 

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

358 
by(metis Longest_common_prefix_prefix Longest_common_prefix_longest 

359 
prefix_length_prefix ex_in_conv) 

360 

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

362 
using Longest_common_prefix_prefix prefix_Nil by blast 

363 

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

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

366 
apply(rule Longest_common_prefix_eq) 

367 
apply(simp) 

368 
apply (simp add: Longest_common_prefix_prefix) 

369 
apply simp 

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

371 
Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc) 

372 

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

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

375 
proof  

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

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

378 
thus ?thesis 

379 
by (metis Longest_common_prefix_image_Cons image_is_empty assms(1)) 

380 
qed 

381 

382 
lemma Longest_common_prefix_eq_Nil: 

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

384 
by (metis Longest_common_prefix_prefix list.inject prefix_Cons) 

385 

386 

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

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

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

390 
"longest_common_prefix _ _ = []" 

391 

392 
lemma longest_common_prefix_prefix1: 

393 
"prefix (longest_common_prefix xs ys) xs" 

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

395 

396 
lemma longest_common_prefix_prefix2: 

397 
"prefix (longest_common_prefix xs ys) ys" 

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

399 

400 
lemma longest_common_prefix_max_prefix: 

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

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

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

404 
(auto simp: prefix_Cons) 

405 

406 

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

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

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

414 

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

419 

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

422 
unfolding parallel_def strict_prefix_def by blast 

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

423 

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

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

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

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

437 
proof (cases ys') 

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

444 
using ys ys' by blast 

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

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

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

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

457 
with neq ys show ?thesis by blast 

10389  458 
qed 
459 
qed 

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

460 

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

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

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

25299  469 

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

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

472 

25356  473 

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

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

49087  478 

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

481 

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

484 

485 
interpretation suffix_bot: order_bot Nil suffix strict_suffix 

486 
by standard (simp add: suffix_def) 

49087  487 

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

21305  490 

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

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

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

498 

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

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

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

507 

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

509 
by (auto simp add: suffix_def) 

510 

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

512 
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

513 

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

516 

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

518 
by (auto simp add: suffix_def) 

49087  519 

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

522 

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

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

533 

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

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

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

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

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

549 
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

550 

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

17201  553 

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

25299  556 

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

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

25299  562 

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

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

567 
unfolding suffix_def by auto 

49087  568 

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

571 

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

573 
by (auto simp add: suffix_def) 

574 

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

576 
by (simp add: suffix_to_prefix) 

577 

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

579 
by (simp add: suffix_to_prefix) 

580 

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

582 
unfolding suffix_def by (auto simp: Cons_eq_append_conv) 

583 

584 
theorem suffix_append: 

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

586 
by (auto simp: suffix_def append_eq_append_conv2) 

587 

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

589 
by (auto simp add: suffix_def) 

590 

591 
lemma suffix_same_cases: 

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

593 
unfolding suffix_def by (force simp: append_eq_append_conv2) 

594 

595 
lemma suffix_length_suffix: 

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

597 
by (auto simp: suffix_to_prefix intro: prefix_length_prefix) 

598 

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

600 
by (auto simp: strict_suffix_def suffix_def) 

601 

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

603 
by (auto simp: strict_suffix_def suffix_def) 

604 

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

606 
proof (induct n arbitrary: xs ys) 

607 
case 0 

608 
then show ?case by (cases ys) simp_all 

609 
next 

610 
case (Suc n) 

611 
then show ?case 

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

613 
qed 

614 

615 
lemma not_suffix_cases: 

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

617 
obtains 

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

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

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

621 
proof (cases ps rule: rev_cases) 

622 
case Nil 

623 
then show ?thesis using pfx by simp 

624 
next 

625 
case (snoc as a) 

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

627 
show ?thesis 

628 
proof (cases ls rule: rev_cases) 

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

630 
next 

631 
case (snoc xs x) 

632 
show ?thesis 

633 
proof (cases "x = a") 

634 
case True 

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

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

637 
next 

638 
case False 

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

640 
qed 

641 
qed 

642 
qed 

643 

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

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

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

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

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

649 
shows "P ps ls" using np 

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

651 
case Nil 

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

653 
next 

654 
case (snoc y ys ps) 

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

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

657 
by (rule not_suffix_cases) auto 

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

659 
qed 

660 

661 

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

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

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

25692  669 
unfolding parallel_def by simp 
25355  670 

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

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

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

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

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

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

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

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

22178  701 

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

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

704 
primrec suffixes where 
65869  705 
"suffixes [] = [[]]" 
706 
 "suffixes (x#xs) = suffixes xs @ [x # xs]" 

707 

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

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

710 

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

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

713 

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

715 
by (induction xs) auto 

716 

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

718 
by (induction xs) auto 

719 

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

721 
by (cases xs) auto 

722 

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

724 
by (induction xs) simp_all 

725 

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

727 
by (cases xs) simp_all 

728 

729 
lemma suffixes_append: 

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

731 
proof (induction ys rule: rev_induct) 

732 
case Nil 

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

734 
next 

735 
case (snoc y ys) 

736 
show ?case 

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

738 
qed 

739 

740 
lemma suffixes_eq_snoc: 

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

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

743 
by (cases ys) auto 

744 

745 
lemma suffixes_tailrec [code]: 

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

747 
proof  

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

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

750 
proof (induction xs arbitrary: ys zs) 

751 
case (Cons x xs ys zs) 

752 
from Cons.IH[of ys zs] 

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

754 
qed simp_all 

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

756 
qed 

757 

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

759 
by auto 

760 

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

762 
by (subst distinct_card) auto 

763 

764 
lemma set_suffixes_append: 

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

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

767 

768 

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

770 
by (induction xs) auto 

771 

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

773 
by (induction xs) auto 

774 

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

776 
by (induction xs) auto 

777 

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

779 
by (induction xs) auto 

780 

49087  781 

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

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

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

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

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

788 
 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

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

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

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

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

793 
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

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

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

796 
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

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

798 

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

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

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

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

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

803 
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

804 
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

805 
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

806 
using assms by (induct xs) auto 
49087  807 

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

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

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

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

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

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

817 

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

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

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

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

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

825 

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

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

827 
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

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

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

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

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

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

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

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

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

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

847 
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

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

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

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

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

858 
shows "list_emb P xs zs" 

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

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

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

862 
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

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

49087  866 

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

867 
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

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

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

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

871 
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

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

874 
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

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

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

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

881 
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

882 
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

883 
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

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

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

888 
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

889 
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

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

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

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

898 
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

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

902 

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

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

904 
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

905 
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

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

907 

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

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

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

912 

913 
lemma list_emb_Cons_iff2 [simp]: 

914 
assumes "\<not>P x y" 

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

916 
using assms by (subst list_emb.simps) auto 

917 

918 
lemma list_emb_code [code]: 

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

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

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

922 
by simp_all 

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

923 

65869  924 

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

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

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

927 
abbreviation subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

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

930 
definition strict_subseq where "strict_subseq xs ys \<longleftrightarrow> xs \<noteq> ys \<and> subseq xs ys" 
49087  931 

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

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

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

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

935 
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

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

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

938 
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

939 
by (metis list_emb_length linorder_not_less) 
49087  940 

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

941 
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

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

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

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

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

946 
using assms by (cases) (rule subseq_Cons') 
49087  947 

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

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

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

950 
shows "x \<noteq> y \<Longrightarrow> subseq (x#xs) ys" 
49087  951 
using assms by (cases) auto 
952 

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

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

954 
"subseq (x#xs) (y#ys) = (if x = y then subseq xs ys else subseq (x#xs) ys)" 
65869  955 
by simp 
49087  956 

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

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

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

960 
interpretation subseq_order: order subseq strict_subseq 
65869  961 
proof 
962 
fix xs ys :: "'a list" 

963 
{ 

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

964 
assume "subseq xs ys" and "subseq ys xs" 
65869  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 

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

974 
hence False using subseq_Cons' by fastforce 
65869  975 
thus ?case .. 
976 
qed 

977 
} 

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

978 
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

979 
by (auto simp: strict_subseq_def) 
65869  980 
qed (auto simp: list_emb_refl intro: list_emb_trans) 
49087  981 

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

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

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

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

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

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

991 
thus "xs \<in> set (subseqs ys)" 
65869  992 
by (induction xs ys rule: list_emb.induct) (auto simp: Let_def) 
49087  993 
qed 
994 

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

995 
lemma set_subseqs_eq: "set (subseqs ys) = {xs. subseq xs ys}" 
65869  996 
by auto 
49087  997 

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

998 
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

999 
by (auto dest: list_emb_length) 
49087  1000 

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

1001 
lemma subseq_singleton_left: "subseq [x] ys \<longleftrightarrow> x \<in> set ys" 
64886  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 

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

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

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

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

1019 
then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> subseq 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 

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

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

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

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

1045 
"subseq xs (ys @ zs) \<longleftrightarrow> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> subseq xs1 ys \<and> subseq xs2 zs)" 
65869  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 

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

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

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

1063 
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

1064 
using assms by (subst (asm) subseq_append_iff) auto 
65869  1065 

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

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

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

1069 
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

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 

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

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

1076 
assumes "subseq xs ys" shows "subseq (map f xs) (map f ys)" 
49087  1077 
using assms by (induct) auto 
1078 

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

1079 
lemma subseq_filter_left [simp]: "subseq (filter P xs) xs" 
49087  1080 
by (induct xs) auto 
1081 

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

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

1083 
assumes "subseq xs ys" shows "subseq (filter P xs) (filter P ys)" 
54483  1084 
using assms by induct auto 
49087  1085 

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

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

1087 
"subseq xs ys \<longleftrightarrow> (\<exists>N. xs = nths ys N)" (is "?L = ?R") 
49087  1088 
proof 
1089 
assume ?L 

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

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

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

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

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

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

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

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

1102 
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

1103 
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

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

1108 
assume ?R 

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

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

1110 
moreover have "subseq (nths ys N) ys" 
49107  1111 
proof (induct ys arbitrary: N) 
49087  1112 
case Nil show ?case by simp 
1113 
next 

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

1114 
case Cons then show ?case by (auto simp: nths_Cons) 
49087  1115 
qed 
1116 
ultimately show ?L by simp 

1117 
qed 

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

1118 

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

1119 

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

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

1121 

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

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

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

1124 

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

1125 
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

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

1127 

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

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

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

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

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

1132 
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

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

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

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

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

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

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

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

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

1141 
where xs: "xs = as @ ys @ bs" and ys: "ys = cs @ xs @ ds" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1143 
have "xs = as @ cs @ xs @ ds @ bs" by (subst xs, subst ys) auto 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1144 
also have "length \<dots> = length as + length cs + length xs + length bs + length ds" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1146 
finally have "as = []" "bs = []" by simp_all 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1147 
with xs show "xs = ys" by simp 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

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

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

1151 
qed (auto simp: strict_sublist_def sublist_def intro: exI[of _ "[]"]) 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1152 

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

1153 
lemma sublist_Nil_left [simp, intro]: "sublist [] ys" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1155 

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

1156 
lemma sublist_Cons_Nil [simp]: "\<not>sublist (x#xs) []" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1158 

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

1159 
lemma sublist_Nil_right [simp]: "sublist xs [] \<longleftrightarrow> xs = []" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1160 
by (cases xs) auto 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1161 

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

1162 
lemma sublist_appendI [simp, intro]: "sublist xs (ps @ xs @ ss)" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1164 

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

1165 
lemma sublist_append_leftI [simp, intro]: "sublist xs (ps @ xs)" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1166 
by (auto simp: sublist_def intro: exI[of _ "[]"]) 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1167 

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

1168 
lemma sublist_append_rightI [simp, intro]: "sublist xs (xs @ ss)" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1169 
by (auto simp: sublist_def intro: exI[of _ "[]"]) 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1170 

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

1171 
lemma sublist_altdef: "sublist xs ys \<longleftrightarrow> (\<exists>ys'. prefix ys' ys \<and> suffix xs ys')" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

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

1174 
then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def) 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1175 
thus "\<exists>ys'. prefix ys' ys \<and> suffix xs ys'" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1176 
by (intro exI[of _ "ps @ xs"] conjI suffix_appendI) auto 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

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

1179 
assume "prefix ys' ys" "suffix xs ys'" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1180 
thus "sublist xs ys" by (auto simp: prefix_def suffix_def) 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1182 

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

1183 
lemma sublist_altdef': "sublist xs ys \<longleftrightarrow> (\<exists>ys'. suffix ys' ys \<and> prefix xs ys')" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

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

1186 
then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def) 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1187 
thus "\<exists>ys'. suffix ys' ys \<and> prefix xs ys'" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1188 
by (intro exI[of _ "xs @ ss"] conjI suffixI) auto 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

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

1191 
assume "suffix ys' ys" "prefix xs ys'" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

1192 
thus "sublist xs ys" by (auto simp: prefix_def suffix_def) 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1194 

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

1195 
lemma sublist_Cons_right: "sublist xs (y # ys) \<longleftrightarrow> prefix xs (y # ys) \<or> sublist xs ys" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset

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

1197 

639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de> 