introduced "sub" as abbreviation for "emb (op =)";
authorChristian Sternagel
Wed Aug 29 16:25:35 2012 +0900 (2012-08-29)
changeset 490854eef5c2ff5ad
parent 49084 e3973567ed4f
child 49086 835fd053d17d
introduced "sub" as abbreviation for "emb (op =)";
Sublist_Order is now based on Sublist.sub;
simplified and moved most lemmas on sub from Sublist_Order to Sublist;
Sublist_Order merely contains ord and order instances for sub plus some lemmas on the strict part of the order
src/HOL/Library/Sublist.thy
src/HOL/Library/Sublist_Order.thy
     1.1 --- a/src/HOL/Library/Sublist.thy	Wed Aug 29 12:24:26 2012 +0900
     1.2 +++ b/src/HOL/Library/Sublist.thy	Wed Aug 29 16:25:35 2012 +0900
     1.3 @@ -433,6 +433,17 @@
     1.4    assumes "emb P xs []" shows "xs = []"
     1.5    using assms by (cases rule: emb.cases) auto
     1.6  
     1.7 +lemma emb_Cons_Nil [simp]:
     1.8 +  "emb P (x#xs) [] = False"
     1.9 +proof -
    1.10 +  { assume "emb P (x#xs) []"
    1.11 +    from emb_Nil2 [OF this] have False by simp
    1.12 +  } moreover {
    1.13 +    assume False
    1.14 +    hence "emb P (x#xs) []" by simp
    1.15 +  } ultimately show ?thesis by blast
    1.16 +qed
    1.17 +
    1.18  lemma emb_append2 [intro]:
    1.19    "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)"
    1.20    by (induct zs) auto
    1.21 @@ -479,4 +490,202 @@
    1.22  lemma emb_length: "emb P xs ys \<Longrightarrow> length xs \<le> length ys"
    1.23    by (induct rule: emb.induct) auto
    1.24  
    1.25 +(*FIXME: move*)
    1.26 +definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
    1.27 +  "transp_on P A \<equiv> \<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c"
    1.28 +lemma transp_onI [Pure.intro]:
    1.29 +  "(\<And>a b c. \<lbrakk>a \<in> A; b \<in> A; c \<in> A; P a b; P b c\<rbrakk> \<Longrightarrow> P a c) \<Longrightarrow> transp_on P A"
    1.30 +  unfolding transp_on_def by blast
    1.31 +
    1.32 +lemma transp_on_emb:
    1.33 +  assumes "transp_on P A"
    1.34 +  shows "transp_on (emb P) (lists A)"
    1.35 +proof
    1.36 +  fix xs ys zs
    1.37 +  assume "emb P xs ys" and "emb P ys zs"
    1.38 +    and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
    1.39 +  thus "emb P xs zs"
    1.40 +  proof (induction arbitrary: zs)
    1.41 +    case emb_Nil show ?case by blast
    1.42 +  next
    1.43 +    case (emb_Cons xs ys y)
    1.44 +    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
    1.45 +      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
    1.46 +    hence "emb P ys (v#vs)" by blast
    1.47 +    hence "emb P ys zs" unfolding zs by (rule emb_append2)
    1.48 +    from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp
    1.49 +  next
    1.50 +    case (emb_Cons2 x y xs ys)
    1.51 +    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
    1.52 +      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
    1.53 +    with emb_Cons2 have "emb P xs vs" by simp
    1.54 +    moreover have "P x v"
    1.55 +    proof -
    1.56 +      from zs and `zs \<in> lists A` have "v \<in> A" by auto
    1.57 +      moreover have "x \<in> A" and "y \<in> A" using emb_Cons2 by simp_all
    1.58 +      ultimately show ?thesis using `P x y` and `P y v` and assms
    1.59 +        unfolding transp_on_def by blast
    1.60 +    qed
    1.61 +    ultimately have "emb P (x#xs) (v#vs)" by blast
    1.62 +    thus ?case unfolding zs by (rule emb_append2)
    1.63 +  qed
    1.64 +qed
    1.65 +
    1.66 +
    1.67 +subsection {* Sublists (special case of embedding) *}
    1.68 +
    1.69 +abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.70 +  "sub xs ys \<equiv> emb (op =) xs ys"
    1.71 +
    1.72 +lemma sub_Cons2: "sub xs ys \<Longrightarrow> sub (x#xs) (x#ys)" by auto
    1.73 +
    1.74 +lemma sub_same_length:
    1.75 +  assumes "sub xs ys" and "length xs = length ys" shows "xs = ys"
    1.76 +  using assms by (induct) (auto dest: emb_length)
    1.77 +
    1.78 +lemma not_sub_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sub xs ys"
    1.79 +  by (metis emb_length linorder_not_less)
    1.80 +
    1.81 +lemma [code]:
    1.82 +  "emb P [] ys \<longleftrightarrow> True"
    1.83 +  "emb P (x#xs) [] \<longleftrightarrow> False"
    1.84 +  by (simp_all)
    1.85 +
    1.86 +lemma sub_Cons': "sub (x#xs) ys \<Longrightarrow> sub xs ys"
    1.87 +  by (induct xs) (auto dest: emb_ConsD)
    1.88 +
    1.89 +lemma sub_Cons2':
    1.90 +  assumes "sub (x#xs) (x#ys)" shows "sub xs ys"
    1.91 +  using assms by (cases) (rule sub_Cons')
    1.92 +
    1.93 +lemma sub_Cons2_neq:
    1.94 +  assumes "sub (x#xs) (y#ys)"
    1.95 +  shows "x \<noteq> y \<Longrightarrow> sub (x#xs) ys"
    1.96 +  using assms by (cases) auto
    1.97 +
    1.98 +lemma sub_Cons2_iff [simp, code]:
    1.99 +  "sub (x#xs) (y#ys) = (if x = y then sub xs ys else sub (x#xs) ys)"
   1.100 +  by (metis emb_Cons emb_Cons2 [of "op =", OF refl] sub_Cons2' sub_Cons2_neq)
   1.101 +
   1.102 +lemma sub_append': "sub (zs @ xs) (zs @ ys) \<longleftrightarrow> sub xs ys"
   1.103 +  by (induct zs) simp_all
   1.104 +
   1.105 +lemma sub_refl [simp, intro!]: "sub xs xs" by (induct xs) simp_all
   1.106 +
   1.107 +lemma sub_antisym:
   1.108 +  assumes "sub xs ys" and "sub ys xs"
   1.109 +  shows "xs = ys"
   1.110 +using assms
   1.111 +proof (induct)
   1.112 +  case emb_Nil
   1.113 +  from emb_Nil2 [OF this] show ?case by simp
   1.114 +next
   1.115 +  case emb_Cons2 thus ?case by simp
   1.116 +next
   1.117 +  case emb_Cons thus ?case
   1.118 +    by (metis sub_Cons' emb_length Suc_length_conv Suc_n_not_le_n)
   1.119 +qed
   1.120 +
   1.121 +lemma transp_on_sub: "transp_on sub UNIV"
   1.122 +proof -
   1.123 +  have "transp_on (op =) UNIV" by (simp add: transp_on_def)
   1.124 +  from transp_on_emb [OF this] show ?thesis by simp
   1.125 +qed
   1.126 +
   1.127 +lemma sub_trans: "sub xs ys \<Longrightarrow> sub ys zs \<Longrightarrow> sub xs zs"
   1.128 +  using transp_on_sub [unfolded transp_on_def] by blast
   1.129 +
   1.130 +lemma sub_append_le_same_iff: "sub (xs @ ys) ys \<longleftrightarrow> xs = []"
   1.131 +  by (auto dest: emb_length)
   1.132 +
   1.133 +lemma emb_append_mono:
   1.134 +  "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> emb P (xs@ys) (xs'@ys')"
   1.135 +apply (induct rule: emb.induct)
   1.136 +  apply (metis eq_Nil_appendI emb_append2)
   1.137 + apply (metis append_Cons emb_Cons)
   1.138 +by (metis append_Cons emb_Cons2)
   1.139 +
   1.140 +
   1.141 +subsection {* Appending elements *}
   1.142 +
   1.143 +lemma sub_append [simp]:
   1.144 +  "sub (xs @ zs) (ys @ zs) \<longleftrightarrow> sub xs ys" (is "?l = ?r")
   1.145 +proof
   1.146 +  { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'"
   1.147 +    hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys"
   1.148 +    proof (induct arbitrary: xs ys zs)
   1.149 +      case emb_Nil show ?case by simp
   1.150 +    next
   1.151 +      case (emb_Cons xs' ys' x)
   1.152 +      { assume "ys=[]" hence ?case using emb_Cons(1) by auto }
   1.153 +      moreover
   1.154 +      { fix us assume "ys = x#us"
   1.155 +        hence ?case using emb_Cons(2) by(simp add: emb.emb_Cons) }
   1.156 +      ultimately show ?case by (auto simp:Cons_eq_append_conv)
   1.157 +    next
   1.158 +      case (emb_Cons2 x y xs' ys')
   1.159 +      { assume "xs=[]" hence ?case using emb_Cons2(1) by auto }
   1.160 +      moreover
   1.161 +      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using emb_Cons2 by auto}
   1.162 +      moreover
   1.163 +      { fix us assume "xs=x#us" "ys=[]" hence ?case using emb_Cons2(2) by bestsimp }
   1.164 +      ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv)
   1.165 +    qed }
   1.166 +  moreover assume ?l
   1.167 +  ultimately show ?r by blast
   1.168 +next
   1.169 +  assume ?r thus ?l by (metis emb_append_mono sub_refl)
   1.170 +qed
   1.171 +
   1.172 +lemma sub_drop_many: "sub xs ys \<Longrightarrow> sub xs (zs @ ys)"
   1.173 +  by (induct zs) auto
   1.174 +
   1.175 +lemma sub_rev_drop_many: "sub xs ys \<Longrightarrow> sub xs (ys @ zs)"
   1.176 +  by (metis append_Nil2 emb_Nil emb_append_mono)
   1.177 +
   1.178 +
   1.179 +subsection {* Relation to standard list operations *}
   1.180 +
   1.181 +lemma sub_map:
   1.182 +  assumes "sub xs ys" shows "sub (map f xs) (map f ys)"
   1.183 +  using assms by (induct) auto
   1.184 +
   1.185 +lemma sub_filter_left [simp]: "sub (filter P xs) xs"
   1.186 +  by (induct xs) auto
   1.187 +
   1.188 +lemma sub_filter [simp]:
   1.189 +  assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)"
   1.190 +  using assms by (induct) auto
   1.191 +
   1.192 +lemma "sub xs ys \<longleftrightarrow> (\<exists> N. xs = sublist ys N)" (is "?L = ?R")
   1.193 +proof
   1.194 +  assume ?L
   1.195 +  thus ?R
   1.196 +  proof (induct)
   1.197 +    case emb_Nil show ?case by (metis sublist_empty)
   1.198 +  next
   1.199 +    case (emb_Cons xs ys x)
   1.200 +    then obtain N where "xs = sublist ys N" by blast
   1.201 +    hence "xs = sublist (x#ys) (Suc ` N)"
   1.202 +      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.203 +    thus ?case by blast
   1.204 +  next
   1.205 +    case (emb_Cons2 x y xs ys)
   1.206 +    then obtain N where "xs = sublist ys N" by blast
   1.207 +    hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   1.208 +      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.209 +    thus ?case unfolding `x = y` by blast
   1.210 +  qed
   1.211 +next
   1.212 +  assume ?R
   1.213 +  then obtain N where "xs = sublist ys N" ..
   1.214 +  moreover have "sub (sublist ys N) ys"
   1.215 +  proof (induct ys arbitrary:N)
   1.216 +    case Nil show ?case by simp
   1.217 +  next
   1.218 +    case Cons thus ?case by (auto simp: sublist_Cons)
   1.219 +  qed
   1.220 +  ultimately show ?L by simp
   1.221 +qed
   1.222 +
   1.223  end
     2.1 --- a/src/HOL/Library/Sublist_Order.thy	Wed Aug 29 12:24:26 2012 +0900
     2.2 +++ b/src/HOL/Library/Sublist_Order.thy	Wed Aug 29 16:25:35 2012 +0900
     2.3 @@ -6,7 +6,9 @@
     2.4  header {* Sublist Ordering *}
     2.5  
     2.6  theory Sublist_Order
     2.7 -imports Main Sublist
     2.8 +imports
     2.9 +  Main
    2.10 +  Sublist
    2.11  begin
    2.12  
    2.13  text {*
    2.14 @@ -21,256 +23,54 @@
    2.15  begin
    2.16  
    2.17  definition
    2.18 -  "(xs :: 'a list) \<le> ys \<longleftrightarrow> emb (op =) xs ys"
    2.19 +  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys"
    2.20  
    2.21  definition
    2.22    "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    2.23  
    2.24 -instance proof qed
    2.25 +instance ..
    2.26  
    2.27  end
    2.28  
    2.29 -lemma empty [simp, intro!]: "[] \<le> xs" by (auto simp: less_eq_list_def)
    2.30 -
    2.31 -lemma drop: "xs \<le> ys \<Longrightarrow> xs \<le> (y # ys)"
    2.32 -  by (unfold less_eq_list_def) blast
    2.33 -
    2.34 -lemma take: "xs \<le> ys \<Longrightarrow> (x#xs) \<le> (x#ys)"
    2.35 -  by (unfold less_eq_list_def) blast
    2.36 -
    2.37 -lemmas le_list_induct [consumes 1, case_names empty drop take] =
    2.38 -  emb.induct [of "op =", folded less_eq_list_def]
    2.39 -
    2.40 -lemmas le_list_cases [consumes 1, case_names empty drop take] =
    2.41 -  emb.cases [of "op =", folded less_eq_list_def]
    2.42 -
    2.43 -lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    2.44 -  by (induct rule: le_list_induct) auto
    2.45 -
    2.46 -lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
    2.47 -  by (induct rule: le_list_induct) (auto dest: le_list_length)
    2.48 -
    2.49 -lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"
    2.50 -by (metis le_list_length linorder_not_less)
    2.51 -
    2.52 -lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
    2.53 -by (auto dest: le_list_length)
    2.54 -
    2.55 -lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
    2.56 -by (induct zs) (auto simp: less_eq_list_def)
    2.57 -
    2.58 -lemma [code]: "[] <= xs \<longleftrightarrow> True"
    2.59 -by (simp add: less_eq_list_def)
    2.60 -
    2.61 -lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"
    2.62 -by simp
    2.63 -
    2.64 -lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys"
    2.65 -proof-
    2.66 -  { fix xs' ys'
    2.67 -    assume "xs' <= ys"
    2.68 -    hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"
    2.69 -    proof (induct rule: le_list_induct)
    2.70 -      case empty thus ?case by simp
    2.71 -    next
    2.72 -      note drop' = drop
    2.73 -      case drop thus ?case by (metis drop')
    2.74 -    next
    2.75 -      note t = take
    2.76 -      case take thus ?case by (simp add: drop)
    2.77 -    qed }
    2.78 -  from this[OF assms] show ?thesis by simp
    2.79 -qed
    2.80 -
    2.81 -lemma le_list_drop_Cons2:
    2.82 -assumes "x#xs <= x#ys" shows "xs <= ys"
    2.83 -using assms
    2.84 -proof (cases rule: le_list_cases)
    2.85 -  case drop thus ?thesis by (metis le_list_drop_Cons list.inject)
    2.86 -qed simp_all
    2.87 -
    2.88 -lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"
    2.89 -shows "x ~= y \<Longrightarrow> x # xs <= ys"
    2.90 -using assms by (cases rule: le_list_cases) auto
    2.91 -
    2.92 -lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>
    2.93 -  (if x=y then xs <= ys else (x#xs) <= ys)"
    2.94 -by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq)
    2.95 -
    2.96 -lemma le_list_take_many_iff: "zs @ xs \<le> zs @ ys \<longleftrightarrow> xs \<le> ys"
    2.97 -by (induct zs) (auto intro: take)
    2.98 -
    2.99 -lemma le_list_Cons_EX:
   2.100 -  assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs"
   2.101 -proof-
   2.102 -  { fix xys zs :: "'a list" assume "xys <= zs"
   2.103 -    hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)"
   2.104 -    proof (induct rule: le_list_induct)
   2.105 -      case empty show ?case by simp
   2.106 -    next
   2.107 -      case take thus ?case by (metis list.inject self_append_conv2)
   2.108 -    next
   2.109 -      case drop thus ?case by (metis append_eq_Cons_conv)
   2.110 -    qed
   2.111 -  } with assms show ?thesis by blast
   2.112 -qed
   2.113 -
   2.114 -instantiation list :: (type) order
   2.115 -begin
   2.116 -
   2.117 -instance proof
   2.118 +instance list :: (type) order
   2.119 +proof
   2.120    fix xs ys :: "'a list"
   2.121    show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
   2.122  next
   2.123    fix xs :: "'a list"
   2.124 -  show "xs \<le> xs" by (induct xs) (auto intro!: drop)
   2.125 +  show "xs \<le> xs" by (simp add: less_eq_list_def)
   2.126  next
   2.127    fix xs ys :: "'a list"
   2.128 -  assume "xs <= ys"
   2.129 -  hence "ys <= xs \<longrightarrow> xs = ys"
   2.130 -  proof (induct rule: le_list_induct)
   2.131 -    case empty show ?case by simp
   2.132 -  next
   2.133 -    case take thus ?case by simp
   2.134 -  next
   2.135 -    case drop thus ?case
   2.136 -      by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n)
   2.137 -  qed
   2.138 -  moreover assume "ys <= xs"
   2.139 -  ultimately show "xs = ys" by blast
   2.140 +  assume "xs <= ys" and "ys <= xs"
   2.141 +  thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym)
   2.142  next
   2.143    fix xs ys zs :: "'a list"
   2.144 -  assume "xs <= ys"
   2.145 -  hence "ys <= zs \<longrightarrow> xs <= zs"
   2.146 -  proof (induct arbitrary:zs rule: le_list_induct)
   2.147 -    case empty show ?case by simp
   2.148 -  next
   2.149 -    note take' = take
   2.150 -    case (take x y xs ys) show ?case
   2.151 -    proof
   2.152 -      assume "y # ys <= zs"
   2.153 -      with take show "x # xs <= zs"
   2.154 -        by(metis le_list_Cons_EX le_list_drop_many take')
   2.155 -    qed
   2.156 -  next
   2.157 -    case drop thus ?case by (metis le_list_drop_Cons)
   2.158 -  qed
   2.159 -  moreover assume "ys <= zs"
   2.160 -  ultimately show "xs <= zs" by blast
   2.161 +  assume "xs <= ys" and "ys <= zs"
   2.162 +  thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
   2.163  qed
   2.164  
   2.165 -end
   2.166 -
   2.167 -lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]"
   2.168 -by (auto dest: le_list_length)
   2.169 -
   2.170 -lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"
   2.171 -apply (induct rule: le_list_induct)
   2.172 -  apply (metis eq_Nil_appendI le_list_drop_many)
   2.173 - apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)
   2.174 -apply simp
   2.175 -done
   2.176 -
   2.177  lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
   2.178 -by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def)
   2.179 +  by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)
   2.180  
   2.181  lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
   2.182 -by (metis empty order_less_le)
   2.183 +  by (metis less_eq_list_def emb_Nil order_less_le)
   2.184  
   2.185 -lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"
   2.186 -by (metis empty less_list_def)
   2.187 +lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
   2.188 +  by (metis emb_Nil less_eq_list_def less_list_def)
   2.189  
   2.190  lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   2.191 -by (unfold less_le) (auto intro: drop)
   2.192 +  by (unfold less_le less_eq_list_def) (auto)
   2.193  
   2.194  lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
   2.195 -by (metis le_list_Cons2_iff less_list_def)
   2.196 +  by (metis sub_Cons2_iff less_list_def less_eq_list_def)
   2.197  
   2.198  lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
   2.199 -by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2)
   2.200 +  by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def)
   2.201  
   2.202  lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
   2.203 -by (metis le_list_take_many_iff less_list_def)
   2.204 -
   2.205 -
   2.206 -subsection {* Appending elements *}
   2.207 -
   2.208 -lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R")
   2.209 -proof
   2.210 -  { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
   2.211 -    hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys"
   2.212 -    proof (induct arbitrary: xs ys zs rule: le_list_induct)
   2.213 -      case empty show ?case by simp
   2.214 -    next
   2.215 -      note drop' = drop
   2.216 -      case (drop xs' ys' x)
   2.217 -      { assume "ys=[]" hence ?case using drop(1) by auto }
   2.218 -      moreover
   2.219 -      { fix us assume "ys = x#us"
   2.220 -        hence ?case using drop(2) by(simp add: drop') }
   2.221 -      ultimately show ?case by (auto simp:Cons_eq_append_conv)
   2.222 -    next
   2.223 -      case (take x y xs' ys')
   2.224 -      { assume "xs=[]" hence ?case using take(1) by auto }
   2.225 -      moreover
   2.226 -      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take by auto}
   2.227 -      moreover
   2.228 -      { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
   2.229 -      ultimately show ?case using `x = y` by (auto simp:Cons_eq_append_conv)
   2.230 -    qed }
   2.231 -  moreover assume ?L
   2.232 -  ultimately show ?R by blast
   2.233 -next
   2.234 -  assume ?R thus ?L by(metis le_list_append_mono order_refl)
   2.235 -qed
   2.236 +  by (metis less_list_def less_eq_list_def sub_append')
   2.237  
   2.238  lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
   2.239 -by (unfold less_le) auto
   2.240 -
   2.241 -lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
   2.242 -by (metis append_Nil2 empty le_list_append_mono)
   2.243 -
   2.244 -
   2.245 -subsection {* Relation to standard list operations *}
   2.246 -
   2.247 -lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   2.248 -by (induct rule: le_list_induct) (auto intro: drop)
   2.249 -
   2.250 -lemma le_list_filter_left[simp]: "filter f xs \<le> xs"
   2.251 -by (induct xs) (auto intro: drop)
   2.252 -
   2.253 -lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
   2.254 -by (induct rule: le_list_induct) (auto intro: drop)
   2.255 -
   2.256 -lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
   2.257 -proof
   2.258 -  assume ?L
   2.259 -  thus ?R
   2.260 -  proof (induct rule: le_list_induct)
   2.261 -    case empty show ?case by (metis sublist_empty)
   2.262 -  next
   2.263 -    case (drop xs ys x)
   2.264 -    then obtain N where "xs = sublist ys N" by blast
   2.265 -    hence "xs = sublist (x#ys) (Suc ` N)"
   2.266 -      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   2.267 -    thus ?case by blast
   2.268 -  next
   2.269 -    case (take x y xs ys)
   2.270 -    then obtain N where "xs = sublist ys N" by blast
   2.271 -    hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   2.272 -      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   2.273 -    thus ?case unfolding `x = y` by blast
   2.274 -  qed
   2.275 -next
   2.276 -  assume ?R
   2.277 -  then obtain N where "xs = sublist ys N" ..
   2.278 -  moreover have "sublist ys N <= ys"
   2.279 -  proof (induct ys arbitrary:N)
   2.280 -    case Nil show ?case by simp
   2.281 -  next
   2.282 -    case Cons thus ?case by (auto simp add:sublist_Cons drop)
   2.283 -  qed
   2.284 -  ultimately show ?L by simp
   2.285 -qed
   2.286 +  by (unfold less_le less_eq_list_def) auto
   2.287  
   2.288  end