# Theory Wqo_Multiset

```(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Multiset Extension Preserves Well-Quasi-Orders›

theory Wqo_Multiset
imports
Multiset_Extension
Well_Quasi_Orders
begin

lemma list_emb_imp_reflclp_mulex_on:
assumes "xs ∈ lists A" and "ys ∈ lists A"
and "list_emb P xs ys"
shows "(mulex_on P A)⇧=⇧= (mset xs) (mset ys)"
using assms(3, 1, 2)
proof (induct)
case (list_emb_Nil ys)
then show ?case
by (cases ys) (auto intro!: empty_mulex_on simp: multisets_def)
next
case (list_emb_Cons xs ys y)
then show ?case by (auto intro!: mulex_on_self_add_singleton_right simp: multisets_def)
next
case (list_emb_Cons2 x y xs ys)
then show ?case
simp: multisets_def)
qed

text ‹The (reflexive closure of the) multiset extension of an almost-full relation
is almost-full.›
lemma almost_full_on_multisets:
assumes "almost_full_on P A"
shows "almost_full_on (mulex_on P A)⇧=⇧= (multisets A)"
proof -
let ?P = "(mulex_on P A)⇧=⇧="
from almost_full_on_hom [OF _ almost_full_on_lists, of A P ?P mset,
OF list_emb_imp_reflclp_mulex_on, simplified]
show ?thesis using assms by blast
qed

lemma wqo_on_multisets:
assumes "wqo_on P A"
shows "wqo_on (mulex_on P A)⇧=⇧= (multisets A)"
proof
from transp_on_mulex_on [of "multisets A" P A]
show "transp_on (multisets A) (mulex_on P A)⇧=⇧="
unfolding transp_on_def by blast
next
from almost_full_on_multisets [OF assms [THEN wqo_on_imp_almost_full_on]]
show "almost_full_on (mulex_on P A)⇧=⇧= (multisets A)" .
qed

end

```