Theory Propositional_Logic_Class.List_Utilities

chapter ‹ List Utility Theorems ›

theory List_Utilities
  imports
    "HOL-Combinatorics.List_Permutation"
begin

text ‹ Throughout our work it will be necessary to reuse common lemmas
       regarding lists and multisets. These results are proved in the
       following section and reused by subsequent lemmas and theorems. ›

section ‹ Multisets ›

lemma length_sub_mset:
  assumes "mset Ψ ⊆# mset Γ"
      and "length Ψ >= length Γ"
    shows "mset Ψ = mset Γ"
  using assms
  by (metis
        append_Nil2
        append_eq_append_conv
        leD
        linorder_neqE_nat
        mset_le_perm_append
        perm_length
        size_mset
        size_mset_mono)

lemma set_exclusion_mset_simplify:
  assumes "¬ ( ψ  set Ψ. ψ  set Σ)"
      and "mset Ψ ⊆# mset (Σ @ Γ)"
    shows "mset Ψ ⊆# mset Γ"
using assms
proof (induct Σ)
  case Nil
  then show ?case by simp
next
  case (Cons σ Σ)
  then show ?case
    by (cases "σ  set Ψ",
        fastforce,
        metis
          add.commute
          add_mset_add_single
          diff_single_trivial
          in_multiset_in_set
          mset.simps(2)
          notin_set_remove1
          remove_hd
          subset_eq_diff_conv
          union_code
          append_Cons)
qed

lemma image_mset_cons_homomorphism:
  "image_mset mset (image_mset ((#) φ) Φ) = image_mset ((+) {# φ #}) (image_mset mset Φ)"
  by (induct Φ, simp+)

lemma image_mset_append_homomorphism:
  "image_mset mset (image_mset ((@) Δ) Φ) = image_mset ((+) (mset Δ)) (image_mset mset Φ)"
  by (induct Φ, simp+)

lemma image_mset_add_collapse:
  fixes A B :: "'a multiset"
  shows "image_mset ((+) A) (image_mset ((+) B) X) = image_mset ((+) (A + B)) X"
  by (induct X, simp, simp)

lemma remove1_remdups_removeAll: "remove1 x (remdups A) = remdups (removeAll x A)"
proof (induct A)
  case Nil
  then show ?case by simp
next
  case (Cons a A)
  then show ?case
    by (cases "a = x", (simp add: Cons)+)
qed

lemma mset_remdups:
  assumes "mset A = mset B"
  shows "mset (remdups A) = mset (remdups B)"
proof -
  have " B. mset A = mset B  mset (remdups A) = mset (remdups B)"
  proof (induct A)
    case Nil
    then show ?case by simp
  next
    case (Cons a A)
    {
      fix B
      assume "mset (a # A) = mset B"
      hence "mset A = mset (remove1 a B)"
        by (metis add_mset_add_mset_same_iff
                  list.set_intros(1)
                  mset.simps(2)
                  mset_eq_setD
                  perm_remove)
      hence "mset (remdups A) = mset (remdups (remove1 a B))"
        using Cons.hyps by blast
      hence "mset (remdups (a # (remdups A))) = mset (remdups (a # (remdups (remove1 a B))))"
        by (metis mset_eq_setD set_eq_iff_mset_remdups_eq list.simps(15))
      hence "  mset (remdups (a # (removeAll a (remdups A))))
             = mset (remdups (a # (removeAll a (remdups (remove1 a B)))))"
        by (metis insert_Diff_single list.set(2) set_eq_iff_mset_remdups_eq set_removeAll)
      hence "  mset (remdups (a # (remdups (removeAll a A))))
             = mset (remdups (a # (remdups (removeAll a (remove1 a B)))))"
        by (metis distinct_remdups distinct_remove1_removeAll remove1_remdups_removeAll)
      hence "mset (remdups (remdups (a # A))) = mset (remdups (remdups (a # (remove1 a B))))"
        by (metis mset A = mset (remove1 a B)
                  list.set(2)
                  mset_eq_setD
                  set_eq_iff_mset_remdups_eq)
      hence "mset (remdups (a # A)) = mset (remdups (a # (remove1 a B)))"
        by (metis remdups_remdups)
      hence "mset (remdups (a # A)) = mset (remdups B)"
        using mset (a # A) = mset B mset_eq_setD set_eq_iff_mset_remdups_eq by blast
    }
    then show ?case by simp
  qed
  thus ?thesis using assms by blast
qed

lemma mset_mset_map_snd_remdups:
  assumes "mset (map mset A) = mset (map mset B)"
  shows "mset (map (mset  (map snd)  remdups) A) = mset (map (mset  (map snd)  remdups) B)"
proof -
  {
    fix B :: "('a × 'b) list list"
    fix b :: "('a × 'b) list"
    assume "b  set B"
    hence "  mset (map (mset  (map snd)  remdups) (b # (remove1 b B)))
         = mset (map (mset  (map snd)  remdups) B)"
    proof (induct B)
      case Nil
      then show ?case by simp
    next
      case (Cons b' B)
      then show ?case
      by (cases "b = b'", simp+)
    qed
  }
  note  = this
  have
    " B :: ('a × 'b) list list.
     mset (map mset A) = mset (map mset B)
        mset (map (mset  (map snd)  remdups) A) = mset (map (mset  (map snd)  remdups) B)"
  proof (induct A)
    case Nil
    then show ?case by simp
  next
    case (Cons a A)
    {
      fix B
      assume : "mset (map mset (a # A)) = mset (map mset B)"
      hence "mset a ∈# mset (map mset B)"
        by (simp,
            metis 
                  image_set
                  list.set_intros(1)
                  list.simps(9)
                  mset_eq_setD)
      from this obtain b where :
        "b  set B"
        "mset a = mset b"
        by auto
      with  have "mset (map mset A) = mset (remove1 (mset b) (map mset B))"
        by (simp add: union_single_eq_diff)
      moreover have "mset B = mset (b # remove1 b B)" using  by simp
      hence "mset (map mset B) = mset (map mset (b # (remove1 b B)))"
        by (simp,
            metis image_mset_add_mset
                  mset.simps(2)
                  mset_remove1)
      ultimately have "mset (map mset A) = mset (map mset (remove1 b B))"
        by simp
      hence "  mset (map (mset  (map snd)  remdups) A)
             = mset (map (mset  (map snd)  remdups) (remove1 b B))"
        using Cons.hyps by blast
      moreover have "(mset  (map snd)  remdups) a = (mset  (map snd)  remdups) b"
        using (2) mset_remdups by fastforce
      ultimately have
        "  mset (map (mset  (map snd)  remdups) (a # A))
         = mset (map (mset  (map snd)  remdups) (b # (remove1 b B)))"
        by simp
      moreover have
        "  mset (map (mset  (map snd)  remdups) (b # (remove1 b B)))
         = mset (map (mset  (map snd)  remdups) B)"
        using (1)  by blast
      ultimately have
        "  mset (map (mset  (map snd)  remdups) (a # A))
         = mset (map (mset  (map snd)  remdups) B)"
        by simp
    }
    then show ?case by blast
  qed
  thus ?thesis using assms by blast
qed

lemma mset_remdups_append_msub:
  "mset (remdups A) ⊆# mset (remdups (B @ A))"
proof -
  have " B. mset (remdups A) ⊆# mset (remdups (B @ A))"
  proof (induct A)
    case Nil
    then show ?case by simp
  next
    case (Cons a A)
    {
      fix B
      have : "mset (remdups (B @ (a # A))) = mset (remdups (a # (B @ A)))"
        by (induct B, simp+)
      have "mset (remdups (a # A)) ⊆# mset (remdups (B @ (a # A)))"
      proof (cases "a  set B  a  set A")
        case True
        hence : "mset (remove1 a (remdups (B @ A))) = mset (remdups ((removeAll a B) @ A))"
          by (simp add: remove1_remdups_removeAll)
        hence "   (add_mset a (mset (remdups A)) ⊆# mset (remdups (B @ A)))
               = (mset (remdups A) ⊆# mset (remdups ((removeAll a B) @ A)))"
          using True
          by (simp add: insert_subset_eq_iff)
        then show ?thesis
          by (metis  Cons True
                    Un_insert_right
                    list.set(2)
                    mset.simps(2)
                    mset_subset_eq_insertD
                    remdups.simps(2)
                    set_append
                    set_eq_iff_mset_remdups_eq
                    set_mset_mset set_remdups)
      next
        case False
        then show ?thesis using  Cons by simp
      qed
    }
    thus ?case by blast
  qed
  thus ?thesis by blast
qed

section ‹ List Mapping ›

text ‹ The following notation for permutations is slightly nicer when
       formatted in \LaTeX. ›

notation perm (infix "" 50)

lemma map_monotonic:
  assumes "mset A ⊆# mset B"
  shows "mset (map f A) ⊆# mset (map f B)"
  by (simp add: assms image_mset_subseteq_mono)

lemma perm_map_perm_list_exists:
  assumes "A  map f B"
  shows " B'. A = map f B'  B'  B"
proof -
  have "B. A  map f B  ( B'. A = map f B'  B'  B)"
  proof (induct A)
    case Nil
    then show ?case by simp
  next
    case (Cons a A)
    {
      fix B
      assume "a # A  map f B"
      from this obtain b where b:
        "b  set B"
        "f b = a"
        by (metis
              (full_types)
              imageE
              list.set_intros(1)
              set_map
              set_mset_mset)
      hence "A  (remove1 (f b) (map f B))"
            "B  b # remove1 b B"
        by (metis
              a # A  map f B
              perm_remove_perm
              remove_hd,
            meson b(1) perm_remove)
      hence "A  (map f (remove1 b B))"
        by (metis (no_types)
              list.simps(9)
              mset_map
              mset_remove1
              remove_hd)
      from this obtain B' where B':
        "A = map f B'"
        "B'  (remove1 b B)"
        using Cons.hyps by blast
      with b have "a # A = map f (b # B')"
        by simp
      moreover have "B  b # B'"
        by (metis B'(2) mset B = mset (b # remove1 b B) mset.simps(2))
      ultimately have "B'. a # A = map f B'  B'  B"
        by (meson perm_sym)
    }
    thus ?case by blast
  qed
  with assms show ?thesis by blast
qed

lemma mset_sub_map_list_exists:
  assumes "mset Φ ⊆# mset (map f Γ)"
  shows " Φ'. mset Φ' ⊆# mset Γ  Φ = (map f Φ')"
proof -
  have " Φ. mset Φ ⊆# mset (map f Γ)
               ( Φ'. mset Φ' ⊆# mset Γ  Φ = (map f Φ'))"
  proof (induct Γ)
    case Nil
    then show ?case by simp
  next
    case (Cons γ Γ)
    {
      fix Φ
      assume "mset Φ ⊆# mset (map f (γ # Γ))"
      have "Φ'. mset Φ' ⊆# mset (γ # Γ)  Φ = map f Φ'"
      proof cases
        assume "f γ  set Φ"
        hence "f γ # (remove1 (f γ) Φ)  Φ"
          by force
        with mset Φ ⊆# mset (map f (γ # Γ))
        have "mset (remove1 (f γ) Φ) ⊆# mset (map f Γ)"
          by (metis
                 insert_subset_eq_iff
                 list.simps(9)
                 mset.simps(2)
                 mset_remove1
                 remove_hd)
        from this Cons obtain Φ' where Φ':
          "mset Φ' ⊆# mset Γ"
          "remove1 (f γ) Φ = map f Φ'"
          by blast
        hence "mset (γ # Φ') ⊆# mset (γ # Γ)"
          and "f γ # (remove1 (f γ) Φ) = map f (γ # Φ')"
          by simp+
        hence "Φ  map f (γ # Φ')"
          using f γ  set Φ perm_remove
          by metis
        from this obtain Φ'' where Φ'':
          "Φ = map f Φ''"
          "Φ''  γ # Φ'"
          using perm_map_perm_list_exists
          by blast
        hence "mset Φ'' ⊆# mset (γ # Γ)"
          by (metis mset (γ # Φ') ⊆# mset (γ # Γ))
        thus ?thesis using Φ'' by blast
      next
        assume "f γ  set Φ"
        have "mset Φ - {#f γ#} = mset Φ"
          by (metis (no_types)
                f γ  set Φ
                diff_single_trivial
                set_mset_mset)
        moreover
        have "mset (map f (γ # Γ))
                = add_mset (f γ) (image_mset f (mset Γ))"
          by simp
        ultimately have "mset Φ ⊆# mset (map f Γ)"
          by (metis (no_types)
                Diff_eq_empty_iff_mset
                mset Φ ⊆# mset (map f (γ # Γ))
                add_mset_add_single
                cancel_ab_semigroup_add_class.diff_right_commute
                diff_diff_add mset_map)
        with Cons show ?thesis
          by (metis
                mset_le_perm_append
                perm_append_single
                subset_mset.order_trans)
      qed
    }
    thus ?case using Cons by blast
  qed
  thus ?thesis using assms by blast
qed

section ‹ Laws for Searching a List ›

lemma find_Some_predicate:
  assumes "find P Ψ = Some ψ"
  shows "P ψ"
  using assms
proof (induct Ψ)
  case Nil
  then show ?case by simp
next
  case (Cons ω Ψ)
  then show ?case by (cases "P ω", fastforce+)
qed

lemma find_Some_set_membership:
  assumes "find P Ψ = Some ψ"
  shows "ψ  set Ψ"
  using assms
proof (induct Ψ)
  case Nil
  then show ?case by simp
next
  case (Cons ω Ψ)
  then show ?case by (cases "P ω", fastforce+)
qed

section ‹ Permutations ›

lemma perm_count_list:
  assumes "Φ  Ψ"
  shows "count_list Φ φ = count_list Ψ φ"
  using assms
proof (induct Φ arbitrary: Ψ)
  case Nil
  then show ?case
    by blast
next
  case (Cons χ Φ Ψ)
  hence : "count_list Φ φ = count_list (remove1 χ Ψ) φ"
    by (metis mset_remove1 remove_hd)
  show ?case
  proof cases
    assume "χ = φ"
    hence "count_list (χ # Φ) φ = count_list Φ φ + 1" by simp
    with  have "count_list (χ # Φ) φ = count_list (remove1 χ Ψ) φ + 1"
      by simp
    moreover
    have "χ  set Ψ"
      by (metis Cons.prems list.set_intros(1) set_mset_mset)
    hence "count_list (remove1 χ Ψ) φ + 1 = count_list Ψ φ"
      using χ = φ
      by (induct Ψ, simp, auto)
    ultimately show ?thesis by simp
  next
    assume "χ  φ"
    with  have "count_list (χ # Φ) φ = count_list (remove1 χ Ψ) φ"
      by simp
    moreover have "count_list (remove1 χ Ψ) φ = count_list Ψ φ"
      using χ  φ
      by (induct Ψ, simp+)
    ultimately show ?thesis by simp
  qed
qed

lemma count_list_append:
  "count_list (A @ B) a = count_list A a + count_list B a"
  by (induct A, simp, simp)

lemma concat_remove1:
  assumes "Ψ  set "
  shows "concat   Ψ @ concat (remove1 Ψ )"
    using assms
    by (induct , simp, simp, metis)

lemma concat_set_membership_mset_containment:
  assumes "concat Γ  Λ"
  and     "Φ  set Γ"
  shows   "mset Φ ⊆# mset Λ"
  using assms
  by (induct Γ, simp, simp, metis concat_remove1 mset_le_perm_append)

lemma (in comm_monoid_add) perm_list_summation:
  assumes "Ψ  Φ"
  shows "(ψ'Ψ. f ψ') = (φ'Φ. f φ')"
  using assms
proof (induct Ψ arbitrary: Φ)
  case Nil
  then show ?case by auto
next
  case (Cons ψ Ψ Φ)
  hence "(ψ'  Ψ. f ψ') = (φ'  (remove1 ψ Φ). f φ')"
    by (metis mset_remove1 remove_hd)
  moreover have "ψ  set Φ"
    by (metis Cons.prems list.set_intros(1) set_mset_mset)
  hence "(φ'  (ψ # (remove1 ψ Φ)). f φ') = (φ'Φ. f φ')"
  proof (induct Φ)
    case Nil
    then show ?case by auto
  next
    case (Cons φ Φ)
    show ?case
    proof cases
      assume "φ = ψ"
      then show ?thesis by simp
    next
      assume "φ  ψ"
      hence "ψ  set Φ"
        using Cons.prems by auto
      hence "(φ'  (ψ # (remove1 ψ Φ)). f φ') = (φ'Φ. f φ')"
        using Cons.hyps by blast
      hence "(φ'(φ # Φ). f φ')
                = (φ'  (ψ # φ # (remove1 ψ Φ)). f φ')"
        by (simp add: add.left_commute)
      moreover
      have "(ψ # (φ # (remove1 ψ Φ))) = (ψ # (remove1 ψ (φ # Φ)))"
        using φ  ψ by simp
      ultimately show ?thesis
        by simp
    qed
  qed
  ultimately show ?case
    by simp
qed

section ‹ List Duplicates ›

primrec duplicates :: "'a list  'a set"
  where
    "duplicates [] = {}"
  | "duplicates (x # xs) =
       (if (x  set xs)
        then insert x (duplicates xs)
        else duplicates xs)"

lemma duplicates_subset:
  "duplicates Φ  set Φ"
  by (induct Φ, simp, auto)

lemma duplicates_alt_def:
  "duplicates xs = {x. count_list xs x  2}"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  assume inductive_hypothesis: "duplicates xs = {x. 2  count_list xs x}"
  then show ?case
  proof cases
    assume "x  set xs"
    hence "count_list (x # xs) x  2"
      by (simp, induct xs, simp, simp, blast)
    hence "{y. 2  count_list (x # xs) y}
              = insert x {y. 2  count_list xs y}"
      by (simp,  blast)
    thus ?thesis using inductive_hypothesis x  set xs
      by simp
  next
    assume "x  set xs"
    hence "{y. 2  count_list (x # xs) y} = {y. 2  count_list xs y}"
      by (simp, auto)
    thus ?thesis using inductive_hypothesis x  set xs
      by simp
  qed
qed

section ‹ List Subtraction ›

primrec list_subtract :: "'a list  'a list  'a list" (infixl "" 70)
  where
      "xs  [] = xs"
    | "xs  (y # ys) = (remove1 y (xs  ys))"

lemma list_subtract_mset_homomorphism [simp]:
  "mset (A  B) = mset A - mset B"
  by (induct B, simp, simp)

lemma list_subtract_empty [simp]:
  "[]  Φ = []"
  by (induct Φ, simp, simp)

lemma list_subtract_remove1_cons_perm:
  "Φ  (φ # Λ)  (remove1 φ Φ)  Λ"
  by (induct Λ, simp, simp add: add_mset_commute)

lemma list_subtract_cons:
  assumes "φ  set Λ"
  shows "(φ # Φ)  Λ = φ # (Φ  Λ)"
  using assms
  by (induct Λ, simp, simp, blast)

lemma list_subtract_cons_absorb:
  assumes "count_list Φ φ  count_list Λ φ"
  shows "φ # (Φ  Λ)  (φ # Φ)  Λ"
  using assms
proof (induct Λ arbitrary: Φ)
  case Nil
  then show ?case using list_subtract_cons by fastforce
next
  case (Cons ψ Λ Φ)
  then show ?case
  proof cases
    assume "φ = ψ"
    hence "φ  set Φ"
      using Cons.prems count_notin by force
    hence "Φ  φ # (remove1 ψ Φ)"
      unfolding φ = ψ
      by force
    thus ?thesis using perm_count_list
      by (metis
            (no_types, lifting)
            Cons.hyps
            Cons.prems
            φ = ψ
            add_le_cancel_right
            add_mset_diff_bothsides
            count_list.simps(2)
            list_subtract_mset_homomorphism
            mset.simps(2))
  next
    assume "φ  ψ"
    hence "count_list (ψ # Λ) φ = count_list Λ φ"
       by simp
    moreover have "count_list Φ φ = count_list (remove1 ψ Φ) φ"
    proof (induct Φ)
      case Nil
      then show ?case by simp
    next
      case (Cons φ' Φ)
      show ?case
      proof cases
        assume "φ' = φ"
        with φ  ψ
        have "count_list (φ' # Φ) φ = 1 + count_list Φ φ"
             "count_list (remove1 ψ (φ' # Φ)) φ
                = 1 + count_list (remove1 ψ Φ) φ"
          by simp+
        with Cons show ?thesis by linarith
      next
        assume "φ'  φ"
        with Cons show ?thesis by (cases "φ' = ψ", simp+)
      qed
    qed
    ultimately show ?thesis
      using count_list (ψ # Λ) φ  count_list Φ φ
      by (metis
            Cons.hyps
            φ  ψ
            list_subtract_remove1_cons_perm
            mset.simps(2)
            remove1.simps(2))
  qed
qed

lemma list_subtract_cons_remove1_perm:
  assumes "φ  set Λ"
  shows "(φ # Φ)  Λ  Φ  (remove1 φ Λ)"
  using assms
  by (metis
        list_subtract_mset_homomorphism
        list_subtract_remove1_cons_perm
        perm_remove
        remove_hd)

lemma list_subtract_removeAll_perm:
  assumes "count_list Φ φ  count_list Λ φ"
  shows "Φ  Λ  (removeAll φ Φ)  (removeAll φ Λ)"
  using assms
proof (induct Φ arbitrary: Λ)
  case Nil
  then show ?case by auto
next
  case (Cons ξ Φ Λ)
  hence "Φ  Λ  (removeAll φ Φ)  (removeAll φ Λ)"
    by (metis add_leE count_list.simps(2))
  show ?case
  proof cases
    assume "ξ = φ"
    hence "count_list Φ φ < count_list Λ φ"
      using count_list (ξ # Φ) φ  count_list Λ φ
      by auto
    hence "count_list Φ φ  count_list (remove1 φ Λ) φ"
      by (induct Λ, simp, auto)
    hence "Φ  (remove1 φ Λ)
              removeAll φ Φ  removeAll φ (remove1 φ Λ)"
      using Cons.hyps by blast
    hence "Φ  (remove1 φ Λ)  removeAll φ Φ  removeAll φ Λ"
      by (simp add: filter_remove1 removeAll_filter_not_eq)
    moreover have "φ  set Λ" and "φ  set (φ # Φ)"
      using ξ = φ
            count_list (ξ # Φ) φ  count_list Λ φ
            gr_implies_not0
      by fastforce+
    hence "(φ # Φ)  Λ  (remove1 φ (φ # Φ))  (remove1 φ Λ)"
      by (metis list_subtract_cons_remove1_perm remove_hd)

    hence "(φ # Φ)  Λ  Φ  (remove1 φ Λ)" by simp
    ultimately show ?thesis using ξ = φ by auto
  next
    assume "ξ  φ"
    show ?thesis
    proof cases
      assume "ξ  set Λ"
      hence "(ξ # Φ)  Λ  Φ  remove1 ξ Λ"
        by (meson list_subtract_cons_remove1_perm)
      moreover have "count_list Λ φ = count_list (remove1 ξ Λ) φ"
        by (metis
              count_list.simps(2)
              ξ  φ
              ξ  set Λ
              perm_count_list
              perm_remove)
      hence "count_list Φ φ  count_list (remove1 ξ Λ) φ"
        using ξ  φ count_list (ξ # Φ) φ  count_list Λ φ by auto
      hence "Φ  remove1 ξ Λ
                (removeAll φ Φ)  (removeAll φ (remove1 ξ Λ))"
        using Cons.hyps by blast
      moreover
      have "(removeAll φ Φ)  (removeAll φ (remove1 ξ Λ)) 
              (removeAll φ Φ)  (remove1 ξ (removeAll φ Λ))"
        by (induct Λ,
              simp,
              metis
                ξ  φ
                list_subtract.simps(2)
                mset_remove1
                remove1.simps(2)
                removeAll.simps(2))
      hence "(removeAll φ Φ)  (removeAll φ (remove1 ξ Λ)) 
               (removeAll φ (ξ # Φ))  (removeAll φ Λ)"
        by (metis
              ξ  set Λ
              ξ  φ
              list_subtract_cons_remove1_perm
              member_remove removeAll.simps(2)
              remove_code(1))
      ultimately show ?thesis
        by presburger
    next
      assume "ξ  set Λ"
      hence "(ξ # Φ)  Λ  ξ # (Φ  Λ)"
        by fastforce
      hence "(ξ # Φ)  Λ  ξ # ((removeAll φ Φ)  (removeAll φ Λ))"
        using Φ  Λ  removeAll φ Φ  removeAll φ Λ
        by simp
      hence "(ξ # Φ)  Λ  (ξ # (removeAll φ Φ))  (removeAll φ Λ)"
        by (simp add: ξ  set Λ list_subtract_cons)
      thus ?thesis using ξ  φ by auto
    qed
  qed
qed

lemma list_subtract_permute:
  assumes "Φ  Ψ"
  shows "Φ  Λ  Ψ  Λ"
  using assms
  by simp

lemma append_perm_list_subtract_intro:
  assumes "A  B @ C"
  shows "A  C  B"
proof -
  from A  B @ C have "mset (A  C) = mset B"
    by simp
  thus ?thesis by blast
qed

lemma list_subtract_concat:
  assumes "Ψ  set "
  shows "concat (  [Ψ])  (concat )  Ψ"
  using assms
  by (simp add: concat_remove1)

lemma (in comm_monoid_add) listSubstract_multisubset_list_summation:
  assumes "mset Ψ ⊆# mset Φ"
  shows "(ψΨ. f ψ) + (φ'(Φ  Ψ). f φ') = (φ'Φ. f φ')"
proof -
  have " Φ. mset Ψ ⊆# mset Φ
           (ψ'Ψ. f ψ') + (φ'(Φ  Ψ). f φ') = (φ'Φ. f φ')"
  proof(induct Ψ)
    case Nil
    then show ?case
      by simp
  next
    case (Cons ψ Ψ)
    {
      fix Φ
      assume hypothesis: "mset (ψ # Ψ) ⊆# mset Φ"
      hence "mset Ψ ⊆# mset (remove1 ψ Φ)"
        by (metis append_Cons mset_le_perm_append perm_remove_perm remove_hd)
      hence
        "(ψ'  Ψ. f ψ') + (φ'((remove1 ψ Φ)  Ψ). f φ')
               = (φ' (remove1 ψ Φ). f φ')"
        using Cons.hyps by blast
      moreover have "(remove1 ψ Φ)  Ψ  Φ  (ψ # Ψ)"
        by (meson list_subtract_remove1_cons_perm perm_sym)
      hence "(φ'((remove1 ψ Φ)  Ψ). f φ') = (φ'(Φ  (ψ # Ψ)). f φ')"
        using perm_list_summation by blast
      ultimately have
        "(ψ'  Ψ. f ψ') + (φ'(Φ  (ψ # Ψ)). f φ')
               = (φ' (remove1 ψ Φ). f φ')"
        by simp
      hence
        "(ψ'  (ψ # Ψ). f ψ') + (φ'(Φ  (ψ # Ψ)). f φ')
               = (φ' (ψ # (remove1 ψ Φ)). f φ')"
        by (simp add: add.assoc)
      moreover have "ψ  set Φ"
        by (metis
              append_Cons
              hypothesis
              list.set_intros(1)
              mset_le_perm_append
              perm_set_eq)
      hence "(ψ # (remove1 ψ Φ))  Φ"
        by auto
      hence "(φ'  (ψ # (remove1 ψ Φ)). f φ') = (φ'Φ. f φ')"
        using perm_list_summation by blast
      ultimately have
        "(ψ'  (ψ # Ψ). f ψ') + (φ'(Φ  (ψ # Ψ)). f φ')
               = (φ'Φ. f φ')"
        by simp
    }
    then show ?case
      by blast
  qed
  with assms show ?thesis by blast
qed

lemma list_subtract_set_difference_lower_bound:
  "set Γ - set Φ  set (Γ  Φ)"
  using subset_Diff_insert
  by (induct Φ, simp, fastforce)

lemma list_subtract_set_trivial_upper_bound:
  "set (Γ  Φ)  set Γ"
      by (induct Φ,
          simp,
          simp,
          meson
            dual_order.trans
            set_remove1_subset)

lemma list_subtract_msub_eq:
  assumes "mset Φ ⊆# mset Γ"
      and "length (Γ  Φ) = m"
    shows "length Γ = m + length Φ"
  using assms
proof -
  have " Γ. mset Φ ⊆# mset Γ
            length (Γ  Φ) = m --> length Γ = m + length Φ"
  proof (induct Φ)
    case Nil
    then show ?case by simp
  next
    case (Cons φ Φ)
    {
      fix Γ :: "'a list"
      assume "mset (φ # Φ) ⊆# mset Γ"
             "length (Γ  (φ # Φ)) = m"
      moreover from this have
        "mset Φ ⊆# mset (remove1 φ Γ)"
        "mset (Γ  (φ # Φ)) = mset ((remove1 φ Γ)  Φ)"
        by (metis
              append_Cons
              mset_le_perm_append
              perm_remove_perm
              remove_hd,
            simp)
      ultimately have "length (remove1 φ Γ) = m + length Φ"
        using Cons.hyps
        by (metis mset_eq_length)
      hence "length (φ # (remove1 φ Γ)) = m + length (φ # Φ)"
        by simp
      moreover have "φ  set Γ"
        by (metis
              mset (Γ  (φ # Φ)) = mset (remove1 φ Γ  Φ)
              mset (φ # Φ) ⊆# mset Γ
              mset Φ ⊆# mset (remove1 φ Γ)
              add_diff_cancel_left'
              add_right_cancel
              eq_iff
              impossible_Cons
              list_subtract_mset_homomorphism
              mset_subset_eq_exists_conv
              remove1_idem size_mset)
      hence "length (φ # (remove1 φ Γ)) = length Γ"
        by (metis
              One_nat_def
              Suc_pred
              length_Cons
              length_pos_if_in_set
              length_remove1)
      ultimately have "length Γ = m + length (φ # Φ)" by simp
    }
    thus ?case by blast
  qed
  thus ?thesis using assms by blast
qed

lemma list_subtract_not_member:
  assumes "b  set A"
  shows "A  B = A  (remove1 b B)"
  using assms
  by (induct B,
      simp,
      simp,
      metis
        add_mset_add_single
        diff_subset_eq_self
        insert_DiffM2
        insert_subset_eq_iff
        list_subtract_mset_homomorphism
        remove1_idem
        set_mset_mset)

lemma list_subtract_monotonic:
  assumes "mset A ⊆# mset B"
  shows "mset (A  C) ⊆# mset (B  C)"
  by (simp,
      meson
        assms
        subset_eq_diff_conv
        subset_mset.dual_order.refl
        subset_mset.order_trans)

lemma map_list_subtract_mset_containment:
  "mset ((map f A)  (map f B)) ⊆# mset (map f (A  B))"
  by (induct B, simp, simp,
      metis
        diff_subset_eq_self
        diff_zero
        image_mset_add_mset
        image_mset_subseteq_mono
        image_mset_union
        subset_eq_diff_conv
        subset_eq_diff_conv)

lemma map_list_subtract_mset_equivalence:
  assumes "mset B ⊆# mset A"
  shows "mset ((map f A)  (map f B)) = mset (map f (A  B))"
  using assms
  by (induct B, simp, simp add: image_mset_Diff)

lemma msub_list_subtract_elem_cons_msub:
  assumes "mset Ξ ⊆# mset Γ"
      and "ψ  set (Γ  Ξ)"
    shows "mset (ψ # Ξ) ⊆# mset Γ"
proof -
  have " Γ. mset Ξ ⊆# mset Γ
              ψ  set (Γ  Ξ) --> mset (ψ # Ξ) ⊆# mset Γ"
  proof(induct Ξ)
    case Nil
    then show ?case by simp
  next
    case (Cons ξ Ξ)
    {
      fix Γ
      assume
        "mset (ξ # Ξ) ⊆# mset Γ"
        "ψ  set (Γ  (ξ # Ξ))"
      hence
         "ξ  set Γ"
         "mset Ξ ⊆# mset (remove1 ξ Γ)"
         "ψ  set ((remove1 ξ Γ)  Ξ)"
        by (simp,
            metis
              ex_mset
              list.set_intros(1)
              mset.simps(2)
              mset_eq_setD
              subset_mset.le_iff_add
              union_mset_add_mset_left,
            metis
              list_subtract.simps(1)
              list_subtract.simps(2)
              list_subtract_monotonic
              remove_hd,
            simp,
            metis
              list_subtract_remove1_cons_perm
              perm_set_eq)
      with Cons.hyps have
        "mset Γ = mset (ξ # (remove1 ξ Γ))"
        "mset (ψ # Ξ) ⊆# mset (remove1 ξ Γ)"
        by (simp, blast)
      hence "mset (ψ # ξ # Ξ) ⊆# mset Γ"
        by (simp,
            metis
              add_mset_commute
              mset_subset_eq_add_mset_cancel)
    }
    then show ?case by auto
  qed
  thus ?thesis using assms by blast
qed

section ‹ Tuple Lists ›

lemma remove1_pairs_list_projections_fst:
  assumes "(γ,σ) ∈# mset Φ"
  shows "mset (map fst (remove1 (γ, σ) Φ)) = mset (map fst Φ) - {# γ #}"
using assms
proof (induct Φ)
  case Nil
  then show ?case by simp
next
  case (Cons φ Φ)
  assume "(γ, σ) ∈# mset (φ # Φ)"
  show ?case
  proof (cases "φ = (γ, σ)")
    assume "φ = (γ, σ)"
    then show ?thesis by simp
  next
    assume "φ  (γ, σ)"
    then have "add_mset φ (mset Φ - {#(γ, σ)#})
             = add_mset φ (mset Φ) - {#(γ, σ)#}"
        by force
    then have "add_mset (fst φ) (image_mset fst (mset Φ - {#(γ, σ)#}))
                = add_mset (fst φ) (image_mset fst (mset Φ)) - {#γ#}"
      by (metis (no_types) Cons.prems
                           add_mset_remove_trivial
                           fst_conv
                           image_mset_add_mset
                           insert_DiffM mset.simps(2))
    with φ  (γ, σ) show ?thesis
      by simp
  qed
qed

lemma remove1_pairs_list_projections_snd:
  assumes "(γ,σ) ∈# mset Φ"
  shows "mset (map snd (remove1 (γ, σ) Φ)) = mset (map snd Φ) - {# σ #}"
using assms
proof (induct Φ)
  case Nil
  then show ?case by simp
next
  case (Cons φ Φ)
  assume "(γ, σ) ∈# mset (φ # Φ)"
  show ?case
  proof (cases "φ = (γ, σ)")
    assume "φ = (γ, σ)"
    then show ?thesis by simp
  next
    assume "φ  (γ, σ)"
    then have "add_mset (snd φ) (image_mset snd (mset Φ - {#(γ, σ)#}))
             = image_mset snd (mset (φ # Φ) - {#(γ, σ)#})"
      by auto
    moreover have "add_mset (snd φ) (image_mset snd (mset Φ))
                 = add_mset σ (image_mset snd (mset (φ # Φ) - {#(γ, σ)#}))"
      by (metis (no_types)
             Cons.prems
             image_mset_add_mset
             insert_DiffM
             mset.simps(2)
             snd_conv)
    ultimately
    have "add_mset (snd φ) (image_mset snd (mset Φ - {#(γ, σ)#}))
                = add_mset (snd φ) (image_mset snd (mset Φ)) - {#σ#}"
      by simp
    with φ  (γ, σ) show ?thesis
      by simp
  qed
qed

lemma triple_list_exists:
  assumes "mset (map snd Ψ) ⊆# mset Σ"
      and "mset Σ ⊆# mset (map snd Δ)"
    shows " Ω. map (λ (ψ, σ, _). (ψ, σ)) Ω = Ψ 
                mset (map (λ (_, σ, γ). (γ, σ)) Ω) ⊆# mset Δ"
  using assms(1)
proof (induct Ψ)
  case Nil
  then show ?case by fastforce
next
  case (Cons ψ Ψ)
  from Cons obtain Ω where Ω:
    "map (λ (ψ, σ, _). (ψ, σ)) Ω = Ψ"
    "mset (map (λ (_, σ, γ). (γ, σ)) Ω) ⊆# mset Δ"
    by (metis
          (no_types, lifting)
          diff_subset_eq_self
          list.set_intros(1)
          remove1_pairs_list_projections_snd
          remove_hd
          set_mset_mset
          subset_mset.dual_order.trans
          surjective_pairing)
  let Ω = "map (λ (_, σ, γ). (γ, σ)) Ω"
  let  = "fst ψ"
  let  = "snd ψ"
  from Cons.prems have "add_mset  (image_mset snd (mset Ψ)) ⊆# mset Σ"
    by simp
  then have "mset Σ - {##} - image_mset snd (mset Ψ)
                 mset Σ - image_mset snd (mset Ψ)"
    by (metis
          (no_types)
          insert_subset_eq_iff
          mset_subset_eq_insertD
          multi_drop_mem_not_eq
          subset_mset.diff_add
          subset_mset_def)
  hence " ∈# mset Σ - mset (map snd Ψ)"
    using diff_single_trivial by fastforce
  have "mset (map snd (ψ # Ψ)) ⊆# mset (map snd Δ)"
    by (meson
          Cons.prems
          mset Σ ⊆# mset (map snd Δ)
          subset_mset.dual_order.trans)
  then have
    "mset (map snd Δ) - mset (map snd (ψ # Ψ)) + ({#} + {#snd ψ#})
       = mset (map snd Δ) + ({#} + {#snd ψ#})
           - add_mset (snd ψ) (mset (map snd Ψ))"
    by (metis
          (no_types)
          list.simps(9)
          mset.simps(2)
          mset_subset_eq_multiset_union_diff_commute)
  then have
    "mset (map snd Δ) - mset (map snd (ψ # Ψ)) + ({#} + {#snd ψ#})
       = mset (map snd Δ) - mset (map snd Ψ)"
    by auto
  hence " ∈# mset (map snd Δ) - mset (map snd Ψ)"
    using add_mset_remove_trivial_eq by fastforce
  moreover have "snd  (λ (ψ, σ, _). (ψ, σ)) = snd  (λ (_, σ, γ). (γ, σ))"
    by auto
  hence "map snd (Ω) = map snd (map (λ (ψ, σ, _). (ψ, σ)) Ω)"
    by fastforce
  hence "map snd (Ω) = map snd Ψ"
    using Ω(1) by simp
  ultimately have " ∈# mset (map snd Δ) - mset (map snd Ω)"
    by simp
  hence " ∈# image_mset snd (mset Δ - mset Ω)"
    using Ω(2) by (metis image_mset_Diff mset_map)
  hence "  snd ` set_mset (mset Δ - mset Ω)"
    by (metis in_image_mset)
  from this obtain ρ where ρ:
    "snd ρ = " "ρ ∈# mset Δ - mset Ω"
    using imageE by auto
  from this obtain γ where
    "(γ, ) = ρ"
    by (metis prod.collapse)
  with ρ(2) have γ: "(γ, ) ∈# mset Δ - mset Ω" by auto
  let  = "(, , γ) # Ω"
  have "map (λ (ψ, σ, _). (ψ, σ))  = ψ # Ψ"
    using Ω(1) by simp
  moreover
  have A: "(γ, snd ψ) = (case (snd ψ, γ) of (a, c)  (c, a))"
    by auto
  have B: "mset (map (λ(b, a, c). (c, a)) Ω)
             + {# case (snd ψ, γ) of (a, c)  (c, a) #}
           = mset (map (λ(b, a, c). (c, a)) ((fst ψ, snd ψ, γ) # Ω))"
    by simp
  obtain mm
     :: "('c × 'a) multiset
      ('c × 'a) multiset
      ('c × 'a) multiset"
    where "x0 x1. (v2. x0 = x1 + v2) = (x0 = x1 + mm x0 x1)"
    by moura
  then have "mset Δ = mset (map (λ(b, a, c). (c, a)) Ω)
                        + mm (mset Δ) (mset (map (λ(b, a, c). (c, a)) Ω))"
    by (metis Ω(2) subset_mset.le_iff_add)
  then have "mset (map (λ (_, σ, γ). (γ, σ)) ) ⊆# mset Δ"
    using A B by
      (metis
         γ
         add_diff_cancel_left'
         single_subset_iff
         subset_mset.add_le_cancel_left)
  ultimately show ?case by meson
qed

section ‹ List Intersection ›

primrec list_intersect :: "'a list => 'a list => 'a list"  (infixl "" 60)
  where
    "_  [] = []"
  | "xs  (y # ys) =
        (if (y  set xs)
         then (y # (remove1 y xs  ys))
         else (xs  ys))"

lemma list_intersect_mset_homomorphism [simp]:
  "mset (Φ  Ψ) = mset Φ ∩# mset Ψ"
proof -
  have " Φ. mset (Φ  Ψ) = mset Φ ∩# mset Ψ"
  proof (induct Ψ)
    case Nil
    then show ?case by simp
  next
    case (Cons ψ Ψ)
    {
      fix Φ
      have "mset (Φ  ψ # Ψ) = mset Φ ∩# mset (ψ # Ψ)"
        using Cons.hyps
        by (cases "ψ  set Φ",
            simp add: inter_add_right2,
            simp add: inter_add_right1)
    }
    then show ?case by blast
  qed
  thus ?thesis by simp
qed

lemma list_intersect_left_empty [simp]: "[]  Φ = []" by (induct Φ, simp+)

lemma list_diff_intersect_comp:
  "mset Φ = mset (Φ  Ψ) + mset (Φ  Ψ)"
  by (metis
        diff_intersect_left_idem
        list_intersect_mset_homomorphism
        list_subtract_mset_homomorphism
        subset_mset.inf_le1
        subset_mset.le_imp_diff_is_add)

lemma list_intersect_left_project: "mset (Φ  Ψ) ⊆# mset Φ"
  by simp

lemma list_intersect_right_project: "mset (Φ  Ψ) ⊆# mset Ψ"
  by simp

end