[isabelle-dev] push request (Sublist.thy)

Christian Sternagel c-sterna at jaist.ac.jp
Sun Dec 9 12:50:12 CET 2012


I fixed an error that only came up during document preparation (which I 
should have tested previously, sorry).

cheers

chris

On 12/09/2012 02:27 PM, Christian Sternagel wrote:
> Dear all,
>
> I have the following changes in my local patch queue:
>
> - In src/HOL/Library/Sublist.thy:
>    renamed "emb" ~> "list_hembeq" and "sub" ~> "sublisteq";
>    slightly changed definition of list_hembeq to make it reflexive
> independent of the base order;
>    dropped predicate "transp_on"
>
> Reasons: the name "emb" was very unspecific (hence the "list_" prefix to
> make clear that it is on lists, and "h" for "homeomorphic" since there
> is an important difference between "plain" embedding (which is just the
> sublist relation) and homeomorphic embedding, where we are allowed to
> replace elements by smaller elements w.r.t. some base order) and in a
> later development I will need an irreflexive variant (hence "eq").
> Furthermore, since the basic use of embedding is as a well-quasi-order
> and wqos are reflexive it seems natural to have a definition where
> embedding is reflexive independent of the base order.
>
> I will add "transp_on" to Restricted_Predicates from the AFP. At some
> point I would like to have the definitions of "reflp_on", "transp_on",
> "irreflp_on", "antisymp_on", ... in the main distribution (but that is
> an orthogonal issue).
>
> Any comments? Any takers (for pushing my changes to the main repo)? I
> checked the changes against f2241b8d0db5 with 'isabelle build -a' and
> prepared a changeset for the AFP (which I can push myself).
>
> cheers
>
> chris
>
> PS: As stated above, currently my changes are in my local patch queue
> and I attached the corresponding patch file from .hg/patches (which
> contains a commit message at the top). Should I transform this into an
> hgbundle?
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
# HG changeset patch
# Parent f2241b8d0db588bedd8e1e9b39ad8ad1970c89ff
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

diff -r f2241b8d0db5 NEWS
--- a/NEWS	Sat Dec 08 22:41:39 2012 +0100
+++ b/NEWS	Sun Dec 09 20:45:02 2012 +0900
@@ -173,8 +173,8 @@
     syntax "xs >>= ys"; use "suffixeq ys xs" instead.  Renamed lemmas
     accordingly.  INCOMPATIBILITY.
 
-  - New constant "emb" for homeomorphic embedding on lists. New
-    abbreviation "sub" for special case "emb (op =)".
+  - New constant "list_hembeq" for homeomorphic embedding on lists. New
+    abbreviation "sublisteq" for special case "list_hembeq (op =)".
 
   - Library/Sublist does no longer provide "order" and "bot" type class
     instances for the prefix order (merely corresponding locale
@@ -182,24 +182,24 @@
     Library/Prefix_Order. INCOMPATIBILITY.
 
   - The sublist relation from Library/Sublist_Order is now based on
-    "Sublist.sub". Replaced lemmas:
-
-      le_list_append_le_same_iff ~> Sublist.sub_append_le_same_iff
-      le_list_append_mono ~> Sublist.emb_append_mono
-      le_list_below_empty ~> Sublist.emb_Nil, Sublist.emb_Nil2
-      le_list_Cons_EX ~> Sublist.emb_ConsD
-      le_list_drop_Cons2 ~> Sublist.sub_Cons2'
-      le_list_drop_Cons_neq ~> Sublist.sub_Cons2_neq
-      le_list_drop_Cons ~> Sublist.sub_Cons'
-      le_list_drop_many ~> Sublist.sub_drop_many
-      le_list_filter_left ~> Sublist.sub_filter_left
-      le_list_rev_drop_many ~> Sublist.sub_rev_drop_many
-      le_list_rev_take_iff ~> Sublist.sub_append
-      le_list_same_length ~> Sublist.sub_same_length
-      le_list_take_many_iff ~> Sublist.sub_append'
+    "Sublist.sublisteq". Replaced lemmas:
+
+      le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
+      le_list_append_mono ~> Sublist.list_hembeq_append_mono
+      le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2
+      le_list_Cons_EX ~> Sublist.list_hembeq_ConsD
+      le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'
+      le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq
+      le_list_drop_Cons ~> Sublist.sublisteq_Cons'
+      le_list_drop_many ~> Sublist.sublisteq_drop_many
+      le_list_filter_left ~> Sublist.sublisteq_filter_left
+      le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many
+      le_list_rev_take_iff ~> Sublist.sublisteq_append
+      le_list_same_length ~> Sublist.sublisteq_same_length
+      le_list_take_many_iff ~> Sublist.sublisteq_append'
       less_eq_list.drop ~> less_eq_list_drop
       less_eq_list.induct ~> less_eq_list_induct
-      not_le_list_length ~> Sublist.not_sub_length
+      not_le_list_length ~> Sublist.not_sublisteq_length
 
     INCOMPATIBILITY.
 
diff -r f2241b8d0db5 src/HOL/BNF/Examples/TreeFI.thy
--- a/src/HOL/BNF/Examples/TreeFI.thy	Sat Dec 08 22:41:39 2012 +0100
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Sun Dec 09 20:45:02 2012 +0900
@@ -12,8 +12,6 @@
 imports ListF
 begin
 
-hide_const (open) Sublist.sub
-
 codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
 
 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
diff -r f2241b8d0db5 src/HOL/BNF/Examples/TreeFsetI.thy
--- a/src/HOL/BNF/Examples/TreeFsetI.thy	Sat Dec 08 22:41:39 2012 +0100
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Sun Dec 09 20:45:02 2012 +0900
@@ -12,7 +12,6 @@
 imports "../BNF"
 begin
 
-hide_const (open) Sublist.sub
 hide_fact (open) Quotient_Product.prod_rel_def
 
 codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
diff -r f2241b8d0db5 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Sat Dec 08 22:41:39 2012 +0100
+++ b/src/HOL/Library/Sublist.thy	Sun Dec 09 20:45:02 2012 +0900
@@ -3,7 +3,7 @@
     Author:     Christian Sternagel, JAIST
 *)
 
-header {* List prefixes, suffixes, and embedding*}
+header {* List prefixes, suffixes, and homeomorphic embedding *}
 
 theory Sublist
 imports Main
@@ -11,10 +11,10 @@
 
 subsection {* Prefix order on lists *}
 
-definition prefixeq :: "'a list => 'a list => bool"
+definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
 
-definition prefix :: "'a list => 'a list => bool"
+definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
 
 interpretation prefix_order: order prefixeq prefix
@@ -23,7 +23,7 @@
 interpretation prefix_bot: bot prefixeq prefix Nil
   by default (simp add: prefixeq_def)
 
-lemma prefixeqI [intro?]: "ys = xs @ zs ==> prefixeq xs ys"
+lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
   unfolding prefixeq_def by blast
 
 lemma prefixeqE [elim?]:
@@ -31,7 +31,7 @@
   obtains zs where "ys = xs @ zs"
   using assms unfolding prefixeq_def by blast
 
-lemma prefixI' [intro?]: "ys = xs @ z # zs ==> prefix xs ys"
+lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
   unfolding prefix_def prefixeq_def by blast
 
 lemma prefixE' [elim?]:
@@ -43,7 +43,7 @@
   with that show ?thesis by (auto simp add: neq_Nil_conv)
 qed
 
-lemma prefixI [intro?]: "prefixeq xs ys ==> xs \<noteq> ys ==> prefix xs ys"
+lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
   unfolding prefix_def by blast
 
 lemma prefixE [elim?]:
@@ -88,7 +88,7 @@
 lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
   by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
 
-lemma prefixeq_prefixeq [simp]: "prefixeq xs ys ==> prefixeq xs (ys @ zs)"
+lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
   by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
 
 lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
@@ -106,12 +106,12 @@
   done
 
 lemma append_one_prefixeq:
-  "prefixeq xs ys ==> length xs < length ys ==> prefixeq (xs @ [ys ! length xs]) ys"
+  "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
   unfolding prefixeq_def
   by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj
     eq_Nil_appendI nth_drop')
 
-theorem prefixeq_length_le: "prefixeq xs ys ==> length xs \<le> length ys"
+theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
   by (auto simp add: prefixeq_def)
 
 lemma prefixeq_same_cases:
@@ -191,10 +191,10 @@
 
 subsection {* Parallel lists *}
 
-definition parallel :: "'a list => 'a list => bool"  (infixl "\<parallel>" 50)
+definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)
   where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
 
-lemma parallelI [intro]: "\<not> prefixeq xs ys ==> \<not> prefixeq ys xs ==> xs \<parallel> ys"
+lemma parallelI [intro]: "\<not> prefixeq xs ys \<Longrightarrow> \<not> prefixeq ys xs \<Longrightarrow> xs \<parallel> ys"
   unfolding parallel_def by blast
 
 lemma parallelE [elim]:
@@ -207,7 +207,7 @@
   unfolding parallel_def prefix_def by blast
 
 theorem parallel_decomp:
-  "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
+  "xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
 proof (induct xs rule: rev_induct)
   case Nil
   then have False by auto
@@ -268,7 +268,7 @@
   "suffix xs ys \<Longrightarrow> suffixeq xs ys"
   by (auto simp: suffixeq_def suffix_def)
 
-lemma suffixeqI [intro?]: "ys = zs @ xs ==> suffixeq xs ys"
+lemma suffixeqI [intro?]: "ys = zs @ xs \<Longrightarrow> suffixeq xs ys"
   unfolding suffixeq_def by blast
 
 lemma suffixeqE [elim?]:
@@ -420,268 +420,262 @@
   unfolding suffix_def by auto
 
 
-subsection {* Embedding on lists *}
+subsection {* Homeomorphic embedding on lists *}
 
-inductive emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+inductive list_hembeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
 where
-  emb_Nil [intro, simp]: "emb P [] ys"
-| emb_Cons [intro] : "emb P xs ys \<Longrightarrow> emb P xs (y#ys)"
-| emb_Cons2 [intro]: "P x y \<Longrightarrow> emb P xs ys \<Longrightarrow> emb P (x#xs) (y#ys)"
+  list_hembeq_Nil [intro, simp]: "list_hembeq P [] ys"
+| list_hembeq_Cons [intro] : "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (y#ys)"
+| list_hembeq_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_hembeq P xs ys \<Longrightarrow> list_hembeq P (x#xs) (y#ys)"
 
-lemma emb_Nil2 [simp]:
-  assumes "emb P xs []" shows "xs = []"
-  using assms by (cases rule: emb.cases) auto
+lemma list_hembeq_Nil2 [simp]:
+  assumes "list_hembeq P xs []" shows "xs = []"
+  using assms by (cases rule: list_hembeq.cases) auto
 
-lemma emb_Cons_Nil [simp]: "emb P (x#xs) [] = False"
+lemma list_hembeq_refl [simp, intro!]:
+  "list_hembeq P xs xs"
+  by (induct xs) auto
+
+lemma list_hembeq_Cons_Nil [simp]: "list_hembeq P (x#xs) [] = False"
 proof -
-  { assume "emb P (x#xs) []"
-    from emb_Nil2 [OF this] have False by simp
+  { assume "list_hembeq P (x#xs) []"
+    from list_hembeq_Nil2 [OF this] have False by simp
   } moreover {
     assume False
-    then have "emb P (x#xs) []" by simp
+    then have "list_hembeq P (x#xs) []" by simp
   } ultimately show ?thesis by blast
 qed
 
-lemma emb_append2 [intro]: "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)"
+lemma list_hembeq_append2 [intro]: "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (zs @ ys)"
   by (induct zs) auto
 
-lemma emb_prefix [intro]:
-  assumes "emb P xs ys" shows "emb P xs (ys @ zs)"
+lemma list_hembeq_prefix [intro]:
+  assumes "list_hembeq P xs ys" shows "list_hembeq P xs (ys @ zs)"
   using assms
   by (induct arbitrary: zs) auto
 
-lemma emb_ConsD:
-  assumes "emb P (x#xs) ys"
-  shows "\<exists>us v vs. ys = us @ v # vs \<and> P x v \<and> emb P xs vs"
+lemma list_hembeq_ConsD:
+  assumes "list_hembeq P (x#xs) ys"
+  shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_hembeq P xs vs"
 using assms
 proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
-  case emb_Cons
+  case list_hembeq_Cons
   then show ?case by (metis append_Cons)
 next
-  case (emb_Cons2 x y xs ys)
+  case (list_hembeq_Cons2 x y xs ys)
   then show ?case by (cases xs) (auto, blast+)
 qed
 
-lemma emb_appendD:
-  assumes "emb P (xs @ ys) zs"
-  shows "\<exists>us vs. zs = us @ vs \<and> emb P xs us \<and> emb P ys vs"
+lemma list_hembeq_appendD:
+  assumes "list_hembeq P (xs @ ys) zs"
+  shows "\<exists>us vs. zs = us @ vs \<and> list_hembeq P xs us \<and> list_hembeq P ys vs"
 using assms
 proof (induction xs arbitrary: ys zs)
   case Nil then show ?case by auto
 next
   case (Cons x xs)
   then obtain us v vs where "zs = us @ v # vs"
-    and "P x v" and "emb P (xs @ ys) vs" by (auto dest: emb_ConsD)
-  with Cons show ?case by (metis append_Cons append_assoc emb_Cons2 emb_append2)
+    and "P\<^sup>=\<^sup>= x v" and "list_hembeq P (xs @ ys) vs" by (auto dest: list_hembeq_ConsD)
+  with Cons show ?case by (metis append_Cons append_assoc list_hembeq_Cons2 list_hembeq_append2)
 qed
 
-lemma emb_suffix:
-  assumes "emb P xs ys" and "suffix ys zs"
-  shows "emb P xs zs"
-  using assms(2) and emb_append2 [OF assms(1)] by (auto simp: suffix_def)
+lemma list_hembeq_suffix:
+  assumes "list_hembeq P xs ys" and "suffix ys zs"
+  shows "list_hembeq P xs zs"
+  using assms(2) and list_hembeq_append2 [OF assms(1)] by (auto simp: suffix_def)
 
-lemma emb_suffixeq:
-  assumes "emb P xs ys" and "suffixeq ys zs"
-  shows "emb P xs zs"
-  using assms and emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto
+lemma list_hembeq_suffixeq:
+  assumes "list_hembeq P xs ys" and "suffixeq ys zs"
+  shows "list_hembeq P xs zs"
+  using assms and list_hembeq_suffix unfolding suffixeq_suffix_reflclp_conv by auto
 
-lemma emb_length: "emb P xs ys \<Longrightarrow> length xs \<le> length ys"
-  by (induct rule: emb.induct) auto
+lemma list_hembeq_length: "list_hembeq P xs ys \<Longrightarrow> length xs \<le> length ys"
+  by (induct rule: list_hembeq.induct) auto
 
-(*FIXME: move*)
-definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
-  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)"
-lemma transp_onI [Pure.intro]:
-  "(\<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"
-  unfolding transp_on_def by blast
-
-lemma transp_on_emb:
-  assumes "transp_on P A"
-  shows "transp_on (emb P) (lists A)"
-proof
+lemma list_hembeq_trans:
+  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"
+  shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A;
+    list_hembeq P xs ys; list_hembeq P ys zs\<rbrakk> \<Longrightarrow> list_hembeq P xs zs"
+proof -
   fix xs ys zs
-  assume "emb P xs ys" and "emb P ys zs"
+  assume "list_hembeq P xs ys" and "list_hembeq P ys zs"
     and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
-  then show "emb P xs zs"
+  then show "list_hembeq P xs zs"
   proof (induction arbitrary: zs)
-    case emb_Nil show ?case by blast
+    case list_hembeq_Nil show ?case by blast
   next
-    case (emb_Cons xs ys y)
-    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
-      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
-    then have "emb P ys (v#vs)" by blast
-    then have "emb P ys zs" unfolding zs by (rule emb_append2)
-    from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp
+    case (list_hembeq_Cons xs ys y)
+    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
+      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
+    then have "list_hembeq P ys (v#vs)" by blast
+    then have "list_hembeq P ys zs" unfolding zs by (rule list_hembeq_append2)
+    from list_hembeq_Cons.IH [OF this] and list_hembeq_Cons.prems show ?case by simp
   next
-    case (emb_Cons2 x y xs ys)
-    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
-      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
-    with emb_Cons2 have "emb P xs vs" by simp
-    moreover have "P x v"
+    case (list_hembeq_Cons2 x y xs ys)
+    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
+      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
+    with list_hembeq_Cons2 have "list_hembeq P xs vs" by simp
+    moreover have "P\<^sup>=\<^sup>= x v"
     proof -
       from zs and `zs \<in> lists A` have "v \<in> A" by auto
-      moreover have "x \<in> A" and "y \<in> A" using emb_Cons2 by simp_all
-      ultimately show ?thesis using `P x y` and `P y v` and assms
-        unfolding transp_on_def by blast
+      moreover have "x \<in> A" and "y \<in> A" using list_hembeq_Cons2 by simp_all
+      ultimately show ?thesis
+        using `P\<^sup>=\<^sup>= x y` and `P\<^sup>=\<^sup>= y v` and assms
+        by blast
     qed
-    ultimately have "emb P (x#xs) (v#vs)" by blast
-    then show ?case unfolding zs by (rule emb_append2)
+    ultimately have "list_hembeq P (x#xs) (v#vs)" by blast
+    then show ?case unfolding zs by (rule list_hembeq_append2)
   qed
 qed
 
 
-subsection {* Sublists (special case of embedding) *}
+subsection {* Sublists (special case of homeomorphic embedding) *}
 
-abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-  where "sub xs ys \<equiv> emb (op =) xs ys"
+abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+  where "sublisteq xs ys \<equiv> list_hembeq (op =) xs ys"
 
-lemma sub_Cons2: "sub xs ys \<Longrightarrow> sub (x#xs) (x#ys)" by auto
+lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
 
-lemma sub_same_length:
-  assumes "sub xs ys" and "length xs = length ys" shows "xs = ys"
-  using assms by (induct) (auto dest: emb_length)
+lemma sublisteq_same_length:
+  assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys"
+  using assms by (induct) (auto dest: list_hembeq_length)
 
-lemma not_sub_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sub xs ys"
-  by (metis emb_length linorder_not_less)
+lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
+  by (metis list_hembeq_length linorder_not_less)
 
 lemma [code]:
-  "emb P [] ys \<longleftrightarrow> True"
-  "emb P (x#xs) [] \<longleftrightarrow> False"
+  "list_hembeq P [] ys \<longleftrightarrow> True"
+  "list_hembeq P (x#xs) [] \<longleftrightarrow> False"
   by (simp_all)
 
-lemma sub_Cons': "sub (x#xs) ys \<Longrightarrow> sub xs ys"
-  by (induct xs) (auto dest: emb_ConsD)
+lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
+  by (induct xs) (auto dest: list_hembeq_ConsD)
 
-lemma sub_Cons2':
-  assumes "sub (x#xs) (x#ys)" shows "sub xs ys"
-  using assms by (cases) (rule sub_Cons')
+lemma sublisteq_Cons2':
+  assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
+  using assms by (cases) (rule sublisteq_Cons')
 
-lemma sub_Cons2_neq:
-  assumes "sub (x#xs) (y#ys)"
-  shows "x \<noteq> y \<Longrightarrow> sub (x#xs) ys"
+lemma sublisteq_Cons2_neq:
+  assumes "sublisteq (x#xs) (y#ys)"
+  shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys"
   using assms by (cases) auto
 
-lemma sub_Cons2_iff [simp, code]:
-  "sub (x#xs) (y#ys) = (if x = y then sub xs ys else sub (x#xs) ys)"
-  by (metis emb_Cons emb_Cons2 [of "op =", OF refl] sub_Cons2' sub_Cons2_neq)
+lemma sublisteq_Cons2_iff [simp, code]:
+  "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"
+  by (metis list_hembeq_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)
 
-lemma sub_append': "sub (zs @ xs) (zs @ ys) \<longleftrightarrow> sub xs ys"
+lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
   by (induct zs) simp_all
 
-lemma sub_refl [simp, intro!]: "sub xs xs" by (induct xs) simp_all
+lemma sublisteq_refl [simp, intro!]: "sublisteq xs xs" by (induct xs) simp_all
 
-lemma sub_antisym:
-  assumes "sub xs ys" and "sub ys xs"
+lemma sublisteq_antisym:
+  assumes "sublisteq xs ys" and "sublisteq ys xs"
   shows "xs = ys"
 using assms
 proof (induct)
-  case emb_Nil
-  from emb_Nil2 [OF this] show ?case by simp
+  case list_hembeq_Nil
+  from list_hembeq_Nil2 [OF this] show ?case by simp
 next
-  case emb_Cons2
+  case list_hembeq_Cons2
   then show ?case by simp
 next
-  case emb_Cons
+  case list_hembeq_Cons
   then show ?case
-    by (metis sub_Cons' emb_length Suc_length_conv Suc_n_not_le_n)
+    by (metis sublisteq_Cons' list_hembeq_length Suc_length_conv Suc_n_not_le_n)
 qed
 
-lemma transp_on_sub: "transp_on sub UNIV"
-proof -
-  have "transp_on (op =) UNIV" by (simp add: transp_on_def)
-  from transp_on_emb [OF this] show ?thesis by simp
-qed
+lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
+  by (rule list_hembeq_trans [of UNIV "op ="]) auto
 
-lemma sub_trans: "sub xs ys \<Longrightarrow> sub ys zs \<Longrightarrow> sub xs zs"
-  using transp_on_sub [unfolded transp_on_def] by blast
+lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
+  by (auto dest: list_hembeq_length)
 
-lemma sub_append_le_same_iff: "sub (xs @ ys) ys \<longleftrightarrow> xs = []"
-  by (auto dest: emb_length)
-
-lemma emb_append_mono:
-  "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> emb P (xs at ys) (xs'@ys')"
-  apply (induct rule: emb.induct)
-    apply (metis eq_Nil_appendI emb_append2)
-   apply (metis append_Cons emb_Cons)
-  apply (metis append_Cons emb_Cons2)
+lemma list_hembeq_append_mono:
+  "\<lbrakk> list_hembeq P xs xs'; list_hembeq P ys ys' \<rbrakk> \<Longrightarrow> list_hembeq P (xs at ys) (xs'@ys')"
+  apply (induct rule: list_hembeq.induct)
+    apply (metis eq_Nil_appendI list_hembeq_append2)
+   apply (metis append_Cons list_hembeq_Cons)
+  apply (metis append_Cons list_hembeq_Cons2)
   done
 
 
 subsection {* Appending elements *}
 
-lemma sub_append [simp]:
-  "sub (xs @ zs) (ys @ zs) \<longleftrightarrow> sub xs ys" (is "?l = ?r")
+lemma sublisteq_append [simp]:
+  "sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r")
 proof
-  { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'"
-    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys"
+  { fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'"
+    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys"
     proof (induct arbitrary: xs ys zs)
-      case emb_Nil show ?case by simp
+      case list_hembeq_Nil show ?case by simp
     next
-      case (emb_Cons xs' ys' x)
-      { assume "ys=[]" then have ?case using emb_Cons(1) by auto }
+      case (list_hembeq_Cons xs' ys' x)
+      { assume "ys=[]" then have ?case using list_hembeq_Cons(1) by auto }
       moreover
       { fix us assume "ys = x#us"
-        then have ?case using emb_Cons(2) by(simp add: emb.emb_Cons) }
+        then have ?case using list_hembeq_Cons(2) by(simp add: list_hembeq.list_hembeq_Cons) }
       ultimately show ?case by (auto simp:Cons_eq_append_conv)
     next
-      case (emb_Cons2 x y xs' ys')
-      { assume "xs=[]" then have ?case using emb_Cons2(1) by auto }
+      case (list_hembeq_Cons2 x y xs' ys')
+      { assume "xs=[]" then have ?case using list_hembeq_Cons2(1) by auto }
       moreover
-      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using emb_Cons2 by auto}
+      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_hembeq_Cons2 by auto}
       moreover
-      { fix us assume "xs=x#us" "ys=[]" then have ?case using emb_Cons2(2) by bestsimp }
-      ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv)
+      { fix us assume "xs=x#us" "ys=[]" then have ?case using list_hembeq_Cons2(2) by bestsimp }
+      ultimately show ?case using `op =\<^sup>=\<^sup>= x y` by (auto simp: Cons_eq_append_conv)
     qed }
   moreover assume ?l
   ultimately show ?r by blast
 next
-  assume ?r then show ?l by (metis emb_append_mono sub_refl)
+  assume ?r then show ?l by (metis list_hembeq_append_mono sublisteq_refl)
 qed
 
-lemma sub_drop_many: "sub xs ys \<Longrightarrow> sub xs (zs @ ys)"
+lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
   by (induct zs) auto
 
-lemma sub_rev_drop_many: "sub xs ys \<Longrightarrow> sub xs (ys @ zs)"
-  by (metis append_Nil2 emb_Nil emb_append_mono)
+lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"
+  by (metis append_Nil2 list_hembeq_Nil list_hembeq_append_mono)
 
 
 subsection {* Relation to standard list operations *}
 
-lemma sub_map:
-  assumes "sub xs ys" shows "sub (map f xs) (map f ys)"
+lemma sublisteq_map:
+  assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)"
   using assms by (induct) auto
 
-lemma sub_filter_left [simp]: "sub (filter P xs) xs"
+lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs"
   by (induct xs) auto
 
-lemma sub_filter [simp]:
-  assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)"
+lemma sublisteq_filter [simp]:
+  assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)"
   using assms by (induct) auto
 
-lemma "sub xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
+lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
 proof
   assume ?L
   then show ?R
   proof (induct)
-    case emb_Nil show ?case by (metis sublist_empty)
+    case list_hembeq_Nil show ?case by (metis sublist_empty)
   next
-    case (emb_Cons xs ys x)
+    case (list_hembeq_Cons xs ys x)
     then obtain N where "xs = sublist ys N" by blast
     then have "xs = sublist (x#ys) (Suc ` N)"
       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
     then show ?case by blast
   next
-    case (emb_Cons2 x y xs ys)
+    case (list_hembeq_Cons2 x y xs ys)
     then obtain N where "xs = sublist ys N" by blast
     then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
-    then show ?case unfolding `x = y` by blast
+    moreover from list_hembeq_Cons2 have "x = y" by simp
+    ultimately show ?case by blast
   qed
 next
   assume ?R
   then obtain N where "xs = sublist ys N" ..
-  moreover have "sub (sublist ys N) ys"
+  moreover have "sublisteq (sublist ys N) ys"
   proof (induct ys arbitrary: N)
     case Nil show ?case by simp
   next
diff -r f2241b8d0db5 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Sat Dec 08 22:41:39 2012 +0100
+++ b/src/HOL/Library/Sublist_Order.thy	Sun Dec 09 20:45:02 2012 +0900
@@ -21,7 +21,7 @@
 begin
 
 definition
-  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys"
+  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
 
 definition
   "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
@@ -40,41 +40,41 @@
 next
   fix xs ys :: "'a list"
   assume "xs <= ys" and "ys <= xs"
-  thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym)
+  thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
 next
   fix xs ys zs :: "'a list"
   assume "xs <= ys" and "ys <= zs"
-  thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
+  thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
 qed
 
 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
-  emb.induct [of "op =", folded less_eq_list_def]
-lemmas less_eq_list_drop = emb.emb_Cons [of "op =", folded less_eq_list_def]
-lemmas le_list_Cons2_iff [simp, code] = sub_Cons2_iff [folded less_eq_list_def]
-lemmas le_list_map = sub_map [folded less_eq_list_def]
-lemmas le_list_filter = sub_filter [folded less_eq_list_def]
-lemmas le_list_length = emb_length [of "op =", folded less_eq_list_def]
+  list_hembeq.induct [of "op =", folded less_eq_list_def]
+lemmas less_eq_list_drop = list_hembeq.list_hembeq_Cons [of "op =", folded less_eq_list_def]
+lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
+lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
+lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
+lemmas le_list_length = list_hembeq_length [of "op =", folded less_eq_list_def]
 
 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
-  by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)
+  by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
 
 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
-  by (metis less_eq_list_def emb_Nil order_less_le)
+  by (metis less_eq_list_def list_hembeq_Nil order_less_le)
 
 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
-  by (metis emb_Nil less_eq_list_def less_list_def)
+  by (metis list_hembeq_Nil less_eq_list_def less_list_def)
 
 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   by (unfold less_le less_eq_list_def) (auto)
 
 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
-  by (metis sub_Cons2_iff less_list_def less_eq_list_def)
+  by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
 
 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
-  by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def)
+  by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
 
 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
-  by (metis less_list_def less_eq_list_def sub_append')
+  by (metis less_list_def less_eq_list_def sublisteq_append')
 
 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
   by (unfold less_le less_eq_list_def) auto


More information about the isabelle-dev mailing list