1.1 --- a/src/HOL/Library/Sublist.thy	Wed Jul 02 17:34:45 2014 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Thu Jul 03 09:55:15 2014 +0200
     1.3 @@ -428,115 +428,115 @@
     1.4  
     1.5  subsection {* Homeomorphic embedding on lists *}
     1.6  
     1.7 -inductive list_hembeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
     1.8 +inductive list_emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
     1.9    for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
    1.10  where
    1.11 -  list_hembeq_Nil [intro, simp]: "list_hembeq P [] ys"
    1.12 -| list_hembeq_Cons [intro] : "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (y#ys)"
    1.13 -| list_hembeq_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_hembeq P xs ys \<Longrightarrow> list_hembeq P (x#xs) (y#ys)"
    1.14 +  list_emb_Nil [intro, simp]: "list_emb P [] ys"
    1.15 +| list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)"
    1.16 +| list_emb_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
    1.17  
    1.18 -lemma list_hembeq_Nil2 [simp]:
    1.19 -  assumes "list_hembeq P xs []" shows "xs = []"
    1.20 -  using assms by (cases rule: list_hembeq.cases) auto
    1.21 +lemma list_emb_Nil2 [simp]:
    1.22 +  assumes "list_emb P xs []" shows "xs = []"
    1.23 +  using assms by (cases rule: list_emb.cases) auto
    1.24  
    1.25 -lemma list_hembeq_refl [simp, intro!]:
    1.26 -  "list_hembeq P xs xs"
    1.27 +lemma list_emb_refl [simp, intro!]:
    1.28 +  "list_emb P xs xs"
    1.29    by (induct xs) auto
    1.30  
    1.31 -lemma list_hembeq_Cons_Nil [simp]: "list_hembeq P (x#xs) [] = False"
    1.32 +lemma list_emb_Cons_Nil [simp]: "list_emb P (x#xs) [] = False"
    1.33  proof -
    1.34 -  { assume "list_hembeq P (x#xs) []"
    1.35 -    from list_hembeq_Nil2 [OF this] have False by simp
    1.36 +  { assume "list_emb P (x#xs) []"
    1.37 +    from list_emb_Nil2 [OF this] have False by simp
    1.38    } moreover {
    1.39      assume False
    1.40 -    then have "list_hembeq P (x#xs) []" by simp
    1.41 +    then have "list_emb P (x#xs) []" by simp
    1.42    } ultimately show ?thesis by blast
    1.43  qed
    1.44  
    1.45 -lemma list_hembeq_append2 [intro]: "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (zs @ ys)"
    1.46 +lemma list_emb_append2 [intro]: "list_emb P xs ys \<Longrightarrow> list_emb P xs (zs @ ys)"
    1.47    by (induct zs) auto
    1.48  
    1.49 -lemma list_hembeq_prefix [intro]:
    1.50 -  assumes "list_hembeq P xs ys" shows "list_hembeq P xs (ys @ zs)"
    1.51 +lemma list_emb_prefix [intro]:
    1.52 +  assumes "list_emb P xs ys" shows "list_emb P xs (ys @ zs)"
    1.53    using assms
    1.54    by (induct arbitrary: zs) auto
    1.55  
    1.56 -lemma list_hembeq_ConsD:
    1.57 -  assumes "list_hembeq P (x#xs) ys"
    1.58 -  shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_hembeq P xs vs"
    1.59 +lemma list_emb_ConsD:
    1.60 +  assumes "list_emb P (x#xs) ys"
    1.61 +  shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_emb P xs vs"
    1.62  using assms
    1.63  proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
    1.64 -  case list_hembeq_Cons
    1.65 +  case list_emb_Cons
    1.66    then show ?case by (metis append_Cons)
    1.67  next
    1.68 -  case (list_hembeq_Cons2 x y xs ys)
    1.69 +  case (list_emb_Cons2 x y xs ys)
    1.70    then show ?case by blast
    1.71  qed
    1.72  
    1.73 -lemma list_hembeq_appendD:
    1.74 -  assumes "list_hembeq P (xs @ ys) zs"
    1.75 -  shows "\<exists>us vs. zs = us @ vs \<and> list_hembeq P xs us \<and> list_hembeq P ys vs"
    1.76 +lemma list_emb_appendD:
    1.77 +  assumes "list_emb P (xs @ ys) zs"
    1.78 +  shows "\<exists>us vs. zs = us @ vs \<and> list_emb P xs us \<and> list_emb P ys vs"
    1.79  using assms
    1.80  proof (induction xs arbitrary: ys zs)
    1.81    case Nil then show ?case by auto
    1.82  next
    1.83    case (Cons x xs)
    1.84    then obtain us v vs where
    1.85 -    zs: "zs = us @ v # vs" and p: "P\<^sup>=\<^sup>= x v" and lh: "list_hembeq P (xs @ ys) vs"
    1.86 -    by (auto dest: list_hembeq_ConsD)
    1.87 +    zs: "zs = us @ v # vs" and p: "P\<^sup>=\<^sup>= x v" and lh: "list_emb P (xs @ ys) vs"
    1.88 +    by (auto dest: list_emb_ConsD)
    1.89    obtain sk\<^sub>0 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" and sk\<^sub>1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.90 -    sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_hembeq P (xs @ x\<^sub>0) x\<^sub>1 \<or> sk\<^sub>0 x\<^sub>0 x\<^sub>1 @ sk\<^sub>1 x\<^sub>0 x\<^sub>1 = x\<^sub>1 \<and> list_hembeq P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_hembeq P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)"
    1.91 +    sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_emb P (xs @ x\<^sub>0) x\<^sub>1 \<or> sk\<^sub>0 x\<^sub>0 x\<^sub>1 @ sk\<^sub>1 x\<^sub>0 x\<^sub>1 = x\<^sub>1 \<and> list_emb P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_emb P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)"
    1.92      using Cons(1) by (metis (no_types))
    1.93 -  hence "\<forall>x\<^sub>2. list_hembeq P (x # xs) (x\<^sub>2 @ v # sk\<^sub>0 ys vs)" using p lh by auto
    1.94 +  hence "\<forall>x\<^sub>2. list_emb P (x # xs) (x\<^sub>2 @ v # sk\<^sub>0 ys vs)" using p lh by auto
    1.95    thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc)
    1.96  qed
    1.97  
    1.98 -lemma list_hembeq_suffix:
    1.99 -  assumes "list_hembeq P xs ys" and "suffix ys zs"
   1.100 -  shows "list_hembeq P xs zs"
   1.101 -  using assms(2) and list_hembeq_append2 [OF assms(1)] by (auto simp: suffix_def)
   1.102 +lemma list_emb_suffix:
   1.103 +  assumes "list_emb P xs ys" and "suffix ys zs"
   1.104 +  shows "list_emb P xs zs"
   1.105 +  using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: suffix_def)
   1.106  
   1.107 -lemma list_hembeq_suffixeq:
   1.108 -  assumes "list_hembeq P xs ys" and "suffixeq ys zs"
   1.109 -  shows "list_hembeq P xs zs"
   1.110 -  using assms and list_hembeq_suffix unfolding suffixeq_suffix_reflclp_conv by auto
   1.111 +lemma list_emb_suffixeq:
   1.112 +  assumes "list_emb P xs ys" and "suffixeq ys zs"
   1.113 +  shows "list_emb P xs zs"
   1.114 +  using assms and list_emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto
   1.115  
   1.116 -lemma list_hembeq_length: "list_hembeq P xs ys \<Longrightarrow> length xs \<le> length ys"
   1.117 -  by (induct rule: list_hembeq.induct) auto
   1.118 +lemma list_emb_length: "list_emb P xs ys \<Longrightarrow> length xs \<le> length ys"
   1.119 +  by (induct rule: list_emb.induct) auto
   1.120  
   1.121 -lemma list_hembeq_trans:
   1.122 +lemma list_emb_trans:
   1.123    assumes "\<And>x y z. \<lbrakk>x \<in> A; y \<in> A; z \<in> A; P x y; P y z\<rbrakk> \<Longrightarrow> P x z"
   1.124    shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A;
   1.125 -    list_hembeq P xs ys; list_hembeq P ys zs\<rbrakk> \<Longrightarrow> list_hembeq P xs zs"
   1.126 +    list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs"
   1.127  proof -
   1.128    fix xs ys zs
   1.129 -  assume "list_hembeq P xs ys" and "list_hembeq P ys zs"
   1.130 +  assume "list_emb P xs ys" and "list_emb P ys zs"
   1.131      and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
   1.132 -  then show "list_hembeq P xs zs"
   1.133 +  then show "list_emb P xs zs"
   1.134    proof (induction arbitrary: zs)
   1.135 -    case list_hembeq_Nil show ?case by blast
   1.136 +    case list_emb_Nil show ?case by blast
   1.137    next
   1.138 -    case (list_hembeq_Cons xs ys y)
   1.139 -    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
   1.140 -      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
   1.141 -    then have "list_hembeq P ys (v#vs)" by blast
   1.142 -    then have "list_hembeq P ys zs" unfolding zs by (rule list_hembeq_append2)
   1.143 -    from list_hembeq_Cons.IH [OF this] and list_hembeq_Cons.prems show ?case by simp
   1.144 +    case (list_emb_Cons xs ys y)
   1.145 +    from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
   1.146 +      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
   1.147 +    then have "list_emb P ys (v#vs)" by blast
   1.148 +    then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2)
   1.149 +    from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by simp
   1.150    next
   1.151 -    case (list_hembeq_Cons2 x y xs ys)
   1.152 -    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
   1.153 -      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
   1.154 -    with list_hembeq_Cons2 have "list_hembeq P xs vs" by simp
   1.155 +    case (list_emb_Cons2 x y xs ys)
   1.156 +    from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
   1.157 +      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
   1.158 +    with list_emb_Cons2 have "list_emb P xs vs" by simp
   1.159      moreover have "P\<^sup>=\<^sup>= x v"
   1.160      proof -
   1.161        from zs and `zs \<in> lists A` have "v \<in> A" by auto
   1.162 -      moreover have "x \<in> A" and "y \<in> A" using list_hembeq_Cons2 by simp_all
   1.163 +      moreover have "x \<in> A" and "y \<in> A" using list_emb_Cons2 by simp_all
   1.164        ultimately show ?thesis
   1.165          using `P\<^sup>=\<^sup>= x y` and `P\<^sup>=\<^sup>= y v` and assms
   1.166          by blast
   1.167      qed
   1.168 -    ultimately have "list_hembeq P (x#xs) (v#vs)" by blast
   1.169 -    then show ?case unfolding zs by (rule list_hembeq_append2)
   1.170 +    ultimately have "list_emb P (x#xs) (v#vs)" by blast
   1.171 +    then show ?case unfolding zs by (rule list_emb_append2)
   1.172    qed
   1.173  qed
   1.174  
   1.175 @@ -544,24 +544,24 @@
   1.176  subsection {* Sublists (special case of homeomorphic embedding) *}
   1.177  
   1.178  abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   1.179 -  where "sublisteq xs ys \<equiv> list_hembeq (op =) xs ys"
   1.180 +  where "sublisteq xs ys \<equiv> list_emb (op =) xs ys"
   1.181  
   1.182  lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
   1.183  
   1.184  lemma sublisteq_same_length:
   1.185    assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys"
   1.186 -  using assms by (induct) (auto dest: list_hembeq_length)
   1.187 +  using assms by (induct) (auto dest: list_emb_length)
   1.188  
   1.189  lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
   1.190 -  by (metis list_hembeq_length linorder_not_less)
   1.191 +  by (metis list_emb_length linorder_not_less)
   1.192  
   1.193  lemma [code]:
   1.194 -  "list_hembeq P [] ys \<longleftrightarrow> True"
   1.195 -  "list_hembeq P (x#xs) [] \<longleftrightarrow> False"
   1.196 +  "list_emb P [] ys \<longleftrightarrow> True"
   1.197 +  "list_emb P (x#xs) [] \<longleftrightarrow> False"
   1.198    by (simp_all)
   1.199  
   1.200  lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
   1.201 -  by (induct xs, simp, blast dest: list_hembeq_ConsD)
   1.202 +  by (induct xs, simp, blast dest: list_emb_ConsD)
   1.203  
   1.204  lemma sublisteq_Cons2':
   1.205    assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
   1.206 @@ -574,7 +574,7 @@
   1.207  
   1.208  lemma sublisteq_Cons2_iff [simp, code]:
   1.209    "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"
   1.210 -  by (metis list_hembeq_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)
   1.211 +  by (metis list_emb_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)
   1.212  
   1.213  lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
   1.214    by (induct zs) simp_all
   1.215 @@ -586,29 +586,29 @@
   1.216    shows "xs = ys"
   1.217  using assms
   1.218  proof (induct)
   1.219 -  case list_hembeq_Nil
   1.220 -  from list_hembeq_Nil2 [OF this] show ?case by simp
   1.221 +  case list_emb_Nil
   1.222 +  from list_emb_Nil2 [OF this] show ?case by simp
   1.223  next
   1.224 -  case list_hembeq_Cons2
   1.225 +  case list_emb_Cons2
   1.226    thus ?case by simp
   1.227  next
   1.228 -  case list_hembeq_Cons
   1.229 +  case list_emb_Cons
   1.230    hence False using sublisteq_Cons' by fastforce
   1.231    thus ?case ..
   1.232  qed
   1.233  
   1.234  lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
   1.235 -  by (rule list_hembeq_trans [of UNIV "op ="]) auto
   1.236 +  by (rule list_emb_trans [of UNIV "op ="]) auto
   1.237  
   1.238  lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
   1.239 -  by (auto dest: list_hembeq_length)
   1.240 +  by (auto dest: list_emb_length)
   1.241  
   1.242 -lemma list_hembeq_append_mono:
   1.243 -  "\<lbrakk> list_hembeq P xs xs'; list_hembeq P ys ys' \<rbrakk> \<Longrightarrow> list_hembeq P (xs@ys) (xs'@ys')"
   1.244 -  apply (induct rule: list_hembeq.induct)
   1.245 -    apply (metis eq_Nil_appendI list_hembeq_append2)
   1.246 -   apply (metis append_Cons list_hembeq_Cons)
   1.247 -  apply (metis append_Cons list_hembeq_Cons2)
   1.248 +lemma list_emb_append_mono:
   1.249 +  "\<lbrakk> list_emb P xs xs'; list_emb P ys ys' \<rbrakk> \<Longrightarrow> list_emb P (xs@ys) (xs'@ys')"
   1.250 +  apply (induct rule: list_emb.induct)
   1.251 +    apply (metis eq_Nil_appendI list_emb_append2)
   1.252 +   apply (metis append_Cons list_emb_Cons)
   1.253 +  apply (metis append_Cons list_emb_Cons2)
   1.254    done
   1.255  
   1.256  
   1.257 @@ -620,34 +620,34 @@
   1.258    { fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'"
   1.259      then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys"
   1.260      proof (induct arbitrary: xs ys zs)
   1.261 -      case list_hembeq_Nil show ?case by simp
   1.262 +      case list_emb_Nil show ?case by simp
   1.263      next
   1.264 -      case (list_hembeq_Cons xs' ys' x)
   1.265 -      { assume "ys=[]" then have ?case using list_hembeq_Cons(1) by auto }
   1.266 +      case (list_emb_Cons xs' ys' x)
   1.267 +      { assume "ys=[]" then have ?case using list_emb_Cons(1) by auto }
   1.268        moreover
   1.269        { fix us assume "ys = x#us"
   1.270 -        then have ?case using list_hembeq_Cons(2) by(simp add: list_hembeq.list_hembeq_Cons) }
   1.271 +        then have ?case using list_emb_Cons(2) by(simp add: list_emb.list_emb_Cons) }
   1.272        ultimately show ?case by (auto simp:Cons_eq_append_conv)
   1.273      next
   1.274 -      case (list_hembeq_Cons2 x y xs' ys')
   1.275 -      { assume "xs=[]" then have ?case using list_hembeq_Cons2(1) by auto }
   1.276 +      case (list_emb_Cons2 x y xs' ys')
   1.277 +      { assume "xs=[]" then have ?case using list_emb_Cons2(1) by auto }
   1.278        moreover
   1.279 -      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_hembeq_Cons2 by auto}
   1.280 +      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_emb_Cons2 by auto}
   1.281        moreover
   1.282 -      { fix us assume "xs=x#us" "ys=[]" then have ?case using list_hembeq_Cons2(2) by bestsimp }
   1.283 +      { fix us assume "xs=x#us" "ys=[]" then have ?case using list_emb_Cons2(2) by bestsimp }
   1.284        ultimately show ?case using `op =\<^sup>=\<^sup>= x y` by (auto simp: Cons_eq_append_conv)
   1.285      qed }
   1.286    moreover assume ?l
   1.287    ultimately show ?r by blast
   1.288  next
   1.289 -  assume ?r then show ?l by (metis list_hembeq_append_mono sublisteq_refl)
   1.290 +  assume ?r then show ?l by (metis list_emb_append_mono sublisteq_refl)
   1.291  qed
   1.292  
   1.293  lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
   1.294    by (induct zs) auto
   1.295  
   1.296  lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"
   1.297 -  by (metis append_Nil2 list_hembeq_Nil list_hembeq_append_mono)
   1.298 +  by (metis append_Nil2 list_emb_Nil list_emb_append_mono)
   1.299  
   1.300  
   1.301  subsection {* Relation to standard list operations *}
   1.302 @@ -668,19 +668,19 @@
   1.303    assume ?L
   1.304    then show ?R
   1.305    proof (induct)
   1.306 -    case list_hembeq_Nil show ?case by (metis sublist_empty)
   1.307 +    case list_emb_Nil show ?case by (metis sublist_empty)
   1.308    next
   1.309 -    case (list_hembeq_Cons xs ys x)
   1.310 +    case (list_emb_Cons xs ys x)
   1.311      then obtain N where "xs = sublist ys N" by blast
   1.312      then have "xs = sublist (x#ys) (Suc ` N)"
   1.313        by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.314      then show ?case by blast
   1.315    next
   1.316 -    case (list_hembeq_Cons2 x y xs ys)
   1.317 +    case (list_emb_Cons2 x y xs ys)
   1.318      then obtain N where "xs = sublist ys N" by blast
   1.319      then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   1.320        by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   1.321 -    moreover from list_hembeq_Cons2 have "x = y" by simp
   1.322 +    moreover from list_emb_Cons2 have "x = y" by simp
   1.323      ultimately show ?case by blast
   1.324    qed
   1.325  next

     2.1 --- a/src/HOL/Library/Sublist_Order.thy	Wed Jul 02 17:34:45 2014 +0200
     2.2 +++ b/src/HOL/Library/Sublist_Order.thy	Thu Jul 03 09:55:15 2014 +0200
     2.3 @@ -48,21 +48,21 @@
     2.4  qed
     2.5  
     2.6  lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
     2.7 -  list_hembeq.induct [of "op =", folded less_eq_list_def]
     2.8 -lemmas less_eq_list_drop = list_hembeq.list_hembeq_Cons [of "op =", folded less_eq_list_def]
     2.9 +  list_emb.induct [of "op =", folded less_eq_list_def]
    2.10 +lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def]
    2.11  lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
    2.12  lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
    2.13  lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
    2.14 -lemmas le_list_length = list_hembeq_length [of "op =", folded less_eq_list_def]
    2.15 +lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
    2.16  
    2.17  lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
    2.18 -  by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
    2.19 +  by (metis list_emb_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
    2.20  
    2.21  lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
    2.22 -  by (metis less_eq_list_def list_hembeq_Nil order_less_le)
    2.23 +  by (metis less_eq_list_def list_emb_Nil order_less_le)
    2.24  
    2.25  lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
    2.26 -  by (metis list_hembeq_Nil less_eq_list_def less_list_def)
    2.27 +  by (metis list_emb_Nil less_eq_list_def less_list_def)
    2.28  
    2.29  lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
    2.30    by (unfold less_le less_eq_list_def) (auto)