author  nipkow 
Sun, 29 May 2016 14:10:48 +0200  
changeset 63173  3413b1cf30cd 
parent 63155  ea8540c71581 
child 63649  e690d6f2185b 
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)" 
95 
by (metis prefix_order.le_less_trans prefixI strict_prefixE strict_prefixI) 

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" 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

159 
apply (induct n arbitrary: xs ys) 
59997  160 
apply (case_tac ys; simp) 
63117  161 
apply (metis prefix_order.less_trans strict_prefixI take_is_prefix) 
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

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

163 

63117  164 
lemma not_prefix_cases: 
165 
assumes pfx: "\<not> prefix ps ls" 

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

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

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

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

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

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

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

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

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

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

177 
proof (cases ls) 
63117  178 
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

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

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

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

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

183 
case True 
63117  184 
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

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

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

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

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

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

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

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

192 

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

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

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

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

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

199 
proof (induct ls arbitrary: ps) 
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
54538
diff
changeset

200 
case Nil then show ?case 
63117  201 
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

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

203 
case (Cons y ys) 
63117  204 
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

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

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

209 

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

210 

63155  211 
subsection \<open>Prefixes\<close> 
212 

213 
fun prefixes where 

214 
"prefixes [] = [[]]"  

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

216 

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

218 
by (induction "xs" arbitrary: "ys"; rename_tac "ys", case_tac "ys"; auto) 

219 

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

221 
by (induction xs) auto 

222 

223 
lemma prefixes_snoc[simp]: 

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

225 
by (induction xs) auto 

226 

227 
lemma prefixes_eq_Snoc: 

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

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

230 
by (cases ys rule: rev_cases) auto 

231 

232 

63173  233 
subsection \<open>Longest Common Prefix\<close> 
234 

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

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

237 

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

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

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

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

242 
case 0 

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

244 
by auto 

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

246 
thus ?case .. 

247 
next 

248 
case (Suc n) 

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

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

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

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

253 
show ?case 

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

255 
case True 

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

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

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

259 
by  (rule Least_equality, fastforce+) 

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

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

262 
{ fix qs 

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

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

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

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

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

268 
} 

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

270 
thus ?thesis .. 

271 
next 

272 
case False 

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

274 
by (auto) (metis list.exhaust) 

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

276 
by auto (metis Cons_prefix_Cons prefix_Cons) 

277 
hence "?P L []" by auto 

278 
thus ?thesis .. 

279 
qed 

280 
qed 

281 

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

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

284 
by(rule ex_ex1I[OF Longest_common_prefix_ex]; 

285 
meson equals0I prefix_length_prefix prefix_order.antisym) 

286 

287 
lemma Longest_common_prefix_eq: 

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

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

290 
\<Longrightarrow> Longest_common_prefix L = ps" 

291 
unfolding Longest_common_prefix_def GreatestM_def 

292 
by(rule some1_equality[OF Longest_common_prefix_unique]) auto 

293 

294 
lemma Longest_common_prefix_prefix: 

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

296 
unfolding Longest_common_prefix_def GreatestM_def 

297 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 

298 

299 
lemma Longest_common_prefix_longest: 

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

301 
unfolding Longest_common_prefix_def GreatestM_def 

302 
by(rule someI2_ex[OF Longest_common_prefix_ex]) auto 

303 

304 
lemma Longest_common_prefix_max_prefix: 

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

306 
by(metis Longest_common_prefix_prefix Longest_common_prefix_longest 

307 
prefix_length_prefix ex_in_conv) 

308 

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

310 
using Longest_common_prefix_prefix prefix_Nil by blast 

311 

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

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

314 
apply(rule Longest_common_prefix_eq) 

315 
apply(simp) 

316 
apply (simp add: Longest_common_prefix_prefix) 

317 
apply simp 

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

319 
Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc) 

320 

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

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

323 
proof  

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

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

326 
thus ?thesis 

327 
by (metis Longest_common_prefix_image_Cons image_is_empty assms(1)) 

328 
qed 

329 

330 
lemma Longest_common_prefix_eq_Nil: 

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

332 
by (metis Longest_common_prefix_prefix list.inject prefix_Cons) 

333 

334 

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

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

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

338 
"longest_common_prefix _ _ = []" 

339 

340 
lemma longest_common_prefix_prefix1: 

341 
"prefix (longest_common_prefix xs ys) xs" 

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

343 

344 
lemma longest_common_prefix_prefix2: 

345 
"prefix (longest_common_prefix xs ys) ys" 

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

347 

348 
lemma longest_common_prefix_max_prefix: 

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

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

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

352 
(auto simp: prefix_Cons) 

353 

354 

60500  355 
subsection \<open>Parallel lists\<close> 
10389  356 

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

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

362 

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

367 

63117  368 
theorem prefix_cases: 
369 
obtains "prefix xs ys"  "strict_prefix ys xs"  "xs \<parallel> ys" 

370 
unfolding parallel_def strict_prefix_def by blast 

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

371 

10389  372 
theorem parallel_decomp: 
50516  373 
"xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 
10408  374 
proof (induct xs rule: rev_induct) 
11987  375 
case Nil 
23254  376 
then have False by auto 
377 
then show ?case .. 

10408  378 
next 
11987  379 
case (snoc x xs) 
380 
show ?case 

63117  381 
proof (rule prefix_cases) 
382 
assume le: "prefix xs ys" 

10408  383 
then obtain ys' where ys: "ys = xs @ ys'" .. 
384 
show ?thesis 

385 
proof (cases ys') 

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

392 
using ys ys' by blast 

10389  393 
qed 
10408  394 
next 
63117  395 
assume "strict_prefix ys xs" 
396 
then have "prefix ys (xs @ [x])" by (simp add: strict_prefix_def) 

11987  397 
with snoc have False by blast 
23254  398 
then show ?thesis .. 
10408  399 
next 
400 
assume "xs \<parallel> ys" 

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

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

405 
with neq ys show ?thesis by blast 

10389  406 
qed 
407 
qed 

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

408 

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

63117  412 
induct rule: not_prefix_induct, simp+)+ 
25692  413 
done 
25299  414 

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

25299  417 

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

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

420 

25356  421 

60500  422 
subsection \<open>Suffix order on lists\<close> 
17201  423 

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

49087  426 

63149  427 
definition strict_suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
428 
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

429 

63149  430 
lemma strict_suffix_imp_suffix: 
431 
"strict_suffix xs ys \<Longrightarrow> suffix xs ys" 

432 
by (auto simp: suffix_def strict_suffix_def) 

49087  433 

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

21305  436 

63149  437 
lemma suffixE [elim?]: 
438 
assumes "suffix xs ys" 

49087  439 
obtains zs where "ys = zs @ xs" 
63149  440 
using assms unfolding suffix_def by blast 
21305  441 

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

444 

49087  445 
lemma suffix_trans: 
446 
"suffix xs ys \<Longrightarrow> suffix ys zs \<Longrightarrow> suffix xs zs" 

447 
by (auto simp: suffix_def) 

63149  448 

449 
lemma strict_suffix_trans: 

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

451 
by (auto simp add: strict_suffix_def) 

49087  452 

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

455 

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

458 

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

461 

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

463 
by (simp add: suffix_def) 

49087  464 

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

467 

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

469 
by (auto simp add: suffix_def) 

470 

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

472 
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

473 

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

476 

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

478 
by (auto simp add: suffix_def) 

49087  479 

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

482 

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

49087  485 

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

493 

63149  494 
lemma suffix_to_prefix [code]: "suffix xs ys \<longleftrightarrow> prefix (rev xs) (rev ys)" 
49087  495 
proof 
63149  496 
assume "suffix xs ys" 
49087  497 
then obtain zs where "ys = zs @ xs" .. 
498 
then have "rev ys = rev xs @ rev zs" by simp 

63117  499 
then show "prefix (rev xs) (rev ys)" .. 
49087  500 
next 
63117  501 
assume "prefix (rev xs) (rev ys)" 
49087  502 
then obtain zs where "rev ys = rev xs @ zs" .. 
503 
then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp 

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

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

507 

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

17201  510 

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

25299  513 

63149  514 
lemma suffix_drop: "suffix (drop n as) as" 
515 
unfolding suffix_def 

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

518 
done 

25299  519 

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

25299  522 

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

525 

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

527 
unfolding suffix_def by auto 

49087  528 

63117  529 
lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefix x y" 
25692  530 
by blast 
25299  531 

63117  532 
lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefix y x" 
25692  533 
by blast 
25355  534 

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

25692  536 
unfolding parallel_def by simp 
25355  537 

25299  538 
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x" 
25692  539 
unfolding parallel_def by simp 
25299  540 

25564  541 
lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" 
25692  542 
by auto 
25299  543 

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

25299  547 
lemma not_equal_is_parallel: 
548 
assumes neq: "xs \<noteq> ys" 

25356  549 
and len: "length xs = length ys" 
550 
shows "xs \<parallel> ys" 

25299  551 
using len neq 
25355  552 
proof (induct rule: list_induct2) 
26445  553 
case Nil 
25356  554 
then show ?case by simp 
25299  555 
next 
26445  556 
case (Cons a as b bs) 
25355  557 
have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact 
25299  558 
show ?case 
559 
proof (cases "a = b") 

25355  560 
case True 
26445  561 
then have "as \<noteq> bs" using Cons by simp 
25355  562 
then show ?thesis by (rule Cons_parallelI2 [OF True ih]) 
25299  563 
next 
564 
case False 

25355  565 
then show ?thesis by (rule Cons_parallelI1) 
25299  566 
qed 
567 
qed 

22178  568 

49087  569 

60500  570 
subsection \<open>Homeomorphic embedding on lists\<close> 
49087  571 

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

572 
inductive list_emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
49087  573 
for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" 
574 
where 

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

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

576 
 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

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

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

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

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

581 
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

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

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

584 
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

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

586 

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

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

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

589 
using assms by (cases rule: list_emb.cases) auto 
49087  590 

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

591 
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

592 
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

593 
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

594 
using assms by (induct xs) auto 
49087  595 

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

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

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

599 
from list_emb_Nil2 [OF this] have False by simp 
49087  600 
} moreover { 
601 
assume False 

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

602 
then have "list_emb P (x#xs) []" by simp 
49087  603 
} ultimately show ?thesis by blast 
604 
qed 

605 

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

606 
lemma list_emb_append2 [intro]: "list_emb P xs ys \<Longrightarrow> list_emb P xs (zs @ ys)" 
49087  607 
by (induct zs) auto 
608 

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

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

610 
assumes "list_emb P xs ys" shows "list_emb P xs (ys @ zs)" 
49087  611 
using assms 
612 
by (induct arbitrary: zs) auto 

613 

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

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

615 
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

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

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

622 
case (list_emb_Cons2 x y xs ys) 
54483  623 
then show ?case by blast 
49087  624 
qed 
625 

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

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

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

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

49107  631 
case Nil then show ?case by auto 
49087  632 
next 
633 
case (Cons x xs) 

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

635 
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

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

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

640 
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  641 
thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc) 
49087  642 
qed 
643 

63149  644 
lemma list_emb_strict_suffix: 
645 
assumes "list_emb P xs ys" and "strict_suffix ys zs" 

646 
shows "list_emb P xs zs" 

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

648 

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

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

650 
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

651 
shows "list_emb P xs zs" 
63149  652 
using assms and list_emb_strict_suffix 
653 
unfolding strict_suffix_reflclp_conv[symmetric] by auto 

49087  654 

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

655 
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

656 
by (induct rule: list_emb.induct) auto 
49087  657 

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

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

659 
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

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

662 
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

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

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

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

669 
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

670 
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

671 
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

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

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

676 
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

677 
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

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

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

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

686 
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

687 
then show ?case unfolding zs by (rule list_emb_append2) 
49087  688 
qed 
689 
qed 

690 

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

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

692 
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

693 
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

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

695 

49087  696 

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

50516  699 
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

700 
where "sublisteq xs ys \<equiv> list_emb (op =) xs ys" 
49087  701 

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

50516  704 
lemma sublisteq_same_length: 
705 
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

706 
using assms by (induct) (auto dest: list_emb_length) 
49087  707 

50516  708 
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

709 
by (metis list_emb_length linorder_not_less) 
49087  710 

711 
lemma [code]: 

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

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

713 
"list_emb P (x#xs) [] \<longleftrightarrow> False" 
49087  714 
by (simp_all) 
715 

50516  716 
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

717 
by (induct xs, simp, blast dest: list_emb_ConsD) 
49087  718 

50516  719 
lemma sublisteq_Cons2': 
720 
assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys" 

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

49087  722 

50516  723 
lemma sublisteq_Cons2_neq: 
724 
assumes "sublisteq (x#xs) (y#ys)" 

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

49087  726 
using assms by (cases) auto 
727 

50516  728 
lemma sublisteq_Cons2_iff [simp, code]: 
729 
"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

730 
by (metis list_emb_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq) 
49087  731 

50516  732 
lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys" 
49087  733 
by (induct zs) simp_all 
734 

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

50516  737 
lemma sublisteq_antisym: 
738 
assumes "sublisteq xs ys" and "sublisteq ys xs" 

49087  739 
shows "xs = ys" 
740 
using assms 

741 
proof (induct) 

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

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

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

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

748 
case list_emb_Cons 
54483  749 
hence False using sublisteq_Cons' by fastforce 
750 
thus ?case .. 

49087  751 
qed 
752 

50516  753 
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

754 
by (rule list_emb_trans [of _ _ _ "op ="]) auto 
49087  755 

50516  756 
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

757 
by (auto dest: list_emb_length) 
49087  758 

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

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

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

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

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

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

764 
apply (metis append_Cons list_emb_Cons2) 
49107  765 
done 
49087  766 

767 

60500  768 
subsection \<open>Appending elements\<close> 
49087  769 

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

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

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

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

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

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

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

782 
then have ?case using list_emb_Cons(2) by(simp add: list_emb.list_emb_Cons) } 
49087  783 
ultimately show ?case by (auto simp:Cons_eq_append_conv) 
784 
next 

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

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

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

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

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

794 
ultimately show ?r by blast 

795 
next 

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

796 
assume ?r then show ?l by (metis list_emb_append_mono sublisteq_refl) 
49087  797 
qed 
798 

50516  799 
lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)" 
49087  800 
by (induct zs) auto 
801 

50516  802 
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

803 
by (metis append_Nil2 list_emb_Nil list_emb_append_mono) 
49087  804 

805 

60500  806 
subsection \<open>Relation to standard list operations\<close> 
49087  807 

50516  808 
lemma sublisteq_map: 
809 
assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)" 

49087  810 
using assms by (induct) auto 
811 

50516  812 
lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs" 
49087  813 
by (induct xs) auto 
814 

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

54483  817 
using assms by induct auto 
49087  818 

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

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

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

826 
case (list_emb_Cons xs ys x) 
49087  827 
then obtain N where "xs = sublist ys N" by blast 
49107  828 
then have "xs = sublist (x#ys) (Suc ` N)" 
49087  829 
by (clarsimp simp add:sublist_Cons inj_image_mem_iff) 
49107  830 
then show ?case by blast 
49087  831 
next 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
55579
diff
changeset

832 
case (list_emb_Cons2 x y xs ys) 
49087  833 
then obtain N where "xs = sublist ys N" by blast 
49107  834 
then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))" 
49087  835 
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

836 
moreover from list_emb_Cons2 have "x = y" by simp 
50516  837 
ultimately show ?case by blast 
49087  838 
qed 
839 
next 

840 
assume ?R 

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

50516  842 
moreover have "sublisteq (sublist ys N) ys" 
49107  843 
proof (induct ys arbitrary: N) 
49087  844 
case Nil show ?case by simp 
845 
next 

49107  846 
case Cons then show ?case by (auto simp: sublist_Cons) 
49087  847 
qed 
848 
ultimately show ?L by simp 

849 
qed 

850 

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

851 
end 