author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64886  cea327ecb8e3 
child 65869  a6ed757b8585 
permissions  rwrr 
49087  1 
(* Title: HOL/Library/Sublist.thy 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

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

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

5 

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

7 

49087  8 
theory Sublist 
9 
imports Main 

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

11 

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

13 

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

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

16 

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

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

19 

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

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

22 

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

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

25 

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

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

28 

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

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

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

33 

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

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

36 

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

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

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

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

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

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

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

45 

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

49 

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

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

54 
using assms unfolding strict_prefix_def by blast 

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

55 

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

56 

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

58 

63155  59 
(* FIXME rm *) 
63117  60 
theorem Nil_prefix [iff]: "prefix [] xs" 
63155  61 
by(fact prefix_bot.bot_least) 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

62 

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

66 

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

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

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

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

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

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

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

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

78 

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

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

81 

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

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

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

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

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

87 

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

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

90 

63117  91 
lemma same_prefix_nil [iff]: "prefix (xs @ ys) xs = (ys = [])" 
92 
by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixI) 

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

93 

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

96 

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

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

99 

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

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

102 

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

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

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

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

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

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

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

110 

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

113 
proof (unfold prefix_def) 

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

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

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

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

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

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

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

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

122 

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

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

125 

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

128 
unfolding prefix_def by (force simp: append_eq_append_conv2) 

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

129 

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

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

133 

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

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

136 

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

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

139 

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

142 

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

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

145 

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

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

148 

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

151 

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

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

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

156 
by (simp_all add: strict_prefix_def cong: conj_cong) 

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

157 

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

161 
then show ?case by (cases ys) simp_all 

162 
next 

163 
case (Suc n) 

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

165 
qed 

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

166 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

195 

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

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

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

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

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

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

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

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

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

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

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

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

213 

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

214 

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

217 
fun prefixes where 

218 
"prefixes [] = [[]]"  

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

220 

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

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

224 
then show ?case by (cases ys) auto 

225 
next 

226 
case (Cons a xs) 

227 
then show ?case by (cases ys) auto 

228 
qed 

63155  229 

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

231 
by (induction xs) auto 

232 

233 
lemma prefixes_snoc[simp]: 

234 
"prefixes (xs@[x]) = prefixes xs @ [xs@[x]]" 

235 
by (induction xs) auto 

236 

237 
lemma prefixes_eq_Snoc: 

238 
"prefixes ys = xs @ [x] \<longleftrightarrow> 

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

240 
by (cases ys rule: rev_cases) auto 

241 

242 

63173  243 
subsection \<open>Longest Common Prefix\<close> 
244 

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

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

247 

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

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

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

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

252 
case 0 

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

254 
by auto 

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

256 
thus ?case .. 

257 
next 

258 
case (Suc n) 

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

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

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

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

263 
show ?case 

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

265 
case True 

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

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

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

269 
by  (rule Least_equality, fastforce+) 

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

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

272 
{ fix qs 

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

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

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

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

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

278 
} 

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

280 
thus ?thesis .. 

281 
next 

282 
case False 

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

284 
by (auto) (metis list.exhaust) 

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

286 
by auto (metis Cons_prefix_Cons prefix_Cons) 

287 
hence "?P L []" by auto 

288 
thus ?thesis .. 

289 
qed 

290 
qed 

291 

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

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

294 
by(rule ex_ex1I[OF Longest_common_prefix_ex]; 

295 
meson equals0I prefix_length_prefix prefix_order.antisym) 

296 

297 
lemma Longest_common_prefix_eq: 

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

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

300 
\<Longrightarrow> Longest_common_prefix L = ps" 

301 
unfolding Longest_common_prefix_def GreatestM_def 

302 
by(rule some1_equality[OF Longest_common_prefix_unique]) auto 

303 

304 
lemma Longest_common_prefix_prefix: 

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

306 
unfolding Longest_common_prefix_def GreatestM_def 

307 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 

308 

309 
lemma Longest_common_prefix_longest: 

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

311 
unfolding Longest_common_prefix_def GreatestM_def 

312 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 

313 

314 
lemma Longest_common_prefix_max_prefix: 

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

316 
by(metis Longest_common_prefix_prefix Longest_common_prefix_longest 

317 
prefix_length_prefix ex_in_conv) 

318 

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

320 
using Longest_common_prefix_prefix prefix_Nil by blast 

321 

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

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

324 
apply(rule Longest_common_prefix_eq) 

325 
apply(simp) 

326 
apply (simp add: Longest_common_prefix_prefix) 

327 
apply simp 

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

329 
Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc) 

330 

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

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

333 
proof  

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

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

336 
thus ?thesis 

337 
by (metis Longest_common_prefix_image_Cons image_is_empty assms(1)) 

338 
qed 

339 

340 
lemma Longest_common_prefix_eq_Nil: 

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

342 
by (metis Longest_common_prefix_prefix list.inject prefix_Cons) 

343 

344 

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

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

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

348 
"longest_common_prefix _ _ = []" 

349 

350 
lemma longest_common_prefix_prefix1: 

351 
"prefix (longest_common_prefix xs ys) xs" 

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

353 

354 
lemma longest_common_prefix_prefix2: 

355 
"prefix (longest_common_prefix xs ys) ys" 

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

357 

358 
lemma longest_common_prefix_max_prefix: 

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

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

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

362 
(auto simp: prefix_Cons) 

363 

364 

60500  365 
subsection \<open>Parallel lists\<close> 
10389  366 

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

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

372 

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

377 

63117  378 
theorem prefix_cases: 
379 
obtains "prefix xs ys"  "strict_prefix ys xs"  "xs \<parallel> ys" 

380 
unfolding parallel_def strict_prefix_def by blast 

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

381 

10389  382 
theorem parallel_decomp: 
50516  383 
"xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 
10408  384 
proof (induct xs rule: rev_induct) 
11987  385 
case Nil 
23254  386 
then have False by auto 
387 
then show ?case .. 

10408  388 
next 
11987  389 
case (snoc x xs) 
390 
show ?case 

63117  391 
proof (rule prefix_cases) 
392 
assume le: "prefix xs ys" 

10408  393 
then obtain ys' where ys: "ys = xs @ ys'" .. 
394 
show ?thesis 

395 
proof (cases ys') 

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

402 
using ys ys' by blast 

10389  403 
qed 
10408  404 
next 
63117  405 
assume "strict_prefix ys xs" 
406 
then have "prefix ys (xs @ [x])" by (simp add: strict_prefix_def) 

11987  407 
with snoc have False by blast 
23254  408 
then show ?thesis .. 
10408  409 
next 
410 
assume "xs \<parallel> ys" 

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

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

415 
with neq ys show ?thesis by blast 

10389  416 
qed 
417 
qed 

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

418 

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

63117  422 
induct rule: not_prefix_induct, simp+)+ 
25692  423 
done 
25299  424 

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

25299  427 

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

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

430 

25356  431 

60500  432 
subsection \<open>Suffix order on lists\<close> 
17201  433 

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

49087  436 

63149  437 
definition strict_suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
438 
where "strict_suffix xs ys \<longleftrightarrow> (\<exists>us. ys = us @ xs \<and> us \<noteq> [])" 

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

439 

63149  440 
lemma strict_suffix_imp_suffix: 
441 
"strict_suffix xs ys \<Longrightarrow> suffix xs ys" 

442 
by (auto simp: suffix_def strict_suffix_def) 

49087  443 

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

21305  446 

63149  447 
lemma suffixE [elim?]: 
448 
assumes "suffix xs ys" 

49087  449 
obtains zs where "ys = zs @ xs" 
63149  450 
using assms unfolding suffix_def by blast 
21305  451 

63149  452 
lemma suffix_refl [iff]: "suffix xs xs" 
453 
by (auto simp add: suffix_def) 

454 

49087  455 
lemma suffix_trans: 
456 
"suffix xs ys \<Longrightarrow> suffix ys zs \<Longrightarrow> suffix xs zs" 

457 
by (auto simp: suffix_def) 

63149  458 

459 
lemma strict_suffix_trans: 

460 
"\<lbrakk>strict_suffix xs ys; strict_suffix ys zs\<rbrakk> \<Longrightarrow> strict_suffix xs zs" 

461 
by (auto simp add: strict_suffix_def) 

49087  462 

63149  463 
lemma suffix_antisym: "\<lbrakk>suffix xs ys; suffix ys xs\<rbrakk> \<Longrightarrow> xs = ys" 
464 
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

465 

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

468 

63149  469 
lemma strict_suffix_tl [simp]: "xs \<noteq> [] \<Longrightarrow> strict_suffix (tl xs) xs" 
470 
by (induct xs) (auto simp: strict_suffix_def) 

471 

472 
lemma Nil_suffix [iff]: "suffix [] xs" 

473 
by (simp add: suffix_def) 

49087  474 

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

477 

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

479 
by (auto simp add: suffix_def) 

480 

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

482 
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

483 

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

486 

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

488 
by (auto simp add: suffix_def) 

49087  489 

63149  490 
lemma strict_suffix_set_subset: "strict_suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" 
491 
by (auto simp: strict_suffix_def) 

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

492 

63149  493 
lemma suffix_set_subset: "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" 
494 
by (auto simp: suffix_def) 

49087  495 

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

503 

63149  504 
lemma suffix_to_prefix [code]: "suffix xs ys \<longleftrightarrow> prefix (rev xs) (rev ys)" 
49087  505 
proof 
63149  506 
assume "suffix xs ys" 
49087  507 
then obtain zs where "ys = zs @ xs" .. 
508 
then have "rev ys = rev xs @ rev zs" by simp 

63117  509 
then show "prefix (rev xs) (rev ys)" .. 
49087  510 
next 
63117  511 
assume "prefix (rev xs) (rev ys)" 
49087  512 
then obtain zs where "rev ys = rev xs @ zs" .. 
513 
then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp 

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

63149  515 
then show "suffix xs ys" .. 
21305  516 
qed 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

517 

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

17201  520 

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

25299  523 

63149  524 
lemma suffix_drop: "suffix (drop n as) as" 
525 
unfolding suffix_def 

25692  526 
apply (rule exI [where x = "take n as"]) 
527 
apply simp 

528 
done 

25299  529 

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

25299  532 

63149  533 
lemma strict_suffix_reflclp_conv: "strict_suffix\<^sup>=\<^sup>= = suffix" 
534 
by (intro ext) (auto simp: suffix_def strict_suffix_def) 

535 

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

537 
unfolding suffix_def by auto 

49087  538 

63117  539 
lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefix x y" 
25692  540 
by blast 
25299  541 

63117  542 
lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefix y x" 
25692  543 
by blast 
25355  544 

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

25692  546 
unfolding parallel_def by simp 
25355  547 

25299  548 
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x" 
25692  549 
unfolding parallel_def by simp 
25299  550 

25564  551 
lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" 
25692  552 
by auto 
25299  553 

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

25299  557 
lemma not_equal_is_parallel: 
558 
assumes neq: "xs \<noteq> ys" 

25356  559 
and len: "length xs = length ys" 
560 
shows "xs \<parallel> ys" 

25299  561 
using len neq 
25355  562 
proof (induct rule: list_induct2) 
26445  563 
case Nil 
25356  564 
then show ?case by simp 
25299  565 
next 
26445  566 
case (Cons a as b bs) 
25355  567 
have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact 
25299  568 
show ?case 
569 
proof (cases "a = b") 

25355  570 
case True 
26445  571 
then have "as \<noteq> bs" using Cons by simp 
25355  572 
then show ?thesis by (rule Cons_parallelI2 [OF True ih]) 
25299  573 
next 
574 
case False 

25355  575 
then show ?thesis by (rule Cons_parallelI1) 
25299  576 
qed 
577 
qed 

22178  578 

49087  579 

60500  580 
subsection \<open>Homeomorphic embedding on lists\<close> 
49087  581 

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

582 
inductive list_emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
49087  583 
for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" 
584 
where 

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

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

586 
 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

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

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

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

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

591 
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

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

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

594 
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

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

596 

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

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

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

599 
using assms by (cases rule: list_emb.cases) auto 
49087  600 

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

601 
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

602 
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

603 
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

604 
using assms by (induct xs) auto 
49087  605 

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

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

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

609 
from list_emb_Nil2 [OF this] have False by simp 
49087  610 
} moreover { 
611 
assume False 

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

612 
then have "list_emb P (x#xs) []" by simp 
49087  613 
} ultimately show ?thesis by blast 
614 
qed 

615 

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

616 
lemma list_emb_append2 [intro]: "list_emb P xs ys \<Longrightarrow> list_emb P xs (zs @ ys)" 
49087  617 
by (induct zs) auto 
618 

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

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

620 
assumes "list_emb P xs ys" shows "list_emb P xs (ys @ zs)" 
49087  621 
using assms 
622 
by (induct arbitrary: zs) auto 

623 

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

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

625 
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

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

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

632 
case (list_emb_Cons2 x y xs ys) 
54483  633 
then show ?case by blast 
49087  634 
qed 
635 

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

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

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

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

49107  641 
case Nil then show ?case by auto 
49087  642 
next 
643 
case (Cons x xs) 

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

645 
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

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

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

650 
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  651 
thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc) 
49087  652 
qed 
653 

63149  654 
lemma list_emb_strict_suffix: 
655 
assumes "list_emb P xs ys" and "strict_suffix ys zs" 

656 
shows "list_emb P xs zs" 

657 
using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: strict_suffix_def) 

658 

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

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

660 
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

661 
shows "list_emb P xs zs" 
63149  662 
using assms and list_emb_strict_suffix 
663 
unfolding strict_suffix_reflclp_conv[symmetric] by auto 

49087  664 

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

665 
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

666 
by (induct rule: list_emb.induct) auto 
49087  667 

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

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

669 
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

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

672 
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

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

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

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

679 
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

680 
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

681 
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

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

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

686 
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

687 
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

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

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

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

696 
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

697 
then show ?case unfolding zs by (rule list_emb_append2) 
49087  698 
qed 
699 
qed 

700 

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

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

702 
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

703 
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

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

705 

49087  706 

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

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

710 
where "sublisteq xs ys \<equiv> list_emb (op =) xs ys" 
49087  711 

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

50516  714 
lemma sublisteq_same_length: 
715 
assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys" 

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

716 
using assms by (induct) (auto dest: list_emb_length) 
49087  717 

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

719 
by (metis list_emb_length linorder_not_less) 
49087  720 

721 
lemma [code]: 

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

722 
"list_emb P [] ys \<longleftrightarrow> True" 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

723 
"list_emb P (x#xs) [] \<longleftrightarrow> False" 
49087  724 
by (simp_all) 
725 

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

727 
by (induct xs, simp, blast dest: list_emb_ConsD) 
49087  728 

50516  729 
lemma sublisteq_Cons2': 
730 
assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys" 

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

49087  732 

50516  733 
lemma sublisteq_Cons2_neq: 
734 
assumes "sublisteq (x#xs) (y#ys)" 

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

49087  736 
using assms by (cases) auto 
737 

50516  738 
lemma sublisteq_Cons2_iff [simp, code]: 
739 
"sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)" 

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

740 
by (metis list_emb_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq) 
49087  741 

50516  742 
lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys" 
49087  743 
by (induct zs) simp_all 
744 

50516  745 
lemma sublisteq_refl [simp, intro!]: "sublisteq xs xs" by (induct xs) simp_all 
49087  746 

50516  747 
lemma sublisteq_antisym: 
748 
assumes "sublisteq xs ys" and "sublisteq ys xs" 

49087  749 
shows "xs = ys" 
750 
using assms 

751 
proof (induct) 

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

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

753 
from list_emb_Nil2 [OF this] show ?case by simp 
49087  754 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

755 
case list_emb_Cons2 
54483  756 
thus ?case by simp 
49087  757 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

758 
case list_emb_Cons 
54483  759 
hence False using sublisteq_Cons' by fastforce 
760 
thus ?case .. 

49087  761 
qed 
762 

50516  763 
lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs" 
57500
5a8b3e9d82a4
weaker assumption for "list_emb_trans"; added lemma
Christian Sternagel
parents:
57499
diff
changeset

764 
by (rule list_emb_trans [of _ _ _ "op ="]) auto 
49087  765 

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

767 
by (auto dest: list_emb_length) 
49087  768 

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

771 

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

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

773 
"\<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

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

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

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

777 
apply (metis append_Cons list_emb_Cons2) 
49107  778 
done 
49087  779 

780 

60500  781 
subsection \<open>Appending elements\<close> 
49087  782 

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

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

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

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

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

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

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

795 
then have ?case using list_emb_Cons(2) by(simp add: list_emb.list_emb_Cons) } 
49087  796 
ultimately show ?case by (auto simp:Cons_eq_append_conv) 
797 
next 

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

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

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

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

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

807 
ultimately show ?r by blast 

808 
next 

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

809 
assume ?r then show ?l by (metis list_emb_append_mono sublisteq_refl) 
49087  810 
qed 
811 

50516  812 
lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)" 
49087  813 
by (induct zs) auto 
814 

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

816 
by (metis append_Nil2 list_emb_Nil list_emb_append_mono) 
49087  817 

818 

60500  819 
subsection \<open>Relation to standard list operations\<close> 
49087  820 

50516  821 
lemma sublisteq_map: 
822 
assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)" 

49087  823 
using assms by (induct) auto 
824 

50516  825 
lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs" 
49087  826 
by (induct xs) auto 
827 

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

54483  830 
using assms by induct auto 
49087  831 

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

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

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

839 
case (list_emb_Cons xs ys x) 
49087  840 
then obtain N where "xs = sublist ys N" by blast 
49107  841 
then have "xs = sublist (x#ys) (Suc ` N)" 
49087  842 
by (clarsimp simp add:sublist_Cons inj_image_mem_iff) 
49107  843 
then show ?case by blast 
49087  844 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

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

849 
moreover from list_emb_Cons2 have "x = y" by simp 
50516  850 
ultimately show ?case by blast 
49087  851 
qed 
852 
next 

853 
assume ?R 

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

50516  855 
moreover have "sublisteq (sublist ys N) ys" 
49107  856 
proof (induct ys arbitrary: N) 
49087  857 
case Nil show ?case by simp 
858 
next 

49107  859 
case Cons then show ?case by (auto simp: sublist_Cons) 
49087  860 
qed 
861 
ultimately show ?L by simp 

862 
qed 

863 

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

864 
end 