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) apply (simp add: Mempty_Bag empty.abs_eq) 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