summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | eberlm <eberlm@in.tum.de> |

Thu, 18 May 2017 12:02:21 +0200 | |

changeset 65869 | a6ed757b8585 |

parent 65861 | f35abc25d7b1 |

child 65870 | 81574a7e7c38 |

more on sublists

src/HOL/Library/Sublist.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Sublist_Order.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/Sublist.thy Wed May 17 23:13:56 2017 +0200 +++ b/src/HOL/Library/Sublist.thy Thu May 18 12:02:21 2017 +0200 @@ -57,12 +57,12 @@ subsection \<open>Basic properties of prefixes\<close> (* FIXME rm *) -theorem Nil_prefix [iff]: "prefix [] xs" -by(fact prefix_bot.bot_least) +theorem Nil_prefix [simp]: "prefix [] xs" + by (fact prefix_bot.bot_least) (* FIXME rm *) theorem prefix_Nil [simp]: "(prefix xs []) = (xs = [])" -by(fact prefix_bot.bot_unique) + by (fact prefix_bot.bot_unique) lemma prefix_snoc [simp]: "prefix xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefix xs ys" proof @@ -88,7 +88,7 @@ lemma same_prefix_prefix [simp]: "prefix (xs @ ys) (xs @ zs) = prefix ys zs" by (induct xs) simp_all -lemma same_prefix_nil [iff]: "prefix (xs @ ys) xs = (ys = [])" +lemma same_prefix_nil [simp]: "prefix (xs @ ys) xs = (ys = [])" by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixI) lemma prefix_prefix [simp]: "prefix xs ys \<Longrightarrow> prefix xs (ys @ zs)" @@ -228,16 +228,57 @@ qed lemma length_prefixes[simp]: "length (prefixes xs) = length xs+1" -by (induction xs) auto + by (induction xs) auto + +lemma distinct_prefixes [intro]: "distinct (prefixes xs)" + by (induction xs) (auto simp: distinct_map) + +lemma prefixes_snoc [simp]: "prefixes (xs@[x]) = prefixes xs @ [xs@[x]]" + by (induction xs) auto + +lemma prefixes_not_Nil [simp]: "prefixes xs \<noteq> []" + by (cases xs) auto -lemma prefixes_snoc[simp]: - "prefixes (xs@[x]) = prefixes xs @ [xs@[x]]" -by (induction xs) auto +lemma hd_prefixes [simp]: "hd (prefixes xs) = []" + by (cases xs) simp_all -lemma prefixes_eq_Snoc: +lemma last_prefixes [simp]: "last (prefixes xs) = xs" + by (induction xs) (simp_all add: last_map) + +lemma prefixes_append: + "prefixes (xs @ ys) = prefixes xs @ map (\<lambda>ys'. xs @ ys') (tl (prefixes ys))" +proof (induction xs) + case Nil + thus ?case by (cases ys) auto +qed simp_all + +lemma prefixes_eq_snoc: "prefixes ys = xs @ [x] \<longleftrightarrow> (ys = [] \<and> xs = [] \<or> (\<exists>z zs. ys = zs@[z] \<and> xs = prefixes zs)) \<and> x = ys" -by (cases ys rule: rev_cases) auto + by (cases ys rule: rev_cases) auto + +lemma prefixes_tailrec [code]: + "prefixes xs = rev (snd (foldl (\<lambda>(acc1, acc2) x. (x#acc1, rev (x#acc1)#acc2)) ([],[[]]) xs))" +proof - + have "foldl (\<lambda>(acc1, acc2) x. (x#acc1, rev (x#acc1)#acc2)) (ys, rev ys # zs) xs = + (rev xs @ ys, rev (map (\<lambda>as. rev ys @ as) (prefixes xs)) @ zs)" for ys zs + proof (induction xs arbitrary: ys zs) + case (Cons x xs ys zs) + from Cons.IH[of "x # ys" "rev ys # zs"] + show ?case by (simp add: o_def) + qed simp_all + from this [of "[]" "[]"] show ?thesis by simp +qed + +lemma set_prefixes_eq: "set (prefixes xs) = {ys. prefix ys xs}" + by auto + +lemma card_set_prefixes [simp]: "card (set (prefixes xs)) = Suc (length xs)" + by (subst distinct_card) auto + +lemma set_prefixes_append: + "set (prefixes (xs @ ys)) = set (prefixes xs) \<union> {xs @ ys' |ys'. ys' \<in> set (prefixes ys)}" + by (subst prefixes_append, cases ys) auto subsection \<open>Longest Common Prefix\<close> @@ -435,11 +476,13 @@ where "suffix xs ys = (\<exists>zs. ys = zs @ xs)" definition strict_suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" - where "strict_suffix xs ys \<longleftrightarrow> (\<exists>us. ys = us @ xs \<and> us \<noteq> [])" + where "strict_suffix xs ys \<longleftrightarrow> suffix xs ys \<and> xs \<noteq> ys" -lemma strict_suffix_imp_suffix: - "strict_suffix xs ys \<Longrightarrow> suffix xs ys" - by (auto simp: suffix_def strict_suffix_def) +interpretation suffix_order: order suffix strict_suffix + by standard (auto simp: suffix_def strict_suffix_def) + +interpretation suffix_bot: order_bot Nil suffix strict_suffix + by standard (simp add: suffix_def) lemma suffixI [intro?]: "ys = zs @ xs \<Longrightarrow> suffix xs ys" unfolding suffix_def by blast @@ -449,27 +492,13 @@ obtains zs where "ys = zs @ xs" using assms unfolding suffix_def by blast -lemma suffix_refl [iff]: "suffix xs xs" - by (auto simp add: suffix_def) - -lemma suffix_trans: - "suffix xs ys \<Longrightarrow> suffix ys zs \<Longrightarrow> suffix xs zs" - by (auto simp: suffix_def) - -lemma strict_suffix_trans: - "\<lbrakk>strict_suffix xs ys; strict_suffix ys zs\<rbrakk> \<Longrightarrow> strict_suffix xs zs" -by (auto simp add: strict_suffix_def) - -lemma suffix_antisym: "\<lbrakk>suffix xs ys; suffix ys xs\<rbrakk> \<Longrightarrow> xs = ys" - by (auto simp add: suffix_def) - lemma suffix_tl [simp]: "suffix (tl xs) xs" by (induct xs) (auto simp: suffix_def) lemma strict_suffix_tl [simp]: "xs \<noteq> [] \<Longrightarrow> strict_suffix (tl xs) xs" - by (induct xs) (auto simp: strict_suffix_def) + by (induct xs) (auto simp: strict_suffix_def suffix_def) -lemma Nil_suffix [iff]: "suffix [] xs" +lemma Nil_suffix [simp]: "suffix [] xs" by (simp add: suffix_def) lemma suffix_Nil [simp]: "(suffix xs []) = (xs = [])" @@ -488,10 +517,10 @@ by (auto simp add: suffix_def) lemma strict_suffix_set_subset: "strict_suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" -by (auto simp: strict_suffix_def) + by (auto simp: strict_suffix_def suffix_def) lemma suffix_set_subset: "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" -by (auto simp: suffix_def) + by (auto simp: suffix_def) lemma suffix_ConsD2: "suffix (x # xs) (y # ys) \<Longrightarrow> suffix xs ys" proof - @@ -514,6 +543,9 @@ then have "ys = rev zs @ xs" by simp then show "suffix xs ys" .. qed + +lemma strict_suffix_to_prefix [code]: "strict_suffix xs ys \<longleftrightarrow> strict_prefix (rev xs) (rev ys)" + by (auto simp: suffix_to_prefix strict_suffix_def strict_prefix_def) lemma distinct_suffix: "distinct ys \<Longrightarrow> suffix xs ys \<Longrightarrow> distinct xs" by (clarsimp elim!: suffixE) @@ -522,20 +554,110 @@ by (auto elim!: suffixE intro: suffixI) lemma suffix_drop: "suffix (drop n as) as" - unfolding suffix_def - apply (rule exI [where x = "take n as"]) - apply simp - done + unfolding suffix_def by (rule exI [where x = "take n as"]) simp lemma suffix_take: "suffix xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs" by (auto elim!: suffixE) lemma strict_suffix_reflclp_conv: "strict_suffix\<^sup>=\<^sup>= = suffix" -by (intro ext) (auto simp: suffix_def strict_suffix_def) + by (intro ext) (auto simp: suffix_def strict_suffix_def) lemma suffix_lists: "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A" unfolding suffix_def by auto +lemma suffix_snoc [simp]: "suffix xs (ys @ [y]) \<longleftrightarrow> xs = [] \<or> (\<exists>zs. xs = zs @ [y] \<and> suffix zs ys)" + by (cases xs rule: rev_cases) (auto simp: suffix_def) + +lemma snoc_suffix_snoc [simp]: "suffix (xs @ [x]) (ys @ [y]) = (x = y \<and> suffix xs ys)" + by (auto simp add: suffix_def) + +lemma same_suffix_suffix [simp]: "suffix (ys @ xs) (zs @ xs) = suffix ys zs" + by (simp add: suffix_to_prefix) + +lemma same_suffix_nil [simp]: "suffix (ys @ xs) xs = (ys = [])" + by (simp add: suffix_to_prefix) + +theorem suffix_Cons: "suffix xs (y # ys) \<longleftrightarrow> xs = y # ys \<or> suffix xs ys" + unfolding suffix_def by (auto simp: Cons_eq_append_conv) + +theorem suffix_append: + "suffix xs (ys @ zs) \<longleftrightarrow> suffix xs zs \<or> (\<exists>xs'. xs = xs' @ zs \<and> suffix xs' ys)" + by (auto simp: suffix_def append_eq_append_conv2) + +theorem suffix_length_le: "suffix xs ys \<Longrightarrow> length xs \<le> length ys" + by (auto simp add: suffix_def) + +lemma suffix_same_cases: + "suffix (xs\<^sub>1::'a list) ys \<Longrightarrow> suffix xs\<^sub>2 ys \<Longrightarrow> suffix xs\<^sub>1 xs\<^sub>2 \<or> suffix xs\<^sub>2 xs\<^sub>1" + unfolding suffix_def by (force simp: append_eq_append_conv2) + +lemma suffix_length_suffix: + "suffix ps xs \<Longrightarrow> suffix qs xs \<Longrightarrow> length ps \<le> length qs \<Longrightarrow> suffix ps qs" + by (auto simp: suffix_to_prefix intro: prefix_length_prefix) + +lemma suffix_length_less: "strict_suffix xs ys \<Longrightarrow> length xs < length ys" + by (auto simp: strict_suffix_def suffix_def) + +lemma suffix_ConsD': "suffix (x#xs) ys \<Longrightarrow> strict_suffix xs ys" + by (auto simp: strict_suffix_def suffix_def) + +lemma drop_strict_suffix: "strict_suffix xs ys \<Longrightarrow> strict_suffix (drop n xs) ys" +proof (induct n arbitrary: xs ys) + case 0 + then show ?case by (cases ys) simp_all +next + case (Suc n) + then show ?case + by (cases xs) (auto intro: Suc dest: suffix_ConsD' suffix_order.less_imp_le) +qed + +lemma not_suffix_cases: + assumes pfx: "\<not> suffix ps ls" + obtains + (c1) "ps \<noteq> []" and "ls = []" + | (c2) a as x xs where "ps = as@[a]" and "ls = xs@[x]" and "x = a" and "\<not> suffix as xs" + | (c3) a as x xs where "ps = as@[a]" and "ls = xs@[x]" and "x \<noteq> a" +proof (cases ps rule: rev_cases) + case Nil + then show ?thesis using pfx by simp +next + case (snoc as a) + note c = \<open>ps = as@[a]\<close> + show ?thesis + proof (cases ls rule: rev_cases) + case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_suffix_nil) + next + case (snoc xs x) + show ?thesis + proof (cases "x = a") + case True + have "\<not> suffix as xs" using pfx c snoc True by simp + with c snoc True show ?thesis by (rule c2) + next + case False + with c snoc show ?thesis by (rule c3) + qed + qed +qed + +lemma not_suffix_induct [consumes 1, case_names Nil Neq Eq]: + assumes np: "\<not> suffix ps ls" + and base: "\<And>x xs. P (xs@[x]) []" + and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (xs@[x]) (ys@[y])" + and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> suffix xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (xs@[x]) (ys@[y])" + shows "P ps ls" using np +proof (induct ls arbitrary: ps rule: rev_induct) + case Nil + then show ?case by (cases ps rule: rev_cases) (auto intro: base) +next + case (snoc y ys ps) + then have npfx: "\<not> suffix ps (ys @ [y])" by simp + then obtain x xs where pv: "ps = xs @ [x]" + by (rule not_suffix_cases) auto + show ?case by (metis snoc.hyps snoc_suffix_snoc npfx pv r1 r2) +qed + + lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefix x y" by blast @@ -576,6 +698,85 @@ qed qed +subsection \<open>Suffixes\<close> + +fun suffixes where + "suffixes [] = [[]]" +| "suffixes (x#xs) = suffixes xs @ [x # xs]" + +lemma in_set_suffixes [simp]: "xs \<in> set (suffixes ys) \<longleftrightarrow> suffix xs ys" + by (induction ys) (auto simp: suffix_def Cons_eq_append_conv) + +lemma distinct_suffixes [intro]: "distinct (suffixes xs)" + by (induction xs) (auto simp: suffix_def) + +lemma length_suffixes [simp]: "length (suffixes xs) = Suc (length xs)" + by (induction xs) auto + +lemma suffixes_snoc [simp]: "suffixes (xs @ [x]) = [] # map (\<lambda>ys. ys @ [x]) (suffixes xs)" + by (induction xs) auto + +lemma suffixes_not_Nil [simp]: "suffixes xs \<noteq> []" + by (cases xs) auto + +lemma hd_suffixes [simp]: "hd (suffixes xs) = []" + by (induction xs) simp_all + +lemma last_suffixes [simp]: "last (suffixes xs) = xs" + by (cases xs) simp_all + +lemma suffixes_append: + "suffixes (xs @ ys) = suffixes ys @ map (\<lambda>xs'. xs' @ ys) (tl (suffixes xs))" +proof (induction ys rule: rev_induct) + case Nil + thus ?case by (cases xs rule: rev_cases) auto +next + case (snoc y ys) + show ?case + by (simp only: append.assoc [symmetric] suffixes_snoc snoc.IH) simp +qed + +lemma suffixes_eq_snoc: + "suffixes ys = xs @ [x] \<longleftrightarrow> + (ys = [] \<and> xs = [] \<or> (\<exists>z zs. ys = z#zs \<and> xs = suffixes zs)) \<and> x = ys" + by (cases ys) auto + +lemma suffixes_tailrec [code]: + "suffixes xs = rev (snd (foldl (\<lambda>(acc1, acc2) x. (x#acc1, (x#acc1)#acc2)) ([],[[]]) (rev xs)))" +proof - + have "foldl (\<lambda>(acc1, acc2) x. (x#acc1, (x#acc1)#acc2)) (ys, ys # zs) (rev xs) = + (xs @ ys, rev (map (\<lambda>as. as @ ys) (suffixes xs)) @ zs)" for ys zs + proof (induction xs arbitrary: ys zs) + case (Cons x xs ys zs) + from Cons.IH[of ys zs] + show ?case by (simp add: o_def case_prod_unfold) + qed simp_all + from this [of "[]" "[]"] show ?thesis by simp +qed + +lemma set_suffixes_eq: "set (suffixes xs) = {ys. suffix ys xs}" + by auto + +lemma card_set_suffixes [simp]: "card (set (suffixes xs)) = Suc (length xs)" + by (subst distinct_card) auto + +lemma set_suffixes_append: + "set (suffixes (xs @ ys)) = set (suffixes ys) \<union> {xs' @ ys |xs'. xs' \<in> set (suffixes xs)}" + by (subst suffixes_append, cases xs rule: rev_cases) auto + + +lemma suffixes_conv_prefixes: "suffixes xs = map rev (prefixes (rev xs))" + by (induction xs) auto + +lemma prefixes_conv_suffixes: "prefixes xs = map rev (suffixes (rev xs))" + by (induction xs) auto + +lemma prefixes_rev: "prefixes (rev xs) = map rev (suffixes xs)" + by (induction xs) auto + +lemma suffixes_rev: "suffixes (rev xs) = map rev (prefixes xs)" + by (induction xs) auto + subsection \<open>Homeomorphic embedding on lists\<close> @@ -654,7 +855,7 @@ lemma list_emb_strict_suffix: assumes "list_emb P xs ys" and "strict_suffix ys zs" shows "list_emb P xs zs" - using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: strict_suffix_def) + using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: strict_suffix_def suffix_def) lemma list_emb_suffix: assumes "list_emb P xs ys" and "suffix ys zs" @@ -703,11 +904,30 @@ obtains y where "y \<in> set ys" and "P x y" using assms by (induct) auto +lemma list_emb_Cons_iff1 [simp]: + assumes "P x y" + shows "list_emb P (x#xs) (y#ys) \<longleftrightarrow> list_emb P xs ys" + using assms by (subst list_emb.simps) (auto dest: list_emb_ConsD) + +lemma list_emb_Cons_iff2 [simp]: + assumes "\<not>P x y" + shows "list_emb P (x#xs) (y#ys) \<longleftrightarrow> list_emb P (x#xs) ys" + using assms by (subst list_emb.simps) auto + +lemma list_emb_code [code]: + "list_emb P [] ys \<longleftrightarrow> True" + "list_emb P (x#xs) [] \<longleftrightarrow> False" + "list_emb P (x#xs) (y#ys) \<longleftrightarrow> (if P x y then list_emb P xs ys else list_emb P (x#xs) ys)" + by simp_all + + subsection \<open>Sublists (special case of homeomorphic embedding)\<close> abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where "sublisteq xs ys \<equiv> list_emb (op =) xs ys" + +definition strict_sublist where "strict_sublist xs ys \<longleftrightarrow> xs \<noteq> ys \<and> sublisteq xs ys" lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto @@ -718,11 +938,6 @@ lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys" by (metis list_emb_length linorder_not_less) -lemma [code]: - "list_emb P [] ys \<longleftrightarrow> True" - "list_emb P (x#xs) [] \<longleftrightarrow> False" - by (simp_all) - lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys" by (induct xs, simp, blast dest: list_emb_ConsD) @@ -735,33 +950,50 @@ shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys" using assms by (cases) auto -lemma sublisteq_Cons2_iff [simp, code]: +lemma sublisteq_Cons2_iff [simp]: "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)" - by (metis list_emb_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq) + by simp lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys" by (induct zs) simp_all - -lemma sublisteq_refl [simp, intro!]: "sublisteq xs xs" by (induct xs) simp_all + +interpretation sublist_order: order sublisteq strict_sublist +proof + fix xs ys :: "'a list" + { + assume "sublisteq xs ys" and "sublisteq ys xs" + thus "xs = ys" + proof (induct) + case list_emb_Nil + from list_emb_Nil2 [OF this] show ?case by simp + next + case list_emb_Cons2 + thus ?case by simp + next + case list_emb_Cons + hence False using sublisteq_Cons' by fastforce + thus ?case .. + qed + } + thus "strict_sublist xs ys \<longleftrightarrow> (sublisteq xs ys \<and> \<not>sublisteq ys xs)" + by (auto simp: strict_sublist_def) +qed (auto simp: list_emb_refl intro: list_emb_trans) -lemma sublisteq_antisym: - assumes "sublisteq xs ys" and "sublisteq ys xs" - shows "xs = ys" -using assms -proof (induct) - case list_emb_Nil - from list_emb_Nil2 [OF this] show ?case by simp +lemma in_set_sublists [simp]: "xs \<in> set (sublists ys) \<longleftrightarrow> sublisteq xs ys" +proof + assume "xs \<in> set (sublists ys)" + thus "sublisteq xs ys" + by (induction ys arbitrary: xs) (auto simp: Let_def) next - case list_emb_Cons2 - thus ?case by simp -next - case list_emb_Cons - hence False using sublisteq_Cons' by fastforce - thus ?case .. + have [simp]: "[] \<in> set (sublists ys)" for ys :: "'a list" + by (induction ys) (auto simp: Let_def) + assume "sublisteq xs ys" + thus "xs \<in> set (sublists ys)" + by (induction xs ys rule: list_emb.induct) (auto simp: Let_def) qed -lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs" - by (rule list_emb_trans [of _ _ _ "op ="]) auto +lemma set_sublists_eq: "set (sublists ys) = {xs. sublisteq xs ys}" + by auto lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []" by (auto dest: list_emb_length) @@ -806,9 +1038,31 @@ moreover assume ?l ultimately show ?r by blast next - assume ?r then show ?l by (metis list_emb_append_mono sublisteq_refl) + assume ?r then show ?l by (metis list_emb_append_mono sublist_order.order_refl) qed +lemma sublisteq_append_iff: + "sublisteq xs (ys @ zs) \<longleftrightarrow> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> sublisteq xs1 ys \<and> sublisteq xs2 zs)" + (is "?lhs = ?rhs") +proof + assume ?lhs thus ?rhs + proof (induction xs "ys @ zs" arbitrary: ys zs rule: list_emb.induct) + case (list_emb_Cons xs ws y ys zs) + from list_emb_Cons(2)[of "tl ys" zs] and list_emb_Cons(2)[of "[]" "tl zs"] and list_emb_Cons(1,3) + show ?case by (cases ys) auto + next + case (list_emb_Cons2 x y xs ws ys zs) + from list_emb_Cons2(3)[of "tl ys" zs] and list_emb_Cons2(3)[of "[]" "tl zs"] + and list_emb_Cons2(1,2,4) + show ?case by (cases ys) (auto simp: Cons_eq_append_conv) + qed auto +qed (auto intro: list_emb_append_mono) + +lemma sublisteq_appendE [case_names append]: + assumes "sublisteq xs (ys @ zs)" + obtains xs1 xs2 where "xs = xs1 @ xs2" "sublisteq xs1 ys" "sublisteq xs2 zs" + using assms by (subst (asm) sublisteq_append_iff) auto + lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)" by (induct zs) auto

--- a/src/HOL/Library/Sublist_Order.thy Wed May 17 23:13:56 2017 +0200 +++ b/src/HOL/Library/Sublist_Order.thy Thu May 18 12:02:21 2017 +0200 @@ -35,9 +35,9 @@ show "xs \<le> xs" by (simp add: less_eq_list_def) show "xs = ys" if "xs \<le> ys" and "ys \<le> xs" - using that unfolding less_eq_list_def by (rule sublisteq_antisym) + using that unfolding less_eq_list_def by (rule sublist_order.antisym) show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" - using that unfolding less_eq_list_def by (rule sublisteq_trans) + using that unfolding less_eq_list_def by (rule sublist_order.order_trans) qed lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =