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