renamed "emb" to "list_hembeq";
authorChristian Sternagel
Thu Dec 13 13:11:38 2012 +0100 (2012-12-13)
changeset 50516ed6b40d15d1c
parent 50515 c4a27ab89c9b
child 50517 8f6c11103820
renamed "emb" to "list_hembeq";
make "list_hembeq" reflexive independent of the base order;
renamed "sub" to "sublisteq";
dropped "transp_on" (state transitivity explicitly instead);
no need to hide "sub" after renaming;
replaced some ASCII symbols by proper Isabelle symbols;
NEWS
NEWS
src/HOL/BNF/Examples/TreeFI.thy
src/HOL/BNF/Examples/TreeFsetI.thy
src/HOL/Library/Sublist.thy
src/HOL/Library/Sublist_Order.thy
     1.1 --- a/NEWS	Thu Dec 13 09:21:45 2012 +0100
     1.2 +++ b/NEWS	Thu Dec 13 13:11:38 2012 +0100
     1.3 @@ -173,8 +173,8 @@
     1.4      syntax "xs >>= ys"; use "suffixeq ys xs" instead.  Renamed lemmas
     1.5      accordingly.  INCOMPATIBILITY.
     1.6  
     1.7 -  - New constant "emb" for homeomorphic embedding on lists. New
     1.8 -    abbreviation "sub" for special case "emb (op =)".
     1.9 +  - New constant "list_hembeq" for homeomorphic embedding on lists. New
    1.10 +    abbreviation "sublisteq" for special case "list_hembeq (op =)".
    1.11  
    1.12    - Library/Sublist does no longer provide "order" and "bot" type class
    1.13      instances for the prefix order (merely corresponding locale
    1.14 @@ -182,24 +182,24 @@
    1.15      Library/Prefix_Order. INCOMPATIBILITY.
    1.16  
    1.17    - The sublist relation from Library/Sublist_Order is now based on
    1.18 -    "Sublist.sub". Replaced lemmas:
    1.19 -
    1.20 -      le_list_append_le_same_iff ~> Sublist.sub_append_le_same_iff
    1.21 -      le_list_append_mono ~> Sublist.emb_append_mono
    1.22 -      le_list_below_empty ~> Sublist.emb_Nil, Sublist.emb_Nil2
    1.23 -      le_list_Cons_EX ~> Sublist.emb_ConsD
    1.24 -      le_list_drop_Cons2 ~> Sublist.sub_Cons2'
    1.25 -      le_list_drop_Cons_neq ~> Sublist.sub_Cons2_neq
    1.26 -      le_list_drop_Cons ~> Sublist.sub_Cons'
    1.27 -      le_list_drop_many ~> Sublist.sub_drop_many
    1.28 -      le_list_filter_left ~> Sublist.sub_filter_left
    1.29 -      le_list_rev_drop_many ~> Sublist.sub_rev_drop_many
    1.30 -      le_list_rev_take_iff ~> Sublist.sub_append
    1.31 -      le_list_same_length ~> Sublist.sub_same_length
    1.32 -      le_list_take_many_iff ~> Sublist.sub_append'
    1.33 +    "Sublist.sublisteq". Replaced lemmas:
    1.34 +
    1.35 +      le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
    1.36 +      le_list_append_mono ~> Sublist.list_hembeq_append_mono
    1.37 +      le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2
    1.38 +      le_list_Cons_EX ~> Sublist.list_hembeq_ConsD
    1.39 +      le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'
    1.40 +      le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq
    1.41 +      le_list_drop_Cons ~> Sublist.sublisteq_Cons'
    1.42 +      le_list_drop_many ~> Sublist.sublisteq_drop_many
    1.43 +      le_list_filter_left ~> Sublist.sublisteq_filter_left
    1.44 +      le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many
    1.45 +      le_list_rev_take_iff ~> Sublist.sublisteq_append
    1.46 +      le_list_same_length ~> Sublist.sublisteq_same_length
    1.47 +      le_list_take_many_iff ~> Sublist.sublisteq_append'
    1.48        less_eq_list.drop ~> less_eq_list_drop
    1.49        less_eq_list.induct ~> less_eq_list_induct
    1.50 -      not_le_list_length ~> Sublist.not_sub_length
    1.51 +      not_le_list_length ~> Sublist.not_sublisteq_length
    1.52  
    1.53      INCOMPATIBILITY.
    1.54  
     2.1 --- a/src/HOL/BNF/Examples/TreeFI.thy	Thu Dec 13 09:21:45 2012 +0100
     2.2 +++ b/src/HOL/BNF/Examples/TreeFI.thy	Thu Dec 13 13:11:38 2012 +0100
     2.3 @@ -12,8 +12,6 @@
     2.4  imports ListF
     2.5  begin
     2.6  
     2.7 -hide_const (open) Sublist.sub
     2.8 -
     2.9  codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
    2.10  
    2.11  lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
     3.1 --- a/src/HOL/BNF/Examples/TreeFsetI.thy	Thu Dec 13 09:21:45 2012 +0100
     3.2 +++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Thu Dec 13 13:11:38 2012 +0100
     3.3 @@ -12,7 +12,6 @@
     3.4  imports "../BNF"
     3.5  begin
     3.6  
     3.7 -hide_const (open) Sublist.sub
     3.8  hide_fact (open) Quotient_Product.prod_rel_def
     3.9  
    3.10  codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
     4.1 --- a/src/HOL/Library/Sublist.thy	Thu Dec 13 09:21:45 2012 +0100
     4.2 +++ b/src/HOL/Library/Sublist.thy	Thu Dec 13 13:11:38 2012 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     Christian Sternagel, JAIST
     4.5  *)
     4.6  
     4.7 -header {* List prefixes, suffixes, and embedding*}
     4.8 +header {* List prefixes, suffixes, and homeomorphic embedding *}
     4.9  
    4.10  theory Sublist
    4.11  imports Main
    4.12 @@ -11,10 +11,10 @@
    4.13  
    4.14  subsection {* Prefix order on lists *}
    4.15  
    4.16 -definition prefixeq :: "'a list => 'a list => bool"
    4.17 +definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    4.18    where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    4.19  
    4.20 -definition prefix :: "'a list => 'a list => bool"
    4.21 +definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    4.22    where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    4.23  
    4.24  interpretation prefix_order: order prefixeq prefix
    4.25 @@ -23,7 +23,7 @@
    4.26  interpretation prefix_bot: bot prefixeq prefix Nil
    4.27    by default (simp add: prefixeq_def)
    4.28  
    4.29 -lemma prefixeqI [intro?]: "ys = xs @ zs ==> prefixeq xs ys"
    4.30 +lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
    4.31    unfolding prefixeq_def by blast
    4.32  
    4.33  lemma prefixeqE [elim?]:
    4.34 @@ -31,7 +31,7 @@
    4.35    obtains zs where "ys = xs @ zs"
    4.36    using assms unfolding prefixeq_def by blast
    4.37  
    4.38 -lemma prefixI' [intro?]: "ys = xs @ z # zs ==> prefix xs ys"
    4.39 +lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
    4.40    unfolding prefix_def prefixeq_def by blast
    4.41  
    4.42  lemma prefixE' [elim?]:
    4.43 @@ -43,7 +43,7 @@
    4.44    with that show ?thesis by (auto simp add: neq_Nil_conv)
    4.45  qed
    4.46  
    4.47 -lemma prefixI [intro?]: "prefixeq xs ys ==> xs \<noteq> ys ==> prefix xs ys"
    4.48 +lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
    4.49    unfolding prefix_def by blast
    4.50  
    4.51  lemma prefixE [elim?]:
    4.52 @@ -88,7 +88,7 @@
    4.53  lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
    4.54    by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
    4.55  
    4.56 -lemma prefixeq_prefixeq [simp]: "prefixeq xs ys ==> prefixeq xs (ys @ zs)"
    4.57 +lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
    4.58    by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
    4.59  
    4.60  lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
    4.61 @@ -106,12 +106,12 @@
    4.62    done
    4.63  
    4.64  lemma append_one_prefixeq:
    4.65 -  "prefixeq xs ys ==> length xs < length ys ==> prefixeq (xs @ [ys ! length xs]) ys"
    4.66 +  "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
    4.67    unfolding prefixeq_def
    4.68    by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj
    4.69      eq_Nil_appendI nth_drop')
    4.70  
    4.71 -theorem prefixeq_length_le: "prefixeq xs ys ==> length xs \<le> length ys"
    4.72 +theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
    4.73    by (auto simp add: prefixeq_def)
    4.74  
    4.75  lemma prefixeq_same_cases:
    4.76 @@ -191,10 +191,10 @@
    4.77  
    4.78  subsection {* Parallel lists *}
    4.79  
    4.80 -definition parallel :: "'a list => 'a list => bool"  (infixl "\<parallel>" 50)
    4.81 +definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)
    4.82    where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
    4.83  
    4.84 -lemma parallelI [intro]: "\<not> prefixeq xs ys ==> \<not> prefixeq ys xs ==> xs \<parallel> ys"
    4.85 +lemma parallelI [intro]: "\<not> prefixeq xs ys \<Longrightarrow> \<not> prefixeq ys xs \<Longrightarrow> xs \<parallel> ys"
    4.86    unfolding parallel_def by blast
    4.87  
    4.88  lemma parallelE [elim]:
    4.89 @@ -207,7 +207,7 @@
    4.90    unfolding parallel_def prefix_def by blast
    4.91  
    4.92  theorem parallel_decomp:
    4.93 -  "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
    4.94 +  "xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
    4.95  proof (induct xs rule: rev_induct)
    4.96    case Nil
    4.97    then have False by auto
    4.98 @@ -268,7 +268,7 @@
    4.99    "suffix xs ys \<Longrightarrow> suffixeq xs ys"
   4.100    by (auto simp: suffixeq_def suffix_def)
   4.101  
   4.102 -lemma suffixeqI [intro?]: "ys = zs @ xs ==> suffixeq xs ys"
   4.103 +lemma suffixeqI [intro?]: "ys = zs @ xs \<Longrightarrow> suffixeq xs ys"
   4.104    unfolding suffixeq_def by blast
   4.105  
   4.106  lemma suffixeqE [elim?]:
   4.107 @@ -420,268 +420,262 @@
   4.108    unfolding suffix_def by auto
   4.109  
   4.110  
   4.111 -subsection {* Embedding on lists *}
   4.112 +subsection {* Homeomorphic embedding on lists *}
   4.113  
   4.114 -inductive emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   4.115 +inductive list_hembeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   4.116    for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
   4.117  where
   4.118 -  emb_Nil [intro, simp]: "emb P [] ys"
   4.119 -| emb_Cons [intro] : "emb P xs ys \<Longrightarrow> emb P xs (y#ys)"
   4.120 -| emb_Cons2 [intro]: "P x y \<Longrightarrow> emb P xs ys \<Longrightarrow> emb P (x#xs) (y#ys)"
   4.121 +  list_hembeq_Nil [intro, simp]: "list_hembeq P [] ys"
   4.122 +| list_hembeq_Cons [intro] : "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (y#ys)"
   4.123 +| list_hembeq_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_hembeq P xs ys \<Longrightarrow> list_hembeq P (x#xs) (y#ys)"
   4.124 +
   4.125 +lemma list_hembeq_Nil2 [simp]:
   4.126 +  assumes "list_hembeq P xs []" shows "xs = []"
   4.127 +  using assms by (cases rule: list_hembeq.cases) auto
   4.128  
   4.129 -lemma emb_Nil2 [simp]:
   4.130 -  assumes "emb P xs []" shows "xs = []"
   4.131 -  using assms by (cases rule: emb.cases) auto
   4.132 +lemma list_hembeq_refl [simp, intro!]:
   4.133 +  "list_hembeq P xs xs"
   4.134 +  by (induct xs) auto
   4.135  
   4.136 -lemma emb_Cons_Nil [simp]: "emb P (x#xs) [] = False"
   4.137 +lemma list_hembeq_Cons_Nil [simp]: "list_hembeq P (x#xs) [] = False"
   4.138  proof -
   4.139 -  { assume "emb P (x#xs) []"
   4.140 -    from emb_Nil2 [OF this] have False by simp
   4.141 +  { assume "list_hembeq P (x#xs) []"
   4.142 +    from list_hembeq_Nil2 [OF this] have False by simp
   4.143    } moreover {
   4.144      assume False
   4.145 -    then have "emb P (x#xs) []" by simp
   4.146 +    then have "list_hembeq P (x#xs) []" by simp
   4.147    } ultimately show ?thesis by blast
   4.148  qed
   4.149  
   4.150 -lemma emb_append2 [intro]: "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)"
   4.151 +lemma list_hembeq_append2 [intro]: "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (zs @ ys)"
   4.152    by (induct zs) auto
   4.153  
   4.154 -lemma emb_prefix [intro]:
   4.155 -  assumes "emb P xs ys" shows "emb P xs (ys @ zs)"
   4.156 +lemma list_hembeq_prefix [intro]:
   4.157 +  assumes "list_hembeq P xs ys" shows "list_hembeq P xs (ys @ zs)"
   4.158    using assms
   4.159    by (induct arbitrary: zs) auto
   4.160  
   4.161 -lemma emb_ConsD:
   4.162 -  assumes "emb P (x#xs) ys"
   4.163 -  shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> emb P xs vs"
   4.164 +lemma list_hembeq_ConsD:
   4.165 +  assumes "list_hembeq P (x#xs) ys"
   4.166 +  shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_hembeq P xs vs"
   4.167  using assms
   4.168  proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
   4.169 -  case emb_Cons
   4.170 +  case list_hembeq_Cons
   4.171    then show ?case by (metis append_Cons)
   4.172  next
   4.173 -  case (emb_Cons2 x y xs ys)
   4.174 +  case (list_hembeq_Cons2 x y xs ys)
   4.175    then show ?case by (cases xs) (auto, blast+)
   4.176  qed
   4.177  
   4.178 -lemma emb_appendD:
   4.179 -  assumes "emb P (xs @ ys) zs"
   4.180 -  shows "\<exists>us vs. zs = us @ vs \<and> emb P xs us \<and> emb P ys vs"
   4.181 +lemma list_hembeq_appendD:
   4.182 +  assumes "list_hembeq P (xs @ ys) zs"
   4.183 +  shows "\<exists>us vs. zs = us @ vs \<and> list_hembeq P xs us \<and> list_hembeq P ys vs"
   4.184  using assms
   4.185  proof (induction xs arbitrary: ys zs)
   4.186    case Nil then show ?case by auto
   4.187  next
   4.188    case (Cons x xs)
   4.189    then obtain us v vs where "zs = us @ v # vs"
   4.190 -    and "P x v" and "emb P (xs @ ys) vs" by (auto dest: emb_ConsD)
   4.191 -  with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2)
   4.192 +    and "P\<^sup>=\<^sup>= x v" and "list_hembeq P (xs @ ys) vs" by (auto dest: list_hembeq_ConsD)
   4.193 +  with Cons show ?case by (metis append_Cons append_assoc list_hembeq_Cons2 list_hembeq_append2)
   4.194  qed
   4.195  
   4.196 -lemma emb_suffix:
   4.197 -  assumes "emb P xs ys" and "suffix ys zs"
   4.198 -  shows "emb P xs zs"
   4.199 -  using assms(2) and emb_append2 [OF assms(1)] by (auto simp: suffix_def)
   4.200 -
   4.201 -lemma emb_suffixeq:
   4.202 -  assumes "emb P xs ys" and "suffixeq ys zs"
   4.203 -  shows "emb P xs zs"
   4.204 -  using assms and emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto
   4.205 +lemma list_hembeq_suffix:
   4.206 +  assumes "list_hembeq P xs ys" and "suffix ys zs"
   4.207 +  shows "list_hembeq P xs zs"
   4.208 +  using assms(2) and list_hembeq_append2 [OF assms(1)] by (auto simp: suffix_def)
   4.209  
   4.210 -lemma emb_length: "emb P xs ys \<Longrightarrow> length xs \<le> length ys"
   4.211 -  by (induct rule: emb.induct) auto
   4.212 +lemma list_hembeq_suffixeq:
   4.213 +  assumes "list_hembeq P xs ys" and "suffixeq ys zs"
   4.214 +  shows "list_hembeq P xs zs"
   4.215 +  using assms and list_hembeq_suffix unfolding suffixeq_suffix_reflclp_conv by auto
   4.216  
   4.217 -(*FIXME: move*)
   4.218 -definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   4.219 -  where "transp_on P A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c)"
   4.220 -lemma transp_onI [Pure.intro]:
   4.221 -  "(\<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"
   4.222 -  unfolding transp_on_def by blast
   4.223 +lemma list_hembeq_length: "list_hembeq P xs ys \<Longrightarrow> length xs \<le> length ys"
   4.224 +  by (induct rule: list_hembeq.induct) auto
   4.225  
   4.226 -lemma transp_on_emb:
   4.227 -  assumes "transp_on P A"
   4.228 -  shows "transp_on (emb P) (lists A)"
   4.229 -proof
   4.230 +lemma list_hembeq_trans:
   4.231 +  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"
   4.232 +  shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A;
   4.233 +    list_hembeq P xs ys; list_hembeq P ys zs\<rbrakk> \<Longrightarrow> list_hembeq P xs zs"
   4.234 +proof -
   4.235    fix xs ys zs
   4.236 -  assume "emb P xs ys" and "emb P ys zs"
   4.237 +  assume "list_hembeq P xs ys" and "list_hembeq P ys zs"
   4.238      and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
   4.239 -  then show "emb P xs zs"
   4.240 +  then show "list_hembeq P xs zs"
   4.241    proof (induction arbitrary: zs)
   4.242 -    case emb_Nil show ?case by blast
   4.243 +    case list_hembeq_Nil show ?case by blast
   4.244    next
   4.245 -    case (emb_Cons xs ys y)
   4.246 -    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
   4.247 -      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
   4.248 -    then have "emb P ys (v#vs)" by blast
   4.249 -    then have "emb P ys zs" unfolding zs by (rule emb_append2)
   4.250 -    from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp
   4.251 +    case (list_hembeq_Cons xs ys y)
   4.252 +    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
   4.253 +      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
   4.254 +    then have "list_hembeq P ys (v#vs)" by blast
   4.255 +    then have "list_hembeq P ys zs" unfolding zs by (rule list_hembeq_append2)
   4.256 +    from list_hembeq_Cons.IH [OF this] and list_hembeq_Cons.prems show ?case by simp
   4.257    next
   4.258 -    case (emb_Cons2 x y xs ys)
   4.259 -    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
   4.260 -      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
   4.261 -    with emb_Cons2 have "emb P xs vs" by simp
   4.262 -    moreover have "P x v"
   4.263 +    case (list_hembeq_Cons2 x y xs ys)
   4.264 +    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
   4.265 +      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
   4.266 +    with list_hembeq_Cons2 have "list_hembeq P xs vs" by simp
   4.267 +    moreover have "P\<^sup>=\<^sup>= x v"
   4.268      proof -
   4.269        from zs and `zs \<in> lists A` have "v \<in> A" by auto
   4.270 -      moreover have "x \<in> A" and "y \<in> A" using emb_Cons2 by simp_all
   4.271 -      ultimately show ?thesis using `P x y` and `P y v` and assms
   4.272 -        unfolding transp_on_def by blast
   4.273 +      moreover have "x \<in> A" and "y \<in> A" using list_hembeq_Cons2 by simp_all
   4.274 +      ultimately show ?thesis
   4.275 +        using `P\<^sup>=\<^sup>= x y` and `P\<^sup>=\<^sup>= y v` and assms
   4.276 +        by blast
   4.277      qed
   4.278 -    ultimately have "emb P (x#xs) (v#vs)" by blast
   4.279 -    then show ?case unfolding zs by (rule emb_append2)
   4.280 +    ultimately have "list_hembeq P (x#xs) (v#vs)" by blast
   4.281 +    then show ?case unfolding zs by (rule list_hembeq_append2)
   4.282    qed
   4.283  qed
   4.284  
   4.285  
   4.286 -subsection {* Sublists (special case of embedding) *}
   4.287 +subsection {* Sublists (special case of homeomorphic embedding) *}
   4.288  
   4.289 -abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   4.290 -  where "sub xs ys \<equiv> emb (op =) xs ys"
   4.291 +abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   4.292 +  where "sublisteq xs ys \<equiv> list_hembeq (op =) xs ys"
   4.293  
   4.294 -lemma sub_Cons2: "sub xs ys \<Longrightarrow> sub (x#xs) (x#ys)" by auto
   4.295 +lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
   4.296  
   4.297 -lemma sub_same_length:
   4.298 -  assumes "sub xs ys" and "length xs = length ys" shows "xs = ys"
   4.299 -  using assms by (induct) (auto dest: emb_length)
   4.300 +lemma sublisteq_same_length:
   4.301 +  assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys"
   4.302 +  using assms by (induct) (auto dest: list_hembeq_length)
   4.303  
   4.304 -lemma not_sub_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sub xs ys"
   4.305 -  by (metis emb_length linorder_not_less)
   4.306 +lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
   4.307 +  by (metis list_hembeq_length linorder_not_less)
   4.308  
   4.309  lemma [code]:
   4.310 -  "emb P [] ys \<longleftrightarrow> True"
   4.311 -  "emb P (x#xs) [] \<longleftrightarrow> False"
   4.312 +  "list_hembeq P [] ys \<longleftrightarrow> True"
   4.313 +  "list_hembeq P (x#xs) [] \<longleftrightarrow> False"
   4.314    by (simp_all)
   4.315  
   4.316 -lemma sub_Cons': "sub (x#xs) ys \<Longrightarrow> sub xs ys"
   4.317 -  by (induct xs) (auto dest: emb_ConsD)
   4.318 +lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
   4.319 +  by (induct xs) (auto dest: list_hembeq_ConsD)
   4.320  
   4.321 -lemma sub_Cons2':
   4.322 -  assumes "sub (x#xs) (x#ys)" shows "sub xs ys"
   4.323 -  using assms by (cases) (rule sub_Cons')
   4.324 +lemma sublisteq_Cons2':
   4.325 +  assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
   4.326 +  using assms by (cases) (rule sublisteq_Cons')
   4.327  
   4.328 -lemma sub_Cons2_neq:
   4.329 -  assumes "sub (x#xs) (y#ys)"
   4.330 -  shows "x \<noteq> y \<Longrightarrow> sub (x#xs) ys"
   4.331 +lemma sublisteq_Cons2_neq:
   4.332 +  assumes "sublisteq (x#xs) (y#ys)"
   4.333 +  shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys"
   4.334    using assms by (cases) auto
   4.335  
   4.336 -lemma sub_Cons2_iff [simp, code]:
   4.337 -  "sub (x#xs) (y#ys) = (if x = y then sub xs ys else sub (x#xs) ys)"
   4.338 -  by (metis emb_Cons emb_Cons2 [of "op =", OF refl] sub_Cons2' sub_Cons2_neq)
   4.339 +lemma sublisteq_Cons2_iff [simp, code]:
   4.340 +  "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"
   4.341 +  by (metis list_hembeq_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)
   4.342  
   4.343 -lemma sub_append': "sub (zs @ xs) (zs @ ys) \<longleftrightarrow> sub xs ys"
   4.344 +lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
   4.345    by (induct zs) simp_all
   4.346  
   4.347 -lemma sub_refl [simp, intro!]: "sub xs xs" by (induct xs) simp_all
   4.348 +lemma sublisteq_refl [simp, intro!]: "sublisteq xs xs" by (induct xs) simp_all
   4.349  
   4.350 -lemma sub_antisym:
   4.351 -  assumes "sub xs ys" and "sub ys xs"
   4.352 +lemma sublisteq_antisym:
   4.353 +  assumes "sublisteq xs ys" and "sublisteq ys xs"
   4.354    shows "xs = ys"
   4.355  using assms
   4.356  proof (induct)
   4.357 -  case emb_Nil
   4.358 -  from emb_Nil2 [OF this] show ?case by simp
   4.359 +  case list_hembeq_Nil
   4.360 +  from list_hembeq_Nil2 [OF this] show ?case by simp
   4.361  next
   4.362 -  case emb_Cons2
   4.363 +  case list_hembeq_Cons2
   4.364    then show ?case by simp
   4.365  next
   4.366 -  case emb_Cons
   4.367 +  case list_hembeq_Cons
   4.368    then show ?case
   4.369 -    by (metis sub_Cons' emb_length Suc_length_conv Suc_n_not_le_n)
   4.370 +    by (metis sublisteq_Cons' list_hembeq_length Suc_length_conv Suc_n_not_le_n)
   4.371  qed
   4.372  
   4.373 -lemma transp_on_sub: "transp_on sub UNIV"
   4.374 -proof -
   4.375 -  have "transp_on (op =) UNIV" by (simp add: transp_on_def)
   4.376 -  from transp_on_emb [OF this] show ?thesis by simp
   4.377 -qed
   4.378 +lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
   4.379 +  by (rule list_hembeq_trans [of UNIV "op ="]) auto
   4.380  
   4.381 -lemma sub_trans: "sub xs ys \<Longrightarrow> sub ys zs \<Longrightarrow> sub xs zs"
   4.382 -  using transp_on_sub [unfolded transp_on_def] by blast
   4.383 +lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
   4.384 +  by (auto dest: list_hembeq_length)
   4.385  
   4.386 -lemma sub_append_le_same_iff: "sub (xs @ ys) ys \<longleftrightarrow> xs = []"
   4.387 -  by (auto dest: emb_length)
   4.388 -
   4.389 -lemma emb_append_mono:
   4.390 -  "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> emb P (xs@ys) (xs'@ys')"
   4.391 -  apply (induct rule: emb.induct)
   4.392 -    apply (metis eq_Nil_appendI emb_append2)
   4.393 -   apply (metis append_Cons emb_Cons)
   4.394 -  apply (metis append_Cons emb_Cons2)
   4.395 +lemma list_hembeq_append_mono:
   4.396 +  "\<lbrakk> list_hembeq P xs xs'; list_hembeq P ys ys' \<rbrakk> \<Longrightarrow> list_hembeq P (xs@ys) (xs'@ys')"
   4.397 +  apply (induct rule: list_hembeq.induct)
   4.398 +    apply (metis eq_Nil_appendI list_hembeq_append2)
   4.399 +   apply (metis append_Cons list_hembeq_Cons)
   4.400 +  apply (metis append_Cons list_hembeq_Cons2)
   4.401    done
   4.402  
   4.403  
   4.404  subsection {* Appending elements *}
   4.405  
   4.406 -lemma sub_append [simp]:
   4.407 -  "sub (xs @ zs) (ys @ zs) \<longleftrightarrow> sub xs ys" (is "?l = ?r")
   4.408 +lemma sublisteq_append [simp]:
   4.409 +  "sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r")
   4.410  proof
   4.411 -  { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'"
   4.412 -    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys"
   4.413 +  { fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'"
   4.414 +    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys"
   4.415      proof (induct arbitrary: xs ys zs)
   4.416 -      case emb_Nil show ?case by simp
   4.417 +      case list_hembeq_Nil show ?case by simp
   4.418      next
   4.419 -      case (emb_Cons xs' ys' x)
   4.420 -      { assume "ys=[]" then have ?case using emb_Cons(1) by auto }
   4.421 +      case (list_hembeq_Cons xs' ys' x)
   4.422 +      { assume "ys=[]" then have ?case using list_hembeq_Cons(1) by auto }
   4.423        moreover
   4.424        { fix us assume "ys = x#us"
   4.425 -        then have ?case using emb_Cons(2) by(simp add: emb.emb_Cons) }
   4.426 +        then have ?case using list_hembeq_Cons(2) by(simp add: list_hembeq.list_hembeq_Cons) }
   4.427        ultimately show ?case by (auto simp:Cons_eq_append_conv)
   4.428      next
   4.429 -      case (emb_Cons2 x y xs' ys')
   4.430 -      { assume "xs=[]" then have ?case using emb_Cons2(1) by auto }
   4.431 +      case (list_hembeq_Cons2 x y xs' ys')
   4.432 +      { assume "xs=[]" then have ?case using list_hembeq_Cons2(1) by auto }
   4.433        moreover
   4.434 -      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using emb_Cons2 by auto}
   4.435 +      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_hembeq_Cons2 by auto}
   4.436        moreover
   4.437 -      { fix us assume "xs=x#us" "ys=[]" then have ?case using emb_Cons2(2) by bestsimp }
   4.438 -      ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv)
   4.439 +      { fix us assume "xs=x#us" "ys=[]" then have ?case using list_hembeq_Cons2(2) by bestsimp }
   4.440 +      ultimately show ?case using `op =\<^sup>=\<^sup>= x y` by (auto simp: Cons_eq_append_conv)
   4.441      qed }
   4.442    moreover assume ?l
   4.443    ultimately show ?r by blast
   4.444  next
   4.445 -  assume ?r then show ?l by (metis emb_append_mono sub_refl)
   4.446 +  assume ?r then show ?l by (metis list_hembeq_append_mono sublisteq_refl)
   4.447  qed
   4.448  
   4.449 -lemma sub_drop_many: "sub xs ys \<Longrightarrow> sub xs (zs @ ys)"
   4.450 +lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
   4.451    by (induct zs) auto
   4.452  
   4.453 -lemma sub_rev_drop_many: "sub xs ys \<Longrightarrow> sub xs (ys @ zs)"
   4.454 -  by (metis append_Nil2 emb_Nil emb_append_mono)
   4.455 +lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"
   4.456 +  by (metis append_Nil2 list_hembeq_Nil list_hembeq_append_mono)
   4.457  
   4.458  
   4.459  subsection {* Relation to standard list operations *}
   4.460  
   4.461 -lemma sub_map:
   4.462 -  assumes "sub xs ys" shows "sub (map f xs) (map f ys)"
   4.463 +lemma sublisteq_map:
   4.464 +  assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)"
   4.465    using assms by (induct) auto
   4.466  
   4.467 -lemma sub_filter_left [simp]: "sub (filter P xs) xs"
   4.468 +lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs"
   4.469    by (induct xs) auto
   4.470  
   4.471 -lemma sub_filter [simp]:
   4.472 -  assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)"
   4.473 +lemma sublisteq_filter [simp]:
   4.474 +  assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)"
   4.475    using assms by (induct) auto
   4.476  
   4.477 -lemma "sub xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
   4.478 +lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
   4.479  proof
   4.480    assume ?L
   4.481    then show ?R
   4.482    proof (induct)
   4.483 -    case emb_Nil show ?case by (metis sublist_empty)
   4.484 +    case list_hembeq_Nil show ?case by (metis sublist_empty)
   4.485    next
   4.486 -    case (emb_Cons xs ys x)
   4.487 +    case (list_hembeq_Cons xs ys x)
   4.488      then obtain N where "xs = sublist ys N" by blast
   4.489      then have "xs = sublist (x#ys) (Suc ` N)"
   4.490        by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   4.491      then show ?case by blast
   4.492    next
   4.493 -    case (emb_Cons2 x y xs ys)
   4.494 +    case (list_hembeq_Cons2 x y xs ys)
   4.495      then obtain N where "xs = sublist ys N" by blast
   4.496      then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   4.497        by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   4.498 -    then show ?case unfolding `x = y` by blast
   4.499 +    moreover from list_hembeq_Cons2 have "x = y" by simp
   4.500 +    ultimately show ?case by blast
   4.501    qed
   4.502  next
   4.503    assume ?R
   4.504    then obtain N where "xs = sublist ys N" ..
   4.505 -  moreover have "sub (sublist ys N) ys"
   4.506 +  moreover have "sublisteq (sublist ys N) ys"
   4.507    proof (induct ys arbitrary: N)
   4.508      case Nil show ?case by simp
   4.509    next
     5.1 --- a/src/HOL/Library/Sublist_Order.thy	Thu Dec 13 09:21:45 2012 +0100
     5.2 +++ b/src/HOL/Library/Sublist_Order.thy	Thu Dec 13 13:11:38 2012 +0100
     5.3 @@ -21,7 +21,7 @@
     5.4  begin
     5.5  
     5.6  definition
     5.7 -  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys"
     5.8 +  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
     5.9  
    5.10  definition
    5.11    "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    5.12 @@ -40,41 +40,41 @@
    5.13  next
    5.14    fix xs ys :: "'a list"
    5.15    assume "xs <= ys" and "ys <= xs"
    5.16 -  thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym)
    5.17 +  thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
    5.18  next
    5.19    fix xs ys zs :: "'a list"
    5.20    assume "xs <= ys" and "ys <= zs"
    5.21 -  thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
    5.22 +  thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
    5.23  qed
    5.24  
    5.25  lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
    5.26 -  emb.induct [of "op =", folded less_eq_list_def]
    5.27 -lemmas less_eq_list_drop = emb.emb_Cons [of "op =", folded less_eq_list_def]
    5.28 -lemmas le_list_Cons2_iff [simp, code] = sub_Cons2_iff [folded less_eq_list_def]
    5.29 -lemmas le_list_map = sub_map [folded less_eq_list_def]
    5.30 -lemmas le_list_filter = sub_filter [folded less_eq_list_def]
    5.31 -lemmas le_list_length = emb_length [of "op =", folded less_eq_list_def]
    5.32 +  list_hembeq.induct [of "op =", folded less_eq_list_def]
    5.33 +lemmas less_eq_list_drop = list_hembeq.list_hembeq_Cons [of "op =", folded less_eq_list_def]
    5.34 +lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
    5.35 +lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
    5.36 +lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
    5.37 +lemmas le_list_length = list_hembeq_length [of "op =", folded less_eq_list_def]
    5.38  
    5.39  lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
    5.40 -  by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)
    5.41 +  by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
    5.42  
    5.43  lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
    5.44 -  by (metis less_eq_list_def emb_Nil order_less_le)
    5.45 +  by (metis less_eq_list_def list_hembeq_Nil order_less_le)
    5.46  
    5.47  lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
    5.48 -  by (metis emb_Nil less_eq_list_def less_list_def)
    5.49 +  by (metis list_hembeq_Nil less_eq_list_def less_list_def)
    5.50  
    5.51  lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
    5.52    by (unfold less_le less_eq_list_def) (auto)
    5.53  
    5.54  lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
    5.55 -  by (metis sub_Cons2_iff less_list_def less_eq_list_def)
    5.56 +  by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
    5.57  
    5.58  lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
    5.59 -  by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def)
    5.60 +  by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
    5.61  
    5.62  lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
    5.63 -  by (metis less_list_def less_eq_list_def sub_append')
    5.64 +  by (metis less_list_def less_eq_list_def sublisteq_append')
    5.65  
    5.66  lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
    5.67    by (unfold less_le less_eq_list_def) auto