summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Sublist.thy

changeset 49077 | 154f25a162e3 |

parent 45236 | ac4a2a66707d |

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/src/HOL/Library/Sublist.thy Wed Aug 29 10:27:56 2012 +0900 1.3 @@ -0,0 +1,382 @@ 1.4 +(* Title: HOL/Library/Sublist.thy 1.5 + Author: Tobias Nipkow and Markus Wenzel, TU Muenchen 1.6 +*) 1.7 + 1.8 +header {* List prefixes and postfixes *} 1.9 + 1.10 +theory Sublist 1.11 +imports List Main 1.12 +begin 1.13 + 1.14 +subsection {* Prefix order on lists *} 1.15 + 1.16 +instantiation list :: (type) "{order, bot}" 1.17 +begin 1.18 + 1.19 +definition 1.20 + prefix_def: "xs \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)" 1.21 + 1.22 +definition 1.23 + strict_prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (ys::'a list)" 1.24 + 1.25 +definition 1.26 + "bot = []" 1.27 + 1.28 +instance proof 1.29 +qed (auto simp add: prefix_def strict_prefix_def bot_list_def) 1.30 + 1.31 +end 1.32 + 1.33 +lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" 1.34 + unfolding prefix_def by blast 1.35 + 1.36 +lemma prefixE [elim?]: 1.37 + assumes "xs \<le> ys" 1.38 + obtains zs where "ys = xs @ zs" 1.39 + using assms unfolding prefix_def by blast 1.40 + 1.41 +lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" 1.42 + unfolding strict_prefix_def prefix_def by blast 1.43 + 1.44 +lemma strict_prefixE' [elim?]: 1.45 + assumes "xs < ys" 1.46 + obtains z zs where "ys = xs @ z # zs" 1.47 +proof - 1.48 + from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys" 1.49 + unfolding strict_prefix_def prefix_def by blast 1.50 + with that show ?thesis by (auto simp add: neq_Nil_conv) 1.51 +qed 1.52 + 1.53 +lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" 1.54 + unfolding strict_prefix_def by blast 1.55 + 1.56 +lemma strict_prefixE [elim?]: 1.57 + fixes xs ys :: "'a list" 1.58 + assumes "xs < ys" 1.59 + obtains "xs \<le> ys" and "xs \<noteq> ys" 1.60 + using assms unfolding strict_prefix_def by blast 1.61 + 1.62 + 1.63 +subsection {* Basic properties of prefixes *} 1.64 + 1.65 +theorem Nil_prefix [iff]: "[] \<le> xs" 1.66 + by (simp add: prefix_def) 1.67 + 1.68 +theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])" 1.69 + by (induct xs) (simp_all add: prefix_def) 1.70 + 1.71 +lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)" 1.72 +proof 1.73 + assume "xs \<le> ys @ [y]" 1.74 + then obtain zs where zs: "ys @ [y] = xs @ zs" .. 1.75 + show "xs = ys @ [y] \<or> xs \<le> ys" 1.76 + by (metis append_Nil2 butlast_append butlast_snoc prefixI zs) 1.77 +next 1.78 + assume "xs = ys @ [y] \<or> xs \<le> ys" 1.79 + then show "xs \<le> ys @ [y]" 1.80 + by (metis order_eq_iff order_trans prefixI) 1.81 +qed 1.82 + 1.83 +lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" 1.84 + by (auto simp add: prefix_def) 1.85 + 1.86 +lemma less_eq_list_code [code]: 1.87 + "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True" 1.88 + "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False" 1.89 + "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys" 1.90 + by simp_all 1.91 + 1.92 +lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" 1.93 + by (induct xs) simp_all 1.94 + 1.95 +lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])" 1.96 + by (metis append_Nil2 append_self_conv order_eq_iff prefixI) 1.97 + 1.98 +lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs" 1.99 + by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI) 1.100 + 1.101 +lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs" 1.102 + by (auto simp add: prefix_def) 1.103 + 1.104 +theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))" 1.105 + by (cases xs) (auto simp add: prefix_def) 1.106 + 1.107 +theorem prefix_append: 1.108 + "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))" 1.109 + apply (induct zs rule: rev_induct) 1.110 + apply force 1.111 + apply (simp del: append_assoc add: append_assoc [symmetric]) 1.112 + apply (metis append_eq_appendI) 1.113 + done 1.114 + 1.115 +lemma append_one_prefix: 1.116 + "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys" 1.117 + unfolding prefix_def 1.118 + by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj 1.119 + eq_Nil_appendI nth_drop') 1.120 + 1.121 +theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys" 1.122 + by (auto simp add: prefix_def) 1.123 + 1.124 +lemma prefix_same_cases: 1.125 + "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1" 1.126 + unfolding prefix_def by (metis append_eq_append_conv2) 1.127 + 1.128 +lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys" 1.129 + by (auto simp add: prefix_def) 1.130 + 1.131 +lemma take_is_prefix: "take n xs \<le> xs" 1.132 + unfolding prefix_def by (metis append_take_drop_id) 1.133 + 1.134 +lemma map_prefixI: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys" 1.135 + by (auto simp: prefix_def) 1.136 + 1.137 +lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys" 1.138 + by (auto simp: strict_prefix_def prefix_def) 1.139 + 1.140 +lemma strict_prefix_simps [simp, code]: 1.141 + "xs < [] \<longleftrightarrow> False" 1.142 + "[] < x # xs \<longleftrightarrow> True" 1.143 + "x # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys" 1.144 + by (simp_all add: strict_prefix_def cong: conj_cong) 1.145 + 1.146 +lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys" 1.147 + apply (induct n arbitrary: xs ys) 1.148 + apply (case_tac ys, simp_all)[1] 1.149 + apply (metis order_less_trans strict_prefixI take_is_prefix) 1.150 + done 1.151 + 1.152 +lemma not_prefix_cases: 1.153 + assumes pfx: "\<not> ps \<le> ls" 1.154 + obtains 1.155 + (c1) "ps \<noteq> []" and "ls = []" 1.156 + | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> as \<le> xs" 1.157 + | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a" 1.158 +proof (cases ps) 1.159 + case Nil then show ?thesis using pfx by simp 1.160 +next 1.161 + case (Cons a as) 1.162 + note c = `ps = a#as` 1.163 + show ?thesis 1.164 + proof (cases ls) 1.165 + case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil) 1.166 + next 1.167 + case (Cons x xs) 1.168 + show ?thesis 1.169 + proof (cases "x = a") 1.170 + case True 1.171 + have "\<not> as \<le> xs" using pfx c Cons True by simp 1.172 + with c Cons True show ?thesis by (rule c2) 1.173 + next 1.174 + case False 1.175 + with c Cons show ?thesis by (rule c3) 1.176 + qed 1.177 + qed 1.178 +qed 1.179 + 1.180 +lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: 1.181 + assumes np: "\<not> ps \<le> ls" 1.182 + and base: "\<And>x xs. P (x#xs) []" 1.183 + and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)" 1.184 + and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)" 1.185 + shows "P ps ls" using np 1.186 +proof (induct ls arbitrary: ps) 1.187 + case Nil then show ?case 1.188 + by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) 1.189 +next 1.190 + case (Cons y ys) 1.191 + then have npfx: "\<not> ps \<le> (y # ys)" by simp 1.192 + then obtain x xs where pv: "ps = x # xs" 1.193 + by (rule not_prefix_cases) auto 1.194 + show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2) 1.195 +qed 1.196 + 1.197 + 1.198 +subsection {* Parallel lists *} 1.199 + 1.200 +definition 1.201 + parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) where 1.202 + "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)" 1.203 + 1.204 +lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" 1.205 + unfolding parallel_def by blast 1.206 + 1.207 +lemma parallelE [elim]: 1.208 + assumes "xs \<parallel> ys" 1.209 + obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs" 1.210 + using assms unfolding parallel_def by blast 1.211 + 1.212 +theorem prefix_cases: 1.213 + obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys" 1.214 + unfolding parallel_def strict_prefix_def by blast 1.215 + 1.216 +theorem parallel_decomp: 1.217 + "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 1.218 +proof (induct xs rule: rev_induct) 1.219 + case Nil 1.220 + then have False by auto 1.221 + then show ?case .. 1.222 +next 1.223 + case (snoc x xs) 1.224 + show ?case 1.225 + proof (rule prefix_cases) 1.226 + assume le: "xs \<le> ys" 1.227 + then obtain ys' where ys: "ys = xs @ ys'" .. 1.228 + show ?thesis 1.229 + proof (cases ys') 1.230 + assume "ys' = []" 1.231 + then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys) 1.232 + next 1.233 + fix c cs assume ys': "ys' = c # cs" 1.234 + then show ?thesis 1.235 + by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI 1.236 + same_prefix_prefix snoc.prems ys) 1.237 + qed 1.238 + next 1.239 + assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) 1.240 + with snoc have False by blast 1.241 + then show ?thesis .. 1.242 + next 1.243 + assume "xs \<parallel> ys" 1.244 + with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" 1.245 + and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" 1.246 + by blast 1.247 + from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp 1.248 + with neq ys show ?thesis by blast 1.249 + qed 1.250 +qed 1.251 + 1.252 +lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d" 1.253 + apply (rule parallelI) 1.254 + apply (erule parallelE, erule conjE, 1.255 + induct rule: not_prefix_induct, simp+)+ 1.256 + done 1.257 + 1.258 +lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y" 1.259 + by (simp add: parallel_append) 1.260 + 1.261 +lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a" 1.262 + unfolding parallel_def by auto 1.263 + 1.264 + 1.265 +subsection {* Postfix order on lists *} 1.266 + 1.267 +definition 1.268 + postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where 1.269 + "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)" 1.270 + 1.271 +lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" 1.272 + unfolding postfix_def by blast 1.273 + 1.274 +lemma postfixE [elim?]: 1.275 + assumes "xs >>= ys" 1.276 + obtains zs where "xs = zs @ ys" 1.277 + using assms unfolding postfix_def by blast 1.278 + 1.279 +lemma postfix_refl [iff]: "xs >>= xs" 1.280 + by (auto simp add: postfix_def) 1.281 +lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs" 1.282 + by (auto simp add: postfix_def) 1.283 +lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys" 1.284 + by (auto simp add: postfix_def) 1.285 + 1.286 +lemma Nil_postfix [iff]: "xs >>= []" 1.287 + by (simp add: postfix_def) 1.288 +lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" 1.289 + by (auto simp add: postfix_def) 1.290 + 1.291 +lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys" 1.292 + by (auto simp add: postfix_def) 1.293 +lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys" 1.294 + by (auto simp add: postfix_def) 1.295 + 1.296 +lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys" 1.297 + by (auto simp add: postfix_def) 1.298 +lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys" 1.299 + by (auto simp add: postfix_def) 1.300 + 1.301 +lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs" 1.302 +proof - 1.303 + assume "xs >>= ys" 1.304 + then obtain zs where "xs = zs @ ys" .. 1.305 + then show ?thesis by (induct zs) auto 1.306 +qed 1.307 + 1.308 +lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" 1.309 +proof - 1.310 + assume "x#xs >>= y#ys" 1.311 + then obtain zs where "x#xs = zs @ y#ys" .. 1.312 + then show ?thesis 1.313 + by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) 1.314 +qed 1.315 + 1.316 +lemma postfix_to_prefix [code]: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs" 1.317 +proof 1.318 + assume "xs >>= ys" 1.319 + then obtain zs where "xs = zs @ ys" .. 1.320 + then have "rev xs = rev ys @ rev zs" by simp 1.321 + then show "rev ys <= rev xs" .. 1.322 +next 1.323 + assume "rev ys <= rev xs" 1.324 + then obtain zs where "rev xs = rev ys @ zs" .. 1.325 + then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp 1.326 + then have "xs = rev zs @ ys" by simp 1.327 + then show "xs >>= ys" .. 1.328 +qed 1.329 + 1.330 +lemma distinct_postfix: "distinct xs \<Longrightarrow> xs >>= ys \<Longrightarrow> distinct ys" 1.331 + by (clarsimp elim!: postfixE) 1.332 + 1.333 +lemma postfix_map: "xs >>= ys \<Longrightarrow> map f xs >>= map f ys" 1.334 + by (auto elim!: postfixE intro: postfixI) 1.335 + 1.336 +lemma postfix_drop: "as >>= drop n as" 1.337 + unfolding postfix_def 1.338 + apply (rule exI [where x = "take n as"]) 1.339 + apply simp 1.340 + done 1.341 + 1.342 +lemma postfix_take: "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys" 1.343 + by (clarsimp elim!: postfixE) 1.344 + 1.345 +lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y" 1.346 + by blast 1.347 + 1.348 +lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> y \<le> x" 1.349 + by blast 1.350 + 1.351 +lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []" 1.352 + unfolding parallel_def by simp 1.353 + 1.354 +lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x" 1.355 + unfolding parallel_def by simp 1.356 + 1.357 +lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" 1.358 + by auto 1.359 + 1.360 +lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs" 1.361 + by (metis Cons_prefix_Cons parallelE parallelI) 1.362 + 1.363 +lemma not_equal_is_parallel: 1.364 + assumes neq: "xs \<noteq> ys" 1.365 + and len: "length xs = length ys" 1.366 + shows "xs \<parallel> ys" 1.367 + using len neq 1.368 +proof (induct rule: list_induct2) 1.369 + case Nil 1.370 + then show ?case by simp 1.371 +next 1.372 + case (Cons a as b bs) 1.373 + have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact 1.374 + show ?case 1.375 + proof (cases "a = b") 1.376 + case True 1.377 + then have "as \<noteq> bs" using Cons by simp 1.378 + then show ?thesis by (rule Cons_parallelI2 [OF True ih]) 1.379 + next 1.380 + case False 1.381 + then show ?thesis by (rule Cons_parallelI1) 1.382 + qed 1.383 +qed 1.384 + 1.385 +end