theory SubList
imports
"HOL-Library.Sublist"
"HOL-Library.Multiset"
begin
lemmas subseq_trans = subseq_order.order.trans
lemma subseq_Cons_Cons:
assumes "subseq (a # as) (b # bs)"
shows "subseq as bs"
using assms by (cases "a = b") (auto intro: subseq_Cons')
lemma subseq_induct2:
"⟦ subseq xs ys;
⋀ bs. P [] bs;
⋀ a as bs. ⟦ subseq as bs; P as bs ⟧ ⟹ P (a # as) (a # bs);
⋀ a as b bs. ⟦ a ≠ b; subseq as bs; subseq (a # as) bs; P as bs; P (a # as) bs ⟧ ⟹ P (a # as) (b # bs) ⟧
⟹ P xs ys"
proof (induct ys arbitrary: xs)
case Nil then show ?case by (metis list_emb_Nil2)
next
case (Cons y ys')
note Cons_ys = Cons
note sl = Cons(2)
note step_eq = Cons(4)
note step_neq = Cons(5)
show ?case proof (cases xs)
case Nil show ?thesis unfolding Nil using Cons.prems(2) by auto
next
case (Cons x xs')
have sl': "subseq xs' ys'" by (metis Cons sl subseq_Cons_Cons)
from sl' have P': "P xs' ys'" using Cons_ys by auto
show ?thesis proof (cases "x = y")
case False
have sl'': "subseq (x # xs') ys'" using sl unfolding Cons using False by auto
then have P'': "P (x # xs') ys'" by (metis Cons.hyps Cons_ys(3) step_eq step_neq)
show ?thesis using step_neq[OF False sl' sl'' P' P''] unfolding Cons by auto
next
case True
show ?thesis using step_eq[OF sl' P'] unfolding Cons True[symmetric] by auto
qed
qed
qed
lemma subseq_submultiset:
"subseq xs ys ⟹ mset xs ⊆# mset ys"
by (induct rule: list_emb.induct) (auto intro: subset_mset.order.trans)
lemma subseq_subset:
"subseq xs ys ⟹ set xs ⊆ set ys"
by (induct rule: list_emb.induct) auto
lemma remove1_subseq:
"subseq (remove1 x xs) xs"
by (induct xs) auto
lemma subseq_concat:
assumes "⋀x. x ∈ set xs ⟹ subseq (f x) (g x)"
shows "subseq (concat (map f xs)) (concat (map g xs))"
using assms by (induct xs) (auto intro: list_emb_append_mono)
end