Theory Multiset_Extension_Pair_Impl

subsection ‹Executable version›

theory Multiset_Extension_Pair_Impl
  imports 
    Multiset_Extension_Pair
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
  define Y11 Y12 X2 where "Y11 = Y1 ∩# X" and "Y12 = Y1 - X" and "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) le_diff_conv 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 mem_multiset_diff: "x ∈# A ⟹ x ≠ y ⟹ x ∈# (A - {#y#})" 
  by (metis add_mset_remove_trivial_If diff_single_trivial insert_noteq_member)

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
      define X2' where "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
    define X2' where "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) 
    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

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(1)[unfolded mult2_impl0_sound if_True if_False]
end