theory Multiset_Extension_Pair_Impl
imports
Multiset_Extension_Pair
QTRS.Multiset2
begin
lemma subset_mult2_alt:
assumes "X ⊆# Y" "(Y, Z) ∈ mult2_alt b ns s" "b ⟹ b'"
shows "(X, Z) ∈ mult2_alt b' ns s"
proof -
from assms(2) obtain Y1 Y2 Z1 Z2 where *: "Y = Y1 + Y2" "Z = Z1 + Z2"
"(Y1, Z1) ∈ multpw ns" "b ∨ Z2 ≠ {#}" "∀y. y ∈# Y2 ⟶ (∃z. z ∈# Z2 ∧ (y, z) ∈ s)"
unfolding mult2_alt_def by blast
def Y11 ≡ "Y1 ∩# X" and Y12 ≡ "Y1 - X" def X2 ≡ "X - Y11"
have **: "X = Y11 + X2" "X2 ⊆# Y2" "Y1 = Y11 + Y12" using *(1)
by (auto simp: Y11_def Y12_def X2_def multiset_eq_iff subseteq_mset_def)
(metis add.commute assms(1) diff_is_0_eq le_diff_conv le_less min_def not_gr0 subseteq_mset_def)
obtain Z11 Z12 where ***: "Z = Z11 + (Z12 + Z2)" "Z1 = Z11 + Z12" "(Y11, Z11) ∈ multpw ns"
using *(2,3) **(3) by (auto elim: multpw_splitR simp: ac_simps)
moreover have "∀y. y ∈# X2 ⟶ (∃z. z ∈# Z12 + Z2 ∧ (y, z) ∈ s)" "b ∨ Z12 + Z2 ≠ {#}"
using *(4,5) **(2) by (auto dest!: mset_subset_eqD)
ultimately show ?thesis using *(2) **(1) assms(3) unfolding mult2_alt_def by blast
qed
text ‹Case distinction for recursion on left argument›
lemma mult2_alt_addL: "(add_mset x X, Y) ∈ mult2_alt b ns s ⟷
(∃y. y ∈# Y ∧ (x, y) ∈ s ∧ ({# x ∈# X. (x, y) ∉ s #}, Y - {#y#}) ∈ mult2_alt_ns ns s) ∨
(∃y. y ∈# Y ∧ (x, y) ∈ ns ∧ (x, y) ∉ s ∧ (X, Y - {#y#}) ∈ mult2_alt b ns s)" (is "?L ⟷ ?R1 ∨ ?R2")
proof (intro iffI; (elim disjE)?)
assume ?L then obtain X1 X2 Y1 Y2 where *: "add_mset x X = X1 + X2" "Y = Y1 + Y2"
"(X1, Y1) ∈ multpw ns" "b ∨ Y2 ≠ {#}" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)"
unfolding mult2_alt_def by blast
from union_single_eq_member[OF this(1)] multi_member_split
consider X1' where "X1 = add_mset x X1'" "x ∈# X1" | X2' where "X2 = add_mset x X2'" "x ∈# X2"
unfolding set_mset_union Un_iff by metis
then show "?R1 ∨ ?R2"
proof cases
case 1 then obtain y Y1' where **: "y ∈# Y1" "Y1 = add_mset y Y1'" "(X1', Y1') ∈ multpw ns" "(x, y) ∈ ns"
using * by (auto elim: multpw_split1R)
show ?thesis
proof (cases "(x, y) ∈ s")
case False then show ?thesis using mult2_altI[OF refl refl **(3) *(4,5)] *
by (auto simp: 1 ** intro: exI[of _ y])
next
case True
def X2' ≡ "{# x ∈# X2. (x, y) ∉ s #}"
have x3: "∀x. x ∈# X2' ⟶ (∃z. z ∈# Y2 ∧ (x, z) ∈ s)" using *(5) **(1,2) by (auto simp: X2'_def)
have x4: "{# x ∈# X. (x, y) ∉ s#} ⊆# X1' + X2'" using *(1) 1
by (auto simp: X2'_def multiset_eq_iff intro!: mset_subset_eqI split: if_splits elim!: in_countE) (metis le_refl)
show ?thesis using mult2_alt_nsI[OF refl refl **(3) x3, THEN subset_mult2_alt[OF x4]]
**(2) *(2) True by (auto intro: exI[of _ y])
qed
next
case 2 then obtain y where **: "y ∈# Y2" "(x, y) ∈ s" using * by blast
def X2' ≡ "{# x ∈# X2. (x, y) ∉ s #}"
have x3: "∀x. x ∈# X2' ⟶ (∃z. z ∈# Y2 - {#y#} ∧ (x, z) ∈ s)"
using *(5) **(1,2) by (auto simp: X2'_def) (metis mem_multiset_diff_compat)
have x4: "{# x ∈# X. (x, y) ∉ s#} ⊆# X1 + X2'"
using *(1) **(2) by (auto simp: X2'_def multiset_eq_iff intro!: mset_subset_eqI split: if_splits)
show ?thesis
using mult2_alt_nsI[OF refl refl *(3) x3, THEN subset_mult2_alt[OF x4], of True] **(1,2) *(2)
by (auto simp: diff_union_single_conv[symmetric])
qed
next
assume ?R1
then obtain y where *: "y ∈# Y" "(x, y) ∈ s" "({# x ∈# X. (x, y) ∉ s #}, Y - {#y#}) ∈ mult2_alt_ns ns s"
by blast
then have **: "({# x ∈# X. (x, y) ∈ s #} + {#x#}, {#y#}) ∈ mult2_alt b ns s"
"{# x ∈# X. (x, y) ∉ s #} + {# x ∈# X. (x, y) ∈ s #} = X"
by (auto intro: mult2_altI[of _ "{#}" _ _ "{#}"] multiset_eqI split: if_splits)
show ?L using mult2_alt_add[OF *(3) **(1)] * ** by (auto simp: union_assoc[symmetric])
next
assume ?R2
then obtain y where *: "y ∈# Y" "(x, y) ∈ ns" "(X, Y - {#y#}) ∈ mult2_alt b ns s" by blast
then show ?L using mult2_alt_add[OF *(3) multpw_implies_mult2_alt_ns, of "{#x#}" "{#y#}"]
by (auto intro: multpw_single)
qed
subsection ‹Executable version›
text ‹Auxiliary version with an extra @{typ bool} argument for distinguishing between the
non-strict and the strict orders›
context fixes nss :: "'a ⇒ 'a ⇒ bool ⇒ bool"
begin
fun mult2_impl0 :: "'a list ⇒ 'a list ⇒ bool ⇒ bool"
and mult2_ex_dom0 :: "'a ⇒ 'a list ⇒ 'a list ⇒ 'a list ⇒ bool ⇒ bool"
where
"mult2_impl0 [] [] b ⟷ b"
| "mult2_impl0 xs [] b ⟷ False"
| "mult2_impl0 [] ys b ⟷ True"
| "mult2_impl0 (x # xs) ys b ⟷ mult2_ex_dom0 x xs ys [] b"
| "mult2_ex_dom0 x xs [] ys' b ⟷ False"
| "mult2_ex_dom0 x xs (y # ys) ys' b ⟷
nss x y False ∧ mult2_impl0 (filter (λx. ¬ nss x y False) xs) (ys @ ys') True ∨
nss x y True ∧ ¬ nss x y False ∧ mult2_impl0 xs (ys @ ys') b ∨
mult2_ex_dom0 x xs ys (y # ys') b"
end
lemma mult2_impl0_sound:
fixes nss
defines "ns ≡ {(x, y). nss x y True}" and "s ≡ {(x, y). nss x y False}"
shows "mult2_impl0 nss xs ys b ⟷ (mset xs, mset ys) ∈ mult2_alt b ns s"
"mult2_ex_dom0 nss x xs ys ys' b ⟷
(∃y. y ∈# mset ys ∧ (x, y) ∈ s ∧ (mset (filter (λx. (x, y) ∉ s) xs), mset (ys @ ys') - {#y#}) ∈ mult2_alt True ns s) ∨
(∃y. y ∈# mset ys ∧ (x, y) ∈ ns ∧ (x, y) ∉ s ∧ (mset xs, mset (ys @ ys') - {#y#}) ∈ mult2_alt b ns s)"
proof (induct xs ys b and x xs ys ys' b taking: nss rule: mult2_impl0_mult2_ex_dom0.induct)
case (4 x xs y ys b) show ?case unfolding mult2_impl0.simps 4
using mult2_alt_addL[of x "mset xs" "mset (y # ys)" b ns s] by (simp add: mset_filter)
next
case (6 x xs y ys ys' b) show ?case unfolding mult2_ex_dom0.simps 6
using subset_mult2_alt[of "mset [x←xs . (x, y) ∉ s]" "mset xs" "mset (ys @ ys')" b ns s True]
apply (intro iffI; elim disjE conjE exE; simp add: mset_filter ns_def s_def; (elim disjE)?)
subgoal by (intro disjI1 exI[of _ y]) auto
subgoal by (intro disjI2 exI[of _ y]) auto
subgoal for y' by (intro disjI1 exI[of _ y']) auto
subgoal for y' by (intro disjI2 exI[of _ y']) auto
subgoal for y' by simp
subgoal for y' by (rule disjI2, rule disjI2, rule disjI1, rule exI[of _ y']) simp
subgoal for y' by simp
subgoal for y' by (rule disjI2, rule disjI2, rule disjI2, rule exI[of _ y']) simp
done
qed (auto simp: mult2_alt_emptyL mult2_alt_emptyR)
text ‹Now, instead of functions of type @{typ "bool ⇒ bool"}, use pairs of type
@{typ "bool × bool"}›
definition [simp]: "or2 a b = (fst a ∨ fst b, snd a ∨ snd b)"
context fixes sns :: "'a ⇒ 'a ⇒ bool × bool"
begin
fun mult2_impl :: "'a list ⇒ 'a list ⇒ bool × bool"
and mult2_ex_dom :: "'a ⇒ 'a list ⇒ 'a list ⇒ 'a list ⇒ bool × bool"
where
"mult2_impl [] [] = (False, True)"
| "mult2_impl xs [] = (False, False)"
| "mult2_impl [] ys = (True, True)"
| "mult2_impl (x # xs) ys = mult2_ex_dom x xs ys []"
| "mult2_ex_dom x xs [] ys' = (False, False)"
| "mult2_ex_dom x xs (y # ys) ys' =
(case sns x y of
(True, _) ⇒ if snd (mult2_impl (filter (λx. ¬ fst (sns x y)) xs) (ys @ ys')) then (True, True)
else mult2_ex_dom x xs ys (y # ys')
| (False, True) ⇒ or2 (mult2_impl xs (ys @ ys')) (mult2_ex_dom x xs ys (y # ys'))
| _ ⇒ mult2_ex_dom x xs ys (y # ys'))"
end
lemma mult2_impl_sound0:
defines "pair ≡ λf. (f False, f True)" and "fun ≡ λp b. if b then snd p else fst p"
shows "mult2_impl sns xs ys = pair (mult2_impl0 (λx y. fun (sns x y)) xs ys)" (is ?P)
"mult2_ex_dom sns x xs ys ys' = pair (mult2_ex_dom0 (λx y. fun (sns x y)) x xs ys ys')" (is ?Q)
proof -
show ?P ?Q
proof (induct xs ys and x xs ys ys' taking: sns rule: mult2_impl_mult2_ex_dom.induct)
case (6 x xs y ys ys')
show ?case unfolding mult2_ex_dom.simps mult2_ex_dom0.simps
by (fastforce simp: pair_def fun_def 6 if_bool_eq_conj split: prod.splits bool.splits)
qed (auto simp: pair_def fun_def if_bool_eq_conj)
qed
lemmas mult2_impl_sound = mult2_impl_sound0[unfolded mult2_impl0_sound if_True if_False]
end