# Theory Multiset_Extension2_Impl

```subsection ‹Executable version›
theory Multiset_Extension2_Impl
imports
"HOL-Library.DAList_Multiset"
List_Order
Multiset_Extension2
Multiset_Extension_Pair_Impl
begin

(**
We use the lifting when it is sufficient to prove the non-strict
domination to also prove the strict one. For example if [a > x] then
it is sufficient to prove that [A ≥ X] to get [A + {#a#} > X + {#x#}]
**)

lemma mul_ext_list_ext: "∃ s ns. list_order_extension_impl s ns mul_ext"
proof(intro exI)
let ?s = "λ s ns. {(as,bs). (mset as, mset bs) ∈ s_mul_ext ns s}"
let ?ns = "λ s ns. {(as,bs). (mset as, mset bs) ∈ ns_mul_ext ns s}"
let ?m = mset
show "list_order_extension_impl ?s ?ns mul_ext"
proof
fix s ns
show "?s {(a,b). s a b} {(a,b). ns a b} = {(as,bs). fst (mul_ext (λ a b. (s a b, ns a b)) as bs)}"
unfolding mul_ext_def Let_def by auto
next
fix s ns
show "?ns {(a,b). s a b} {(a,b). ns a b} = {(as,bs). snd (mul_ext (λ a b. (s a b, ns a b)) as bs)}"
unfolding mul_ext_def Let_def by auto
next
fix s ns s' ns' as bs
assume "set as × set bs ∩ ns ⊆ ns'"
"set as × set bs ∩ s ⊆ s'"
"(as,bs) ∈ ?s s ns"
then show "(as,bs) ∈ ?s s' ns'"
using s_mul_ext_local_mono[of "?m as" "?m bs" ns ns' s s']
unfolding set_mset_mset by auto
next
fix s ns s' ns' as bs
assume "set as × set bs ∩ ns ⊆ ns'"
"set as × set bs ∩ s ⊆ s'"
"(as,bs) ∈ ?ns s ns"
then show "(as,bs) ∈ ?ns s' ns'"
using ns_mul_ext_local_mono[of "?m as" "?m bs" ns ns' s s']
unfolding set_mset_mset by auto
qed
qed

context fixes sns :: "'a ⇒ 'a ⇒ bool × bool"
begin

fun mul_ext_impl :: "'a list ⇒ 'a list ⇒ bool × bool"
and mul_ex_dom :: "'a list ⇒ 'a list ⇒ 'a ⇒ 'a list ⇒ bool × bool"
where
"mul_ext_impl [] []       = (False, True)"
| "mul_ext_impl [] ys       = (False, False)"
| "mul_ext_impl xs []       = (True, True)"
| "mul_ext_impl xs (y # ys) = mul_ex_dom xs [] y ys"

| "mul_ex_dom []       xs' y ys = (False, False)"
| "mul_ex_dom (x # xs) xs' y ys =
(case sns x y of
(True, _) ⇒ if snd (mul_ext_impl (xs @ xs') (filter (λy. ¬ fst (sns x y)) ys)) then (True, True)
else mul_ex_dom xs (x # xs') y ys
| (False, True) ⇒ or2 (mul_ext_impl (xs @ xs') ys) (mul_ex_dom xs (x # xs') y ys)
| _ ⇒ mul_ex_dom xs (x # xs') y ys)"

end

context
begin
lemma mul_ext_impl_sound0:
"mul_ext_impl sns xs ys = mult2_impl (λx y. sns y x) ys xs"
"mul_ex_dom sns xs xs' y ys = mult2_ex_dom (λx y. sns y x) y ys xs xs'"
by (induct xs ys and xs xs' y ys taking: sns rule: mul_ext_impl_mul_ex_dom.induct)
(auto split: prod.splits bool.splits)

private definition cond1 where
"cond1 f bs y xs ys ≡
((∃b. b ∈ set bs ∧ fst (f b y) ∧ snd (mul_ext f (remove1 b xs) [y←ys . ¬ fst (f b y)]))
∨ (∃b. b ∈ set bs ∧ snd (f b y) ∧ fst (mul_ext f (remove1 b xs) ys)))"

private lemma cond1_propagate:
assumes "cond1 f bs y xs ys"
shows "cond1 f (b # bs) y xs ys"
using assms unfolding cond1_def by auto

private definition cond2 where
"cond2 f bs y xs ys ≡ (cond1 f bs y xs ys
∨ (∃b. b ∈ set bs ∧ snd (f b y) ∧ snd (mul_ext f (remove1 b xs) ys)))"

private lemma cond2_propagate:
assumes "cond2 f bs y xs ys"
shows "cond2 f (b # bs) y xs ys"
using assms and cond1_propagate[of f bs y xs ys]
unfolding cond2_def by auto

private lemma cond1_cond2:
assumes "cond1 f bs y xs ys"
shows "cond2 f bs y xs ys"
using assms unfolding cond2_def by simp

lemma mul_ext_impl_sound:
shows "mul_ext_impl f xs ys = mul_ext f xs ys"
unfolding mul_ext_def s_mul_ext_def ns_mul_ext_def
by (auto simp: Let_def converse_def mul_ext_impl_sound0 mult2_impl_sound)

lemma mul_ext_code [code]: "mul_ext = mul_ext_impl"
by (intro ext, unfold mul_ext_impl_sound, auto)

lemma mul_ext_impl_cong[fundef_cong]:
assumes "⋀x x'. x ∈ set xs ⟹ x' ∈ set ys ⟹ f x x' = g x x'"
shows "mul_ext_impl f xs ys = mul_ext_impl g xs ys"
using assms
stri_mul_ext_map[of xs ys g f id] nstri_mul_ext_map[of xs ys g f id]
stri_mul_ext_map[of xs ys f g id] nstri_mul_ext_map[of xs ys f g id]
by (auto simp: mul_ext_impl_sound mul_ext_def Let_def)
end

fun ass_list_to_single_list :: "('a × nat) list ⇒ 'a list"
where
"ass_list_to_single_list [] = []"
| "ass_list_to_single_list ((x, n) # xs) = replicate n x @ ass_list_to_single_list xs"

lemma set_ass_list_to_single_list [simp]:
"set (ass_list_to_single_list xs) = {x. ∃n. (x, n) ∈ set xs ∧ n > 0}"
by (induct xs rule: ass_list_to_single_list.induct) auto

lemma count_mset_replicate [simp]:
"count (mset (replicate n x)) x = n"
by (induct n) (auto)

lemma count_mset_lal_ge:
"(x, n) ∈ set xs ⟹ count (mset (ass_list_to_single_list xs)) x ≥ n"
by (induct xs) auto

lemma count_of_count_mset_lal [simp]:
"distinct (map fst y) ⟹ count_of y x = count (mset (ass_list_to_single_list y)) x"
by (induct y) (auto simp: count_mset_lal_ge count_of_empty)

lemma Bag_mset: "Bag xs = mset (ass_list_to_single_list (DAList.impl_of xs))"
by (intro multiset_eqI, induct xs) (auto simp: Alist_inverse)

lemma Bag_Alist_Cons:
"x ∉ fst ` set xs ⟹ distinct (map fst xs) ⟹
Bag (Alist ((x, n) # xs)) = mset (replicate n x) + Bag (Alist xs)"
by (induct xs) (auto simp: Bag_mset Alist_inverse)

lemma mset_lal [simp]:
"distinct (map fst xs) ⟹ mset (ass_list_to_single_list xs) = Bag (Alist xs)"
apply (induct xs) apply (auto simp: Bag_Alist_Cons)
done

lemma Bag_s_mul_ext:
"(Bag xs, Bag ys) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)} ⟷
fst (mul_ext f (ass_list_to_single_list (DAList.impl_of xs)) (ass_list_to_single_list (DAList.impl_of ys)))"
by (auto simp: mul_ext_def Let_def Alist_impl_of)

lemma Bag_ns_mul_ext:
"(Bag xs, Bag ys) ∈ ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)} ⟷
snd (mul_ext f (ass_list_to_single_list (DAList.impl_of xs)) (ass_list_to_single_list (DAList.impl_of ys)))"
by (auto simp: mul_ext_def Let_def Alist_impl_of)

lemma smulextp_code[code]:
"smulextp f (Bag xs) (Bag ys) ⟷ fst (mul_ext f (ass_list_to_single_list (DAList.impl_of xs)) (ass_list_to_single_list (DAList.impl_of ys)))"
unfolding smulextp_def Bag_s_mul_ext ..

lemma nsmulextp_code[code]:
"nsmulextp f (Bag xs) (Bag ys) ⟷ snd (mul_ext f (ass_list_to_single_list (DAList.impl_of xs)) (ass_list_to_single_list (DAList.impl_of ys)))"
unfolding nsmulextp_def Bag_ns_mul_ext ..

lemma mulextp_code[code]:
"mulextp f (Bag xs) (Bag ys) = mul_ext f (ass_list_to_single_list (DAList.impl_of xs)) (ass_list_to_single_list (DAList.impl_of ys))"
unfolding mulextp_def by (simp add: nsmulextp_code smulextp_code)

end
```