src/HOL/Library/Sublist.thy
changeset 55579 207538943038
parent 54538 ba7392b52a7c
child 57497 4106a2bc066a
     1.1 --- a/src/HOL/Library/Sublist.thy	Wed Feb 19 10:21:02 2014 +0100
     1.2 +++ b/src/HOL/Library/Sublist.thy	Wed Feb 19 10:30:21 2014 +0100
     1.3 @@ -3,12 +3,198 @@
     1.4      Author:     Christian Sternagel, JAIST
     1.5  *)
     1.6  
     1.7 -header {* Parallel lists, list suffixes, and homeomorphic embedding *}
     1.8 +header {* List prefixes, suffixes, and homeomorphic embedding *}
     1.9  
    1.10  theory Sublist
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 +subsection {* Prefix order on lists *}
    1.15 +
    1.16 +definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.17 +  where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    1.18 +
    1.19 +definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.20 +  where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    1.21 +
    1.22 +interpretation prefix_order: order prefixeq prefix
    1.23 +  by default (auto simp: prefixeq_def prefix_def)
    1.24 +
    1.25 +interpretation prefix_bot: order_bot Nil prefixeq prefix
    1.26 +  by default (simp add: prefixeq_def)
    1.27 +
    1.28 +lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
    1.29 +  unfolding prefixeq_def by blast
    1.30 +
    1.31 +lemma prefixeqE [elim?]:
    1.32 +  assumes "prefixeq xs ys"
    1.33 +  obtains zs where "ys = xs @ zs"
    1.34 +  using assms unfolding prefixeq_def by blast
    1.35 +
    1.36 +lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
    1.37 +  unfolding prefix_def prefixeq_def by blast
    1.38 +
    1.39 +lemma prefixE' [elim?]:
    1.40 +  assumes "prefix xs ys"
    1.41 +  obtains z zs where "ys = xs @ z # zs"
    1.42 +proof -
    1.43 +  from `prefix xs ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    1.44 +    unfolding prefix_def prefixeq_def by blast
    1.45 +  with that show ?thesis by (auto simp add: neq_Nil_conv)
    1.46 +qed
    1.47 +
    1.48 +lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
    1.49 +  unfolding prefix_def by blast
    1.50 +
    1.51 +lemma prefixE [elim?]:
    1.52 +  fixes xs ys :: "'a list"
    1.53 +  assumes "prefix xs ys"
    1.54 +  obtains "prefixeq xs ys" and "xs \<noteq> ys"
    1.55 +  using assms unfolding prefix_def by blast
    1.56 +
    1.57 +
    1.58 +subsection {* Basic properties of prefixes *}
    1.59 +
    1.60 +theorem Nil_prefixeq [iff]: "prefixeq [] xs"
    1.61 +  by (simp add: prefixeq_def)
    1.62 +
    1.63 +theorem prefixeq_Nil [simp]: "(prefixeq xs []) = (xs = [])"
    1.64 +  by (induct xs) (simp_all add: prefixeq_def)
    1.65 +
    1.66 +lemma prefixeq_snoc [simp]: "prefixeq xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefixeq xs ys"
    1.67 +proof
    1.68 +  assume "prefixeq xs (ys @ [y])"
    1.69 +  then obtain zs where zs: "ys @ [y] = xs @ zs" ..
    1.70 +  show "xs = ys @ [y] \<or> prefixeq xs ys"
    1.71 +    by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs)
    1.72 +next
    1.73 +  assume "xs = ys @ [y] \<or> prefixeq xs ys"
    1.74 +  then show "prefixeq xs (ys @ [y])"
    1.75 +    by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI)
    1.76 +qed
    1.77 +
    1.78 +lemma Cons_prefixeq_Cons [simp]: "prefixeq (x # xs) (y # ys) = (x = y \<and> prefixeq xs ys)"
    1.79 +  by (auto simp add: prefixeq_def)
    1.80 +
    1.81 +lemma prefixeq_code [code]:
    1.82 +  "prefixeq [] xs \<longleftrightarrow> True"
    1.83 +  "prefixeq (x # xs) [] \<longleftrightarrow> False"
    1.84 +  "prefixeq (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefixeq xs ys"
    1.85 +  by simp_all
    1.86 +
    1.87 +lemma same_prefixeq_prefixeq [simp]: "prefixeq (xs @ ys) (xs @ zs) = prefixeq ys zs"
    1.88 +  by (induct xs) simp_all
    1.89 +
    1.90 +lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
    1.91 +  by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
    1.92 +
    1.93 +lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
    1.94 +  by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
    1.95 +
    1.96 +lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
    1.97 +  by (auto simp add: prefixeq_def)
    1.98 +
    1.99 +theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefixeq zs ys))"
   1.100 +  by (cases xs) (auto simp add: prefixeq_def)
   1.101 +
   1.102 +theorem prefixeq_append:
   1.103 +  "prefixeq xs (ys @ zs) = (prefixeq xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefixeq us zs))"
   1.104 +  apply (induct zs rule: rev_induct)
   1.105 +   apply force
   1.106 +  apply (simp del: append_assoc add: append_assoc [symmetric])
   1.107 +  apply (metis append_eq_appendI)
   1.108 +  done
   1.109 +
   1.110 +lemma append_one_prefixeq:
   1.111 +  "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
   1.112 +  proof (unfold prefixeq_def)
   1.113 +    assume a1: "\<exists>zs. ys = xs @ zs"
   1.114 +    then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
   1.115 +    assume a2: "length xs < length ys"
   1.116 +    have f1: "\<And>v. ([]\<Colon>'a list) @ v = v" using append_Nil2 by simp
   1.117 +    have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force
   1.118 +    hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl)
   1.119 +    thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce
   1.120 +  qed
   1.121 +
   1.122 +theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
   1.123 +  by (auto simp add: prefixeq_def)
   1.124 +
   1.125 +lemma prefixeq_same_cases:
   1.126 +  "prefixeq (xs\<^sub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^sub>2 ys \<Longrightarrow> prefixeq xs\<^sub>1 xs\<^sub>2 \<or> prefixeq xs\<^sub>2 xs\<^sub>1"
   1.127 +  unfolding prefixeq_def by (force simp: append_eq_append_conv2)
   1.128 +
   1.129 +lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys"
   1.130 +  by (auto simp add: prefixeq_def)
   1.131 +
   1.132 +lemma take_is_prefixeq: "prefixeq (take n xs) xs"
   1.133 +  unfolding prefixeq_def by (metis append_take_drop_id)
   1.134 +
   1.135 +lemma map_prefixeqI: "prefixeq xs ys \<Longrightarrow> prefixeq (map f xs) (map f ys)"
   1.136 +  by (auto simp: prefixeq_def)
   1.137 +
   1.138 +lemma prefixeq_length_less: "prefix xs ys \<Longrightarrow> length xs < length ys"
   1.139 +  by (auto simp: prefix_def prefixeq_def)
   1.140 +
   1.141 +lemma prefix_simps [simp, code]:
   1.142 +  "prefix xs [] \<longleftrightarrow> False"
   1.143 +  "prefix [] (x # xs) \<longleftrightarrow> True"
   1.144 +  "prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys"
   1.145 +  by (simp_all add: prefix_def cong: conj_cong)
   1.146 +
   1.147 +lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
   1.148 +  apply (induct n arbitrary: xs ys)
   1.149 +   apply (case_tac ys, simp_all)[1]
   1.150 +  apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
   1.151 +  done
   1.152 +
   1.153 +lemma not_prefixeq_cases:
   1.154 +  assumes pfx: "\<not> prefixeq ps ls"
   1.155 +  obtains
   1.156 +    (c1) "ps \<noteq> []" and "ls = []"
   1.157 +  | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefixeq as xs"
   1.158 +  | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
   1.159 +proof (cases ps)
   1.160 +  case Nil
   1.161 +  then show ?thesis using pfx by simp
   1.162 +next
   1.163 +  case (Cons a as)
   1.164 +  note c = `ps = a#as`
   1.165 +  show ?thesis
   1.166 +  proof (cases ls)
   1.167 +    case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil)
   1.168 +  next
   1.169 +    case (Cons x xs)
   1.170 +    show ?thesis
   1.171 +    proof (cases "x = a")
   1.172 +      case True
   1.173 +      have "\<not> prefixeq as xs" using pfx c Cons True by simp
   1.174 +      with c Cons True show ?thesis by (rule c2)
   1.175 +    next
   1.176 +      case False
   1.177 +      with c Cons show ?thesis by (rule c3)
   1.178 +    qed
   1.179 +  qed
   1.180 +qed
   1.181 +
   1.182 +lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]:
   1.183 +  assumes np: "\<not> prefixeq ps ls"
   1.184 +    and base: "\<And>x xs. P (x#xs) []"
   1.185 +    and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
   1.186 +    and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefixeq xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
   1.187 +  shows "P ps ls" using np
   1.188 +proof (induct ls arbitrary: ps)
   1.189 +  case Nil then show ?case
   1.190 +    by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base)
   1.191 +next
   1.192 +  case (Cons y ys)
   1.193 +  then have npfx: "\<not> prefixeq ps (y # ys)" by simp
   1.194 +  then obtain x xs where pv: "ps = x # xs"
   1.195 +    by (rule not_prefixeq_cases) auto
   1.196 +  show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2)
   1.197 +qed
   1.198 +
   1.199 +
   1.200  subsection {* Parallel lists *}
   1.201  
   1.202  definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)