src/HOL/Library/Sublist.thy
changeset 54538 ba7392b52a7c
parent 54483 9f24325c2550
child 55579 207538943038
     1.1 --- a/src/HOL/Library/Sublist.thy	Wed Nov 20 18:32:25 2013 +0100
     1.2 +++ b/src/HOL/Library/Sublist.thy	Wed Nov 20 18:58:00 2013 +0100
     1.3 @@ -3,198 +3,12 @@
     1.4      Author:     Christian Sternagel, JAIST
     1.5  *)
     1.6  
     1.7 -header {* List prefixes, suffixes, and homeomorphic embedding *}
     1.8 +header {* Parallel lists, list 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)