Theory WB_List_More

theory WB_List_More
  imports "HOL-Library.Finite_Map"
    Nested_Multisets_Ordinals.Duplicate_Free_Multiset
    "HOL-Eisbach.Eisbach"
    "HOL-Eisbach.Eisbach_Tools"
    "HOL-Library.FuncSet"
begin
text ‹This theory contains various lemmas that have been used in the formalisation. Some of them
could probably be moved to the Isabelle distribution or
\<^theory>‹Nested_Multisets_Ordinals.Multiset_More›.
›
text ‹More Sledgehammer parameters›
(* sledgehammer_params[debug] *)

section ‹Various Lemmas›

subsection ‹Not-Related to Refinement or lists›

text ‹
  Unlike clarify/auto/simp, this does not split tuple of the form \<^term>‹∃T. P T› in the assumption.
  After calling it, as the variable are not quantified anymore, the simproc does not trigger,
  allowing to safely call auto/simp/...
›
method normalize_goal =
  (match premises in
    J[thin]: ‹∃x. _› ⇒ ‹rule exE[OF J]›
  ¦ J[thin]: ‹_ ∧ _› ⇒ ‹rule conjE[OF J]›
  )

text ‹Close to the theorem @{thm [source] nat_less_induct} (@{thm nat_less_induct}), but with a
  separation between the zero and non-zero case.›
lemma nat_less_induct_case[case_names 0 Suc]:
  assumes
    ‹P 0› and
    ‹⋀n. (∀m < Suc n. P m) ⟹ P (Suc n)›
  shows ‹P n›
  apply (induction rule: nat_less_induct)
  by (rename_tac n, case_tac n) (auto intro: assms)

text ‹This is only proved in simple cases by auto. In assumptions, nothing happens, and
  the theorem @{thm [source] if_split_asm} can blow up goals (because of other if-expressions either
  in the context or as simplification rules).›
lemma if_0_1_ge_0[simp]:
  ‹0 < (if P then a else (0::nat)) ⟷ P ∧ 0 < a›
  by auto

lemma bex_lessI: "P j ⟹ j < n ⟹ ∃j<n. P j"
  by auto

lemma bex_gtI: "P j ⟹ j > n ⟹ ∃j>n. P j"
  by auto

lemma bex_geI: "P j ⟹ j ≥ n ⟹ ∃j≥n. P j"
  by auto

lemma bex_leI: "P j ⟹ j ≤ n ⟹ ∃j≤n. P j"
  by auto

text ‹Bounded function have not yet been defined in Isabelle.›
definition bounded :: "('a ⇒ 'b::ord) ⇒ bool" where
‹bounded f ⟷ (∃b. ∀n. f n ≤ b)›

abbreviation unbounded :: ‹('a ⇒ 'b::ord) ⇒ bool› where
‹unbounded f ≡ ¬ bounded f›

lemma not_bounded_nat_exists_larger:
  fixes f :: ‹nat ⇒ nat›
  assumes unbound: ‹unbounded f›
  shows ‹∃n. f n > m ∧ n > n⇩0›
proof (rule ccontr)
  assume H: ‹¬ ?thesis›
  have ‹finite {f n|n. n ≤ n⇩0}›
    by auto
  have ‹⋀n. f n ≤ Max ({f n|n. n ≤ n⇩0} ∪ {m})›
    apply (case_tac ‹n ≤ n⇩0›)
    apply (metis (mono_tags, lifting) Max_ge Un_insert_right ‹finite {f n |n. n ≤ n⇩0}›
      finite_insert insertCI mem_Collect_eq sup_bot.right_neutral)
    by (metis (no_types, lifting) H Max_less_iff Un_insert_right ‹finite {f n |n. n ≤ n⇩0}›
      finite_insert insertI1 insert_not_empty leI sup_bot.right_neutral)
  then show False
    using unbound unfolding bounded_def by auto
qed

text ‹A function is bounded iff its product with a non-zero constant is bounded. The non-zero
  condition is needed only for the reverse implication (see for example @{term ‹k = (0::nat)›} and
  @{term ‹f = (λi. i)›} for a counter-example).›
lemma bounded_const_product:
  fixes k :: nat and f :: ‹nat ⇒ nat›
  assumes ‹k > 0›
  shows ‹bounded f ⟷ bounded (λi. k * f i)›
  unfolding bounded_def apply (rule iffI)
  using mult_le_mono2 apply blast
  by (metis Suc_leI add.right_neutral assms mult.commute mult_0_right mult_Suc_right mult_le_mono
      nat_mult_le_cancel1)

lemma bounded_const_add:
  fixes k :: nat and f :: ‹nat ⇒ nat›
  assumes ‹k > 0›
  shows ‹bounded f ⟷ bounded (λi. k + f i)›
  unfolding bounded_def apply (rule iffI)
   using nat_add_left_cancel_le apply blast
  using add_leE by blast

text ‹This lemma is not used, but here to show that property that can be expected from
  @{term bounded} holds.›
lemma bounded_finite_linorder:
  fixes f :: ‹'a::finite ⇒ 'b :: {linorder}›
  shows ‹bounded f›
proof -
  have ‹finite (f ` UNIV)›
    by simp
  then have ‹⋀x. f x ≤ Max (f ` UNIV)›
    by (auto intro: Max_ge)
  then show ?thesis
    unfolding bounded_def by blast
qed


section ‹More Lists›

subsection ‹set, nth, tl›

lemma ex_geI: ‹P n ⟹ n ≥ m ⟹ ∃n≥m. P n›
  by auto

lemma Ball_atLeastLessThan_iff: ‹(∀L∈{a..<b}. P L) ⟷ (∀L. L ≥ a ∧ L < b ⟶ P L) ›
  unfolding set_nths by auto

lemma nth_in_set_tl: ‹i > 0 ⟹ i < length xs ⟹ xs ! i ∈ set (tl xs)›
  by (cases xs) auto

lemma tl_drop_def: ‹tl N = drop 1 N›
  by (cases N) auto

lemma in_set_remove1D:
  ‹a ∈ set (remove1 x xs) ⟹ a ∈ set xs›
  by (meson notin_set_remove1)

lemma take_length_takeWhile_eq_takeWhile:
  ‹take (length (takeWhile P xs)) xs = takeWhile P xs›
  by (induction xs) auto

lemma fold_cons_replicate: ‹fold (λ_ xs. a # xs) [0..<n] xs = replicate n a @ xs›
  by (induction n) auto

lemma Collect_minus_single_Collect: ‹{x. P x} - {a} = {x . P x ∧ x ≠ a}›
  by auto

lemma in_set_image_subsetD: ‹ f ` A ⊆ B ⟹ x ∈ A ⟹f x ∈ B›
  by blast

lemma mset_tl:
  ‹mset (tl xs) = remove1_mset (hd xs) (mset xs)›
  by (cases xs) auto

lemma hd_list_update_If:
  ‹outl' ≠ [] ⟹ hd (outl'[i := w]) = (if i = 0 then w else hd outl')›
  by (cases outl') (auto split: nat.splits)

lemma list_update_id':
  ‹x = xs ! i ⟹ xs[i := x] = xs›
  by auto


text ‹
  This lemma is not general enough to move to Isabelle, but might be interesting in other
  cases.›
lemma set_Collect_Pair_to_fst_snd:
  ‹{((a, b), (a', b')). P a b a' b'} = {(e, f). P (fst e) (snd e) (fst f) (snd f)}›
  by auto

lemma butlast_Nil_iff: ‹butlast xs = [] ⟷ length xs = 1 ∨ length xs = 0›
  by (cases xs) auto

lemma Set_remove_diff_insert: ‹a ∈ B - A ⟹ B - Set.remove a A = insert a (B - A)›
  by auto

lemma Set_insert_diff_remove: ‹B - insert a A = Set.remove a (B - A)›
  by auto

lemma Set_remove_insert: ‹a ∉ A' ⟹ Set.remove a (insert a A') = A'›
  by (auto simp: Set.remove_def)

lemma diff_eq_insertD:
  ‹B - A = insert a A' ⟹ a ∈ B›
  by auto

lemma in_set_tlD: ‹x ∈ set (tl xs) ⟹ x ∈ set xs›
  by (cases xs) auto

text ‹This lemmma is only useful if \<^term>‹set xs› can be simplified (which also means that this
  simp-rule should not be used...)›
lemma (in -) in_list_in_setD: ‹xs = it @ x # σ ⟹ x ∈ set xs›
  by auto

lemma Collect_eq_comp': ‹ {(x, y). P x y} O {(c, a). c = f a} = {(x, a). P x (f a)}›
  by auto

lemma (in -) filter_disj_eq:
  ‹{x ∈ A. P x ∨ Q x} = {x ∈ A. P x} ∪ {x ∈ A. Q x}›
  by auto


lemma zip_cong:
  ‹(⋀i. i < min (length xs) (length ys) ⟹ (xs ! i, ys ! i) = (xs' ! i, ys' ! i)) ⟹
     length xs = length xs' ⟹ length ys = length ys' ⟹ zip xs ys = zip xs' ys'›
proof (induction xs arbitrary: xs' ys' ys)
  case Nil
  then show ?case by auto
next
  case (Cons x xs xs' ys' ys) note IH = this(1) and eq = this(2) and p = this(3-)
thm IH
  have ‹zip xs (tl ys) = zip (tl xs') (tl ys')› for i
    apply (rule IH)
    subgoal for i
      using p eq[of ‹Suc i›] by (auto simp: nth_tl)
    subgoal using p by auto
    subgoal using p by auto
    done
  moreover have ‹hd xs' = x› ‹hd ys = hd ys'› if ‹ys ≠ []›
    using eq[of 0] that p[symmetric] apply (auto simp: hd_conv_nth)
    apply (subst hd_conv_nth)
    apply auto
    apply (subst hd_conv_nth)
    apply auto
    done
  ultimately show ?case
    using p by (cases xs'; cases ys'; cases ys)
      auto
qed

lemma zip_cong2:
  ‹(⋀i. i < min (length xs) (length ys) ⟹ (xs ! i, ys ! i) = (xs' ! i, ys' ! i)) ⟹
     length xs = length xs' ⟹ length ys ≤ length ys' ⟹ length ys ≥ length xs ⟹
     zip xs ys = zip xs' ys'›
proof (induction xs arbitrary: xs' ys' ys)
  case Nil
  then show ?case by auto
next
  case (Cons x xs xs' ys' ys) note IH = this(1) and eq = this(2) and p = this(3-)
  have ‹zip xs (tl ys) = zip (tl xs') (tl ys')› for i
    apply (rule IH)
    subgoal for i
      using p eq[of ‹Suc i›] by (auto simp: nth_tl)
    subgoal using p by auto
    subgoal using p by auto
    subgoal using p by auto
    done
  moreover have ‹hd xs' = x› ‹hd ys = hd ys'› if ‹ys ≠ []›
    using eq[of 0] that p apply (auto simp: hd_conv_nth)
    apply (subst hd_conv_nth)
    apply auto
    apply (subst hd_conv_nth)
    apply auto
    done
  ultimately show ?case
    using p by (cases xs'; cases ys'; cases ys)
      auto
qed


subsection ‹List Updates›

lemma tl_update_swap:
  ‹i ≥ 1 ⟹ tl (N[i := C]) = (tl N)[i-1 := C]›
  by (auto simp:  drop_Suc[of 0, symmetric, simplified] drop_update_swap)

lemma tl_update_0[simp]: ‹tl (N[0 := x]) = tl N›
  by (cases N) auto

declare nth_list_update[simp]
text ‹
  This a version of @{thm nth_list_update} with a different condition (\<^term>‹j›
  instead of \<^term>‹i›). This is more useful in some cases.
  ›
lemma nth_list_update_le'[simp]:
  "j < length xs ⟹ (xs[i:=x])!j = (if i = j then x else xs!j)"
  by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)


subsection ‹Take and drop›

lemma take_2_if:
  ‹take 2 C = (if C = [] then [] else if length C = 1 then [hd C] else [C!0, C!1])›
  by (cases C; cases ‹tl C›) auto


lemma in_set_take_conv_nth:
  ‹x ∈ set (take n xs) ⟷ (∃m<min n (length xs). xs ! m = x)›
  by (metis in_set_conv_nth length_take min.commute min.strict_boundedE nth_take)

lemma in_set_dropI:
  ‹m < length xs ⟹ m ≥ n ⟹ xs ! m ∈ set (drop n xs)›
  unfolding in_set_conv_nth
  by (rule exI[of _ ‹m - n›]) auto

lemma in_set_drop_conv_nth:
  ‹x ∈ set (drop n xs) ⟷ (∃m ≥ n. m < length xs ∧ xs ! m = x)›
  apply (rule iffI)
  subgoal
    apply (subst (asm) in_set_conv_nth)
    apply clarsimp
    apply (rule_tac x = ‹n+i› in exI)
    apply (auto)
    done
  subgoal
    by (auto intro: in_set_dropI)
  done

text ‹Taken from the Word library.›
lemma atd_lem: ‹take n xs = t ⟹ drop n xs = d ⟹ xs = t @ d›
  by (auto intro: append_take_drop_id [symmetric])

lemma drop_take_drop_drop:
  ‹j ≥ i ⟹ drop i xs = take (j - i) (drop i xs) @ drop j xs›
  apply (induction ‹j - i› arbitrary: j i)
  subgoal by auto
  subgoal by (auto simp add: atd_lem)
  done

lemma in_set_conv_iff:
  ‹x ∈ set (take n xs) ⟷ (∃i < n. i < length xs ∧ xs ! i = x)›
  apply (induction n)
  subgoal by auto
  subgoal for n
    apply (cases ‹Suc n < length xs›)
    subgoal by (auto simp: take_Suc_conv_app_nth less_Suc_eq dest: in_set_takeD)
    subgoal
      apply (cases ‹n < length xs›)
      subgoal
        apply (auto simp: in_set_conv_nth)
        by (rule_tac x=i in exI; auto; fail)+
      subgoal
        apply (auto simp: take_Suc_conv_app_nth dest: in_set_takeD)
        by (rule_tac x=i in exI; auto; fail)+
      done
    done
  done

lemma distinct_in_set_take_iff:
  ‹distinct D ⟹ b < length D ⟹ D ! b ∈ set (take a D) ⟷ b < a›
  apply (induction a arbitrary: b)
  subgoal by simp
  subgoal for a
    by (cases ‹Suc a < length D›)
      (auto simp: take_Suc_conv_app_nth nth_eq_iff_index_eq)
  done

lemma in_set_distinct_take_drop_iff:
  assumes
    ‹distinct D› and
    ‹b < length D›
  shows ‹D ! b ∈ set (take (a - init) (drop init D)) ⟷ (init ≤ b ∧ b < a)›
  using assms apply (auto 5 5 simp: distinct_in_set_take_iff in_set_conv_iff
      nth_eq_iff_index_eq dest: in_set_takeD)
  by (metis add_diff_cancel_left' diff_less_mono le_iff_add)


subsection ‹Replicate›

lemma list_eq_replicate_iff_nempty:
  ‹n > 0 ⟹ xs = replicate n x ⟷ n = length xs ∧ set xs = {x}›
  by (metis length_replicate neq0_conv replicate_length_same set_replicate singletonD)

lemma list_eq_replicate_iff:
  ‹xs = replicate n x ⟷ (n = 0 ∧ xs = []) ∨ (n = length xs ∧ set xs = {x})›
  by (cases n) (auto simp: list_eq_replicate_iff_nempty simp del: replicate.simps)


subsection ‹List intervals (@{term upt})›

text ‹
  The simplification rules are not very handy, because theorem @{thm [source] upt.simps(2)}
  (i.e.\ @{thm upt.simps(2)}) leads to a case distinction, that we usually do not want if the
  condition is not already in the context.
›
lemma upt_Suc_le_append: ‹¬i ≤ j ⟹ [i..<Suc j] = []›
  by auto

lemmas upt_simps[simp] = upt_Suc_append upt_Suc_le_append

declare upt.simps(2)[simp del]

text ‹The counterpart for this lemma when @{term ‹i > n-m›} is theorem @{thm [source] take_all}. It
  is close to theorem @{thm take_upt}, but seems more general.›
lemma take_upt_bound_minus[simp]:
  assumes ‹i ≤ n - m›
  shows ‹take i [m..<n] = [m ..<m+i]›
  using assms by (induction i) auto

lemma append_cons_eq_upt:
  assumes ‹A @ B = [m..<n]›
  shows ‹A = [m ..<m+length A]› and ‹B = [m + length A..<n]›
proof -
  have ‹take (length A) (A @ B) = A› by auto
  moreover {
    have ‹length A ≤ n - m› using assms linear calculation by fastforce
    then have ‹take (length A) [m..<n] = [m ..<m+length A]› by auto }
  ultimately show ‹A = [m ..<m+length A]› using assms by auto
  show ‹B = [m + length A..<n]› using assms by (metis append_eq_conv_conj drop_upt)
qed

text ‹The converse of theorem @{thm [source] append_cons_eq_upt} does not hold, for example if @
  {term ‹B:: nat list›} is empty and @{term ‹A :: nat list›} is @{term ‹[0]›}:›
lemma ‹A @ B = [m..< n] ⟷ A = [m ..<m+length A] ∧ B = [m + length A..<n]›
oops

text ‹A more restrictive version holds:›
lemma ‹B ≠ [] ⟹ A @ B = [m..< n] ⟷ A = [m ..<m+length A] ∧ B = [m + length A..<n]›
  (is ‹?P ⟹ ?A = ?B›)
proof
  assume ?A then show ?B by (auto simp add: append_cons_eq_upt)
next
  assume ?P and ?B
  then show ?A using append_eq_conv_conj by fastforce
qed

lemma append_cons_eq_upt_length_i:
  assumes ‹A @ i # B = [m..<n]›
  shows ‹A = [m ..<i]›
proof -
  have ‹A = [m ..< m + length A]› using assms append_cons_eq_upt by auto
  have ‹(A @ i # B) ! (length A) = i› by auto
  moreover have ‹n - m = length (A @ i # B)›
    using assms length_upt by presburger
  then have ‹[m..<n] ! (length A) = m + length A› by simp
  ultimately have ‹i = m + length A› using assms by auto
  then show ?thesis using ‹A = [m ..< m + length A]› by auto
qed

lemma append_cons_eq_upt_length:
  assumes ‹A @ i # B = [m..<n]›
  shows ‹length A = i - m›
  using assms
proof (induction A arbitrary: m)
  case Nil
  then show ?case by (metis append_Nil diff_is_0_eq list.size(3) order_refl upt_eq_Cons_conv)
next
  case (Cons a A)
  then have A: ‹A @ i # B = [m + 1..<n]› by (metis append_Cons upt_eq_Cons_conv)
  then have ‹m < i› by (metis Cons.prems append_cons_eq_upt_length_i upt_eq_Cons_conv)
  with Cons.IH[OF A] show ?case by auto
qed

lemma append_cons_eq_upt_length_i_end:
  assumes ‹A @ i # B = [m..<n]›
  shows ‹B = [Suc i ..<n]›
proof -
  have ‹B = [Suc m + length A..<n]› using assms append_cons_eq_upt[of ‹A @ [i]› B m n] by auto
  have ‹(A @ i # B) ! (length A) = i› by auto
  moreover have ‹n - m = length (A @ i # B)›
    using assms length_upt by auto
  then have ‹[m..<n]! (length A) = m + length A› by simp
  ultimately have ‹i = m + length A› using assms by auto
  then show ?thesis using ‹B = [Suc m + length A..<n]› by auto
qed

lemma Max_n_upt: ‹Max (insert 0 {Suc 0..<n}) = n - Suc 0›
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n) note IH = this
  have i: ‹insert 0 {Suc 0..<Suc n} = insert 0 {Suc 0..< n} ∪ {n}› by auto
  show ?case using IH unfolding i by auto
qed

lemma upt_decomp_lt:
  assumes H: ‹xs @ i # ys @ j # zs = [m ..< n]›
  shows ‹i < j›
proof -
  have xs: ‹xs = [m ..< i]› and ys: ‹ys = [Suc i ..< j]› and zs: ‹zs = [Suc j ..< n]›
    using H by (auto dest: append_cons_eq_upt_length_i append_cons_eq_upt_length_i_end)
  show ?thesis
    by (metis append_cons_eq_upt_length_i_end assms lessI less_trans self_append_conv2
      upt_eq_Cons_conv upt_rec ys)
qed

lemma nths_upt_upto_Suc: ‹aa < length xs ⟹ nths xs {0..<Suc aa} = nths xs {0..<aa} @ [xs ! aa]›
  by (simp add: atLeast0LessThan take_Suc_conv_app_nth)


text ‹The following two lemmas are useful as simp rules for case-distinction. The case
  @{term ‹length l = 0›} is already simplified by default.›
lemma length_list_Suc_0:
  ‹length W = Suc 0 ⟷ (∃L. W = [L])›
  apply (cases W)
    apply (simp; fail)
  apply (rename_tac a W', case_tac W')
  apply auto
  done

lemma length_list_2: ‹length S = 2 ⟷ (∃a b. S = [a, b])›
  apply (cases S)
   apply (simp; fail)
  apply (rename_tac a S')
  apply (case_tac S')
  by simp_all

lemma finite_bounded_list:
  fixes b :: nat
  shows ‹finite {xs. length xs < s ∧ (∀i< length xs. xs ! i < b)}› (is ‹finite (?S s)›)
proof -
  have H: ‹finite {xs. set xs ⊆ {0..<b} ∧ length xs ≤ s}›
    by (rule finite_lists_length_le[of ‹{0..<b}› ‹s›]) auto
  show ?thesis
    by (rule finite_subset[OF _ H]) (auto simp: in_set_conv_nth)
qed

lemma last_in_set_dropWhile:
  assumes ‹∃L ∈ set (xs @ [x]). ¬P L›
  shows ‹x ∈ set (dropWhile P (xs @ [x]))›
  using assms by (induction xs) auto

lemma mset_drop_upto: ‹mset (drop a N) = {#N!i. i ∈# mset_set {a..<length N}#}›
proof (induction N arbitrary: a)
  case Nil
  then show ?case by simp
next
  case (Cons c N)
  have upt: ‹{0..<Suc (length N)} = insert 0 {1..<Suc (length N)}›
    by auto
  then have H: ‹mset_set {0..<Suc (length N)} = add_mset 0 (mset_set {1..<Suc (length N)})›
    unfolding upt by auto
  have mset_case_Suc: ‹{#case x of 0 ⇒ c | Suc x ⇒ N ! x . x ∈# mset_set {Suc a..<Suc b}#} =
    {#N ! (x-1) . x ∈# mset_set {Suc a..<Suc b}#}› for a b
    by (rule image_mset_cong) (auto split: nat.splits)
  have Suc_Suc: ‹{Suc a..<Suc b} = Suc ` {a..<b}› for a b
    by auto
  then have mset_set_Suc_Suc: ‹mset_set {Suc a..<Suc b} = {#Suc n. n ∈# mset_set {a..<b}#}› for a b
    unfolding Suc_Suc by (subst image_mset_mset_set[symmetric]) auto
  have *: ‹{#N ! (x-Suc 0) . x ∈# mset_set {Suc a..<Suc b}#} = {#N ! x . x ∈# mset_set {a..<b}#}›
    for a b
    by (auto simp add: mset_set_Suc_Suc)
  show ?case
    apply (cases a)
    using Cons[of 0] Cons by (auto simp: nth_Cons drop_Cons H mset_case_Suc *)
qed

lemma last_list_update_to_last:
  ‹last (xs[x := last xs]) = last xs›
  by (metis last_list_update list_update.simps(1))

lemma take_map_nth_alt_def: ‹take n xs = map ((!) xs) [0..<min n (length xs)]›
proof (induction xs rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc x xs) note IH = this
  show ?case
  proof (cases ‹n < length (xs @ [x])›)
    case True
    then show ?thesis
      using IH by (auto simp: min_def nth_append)
  next
    case False
    have [simp]:
      ‹map (λa. if a < length xs then xs ! a else [x] ! (a - length xs)) [0..<length xs] =
       map (λa. xs ! a) [0..<length xs]› for xs and x :: 'b
      by (rule map_cong) auto
    show ?thesis
      using IH False by (auto simp: nth_append min_def)
  qed
qed


subsection ‹Lexicographic Ordering›

lemma lexn_Suc:
  ‹(x # xs, y # ys) ∈ lexn r (Suc n) ⟷
  (length xs = n ∧ length ys = n) ∧ ((x, y) ∈ r ∨ (x = y ∧ (xs, ys) ∈ lexn r n))›
  by (auto simp: map_prod_def image_iff lex_prod_def)

lemma lexn_n:
  ‹n > 0 ⟹ (x # xs, y # ys) ∈ lexn r n ⟷
  (length xs = n-1 ∧ length ys = n-1) ∧ ((x, y) ∈ r ∨ (x = y ∧ (xs, ys) ∈ lexn r (n - 1)))›
  apply (cases n)
   apply simp
  by (auto simp: map_prod_def image_iff lex_prod_def)

text ‹
  There is some subtle point in the previous theorem explaining ∗‹why› it is useful. The term
  @{term ‹1::nat›} is converted to @{term ‹Suc 0::nat›}, but @{term ‹2::nat›} is not, meaning
  that @{term ‹1::nat›} is automatically simplified by default allowing the use of the default
  simplification rule @{thm [source] lexn.simps}. However, for 2 one additional simplification rule
  is required (see the proof of the theorem above).
›

lemma lexn2_conv:
  ‹([a, b], [c, d]) ∈ lexn r 2 ⟷ (a, c) ∈ r ∨ (a = c ∧ (b, d) ∈r)›
  by (auto simp: lexn_n simp del: lexn.simps(2))

lemma lexn3_conv:
  ‹([a, b, c], [a', b', c']) ∈ lexn r 3 ⟷
    (a, a') ∈ r ∨ (a = a' ∧ (b, b') ∈ r) ∨ (a = a' ∧ b = b' ∧ (c, c') ∈ r)›
  by (auto simp: lexn_n simp del: lexn.simps(2))

lemma prepend_same_lexn:
  assumes irrefl: ‹irrefl R›
  shows ‹(A @ B, A @ C) ∈ lexn R n ⟷ (B, C) ∈ lexn R (n - length A)› (is ‹?A ⟷ ?B›)
proof
  assume ?A
  then obtain xys x xs y ys where
    len_B: ‹length B = n - length A› and
    len_C: ‹length C = n - length A› and
    AB: ‹A @ B = xys @ x # xs› and
    AC: ‹A @ C = xys @ y # ys› and
    xy: ‹(x, y) ∈ R›
    by (auto simp: lexn_conv)
  have x_neq_y: ‹x ≠ y›
    using xy irrefl by (auto simp add: irrefl_def)
  then have ‹B = drop (length A) xys @ x # xs›
    using arg_cong[OF AB, of ‹drop (length A)›]
    apply (cases ‹length A - length xys›)
     apply (auto; fail)
    by (metis AB AC nth_append nth_append_length zero_less_Suc zero_less_diff)

  moreover have ‹C = drop (length A) xys @ y # ys›
    using arg_cong[OF AC, of ‹drop (length A)›] x_neq_y
    apply (cases ‹length A - length xys›)
     apply (auto; fail)
    by (metis AB AC nth_append nth_append_length zero_less_Suc zero_less_diff)
  ultimately show ?B
    using len_B[symmetric] len_C[symmetric] xy
    by (auto simp: lexn_conv)
next
  assume ?B
  then obtain xys x xs y ys where
    len_B: ‹length B = n - length A› and
    len_C: ‹length C = n - length A› and
    AB: ‹B = xys @ x # xs› and
    AC: ‹C = xys @ y # ys› and
    xy: ‹(x, y) ∈ R›
    by (auto simp: lexn_conv)
  define Axys where ‹Axys = A @ xys›

  have ‹A @ B = Axys @ x # xs›
    using AB Axys_def by auto

  moreover have ‹A @ C = Axys @ y # ys›
    using AC Axys_def by auto
  moreover have ‹Suc (length Axys + length xs) = n› and
    ‹length ys = length xs›
    using len_B len_C AB AC Axys_def by auto
  ultimately show ?A
    using len_B[symmetric] len_C[symmetric] xy
    by (auto simp: lexn_conv)
qed

lemma append_same_lexn:
  assumes irrefl: ‹irrefl R›
  shows ‹(B @ A , C @ A) ∈ lexn R n ⟷ (B, C) ∈ lexn R (n - length A)› (is ‹?A ⟷ ?B›)
proof
  assume ?A
  then obtain xys x xs y ys where
    len_B: ‹n = length B + length A› and
    len_C: ‹n = length C + length A› and
    AB: ‹B @ A = xys @ x # xs› and
    AC: ‹C @ A = xys @ y # ys› and
    xy: ‹(x, y) ∈ R›
    by (auto simp: lexn_conv)
  have x_neq_y: ‹x ≠ y›
    using xy irrefl by (auto simp add: irrefl_def)
  have len_C_B: ‹length C = length B›
    using len_B len_C by simp
  have len_B_xys: ‹length B > length xys›
    apply (rule ccontr)
    using arg_cong[OF AB, of ‹take (length B)›] arg_cong[OF AB, of ‹drop (length B)›]
      arg_cong[OF AC, of ‹drop (length C)›]  x_neq_y len_C_B
    by auto

  then have B: ‹B = xys @ x # take (length B - Suc (length xys)) xs›
    using arg_cong[OF AB, of ‹take (length B)›]
    by (cases ‹length B - length xys›) simp_all

  have C: ‹C = xys @ y # take (length C - Suc (length xys)) ys›
    using arg_cong[OF AC, of ‹take (length C)›] x_neq_y len_B_xys unfolding len_C_B[symmetric]
    by (cases ‹length C - length xys›)  auto
  show ?B
    using len_B[symmetric] len_C[symmetric] xy B C
    by (auto simp: lexn_conv)
next
  assume ?B
  then obtain xys x xs y ys where
    len_B: ‹length B = n - length A› and
    len_C: ‹length C = n - length A› and
    AB: ‹B = xys @ x # xs› and
    AC: ‹C = xys @ y # ys› and
    xy: ‹(x, y) ∈ R›
    by (auto simp: lexn_conv)
  define Ays Axs where ‹Ays = ys @ A› and‹Axs = xs @ A›

  have ‹B @ A = xys @ x # Axs›
    using AB Axs_def by auto

  moreover have ‹C @ A = xys @ y # Ays›
    using AC Ays_def by auto
  moreover have ‹Suc (length xys + length Axs) = n› and
    ‹length Ays = length Axs›
    using len_B len_C AB AC Axs_def Ays_def by auto
  ultimately show ?A
    using len_B[symmetric] len_C[symmetric] xy
    by (auto simp: lexn_conv)
qed

lemma irrefl_less_than [simp]: ‹irrefl less_than›
  by (auto simp: irrefl_def)


subsection ‹Remove›

subsubsection ‹More lemmas about remove›

lemma distinct_remove1_last_butlast:
  ‹distinct xs ⟹ xs ≠ [] ⟹ remove1 (last xs) xs = butlast xs›
  by (metis append_Nil2 append_butlast_last_id distinct_butlast not_distinct_conv_prefix
      remove1.simps(2) remove1_append)

lemma remove1_Nil_iff:
  ‹remove1 x xs = [] ⟷ xs = [] ∨ xs = [x]›
  by (cases xs) auto

lemma removeAll_upt:
  ‹removeAll k [a..<b] = (if k ≥ a ∧ k < b then [a..<k] @ [Suc k..<b] else [a..<b])›
  by (induction b) auto

lemma remove1_upt:
  ‹remove1 k [a..<b] = (if k ≥ a ∧ k < b then [a..<k] @ [Suc k..<b] else [a..<b])›
  by (subst distinct_remove1_removeAll) (auto simp: removeAll_upt)

lemma sorted_removeAll: ‹sorted C ⟹ sorted (removeAll k C)›
  by (metis map_ident removeAll_filter_not_eq sorted_filter)

lemma distinct_remove1_rev: ‹distinct xs ⟹ remove1 x (rev xs) = rev (remove1 x xs)›
  using split_list[of x xs]
  by (cases ‹x ∈ set xs›) (auto simp: remove1_append remove1_idem)


subsubsection ‹Remove under condition›

text ‹This function removes the first element such that the condition @{term f} holds. It
  generalises @{term List.remove1}.›
fun remove1_cond where
‹remove1_cond f [] = []› |
‹remove1_cond f (C' # L) = (if f C' then L else C' # remove1_cond f L)›

lemma ‹remove1 x xs = remove1_cond ((=) x) xs›
  by (induction xs) auto

lemma mset_map_mset_remove1_cond:
  ‹mset (map mset (remove1_cond (λL. mset L = mset a) C)) =
    remove1_mset (mset a) (mset (map mset C))›
  by (induction C) auto

text ‹We can also generalise @{term List.removeAll}, which is close to @{term List.filter}:›
fun removeAll_cond :: ‹('a ⇒ bool) ⇒ 'a list ⇒ 'a list› where
‹removeAll_cond f [] = []› |
‹removeAll_cond f (C' # L) = (if f C' then removeAll_cond f L else C' # removeAll_cond f L)›

lemma removeAll_removeAll_cond: ‹removeAll x xs = removeAll_cond ((=) x) xs›
  by (induction xs) auto

lemma removeAll_cond_filter: ‹removeAll_cond P xs = filter (λx. ¬P x) xs›
  by (induction xs) auto

lemma mset_map_mset_removeAll_cond:
  ‹mset (map mset (removeAll_cond (λb. mset b = mset a) C))
    = removeAll_mset (mset a) (mset (map mset C))›
  by (induction C) auto

lemma count_mset_count_list:
  ‹count (mset xs) x = count_list xs x›
  by (induction xs) auto

lemma length_removeAll_count_list:
  ‹length (removeAll x xs) = length xs - count_list xs x›
proof -
  have ‹length (removeAll x xs) = size (removeAll_mset x (mset xs))›
    by auto
  also have ‹… = size (mset xs) - count (mset xs) x›
    by (metis count_le_replicate_mset_subset_eq le_refl size_Diff_submset size_replicate_mset)
  also have ‹ … = length xs - count_list xs x›
    unfolding count_mset_count_list by simp
  finally show ?thesis .
qed

lemma removeAll_notin: ‹a ∉# A ⟹ removeAll_mset a A = A›
  using count_inI by force


subsubsection ‹Filter›

lemma distinct_filter_eq_if:
  ‹distinct C ⟹ length (filter ((=) L) C) = (if L ∈ set C then 1 else 0)›
  by (induction C) auto

lemma length_filter_update_true:
  assumes ‹i < length xs› and ‹P (xs ! i)›
  shows ‹length (filter P (xs[i := x])) = length (filter P xs) - (if P x then 0 else 1)›
  apply (subst (5) append_take_drop_id[of i, symmetric])
  using assms upd_conv_take_nth_drop[of i xs x] Cons_nth_drop_Suc[of i xs, symmetric]
  unfolding filter_append length_append
  by simp

lemma length_filter_update_false:
  assumes ‹i < length xs› and ‹¬P (xs ! i)›
  shows ‹length (filter P (xs[i := x])) = length (filter P xs) + (if P x then 1 else 0)›
  apply (subst (5) append_take_drop_id[of i, symmetric])
  using assms upd_conv_take_nth_drop[of i xs x] Cons_nth_drop_Suc[of i xs, symmetric]
  unfolding filter_append length_append
  by simp

lemma mset_set_mset_set_minus_id_iff:
  assumes ‹finite A›
  shows ‹mset_set A = mset_set (A - B) ⟷ (∀b ∈ B. b ∉ A)›
proof -
 have f1: "mset_set A = mset_set (A - B) ⟷ A - B = A"
    using assms by (metis (no_types) finite_Diff finite_set_mset_mset_set)
  then show ?thesis
    by blast
qed

lemma mset_set_eq_mset_set_more_conds:
  ‹finite {x. P x} ⟹ mset_set {x. P x} = mset_set {x. Q x ∧ P x} ⟷ (∀x. P x ⟶ Q x)›
  (is ‹?F ⟹ ?A ⟷ ?B›)
proof -
  assume ?F
  then have ‹?A ⟷ (∀x ∈ {x. P x}. x ∈ {x. Q x ∧ P x})›
    by (subst mset_set_eq_iff) auto
  also have ‹… ⟷ (∀x. P x ⟶ Q x)›
    by blast
  finally show ?thesis .
qed

lemma count_list_filter: ‹count_list xs x = length (filter ((=) x) xs)›
  by (induction xs) auto

lemma sum_length_filter_compl': ‹length [x←xs . ¬ P x] + length (filter P xs) = length xs›
  using sum_length_filter_compl[of P xs] by auto


subsection ‹Sorting›

text ‹See @{thm sorted_distinct_set_unique}.›
lemma sorted_mset_unique:
  fixes xs :: ‹'a :: linorder list›
  shows ‹sorted xs ⟹ sorted ys ⟹ mset xs = mset ys ⟹ xs = ys›
  using properties_for_sort by auto

lemma insort_upt: ‹insort k [a..<b] =
  (if k < a then k # [a..<b]
  else if k < b then [a..<k] @ k # [k ..<b]
  else [a..<b] @ [k])›
proof -
  have H: ‹k < Suc b ⟹ ¬ k < a ⟹ {a..<b} = {a..<k} ∪ {k..<b}› for a b :: nat
    by (simp add: ivl_disj_un_two(3))
  show ?thesis
  apply (induction b)
   apply (simp; fail)
  apply (case_tac ‹¬k < a ∧ k < Suc b›)
   apply (rule sorted_mset_unique)
      apply ((auto simp add: sorted_append sorted_insort ac_simps mset_set_Union
        dest!: H; fail)+)[2]
    apply (auto simp: insort_is_Cons sorted_insort_is_snoc sorted_append mset_set_Union
      ac_simps dest: H; fail)+
  done
qed

lemma removeAll_insert_removeAll: ‹removeAll k (insort k xs) = removeAll k xs›
  by (simp add: filter_insort_triv removeAll_filter_not_eq)

lemma filter_sorted: ‹sorted xs ⟹ sorted (filter P xs)›
  by (metis list.map_ident sorted_filter)

lemma removeAll_insort:
  ‹sorted xs ⟹ k ≠ k' ⟹ removeAll k' (insort k xs) = insort k (removeAll k' xs)›
  by (simp add: filter_insort removeAll_filter_not_eq)


subsection ‹Distinct Multisets›

lemma distinct_mset_remdups_mset_id: ‹distinct_mset C ⟹ remdups_mset C = C›
  by (induction C)  auto

lemma notin_add_mset_remdups_mset:
  ‹a ∉# A ⟹ add_mset a (remdups_mset A) = remdups_mset (add_mset a A)›
  by auto

lemma distinct_mset_image_mset:
  ‹distinct_mset (image_mset f (mset xs)) ⟷ distinct (map f xs)›
  apply (subst mset_map[symmetric])
  apply (subst distinct_mset_mset_distinct)
  ..

lemma distinct_image_mset_not_equal:
  assumes
    LL': ‹L ≠ L'› and
    dist: ‹distinct_mset (image_mset f M)› and
    L: ‹L ∈# M› and
    L': ‹L' ∈# M› and
    fLL'[simp]: ‹f L = f L'›
  shows ‹False›
proof -
  obtain M1 where M1: ‹M = add_mset L M1›
    using multi_member_split[OF L] by blast
  obtain M2 where M2: ‹M1 = add_mset L' M2›
    using multi_member_split[of L' M1] LL' L' unfolding M1 by (auto simp: add_mset_eq_add_mset)
  show False
    using dist unfolding M1 M2 by auto
qed

lemma distinct_mset_remdups_mset[simp]: ‹distinct_mset (remdups_mset S)›
  using count_remdups_mset_eq_1 unfolding distinct_mset_def by metis

lemma remdups_mset_idem: ‹remdups_mset (remdups_mset a) = remdups_mset a›
  using distinct_mset_remdups_mset distinct_mset_remdups_mset_id by fast


subsection ‹Set of Distinct Multisets›

definition distinct_mset_set :: ‹'a multiset set ⇒ bool› where
  ‹distinct_mset_set Σ ⟷ (∀S ∈ Σ. distinct_mset S)›

lemma distinct_mset_set_empty[simp]: ‹distinct_mset_set {}›
  unfolding distinct_mset_set_def by auto

lemma distinct_mset_set_singleton[iff]: ‹distinct_mset_set {A} ⟷ distinct_mset A›
  unfolding distinct_mset_set_def by auto

lemma distinct_mset_set_insert[iff]:
  ‹distinct_mset_set (insert S Σ) ⟷ (distinct_mset S ∧ distinct_mset_set Σ)›
  unfolding distinct_mset_set_def by auto

lemma distinct_mset_set_union[iff]:
  ‹distinct_mset_set (Σ ∪ Σ') ⟷ (distinct_mset_set Σ ∧ distinct_mset_set Σ')›
  unfolding distinct_mset_set_def by auto

lemma in_distinct_mset_set_distinct_mset:
  ‹a ∈ Σ ⟹ distinct_mset_set Σ ⟹ distinct_mset a›
  unfolding distinct_mset_set_def by auto

lemma distinct_mset_mset_set: ‹distinct_mset (mset_set A)›
  unfolding distinct_mset_def count_mset_set_if by (auto simp: not_in_iff)

lemma distinct_mset_filter_mset_set[simp]: ‹distinct_mset {#a ∈# mset_set A. P a#}›
  by (simp add: distinct_mset_filter distinct_mset_mset_set)

lemma distinct_mset_set_distinct: ‹distinct_mset_set (mset ` set Cs) ⟷ (∀c∈ set Cs. distinct c)›
  unfolding distinct_mset_set_def by auto


subsection ‹Sublists›

lemma nths_single_if: ‹nths l {n} = (if n < length l then [l!n] else [])›
proof -
  have [simp]: ‹0 < n ⟹ {j. Suc j = n} = {n-1}› for n
    by auto
  show ?thesis
    apply (induction l arbitrary: n)
    subgoal by (auto simp: nths_def)
    subgoal by (auto simp: nths_Cons)
    done
qed

lemma atLeastLessThan_Collect: ‹{a..<b} = {j. j ≥ a ∧ j < b}›
  by auto

lemma mset_nths_subset_mset: ‹mset (nths xs A) ⊆# mset xs›
  apply (induction xs arbitrary: A)
  subgoal by auto
  subgoal for a xs A
    using subset_mset.add_increasing2[of ‹add_mset _ {#}› ‹mset (nths xs {j. Suc j ∈ A})›
      ‹mset xs›]
    by (auto simp: nths_Cons)
  done

lemma nths_id_iff:
  ‹nths xs A = xs ⟷ {0..<length xs} ⊆ A ›
proof -
  have ‹{j. Suc j ∈ A} =  (λj. j-1) ` (A - {0})› for A
    using DiffI by (fastforce simp: image_iff)
  have 1: ‹{0..<b} ⊆ {j. Suc j ∈ A} ⟷ (∀x. x-1 < b ⟶ x ≠ 0 ⟶ x ∈ A)›
    for A :: ‹nat set› and b :: nat
    by auto
  have [simp]: ‹{0..<b} ⊆ {j. Suc j ∈ A} ⟷ (∀x. x-1 < b ⟶ x ∈ A)›
    if ‹0 ∈ A› for A :: ‹nat set› and b :: nat
    using that unfolding 1 by auto
  have [simp]: ‹nths xs {j. Suc j ∈ A} = a # xs ⟷ False›
    for a :: 'a and xs :: ‹'a list› and A :: ‹nat set›
    using mset_nths_subset_mset[of xs ‹{j. Suc j ∈ A}›] by auto
  show ?thesis
    apply (induction xs arbitrary: A)
    subgoal by auto
    subgoal
      by (auto 5 5 simp: nths_Cons) fastforce
    done
qed

lemma nts_upt_length[simp]: ‹nths xs {0..<length xs} = xs›
  by (auto simp: nths_id_iff)

lemma nths_shift_lemma':
  ‹map fst [p←zip xs [i..<i + n]. snd p + b ∈ A] = map fst [p←zip xs [0..<n]. snd p + b + i ∈ A]›
proof (induct xs arbitrary: i n b)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  have 1: ‹map fst [p←zip (a # xs) (i # [Suc i..<i + n]). snd p + b ∈ A] =
     (if i + b ∈ A then a#map fst [p←zip xs [Suc i..<i + n]. snd p + b ∈ A]
     else map fst [p←zip xs [Suc i..<i + n]. snd p + b ∈A])›
    by simp
  have 2: ‹map fst [p←zip (a # xs) [0..<n] . snd p + b + i ∈ A] =
     (if i + b ∈ A then a # map fst [p←zip xs [1..<n]. snd p + b + i ∈ A]
      else map fst [p←zip (xs) [1..<n] . snd p + b + i ∈ A])›
    if ‹n > 0›
    by (subst upt_conv_Cons) (use that in ‹auto simp: ac_simps›)
  show ?case
  proof (cases n)
    case 0
    then show ?thesis by simp
  next
    case n: (Suc m)
    then have i_n_m: ‹i + n = Suc i + m›
      by auto
    have 3: ‹map fst [p←zip xs [Suc i..<i+n] . snd p + b ∈ A] =
             map fst [p←zip xs [0..<m] . snd p + b + Suc i ∈ A]›
      using Cons[of b ‹Suc i› m] unfolding i_n_m .
    have 4: ‹map fst [p←zip xs [1..<n] . snd p + b + i ∈ A] =
                 map fst [p←zip xs [0..<m] . Suc (snd p + b + i) ∈ A]›
      using Cons[of ‹b+i› 1 m] unfolding n Suc_eq_plus1_left add.commute[of 1]
      by (simp_all add: ac_simps)
    show ?thesis
      apply (subst upt_conv_Cons)
      using n apply (simp; fail)
      apply (subst 1)
      apply (subst 2)
      using n apply (simp; fail)
      apply (subst 3)
      apply (subst 3)

      apply (subst 4)
      apply (subst 4)
      by force
  qed
qed

lemma nths_Cons_upt_Suc: ‹nths (a # xs) {0..<Suc n} = a # nths xs {0..<n}›
  unfolding nths_def
  apply (subst upt_conv_Cons)
   apply simp
  using nths_shift_lemma'[of 0 ‹{0..<Suc n}› ‹xs› 1 ‹length xs›]
  by (simp_all add: ac_simps)


lemma nths_empty_iff: ‹nths xs A = [] ⟷ {..<length xs} ∩ A = {}›
proof (induction xs arbitrary: A)
  case Nil
  then show ?case by auto
next
  case (Cons a xs) note IH = this(1)
  have ‹(∀x<length xs. x ≠ 0 ⟶ x ∉ A)›
    if a1: ‹{..<length xs} ∩ {j. Suc j ∈ A} = {}›
  proof (intro allI impI)
    fix nn
    assume nn: ‹nn < length xs› ‹nn ≠ 0›
    moreover have "∀n. Suc n ∉ A ∨ ¬ n < length xs"
      using a1 by blast
    then show "nn ∉ A"
      using nn
      by (metis (no_types) lessI less_trans list_decode.cases)
  qed
  show ?case
  proof (cases ‹0 ∈ A›)
    case True
    then show ?thesis by (subst nths_Cons) auto
  next
    case False
    then show ?thesis
      by (subst nths_Cons) (use less_Suc_eq_0_disj IH in auto)
  qed
qed

lemma nths_upt_Suc:
  assumes ‹i < length xs›
  shows ‹nths xs {i..<length xs} = xs!i # nths xs {Suc i..<length xs}›
proof -
  have upt: ‹{i..<k} = {j. i ≤ j ∧ j < k}› for i k :: nat
    by auto
  show ?thesis
    using assms
  proof (induction xs arbitrary: i)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs i) note IH = this(1) and i_le = this(2)
    have [simp]: ‹i - Suc 0 ≤ j ⟷ i ≤ Suc j› if ‹i > 0› for j
      using that by auto
    show ?case
      using IH[of ‹i-1›] i_le
      by (auto simp add: nths_Cons upt)
  qed
qed

lemma nths_upt_Suc':
  assumes ‹i < b› and ‹b <= length xs›
  shows ‹nths xs {i..<b} = xs!i # nths xs {Suc i..<b}›
proof -
  have S1: ‹{j. i ≤ Suc j ∧ j < b - Suc 0}  = {j. i ≤ Suc j ∧ Suc j < b}› for i b
    by auto
  have S2: ‹{j. i ≤ j ∧ j < b - Suc 0}  = {j. i ≤ j ∧ Suc j < b}› for i b
    by auto
  have upt: ‹{i..<k} = {j. i ≤ j ∧ j < k}› for i k :: nat
    by auto
  show ?thesis
    using assms
  proof (induction xs arbitrary: i b)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs i) note IH = this(1) and i_le = this(2,3)
    have [simp]: ‹i - Suc 0 ≤ j ⟷ i ≤ Suc j› if ‹i > 0› for j
      using that by auto
    have ‹i - Suc 0 < b - Suc 0 ∨ (i = 0)›
      using i_le by linarith
    moreover have ‹b - Suc 0 ≤ length xs ∨ xs = []›
      using i_le by auto
    ultimately show ?case
      using IH[of ‹i-1› ‹b-1›] i_le
      apply (subst nths_Cons)
      apply (subst nths_Cons)
      by (auto simp: upt S1 S2)
  qed
qed

lemma Ball_set_nths: ‹(∀L∈set (nths xs A). P L) ⟷ (∀i ∈ A ∩ {0..<length xs}. P (xs ! i)) ›
  unfolding set_nths by fastforce


subsection ‹Product Case›

text ‹The splitting of tuples is done for sizes strictly less than 8. As we want to manipulate
  tuples of size 8, here is some more setup for larger sizes.›

lemma prod_cases8 [cases type]:
  obtains (fields) a b c d e f g h where "y = (a, b, c, d, e, f, g, h)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct8 [case_names fields, induct type]:
  "(⋀a b c d e f g h. P (a, b, c, d, e, f, g, h)) ⟹ P x"
  by (cases x) blast

lemma prod_cases9 [cases type]:
  obtains (fields) a b c d e f g h i where "y = (a, b, c, d, e, f, g, h, i)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct9 [case_names fields, induct type]:
  "(⋀a b c d e f g h i. P (a, b, c, d, e, f, g, h, i)) ⟹ P x"
  by (cases x) blast

lemma prod_cases10 [cases type]:
  obtains (fields) a b c d e f g h i j where "y = (a, b, c, d, e, f, g, h, i, j)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct10 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j. P (a, b, c, d, e, f, g, h, i, j)) ⟹ P x"
  by (cases x) blast

lemma prod_cases11 [cases type]:
  obtains (fields) a b c d e f g h i j k where "y = (a, b, c, d, e, f, g, h, i, j, k)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct11 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k. P (a, b, c, d, e, f, g, h, i, j, k)) ⟹ P x"
  by (cases x) blast

lemma prod_cases12 [cases type]:
  obtains (fields) a b c d e f g h i j k l where "y = (a, b, c, d, e, f, g, h, i, j, k, l)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct12 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l. P (a, b, c, d, e, f, g, h, i, j, k, l)) ⟹ P x"
  by (cases x) blast

lemma prod_cases13 [cases type]:
  obtains (fields) a b c d e f g h i j k l m where "y = (a, b, c, d, e, f, g, h, i, j, k, l, m)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct13 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m. P (a, b, c, d, e, f, g, h, i, j, k, l, m)) ⟹ P x"
  by (cases x) blast

lemma prod_cases14 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n where "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct14 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n)) ⟹ P x"
  by (cases x) blast

lemma prod_cases15 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n p where
    "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct15 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n p. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p)) ⟹ P x"
  by (cases x) blast

lemma prod_cases16 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n p q where
    "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct16 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n p q. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q)) ⟹ P x"
  by (cases x) blast

lemma prod_cases17 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n p q r where
    "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct17 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n p q r. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r)) ⟹ P x"
  by (cases x) blast

lemma prod_cases18 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n p q r s where
    "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct18 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n p q r s. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s)) ⟹ P x"
  by (cases x) blast

lemma prod_cases19 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n p q r s t where
    "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct19 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n p q r s t.
     P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t)) ⟹ P x"
  by (cases x) blast

lemma prod_cases20 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n p q r s t u where
    "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct20 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n p q r s t u.
      P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u)) ⟹ P x"
  by (cases x) blast

lemma prod_cases21 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n p q r s t u v where
    "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct21 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n p q r s t u v.
      P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v)) ⟹ P x"
  by (cases x) (blast 43)

lemma prod_cases22 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n p q r s t u v w where
    "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v, w)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct22 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n p q r s t u v w.
      P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v, w)) ⟹ P x"
  by (cases x) (blast 43)

lemma prod_cases23 [cases type]:
  obtains (fields) a b c d e f g h i j k l m n p q r s t u v w x where
    "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v, w, x)"
  by (cases y, cases ‹snd y›) auto

lemma prod_induct23 [case_names fields, induct type]:
  "(⋀a b c d e f g h i j k l m n p q r s t u v w y.
      P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v, w, y)) ⟹ P x"
  by (cases x) (blast 43)


subsection ‹More about @{term list_all2} and @{term map}›

text ‹
  More properties on the relator \<^term>‹list_all2› and \<^term>‹map›. These theorems are
  mostly used during the refinement and especially the lifting from a deterministic relator to
  its list version.
›
lemma list_all2_op_eq_map_right_iff: ‹list_all2 (λL. (=) (f L)) a aa ⟷ aa = map f a ›
  apply (induction a arbitrary: aa)
   apply (auto; fail)
  by (rename_tac aa, case_tac aa) (auto)

lemma list_all2_op_eq_map_right_iff': ‹list_all2 (λL L'. L' = f L) a aa ⟷ aa = map f a›
  apply (induction a arbitrary: aa)
   apply (auto; fail)
  by (rename_tac aa, case_tac aa) auto

lemma list_all2_op_eq_map_left_iff: ‹list_all2 (λL' L. L'  = (f L)) a aa ⟷ a = map f aa›
  apply (induction a arbitrary: aa)
   apply (auto; fail)
  by (rename_tac aa, case_tac aa) (auto)

lemma list_all2_op_eq_map_map_right_iff:
  ‹list_all2 (list_all2 (λL. (=) (f L))) xs' x ⟷ x = map (map f) xs'› for x
    apply (induction xs' arbitrary: x)
     apply (auto; fail)
    apply (case_tac x)
  by (auto simp: list_all2_op_eq_map_right_iff)

lemma list_all2_op_eq_map_map_left_iff:
  ‹list_all2 (list_all2 (λL' L. L' = f L)) xs' x ⟷ xs' = map (map f) x›
    apply (induction xs' arbitrary: x)
     apply (auto; fail)
    apply (rename_tac x, case_tac x)
  by (auto simp: list_all2_op_eq_map_left_iff)

lemma list_all2_conj:
  ‹list_all2 (λx y. P x y ∧ Q x y) xs ys ⟷ list_all2 P xs ys ∧ list_all2 Q xs ys›
  by (auto simp: list_all2_conv_all_nth)

lemma list_all2_replicate:
  ‹(bi, b) ∈ R' ⟹ list_all2 (λx x'. (x, x') ∈ R') (replicate n bi) (replicate n b)›
  by (induction n) auto


subsection ‹Multisets›

text ‹We have a lit of lemmas about multisets. Some of them have already moved to
 \<^theory>‹Nested_Multisets_Ordinals.Multiset_More›, but others are too specific (especially the
 \<^term>‹distinct_mset› property, which roughly corresponds to finite sets).
›
notation image_mset (infixr "`#" 90)

lemma in_multiset_nempty: ‹L ∈# D ⟹ D ≠ {#}›
  by auto

text ‹The definition and the correctness theorem are from the multiset theory
  @{file ‹~~/src/HOL/Library/Multiset.thy›}, but a name is necessary to refer to them:›
definition union_mset_list where
‹union_mset_list xs ys ≡ case_prod append (fold (λx (ys, zs). (remove1 x ys, x # zs)) xs (ys, []))›

lemma union_mset_list:
  ‹mset xs ∪# mset ys = mset (union_mset_list xs ys)›
proof -
  have ‹⋀zs. mset (case_prod append (fold (λx (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
      (mset xs ∪# mset ys) + mset zs›
    by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
  then show ?thesis by (simp add: union_mset_list_def)
qed

lemma union_mset_list_Nil[simp]: ‹union_mset_list [] bi = bi›
  by (auto simp: union_mset_list_def)

lemma size_le_Suc_0_iff: ‹size M ≤ Suc 0 ⟷ ((∃a b. M = {#a#}) ∨ M = {#})›
   using size_1_singleton_mset by (auto simp: le_Suc_eq)

lemma size_2_iff: ‹size M = 2 ⟷ (∃a b. M = {#a, b#})›
  by (metis One_nat_def Suc_1 Suc_pred empty_not_add_mset nonempty_has_size size_Diff_singleton
      size_eq_Suc_imp_eq_union size_single union_single_eq_diff union_single_eq_member)

lemma subset_eq_mset_single_iff: ‹x2 ⊆# {#L#} ⟷ x2 = {#} ∨ x2 = {#L#}›
  by (metis single_is_union subset_mset.add_diff_inverse subset_mset.eq_refl subset_mset.zero_le)

lemma mset_eq_size_2:
  ‹mset xs = {#a, b#} ⟷ xs = [a, b] ∨ xs = [b, a]›
  by (cases xs) (auto simp: add_mset_eq_add_mset Diff_eq_empty_iff_mset subset_eq_mset_single_iff)


lemma butlast_list_update:
  ‹w < length xs ⟹ butlast (xs[w := last xs]) = take w xs @ butlast (last xs # drop (Suc w) xs)›
  by (induction xs arbitrary: w) (auto split: nat.splits if_splits simp: upd_conv_take_nth_drop)

lemma mset_butlast_remove1_mset: ‹xs ≠ [] ⟹ mset (butlast xs) = remove1_mset (last xs) (mset xs)›
  apply (subst(2) append_butlast_last_id[of xs, symmetric])
   apply assumption
  apply (simp only: mset_append)
  by auto

lemma distinct_mset_mono: ‹D' ⊆# D ⟹ distinct_mset D ⟹ distinct_mset D'›
  by (metis distinct_mset_union subset_mset.le_iff_add)

lemma distinct_mset_mono_strict: ‹D' ⊂# D ⟹ distinct_mset D ⟹ distinct_mset D'›
  using distinct_mset_mono by auto

lemma subset_mset_trans_add_mset:
  ‹D ⊆# D' ⟹ D ⊆# add_mset L D'›
  by (metis add_mset_remove_trivial diff_subset_eq_self subset_mset.dual_order.trans)

lemma subset_add_mset_notin_subset: ‹L ∉# E ⟹ E ⊆# add_mset L D ⟷ E ⊆# D›
  by (meson subset_add_mset_notin_subset_mset subset_mset_trans_add_mset)

lemma remove1_mset_empty_iff: ‹remove1_mset L N = {#} ⟷ N = {#L#} ∨ N = {#}›
  by (cases ‹L ∈# N›; cases N) auto

lemma mset_set_subset_iff:
  ‹mset_set A ⊆# I ⟷ infinite A ∨ A ⊆ set_mset I›
  by (metis finite_set_mset finite_set_mset_mset_set mset_set.infinite mset_set_set_mset_subseteq
    set_mset_mono subset_imp_msubset_mset_set subset_mset.dual_order.trans subset_mset.max_bot
    subset_mset.max_def)

lemma distinct_subseteq_iff:
  assumes dist: ‹distinct_mset M›
  shows ‹set_mset M ⊆ set_mset N ⟷ M ⊆# N›
proof
  assume ‹set_mset M ⊆ set_mset N›
  then show ‹M ⊆# N›
    using dist by (metis distinct_mset_set_mset_ident mset_set_subset_iff)
next
  assume ‹M ⊆# N›
  then show ‹set_mset M ⊆ set_mset N›
    by (metis set_mset_mono)
qed

lemma distinct_set_mset_eq_iff:
  assumes ‹distinct_mset M› ‹distinct_mset N›
  shows ‹set_mset M = set_mset N ⟷ M = N›
  using assms distinct_mset_set_mset_ident by fastforce

lemma (in -) distinct_mset_union2:
  ‹distinct_mset (A + B) ⟹ distinct_mset B›
  using distinct_mset_union[of B A]
  by (auto simp: ac_simps)

lemma in_remove1_msetI: ‹x ≠ a ⟹ x ∈# M ⟹ x ∈# remove1_mset a M›
  by (simp add: in_remove1_mset_neq)

lemma count_multi_member_split:
   ‹count M a ≥ n ⟹ ∃M'. M = replicate_mset n a + M'›
  apply (induction n arbitrary: M)
  subgoal by auto
  subgoal premises IH for n M
    using IH(1)[of ‹remove1_mset a M›] IH(2)
    apply (cases ‹n ≤ count M a - Suc 0›)
     apply (auto dest!: Suc_le_D)
    by (metis count_greater_zero_iff insert_DiffM zero_less_Suc)
  done

lemma count_image_mset_multi_member_split:
  ‹count (image_mset f M) L ≥ Suc 0 ⟹  ∃K. f K = L ∧ K ∈# M›
  by auto

lemma count_image_mset_multi_member_split_2:
  assumes count: ‹count (image_mset f M) L ≥ 2›
  shows ‹∃K K' M'. f K = L ∧ K ∈# M ∧ f K' = L ∧ K' ∈# remove1_mset K M ∧
       M = {#K, K'#} + M'›
proof -
  obtain K where
    K: ‹f K = L› ‹K ∈# M›
    using count_image_mset_multi_member_split[of f M L] count by fastforce
  then obtain K' where
    K': ‹f K' = L› ‹K' ∈# remove1_mset K M›
    using count_image_mset_multi_member_split[of f ‹remove1_mset K M› L] count
    by (auto dest!: multi_member_split)
  moreover have ‹∃M'. M = {#K, K'#} + M'›
    using multi_member_split[of K M] multi_member_split[of K' ‹remove1_mset K M›] K K'
    by (auto dest!: multi_member_split)
  then show ?thesis
    using K K' by blast
qed

lemma minus_notin_trivial: "L ∉# A ⟹ A - add_mset L B = A - B"
  by (metis diff_intersect_left_idem inter_add_right1)

lemma minus_notin_trivial2: ‹b ∉# A ⟹ A - add_mset e (add_mset b B) = A - add_mset e B›
  by (subst add_mset_commute) (auto simp: minus_notin_trivial)

lemma diff_union_single_conv3: ‹a ∉# I ⟹ remove1_mset a (I + J) = I + remove1_mset a J›
  by (metis diff_union_single_conv remove_1_mset_id_iff_notin union_iff)

lemma filter_union_or_split:
  ‹{#L ∈# C. P L ∨ Q L#} = {#L ∈# C. P L#} + {#L ∈# C. ¬P L ∧ Q L#}›
  by (induction C) auto

lemma subset_mset_minus_eq_add_mset_noteq: ‹A ⊂# C ⟹ A - B ≠ C›
  by (auto simp: dest: in_diffD)

lemma minus_eq_id_forall_notin_mset:
  ‹A - B = A ⟷ (∀L ∈# B. L ∉# A)›
  by (induction A)
   (auto dest!: multi_member_split simp: subset_mset_minus_eq_add_mset_noteq)

lemma in_multiset_minus_notin_snd[simp]: ‹a ∉# B ⟹ a ∈# A - B ⟷ a ∈# A›
  by (metis count_greater_zero_iff count_inI in_diff_count)

lemma distinct_mset_in_diff:
  ‹distinct_mset C ⟹ a ∈# C - D ⟷ a ∈# C ∧ a ∉# D›
  by (meson distinct_mem_diff_mset in_multiset_minus_notin_snd)

lemma diff_le_mono2_mset: ‹A ⊆# B ⟹ C - B ⊆# C - A›
  apply (auto simp: subseteq_mset_def ac_simps)
  by (simp add: diff_le_mono2)

lemma subseteq_remove1[simp]: ‹C ⊆# C' ⟹ remove1_mset L C ⊆# C'›
  by (meson diff_subset_eq_self subset_mset.dual_order.trans)

lemma filter_mset_cong2:
  "(⋀x. x ∈# M ⟹ f x = g x) ⟹ M = N ⟹ filter_mset f M = filter_mset g N"
  by (hypsubst, rule filter_mset_cong, simp)

lemma filter_mset_cong_inner_outer:
  assumes
     M_eq: ‹(⋀x. x ∈# M ⟹ f x = g x)› and
     notin: ‹(⋀x. x ∈# N - M ⟹ ¬g x)› and
     MN: ‹M ⊆# N›
  shows ‹filter_mset f M = filter_mset g N›
proof -
  define NM where ‹NM = N - M›
  have N: ‹N = M + NM›
    unfolding NM_def using MN by simp
  have ‹filter_mset g NM = {#}›
    using notin unfolding NM_def[symmetric] by (auto simp: filter_mset_empty_conv)
  moreover have ‹filter_mset f M = filter_mset g M›
    by (rule filter_mset_cong) (use M_eq in auto)
  ultimately show ?thesis
    unfolding N by simp
qed

lemma notin_filter_mset:
  ‹K ∉# C ⟹ filter_mset P C = filter_mset (λL. P L ∧ L ≠ K) C›
  by (rule filter_mset_cong) auto

lemma distinct_mset_add_mset_filter:
  assumes ‹distinct_mset C› and ‹L ∈# C› and ‹¬P L›
  shows ‹add_mset L (filter_mset P C) = filter_mset (λx. P x ∨ x = L) C›
  using assms
proof (induction C)
  case empty
  then show ?case by simp
next
  case (add x C) note dist = this(2) and LC = this(3) and P[simp] = this(4) and _ = this
  then have IH: ‹L ∈# C ⟹ add_mset L (filter_mset P C) = {#x ∈# C. P x ∨ x = L#}› by auto
  show ?case
  proof (cases ‹x = L›)
    case [simp]: True
    have ‹filter_mset P C = {#x ∈# C. P x ∨ x = L#}›
      by (rule filter_mset_cong2) (use dist in auto)
    then show ?thesis
      by auto
  next
    case False
    then show ?thesis
      using IH LC by auto
  qed
qed

lemma set_mset_set_mset_eq_iff: ‹set_mset A = set_mset B ⟷ (∀a∈#A. a ∈# B) ∧ (∀a∈#B. a ∈# A)›
  by blast

lemma remove1_mset_union_distrib:
  ‹remove1_mset a (M ∪# N) = remove1_mset a M ∪# remove1_mset a N›
  by (auto simp: multiset_eq_iff)

(* useful for sledgehammer/proof reconstruction ?*)
lemma member_add_mset: ‹a ∈# add_mset x xs ⟷ a = x ∨ a ∈# xs›
  by simp

lemma sup_union_right_if:
  ‹N ∪# add_mset x M =
     (if x ∉# N then add_mset x (N ∪# M) else add_mset x (remove1_mset x N ∪# M))›
  by (auto simp: sup_union_right2)

lemma same_mset_distinct_iff:
  ‹mset M = mset M' ⟹ distinct M ⟷ distinct M'›
  by (auto simp: distinct_mset_mset_distinct[symmetric] simp del: distinct_mset_mset_distinct)

lemma inj_on_image_mset_eq_iff:
  assumes inj: ‹inj_on f (set_mset (M + M'))›
  shows ‹image_mset f M' = image_mset f M ⟷ M' = M› (is ‹?A = ?B›)
proof
  assume ?B
  then show ?A by auto
next
  assume ?A
  then show ?B
    using inj
  proof(induction M arbitrary: M')
    case empty
    then show ?case by auto
  next
    case (add x M) note IH = this(1) and H = this(2) and inj = this(3)

    obtain M1 x' where
      M': ‹M' = add_mset x' M1› and
      f_xx': ‹f x' = f x› and
      M1_M: ‹image_mset f M1 = image_mset f M›
      using H by (auto dest!: msed_map_invR)
    moreover have ‹M1 = M›
      apply (rule IH[OF M1_M])
      using inj by (auto simp: M')
    moreover have ‹x = x'›
      using inj f_xx' by (auto simp: M')
    ultimately show ?case by fast
  qed
qed

lemma image_msetI: ‹x ∈# A ⟹ f x ∈# f `# A›
  by (auto)

lemma inj_image_mset_eq_iff:
  assumes inj: ‹inj f›
  shows ‹image_mset f M' = image_mset f M ⟷ M' = M›
  using inj_on_image_mset_eq_iff[of f M' M] assms
  by (simp add: inj_eq multiset.inj_map)

lemma singleton_eq_image_mset_iff:  ‹{#a#} = f `# NE' ⟷ (∃b. NE' = {#b#} ∧ f b = a)›
  by (cases NE') auto

lemma image_mset_If_eq_notin:
   ‹C ∉# A ⟹ {#f (if x = C then a x else b x). x ∈# A#} = {# f(b x). x ∈# A #}›
  by (induction A) auto

lemma finite_mset_set_inter:
  ‹finite A ⟹ finite B ⟹ mset_set (A ∩ B) = mset_set A ∩# mset_set B›
  apply (induction A rule: finite_induct)
  subgoal by auto
  subgoal for a A
    apply (cases ‹a ∈ B›; cases ‹a ∈# mset_set B›)
    using multi_member_split[of a ‹mset_set B›]
    by (auto simp: mset_set.insert_remove)
  done

lemma distinct_mset_inter_remdups_mset:
  assumes dist: ‹distinct_mset A›
  shows ‹A ∩# remdups_mset B = A ∩# B›
proof -
  have [simp]: ‹A' ∩# remove1_mset a (remdups_mset Aa) = A' ∩# Aa›
    if
      ‹A' ∩# remdups_mset Aa = A' ∩# Aa› and
      ‹a ∉# A'› and
      ‹a ∈# Aa›
    for A' Aa :: ‹'a multiset› and a
  by (metis insert_DiffM inter_add_right1 set_mset_remdups_mset that)

  show ?thesis
    using dist
    apply (induction A)
    subgoal by auto
     subgoal for a A'
      apply (cases ‹a ∈# B›)
      using multi_member_split[of a ‹B›]  multi_member_split[of a ‹A›]
      by (auto simp: mset_set.insert_remove)
    done
qed

lemma mset_butlast_update_last[simp]:
  ‹w < length xs ⟹ mset (butlast (xs[w := last (xs)])) = remove1_mset (xs ! w) (mset xs)›
  by (cases ‹xs = []›)
    (auto simp add: last_list_update_to_last mset_butlast_remove1_mset mset_update)

lemma in_multiset_ge_Max: ‹a ∈# N ⟹ a > Max (insert 0 (set_mset N)) ⟹ False›
  by (simp add: leD)

lemma distinct_mset_set_mset_remove1_mset:
  ‹distinct_mset M ⟹ set_mset (remove1_mset c M) = set_mset M - {c}›
  by (cases ‹c ∈# M›) (auto dest!: multi_member_split simp: add_mset_eq_add_mset)

lemma distinct_count_msetD:
  ‹distinct xs ⟹ count (mset xs) a = (if a ∈ set xs then 1 else 0)›
  unfolding distinct_count_atmost_1 by auto

lemma filter_mset_and_implied:
  ‹(⋀ia. ia ∈# xs ⟹ Q ia ⟹ P ia) ⟹ {#ia ∈# xs. P ia ∧ Q ia#} = {#ia ∈# xs. Q ia#}›
  by (rule filter_mset_cong2) auto

lemma filter_mset_eq_add_msetD: ‹filter_mset P xs = add_mset a A ⟹ a ∈# xs ∧ P a›
  by (induction xs arbitrary: A)
    (auto split: if_splits simp: add_mset_eq_add_mset)

lemma filter_mset_eq_add_msetD': ‹add_mset a A  = filter_mset P xs ⟹ a ∈# xs ∧ P a›
  using filter_mset_eq_add_msetD[of P xs a A] by auto

lemma image_filter_replicate_mset:
  ‹{#Ca ∈# replicate_mset m C. P Ca#} = (if P C then replicate_mset m C else {#})›
  by (induction m) auto

lemma size_Union_mset_image_mset:
  ‹size (∑⇩# (A :: 'a multiset multiset)) = (∑i ∈# A. size i)›
  by (induction A) auto

lemma image_mset_minus_inj_on:
  ‹inj_on f (set_mset A ∪ set_mset B) ⟹ f `# (A - B) = f `# A - f `# B›
  apply (induction A arbitrary: B)
  subgoal by auto
  subgoal for x A B
    apply (cases ‹x ∈# B›)
    apply (auto dest!: multi_member_split)
    apply (subst diff_add_mset_swap)
    apply auto
    done
  done

lemma filter_mset_mono_subset:
  ‹A ⊆# B ⟹ (⋀x. x ∈# A ⟹ P x ⟹ Q x) ⟹ filter_mset P A ⊆# filter_mset Q B›
  by (metis multiset_filter_mono multiset_filter_mono2 subset_mset.order_trans)


lemma mset_inter_empty_set_mset: ‹M ∩# xc = {#} ⟷ set_mset M ∩ set_mset xc = {}›
  by (induction xc) auto

lemma sum_mset_cong:
  ‹(⋀A. A ∈# M ⟹ f A = g A) ⟹ (∑ A ∈# M. f A) = (∑ A ∈# M. g A)›
  by (induction M) auto

lemma sum_mset_mset_set_sum_set:
  ‹(∑A ∈# mset_set As. f A) = (∑A ∈ As. f A)›
  apply (cases ‹finite As›)
  by (induction As rule: finite_induct) auto

lemma sum_mset_sum_count:
  ‹(∑A ∈# As. f A) = (∑A ∈ set_mset As. count As A * f A)›
proof (induction As)
  case empty
  then show ?case by auto
next
  case (add x As)
  define n where ‹n = count As x›
  define As' where ‹As' ≡ removeAll_mset x As›
  have As: ‹As = As' + replicate_mset n x›
    by (auto simp: As'_def n_def intro!: multiset_eqI)
  have [simp]: ‹set_mset As' - {x} = set_mset As'› ‹count As' x = 0› ‹x ∉# As'›
    unfolding As'_def
    by auto
  have ‹ (∑A∈set_mset As'.
       (if x = A then Suc (count (As' + replicate_mset n x) A)
        else count (As' + replicate_mset n x) A) *
       f A) =
       (∑A∈set_mset As'.
       (count (As' + replicate_mset n x) A) *
       f A)›
    by (rule sum.cong) auto
  then show ?case using add by (auto simp: As sum.insert_remove)
qed

lemma sum_mset_inter_restrict:
  ‹(∑ x ∈# filter_mset P M. f x) = (∑ x ∈# M. if P x then f x else 0)›
  by (induction M) auto

lemma sumset_diff_constant_left:
  assumes ‹⋀x. x ∈# A ⟹ f x ≤ n›
  shows ‹(∑x∈# A . n - f x) = size A * n - (∑x∈# A . f x)›
proof -
  have ‹size A * n ≥ (∑x∈# A . f x)›
    if ‹⋀x. x ∈# A ⟹ f x ≤ n› for A
    using that
    by (induction A) (force simp: ac_simps)+
  then show ?thesis
    using assms
    by (induction A) (auto simp: ac_simps)
qed

lemma mset_set_eq_mset_iff: ‹finite x ⟹  mset_set x = mset xs ⟷ distinct xs ∧ x = set xs›
  apply (auto simp flip: distinct_mset_mset_distinct eq_commute[of _ ‹mset_set _›]
    simp: distinct_mset_mset_set mset_set_set)
  apply (metis finite_set_mset_mset_set set_mset_mset)
  apply (metis finite_set_mset_mset_set set_mset_mset)
  done

lemma distinct_mset_iff:
  ‹¬distinct_mset C ⟷ (∃a C'. C = add_mset a (add_mset a C'))›
  by (metis (no_types, opaque_lifting) One_nat_def
      count_add_mset distinct_mset_add_mset distinct_mset_def
      member_add_mset mset_add not_in_iff)

lemma diff_add_mset_remove1: ‹NO_MATCH {#} N ⟹ M - add_mset a N = remove1_mset a (M - N)›
  by auto

lemma remdups_mset_sum_subset:  ‹C ⊆# C' ⟹ remdups_mset (C + C') = remdups_mset C'›
   ‹C ⊆# C' ⟹ remdups_mset (C' + C) = remdups_mset C'›
  apply (metis remdups_mset_def set_mset_mono set_mset_union sup.absorb_iff2)
  by (metis add.commute le_iff_sup remdups_mset_def set_mset_mono set_mset_union)

lemma distinct_mset_subset_iff_remdups:
  ‹distinct_mset a ⟹ a ⊆# b ⟷ a ⊆# remdups_mset b›
  by (simp add: distinct_mset_inter_remdups_mset subset_mset.le_iff_inf)

lemma remdups_mset_subset_add_mset: ‹remdups_mset C' ⊆# add_mset L C'›
  by (meson distinct_mset_remdups_mset distinct_mset_subset_iff_remdups subset_mset.order_refl
    subset_mset_trans_add_mset)

lemma subset_mset_removeAll_iff:
  ‹M ⊆# removeAll_mset a M' ⟷ a ∉# M ∧ M ⊆# M'›
  by (smt (verit, del_insts) count_replicate_mset diff_le_mono diff_subset_eq_self in_diff_count
    in_replicate_mset minus_eq_id_forall_notin_mset minus_multiset.rep_eq mset_subset_eqD
    nat_less_le subset_mset.trans subseteq_mset_def)

lemma remdups_mset_removeAll: ‹remdups_mset (removeAll_mset a A) = removeAll_mset a (remdups_mset A)›
  by (smt (verit, ccfv_threshold) add_mset_remove_trivial count_eq_zero_iff diff_zero
    distinct_mset_remdups_mset distinct_mset_remove1_All insert_DiffM order.refl remdups_mset_def
    remdups_mset_singleton_sum removeAll_subseteq_remove1_mset replicate_mset_eq_empty_iff
    set_mset_minus_replicate_mset(1) set_mset_remdups_mset subset_mset_removeAll_iff)

text ‹This is an alternative to @{thm [source] remdups_mset_singleton_sum}.›
lemma remdups_mset_singleton_removeAll:
  "remdups_mset (add_mset a A) = add_mset a (removeAll_mset a (remdups_mset A))"
  by (metis dual_order.refl finite_set_mset mset_set.insert_remove remdups_mset_def
    remdups_mset_removeAll set_mset_add_mset_insert set_mset_minus_replicate_mset(1))

lemma mset_remove_filtered: ‹C - {#x ∈# C. P x#} = {#x ∈# C. ¬P x#}›
  by (metis add_implies_diff union_filter_mset_complement)


section ‹Finite maps and multisets›

subsubsection ‹Finite sets and multisets›

abbreviation mset_fset :: ‹'a fset ⇒ 'a multiset› where
  ‹mset_fset N ≡ mset_set (fset N)›

definition fset_mset :: ‹'a multiset ⇒ 'a fset› where
  ‹fset_mset N ≡ Abs_fset (set_mset N)›

lemma fset_mset_mset_fset: ‹fset_mset (mset_fset N) = N›
  by (auto simp: fset.fset_inverse fset_mset_def)

lemma mset_fset_fset_mset[simp]:
  ‹mset_fset (fset_mset N) = remdups_mset N›
  by (auto simp: fset.fset_inverse fset_mset_def Abs_fset_inverse remdups_mset_def)

lemma in_mset_fset_fmember[simp]: ‹x ∈# mset_fset N ⟷ x |∈| N›
  by (auto simp: fmember.rep_eq)

lemma in_fset_mset_mset[simp]: ‹x |∈| fset_mset N ⟷ x ∈# N›
  by (auto simp: fmember.rep_eq fset_mset_def Abs_fset_inverse)


subsubsection ‹Finite map and multisets›

text ‹Roughly the same as \<^term>‹ran› and \<^term>‹dom›, but with duplication in the content (unlike their
  finite sets counterpart) while still working on finite domains (unlike a function mapping).
  Remark that \<^term>‹dom_m› (the keys) does not contain duplicates, but we keep for symmetry (and for
  easier use of multiset operators as in the definition of \<^term>‹ran_m›).
›
definition dom_m where
  ‹dom_m N = mset_fset (fmdom N)›

definition ran_m where
  ‹ran_m N = the `# fmlookup N `# dom_m N›

lemma dom_m_fmdrop[simp]: ‹dom_m (fmdrop C N) = remove1_mset C (dom_m N)›
  unfolding dom_m_def
  by (cases ‹C |∈| fmdom N›)
    (auto simp: mset_set.remove fmember.rep_eq)

lemma dom_m_fmdrop_All: ‹dom_m (fmdrop C N) = removeAll_mset C (dom_m N)›
  unfolding dom_m_def
  by (cases ‹C |∈| fmdom N›)
    (auto simp: mset_set.remove fmember.rep_eq)

lemma dom_m_fmupd[simp]: ‹dom_m (fmupd k C N) = add_mset k (remove1_mset k (dom_m N))›
  unfolding dom_m_def
  by (cases ‹k |∈| fmdom N›)
    (auto simp: mset_set.remove fmember.rep_eq mset_set.insert_remove)

lemma distinct_mset_dom: ‹distinct_mset (dom_m N)›
  by (simp add: distinct_mset_mset_set dom_m_def)

lemma in_dom_m_lookup_iff: ‹C ∈# dom_m N' ⟷ fmlookup N' C ≠ None›
  by (auto simp: dom_m_def fmdom.rep_eq fmlookup_dom'_iff)

lemma in_dom_in_ran_m[simp]: ‹i ∈# dom_m N ⟹ the (fmlookup N i) ∈# ran_m N›
  by (auto simp: ran_m_def)

lemma fmupd_same[simp]:
  ‹x1 ∈# dom_m x1aa ⟹ fmupd x1 (the (fmlookup x1aa x1)) x1aa = x1aa›
  by (metis fmap_ext fmupd_lookup in_dom_m_lookup_iff option.collapse)

lemma ran_m_fmempty[simp]: ‹ran_m fmempty = {#}› and
    dom_m_fmempty[simp]: ‹dom_m fmempty = {#}›
  by (auto simp: ran_m_def dom_m_def)

lemma fmrestrict_set_fmupd:
  ‹a ∈ xs ⟹ fmrestrict_set xs (fmupd a C N) = fmupd a C (fmrestrict_set xs N)›
  ‹a ∉ xs ⟹ fmrestrict_set xs (fmupd a C N) = fmrestrict_set xs N›
  by (auto simp: fmfilter_alt_defs)

lemma fset_fmdom_fmrestrict_set:
  ‹fset (fmdom (fmrestrict_set xs N)) = fset (fmdom N) ∩ xs›
  by (auto simp: fmfilter_alt_defs)

lemma dom_m_fmrestrict_set: ‹dom_m (fmrestrict_set (set xs) N) = mset xs ∩# dom_m N›
  using fset_fmdom_fmrestrict_set[of ‹set xs› N] distinct_mset_dom[of N]
  distinct_mset_inter_remdups_mset[of ‹mset_fset (fmdom N)› ‹mset xs›]
  by (auto simp: dom_m_def fset_mset_mset_fset finite_mset_set_inter multiset_inter_commute
    remdups_mset_def)

lemma dom_m_fmrestrict_set': ‹dom_m (fmrestrict_set xs N) = mset_set (xs ∩ set_mset (dom_m N))›
  using fset_fmdom_fmrestrict_set[of ‹xs› N] distinct_mset_dom[of N]
  by (auto simp: dom_m_def fset_mset_mset_fset finite_mset_set_inter multiset_inter_commute
    remdups_mset_def)

lemma indom_mI: ‹fmlookup m x = Some y ⟹ x ∈# dom_m m›
  by (drule fmdomI)  (auto simp: dom_m_def fmember.rep_eq)

lemma fmupd_fmdrop_id:
  assumes ‹k |∈| fmdom N'›
  shows ‹fmupd k (the (fmlookup N' k)) (fmdrop k N') = N'›
proof -
  have [simp]: ‹map_upd k (the (fmlookup N' k))
       (λx. if x ≠ k then fmlookup N' x else None) =
     map_upd k (the (fmlookup N' k))
       (fmlookup N')›
    by (auto intro!: ext simp: map_upd_def)
  have [simp]: ‹map_upd k (the (fmlookup N' k)) (fmlookup N') = fmlookup N'›
    using assms
    by (auto intro!: ext simp: map_upd_def)
  have [simp]: ‹finite (dom (λx. if x = k then None else fmlookup N' x))›
    by (subst dom_if) auto
  show ?thesis
    apply (auto simp: fmupd_def fmupd.abs_eq[symmetric])
    unfolding fmlookup_drop
    apply (simp add: fmlookup_inverse)
    done
qed

lemma fm_member_split: ‹k |∈| fmdom N' ⟹ ∃N'' v. N' = fmupd k v N'' ∧ the (fmlookup N' k) = v ∧
    k |∉| fmdom N''›
  by (rule exI[of _ ‹fmdrop k N'›])
    (auto simp: fmupd_fmdrop_id)

lemma ‹fmdrop k (fmupd k va N'') = fmdrop k N''›
  by (simp add: fmap_ext)

lemma fmap_ext_fmdom:
  ‹(fmdom N = fmdom N') ⟹ (⋀ x. x |∈| fmdom N ⟹ fmlookup N x = fmlookup N' x) ⟹
       N = N'›
  by (rule fmap_ext)
    (case_tac ‹x |∈| fmdom N›, auto simp: fmdom_notD)

lemma fmrestrict_set_insert_in:
  ‹xa  ∈ fset (fmdom N) ⟹
    fmrestrict_set (insert xa l1) N = fmupd xa (the (fmlookup N xa)) (fmrestrict_set l1 N)›
  apply (rule fmap_ext_fmdom)
   apply (auto simp: fset_fmdom_fmrestrict_set fmember.rep_eq notin_fset; fail)[]
  apply (auto simp: fmlookup_dom_iff; fail)
  done

lemma fmrestrict_set_insert_notin:
  ‹xa  ∉ fset (fmdom N) ⟹
    fmrestrict_set (insert xa l1) N = fmrestrict_set l1 N›
  by (rule fmap_ext_fmdom)
     (auto simp: fset_fmdom_fmrestrict_set fmember.rep_eq notin_fset)

lemma fmrestrict_set_insert_in_dom_m[simp]:
  ‹xa  ∈# dom_m N ⟹
    fmrestrict_set (insert xa l1) N = fmupd xa (the (fmlookup N xa)) (fmrestrict_set l1 N)›
  by (simp add: fmrestrict_set_insert_in dom_m_def)

lemma fmrestrict_set_insert_notin_dom_m[simp]:
  ‹xa  ∉# dom_m N ⟹
    fmrestrict_set (insert xa l1) N = fmrestrict_set l1 N›
  by (simp add: fmrestrict_set_insert_notin dom_m_def)

lemma fmlookup_restrict_set_id: ‹fset (fmdom N) ⊆ A ⟹ fmrestrict_set A N = N›
  by (metis fmap_ext fmdom'_alt_def fmdom'_notD fmlookup_restrict_set subset_iff)

lemma fmlookup_restrict_set_id': ‹set_mset (dom_m N) ⊆ A ⟹ fmrestrict_set A N = N›
  by (rule fmlookup_restrict_set_id)
    (auto simp: dom_m_def)

lemma ran_m_mapsto_upd:
  assumes
    NC: ‹C ∈# dom_m N›
  shows ‹ran_m (fmupd C C' N) =
         add_mset C' (remove1_mset (the (fmlookup N C)) (ran_m N))›
proof -
  define N' where
    ‹N' = fmdrop C N›
  have N_N': ‹dom_m N = add_mset C (dom_m N')›
    using NC unfolding N'_def by auto
  have ‹C ∉# dom_m N'›
    using NC distinct_mset_dom[of N] unfolding N_N' by auto
  then show ?thesis
    by (auto simp: N_N' ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
      intro!: image_mset_cong)
qed

lemma ran_m_mapsto_upd_notin:
  assumes NC: ‹C ∉# dom_m N›
  shows ‹ran_m (fmupd C C' N) = add_mset C' (ran_m N)›
  using NC
  by (auto simp: ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
      intro!: image_mset_cong split: if_splits)

lemma ran_m_fmdrop:
  ‹C ∈# dom_m N ⟹  ran_m (fmdrop C N) = remove1_mset (the (fmlookup N C)) (ran_m N)›
  using distinct_mset_dom[of N]
  by (cases ‹fmlookup N C›)
    (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
     dest!: multi_member_split
    intro!: filter_mset_cong2 image_mset_cong2)

lemma ran_m_fmdrop_notin:
  ‹C ∉# dom_m N ⟹ ran_m (fmdrop C N) = ran_m N›
  using distinct_mset_dom[of N]
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
    dest!: multi_member_split
    intro!: filter_mset_cong2 image_mset_cong2)

lemma ran_m_fmdrop_If:
  ‹ran_m (fmdrop C N) = (if C ∈# dom_m N then remove1_mset (the (fmlookup N C)) (ran_m N) else ran_m N)›
  using distinct_mset_dom[of N]
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
    dest!: multi_member_split
    intro!: filter_mset_cong2 image_mset_cong2)


subsubsection ‹Compact domain for finite maps›

text ‹\<^term>‹packed› is a predicate to indicate that the domain of finite mapping starts at
   \<^term>‹1::nat› and does not contain holes. We used it in the SAT solver for the mapping from
   indexes to clauses, to ensure that there not holes and therefore giving an upper bound on the
   highest key.

TODO KILL!
›
definition Max_dom where
  ‹Max_dom N = Max (set_mset (add_mset 0 (dom_m N)))›

definition packed where
  ‹packed N ⟷ dom_m N = mset [1..<Suc (Max_dom N)]›

text ‹Marking this rule as simp is not compatible with unfolding the definition of packed when
marked as:›
lemma Max_dom_empty: ‹dom_m b = {#} ⟹ Max_dom b = 0›
  by (auto simp: Max_dom_def)

lemma Max_dom_fmempty: ‹Max_dom fmempty = 0›
  by (auto simp: Max_dom_empty)

lemma packed_empty[simp]: ‹packed fmempty›
  by (auto simp: packed_def Max_dom_empty)

lemma packed_Max_dom_size:
  assumes p: ‹packed N›
  shows ‹Max_dom N = size (dom_m N)›
proof -
  have 1: ‹dom_m N = mset [1..<Suc (Max_dom N)]›
    using p unfolding packed_def Max_dom_def[symmetric] .
  have ‹size (dom_m N) = size (mset [1..<Suc (Max_dom N)])›
    unfolding 1 ..
  also have ‹… = length [1..<Suc (Max_dom N)]›
    unfolding size_mset ..
  also have ‹… = Max_dom N›
    unfolding length_upt by simp
  finally show ?thesis
    by simp
qed

lemma Max_dom_le:
  ‹L ∈# dom_m N ⟹ L ≤ Max_dom N›
  by (auto simp: Max_dom_def)

lemma remove1_mset_ge_Max_some: ‹a > Max_dom b ⟹ remove1_mset a (dom_m b) = dom_m b›
  by (auto simp: Max_dom_def remove_1_mset_id_iff_notin
      dest!: multi_member_split)

lemma Max_dom_fmupd_irrel:
  assumes
    ‹(a :: 'a :: {zero,linorder}) > Max_dom M›
  shows ‹Max_dom (fmupd a C M) = max a (Max_dom M)›
proof -
  have [simp]: ‹max 0 (max a A) = max a A› for A
    using assms
    by (auto simp: Max_dom_def remove1_mset_ge_Max_some ac_simps
      Max.insert_remove split: if_splits)
  have [iff]: "max a A = a ⟷ (A ≤ a)" for A
    by (auto split: if_splits simp: max_def)

  show ?thesis
    using assms
    apply (cases ‹dom_m M›)
    apply (auto simp: Max_dom_def remove1_mset_ge_Max_some ac_simps)[]
    apply (auto simp: Max_dom_def remove1_mset_ge_Max_some ac_simps)
    using order_less_imp_le apply blast
      by (meson in_diffD less_le_not_le)
qed

lemma Max_dom_alt_def: ‹Max_dom b = Max (insert 0 (set_mset (dom_m b)))›
  unfolding Max_dom_def by auto

lemma Max_insert_Suc_Max_dim_dom[simp]:
  ‹Max (insert (Suc (Max_dom b)) (set_mset (dom_m b))) = Suc (Max_dom b)›
  unfolding Max_dom_alt_def
  by (cases ‹set_mset (dom_m b) = {}›) auto

lemma size_dom_m_Max_dom:
  ‹size (dom_m N) ≤ Suc (Max_dom N)›
proof -
  have ‹dom_m N ⊆# mset_set {0..< Suc (Max_dom N)}›
    apply (rule distinct_finite_set_mset_subseteq_iff[THEN iffD1])
    subgoal by (auto simp: distinct_mset_dom)
    subgoal by auto
    subgoal by (auto dest: Max_dom_le)
    done
  from size_mset_mono[OF this] show ?thesis by auto
qed

lemma Max_atLeastLessThan_plus: ‹Max {(a::nat) ..< a+n} = (if n = 0 then Max {} else a+n - 1)›
  apply (induction n arbitrary: a)
  subgoal by auto
  subgoal for n a
    by (cases n)
      (auto simp: image_Suc_atLeastLessThan[symmetric] mono_Max_commute[symmetric] mono_def
          atLeastLessThanSuc
        simp del: image_Suc_atLeastLessThan)
  done

lemma Max_atLeastLessThan: ‹Max {(a::nat) ..< b} = (if b ≤ a then Max {} else b - 1)›
  using Max_atLeastLessThan_plus[of a ‹b-a›]
  by auto

lemma Max_insert_Max_dom_into_packed:
   ‹Max (insert (Max_dom bc) {Suc 0..<Max_dom bc}) = Max_dom bc›
  by (cases ‹Max_dom bc›; cases ‹Max_dom bc - 1›)
    (auto simp: Max_dom_empty Max_atLeastLessThan)

lemma packed0_fmud_Suc_Max_dom: ‹packed b ⟹ packed (fmupd (Suc (Max_dom b)) C b)›
  by (auto simp: packed_def remove1_mset_ge_Max_some Max_dom_fmupd_irrel max_def)

lemma ge_Max_dom_notin_dom_m: ‹a > Max_dom ao ⟹ a ∉# dom_m ao›
  by (auto simp: Max_dom_def)

lemma packed_in_dom_mI: ‹packed bc ⟹ j ≤ Max_dom bc ⟹ 0 < j ⟹ j ∈# dom_m bc›
  by (auto simp: packed_def)


lemma mset_fset_empty_iff: ‹mset_fset a = {#} ⟷ a = fempty›
  by (cases a) (auto simp: mset_set_empty_iff)

lemma dom_m_empty_iff[iff]:
  ‹dom_m NU = {#} ⟷ NU = fmempty›
  by (cases NU) (auto simp: dom_m_def mset_fset_empty_iff mset_set.insert_remove)



lemma nat_power_div_base:
  fixes k :: nat
  assumes "0 < m" "0 < k"
  shows "k ^ m div k = (k::nat) ^ (m - Suc 0)"
proof -
  have eq: "k ^ m = k ^ ((m - Suc 0) + Suc 0)"
    by (simp add: assms)
  show ?thesis
    using assms by (simp only: power_add eq) auto
qed

lemma eq_insertD: ‹A = insert a B ⟹ a ∈ A ∧ B ⊆ A›
  by auto

lemma length_list_ge2: ‹length S ≥ 2 ⟷ (∃a b S'. S = [a, b] @ S')›
  apply (cases S)
   apply (simp; fail)
  apply (rename_tac a S')
  apply (case_tac S')
  by simp_all


subsection ‹Multiset version of Pow›
text ‹
  This development was never useful in my own formalisation, but some people saw an interest
  in this or in things related to this (even if they discarded it eventually). Therefore, I finally
  decided to save the definition from my mailbox.

  If anyone ever uses that and adds the concept to the AFP, please tell me such that I can delete
  it.
›


definition Pow_mset where
‹Pow_mset A = fold_mset (λa A. (A + (add_mset a) `# A)) {#{#}#} A›

interpretation pow_mset_commute: comp_fun_commute ‹(λa A. (A + (add_mset a) `# A))›
  by (auto simp: comp_fun_commute_def add_mset_commute intro!: ext)

lemma Pow_mset_alt_def:
  "Pow_mset (mset A) = mset `# mset (subseqs A)"
  apply (induction A)
  subgoal by (auto simp: Pow_mset_def)
  subgoal
    by (auto simp: Let_def Pow_mset_def)
  done


lemma Pow_mset_empty[simp]:
  ‹Pow_mset {#} = {#{#}#}›
  by (auto simp: Pow_mset_def)

lemma Pow_mset_add_mset[simp]:
  ‹Pow_mset (add_mset a A) = Pow_mset A + (add_mset a) `# Pow_mset A›
  by (auto simp: Let_def Pow_mset_def)

lemma in_Pow_mset_iff:
  ‹A ∈# Pow_mset B ⟷ A ⊆# B›
proof
  assume ‹A ⊆# B›
  then show ‹A ∈# Pow_mset B›
    apply (induction B arbitrary: A)
    subgoal by auto
    subgoal premises p for b B A
      using p(1)[of A] p(1)[of ‹A - {#b#}›] p(2)
      apply (cases ‹b ∈# A›)
      by (auto dest: subset_add_mset_notin_subset_mset
          dest!: multi_member_split)
    done
next
  assume ‹A ∈# Pow_mset B›
  then show ‹A ⊆# B›
    apply (induction B arbitrary: A)
    subgoal by auto
    subgoal premises p for b B A
      using p by (auto simp: subset_mset_trans_add_mset)
    done
qed

lemma size_Pow_mset[simp]: ‹size (Pow_mset A) = 2^(size A)›
  by (induction A) auto

lemma set_Pow_mset:
  ‹set_mset (Pow_mset A) = {B. B ⊆# A}›
  by (auto simp: in_Pow_mset_iff)

text ‹Proof by Manuel Eberl on Zulip
  🌐‹https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/Cardinality.20of.20powerset.20of.20a.20multiset/near/220827959›.
›
lemma bij_betw_submultisets:
  "card {B. B ⊆# A} = (∏x∈set_mset A. count A x + 1)"
proof -
  define f :: "'a multiset ⇒ 'a ⇒ nat"
    where "f = (λB x. if x ∈# A then count B x else undefined)"
  define g :: "('a ⇒ nat) ⇒ 'a multiset"
    where "g = (λh. Abs_multiset (λx. if x ∈# A then h x else 0))"

  have count_g: "count (g h) x = (if x ∈# A then h x else 0)"
    if "h ∈ (Π⇩E x∈set_mset A. {0..count A x})" for h x
  proof -
    have "finite {x. (if x ∈# A then h x else 0) > 0}"
      by (rule finite_subset[of _ "set_mset A"]) (use that in auto)
    thus ?thesis
      using g_def by auto
  qed

  have f: "f B ∈ (Π⇩E x∈set_mset A. {0..count A x})" if "B ⊆# A" for B
      using that by (auto simp: f_def subseteq_mset_def)

  have "bij_betw f {B. B ⊆# A} (Π⇩E x∈set_mset A. {0..count A x})"
  proof (rule bij_betwI[where g = g], goal_cases)
    case 1
    thus ?case using f by auto
  next
    case 2
    show ?case
      by (auto simp: Pi_def PiE_def count_g subseteq_mset_def)
  next
    case (3 B)
    have "count (g (f B)) x = count B x" for x
    proof -
      have "count (g (f B)) x = (if x ∈# A then f B x else 0)"
        using f 3 by (simp add: count_g)
      also have "… = count B x"
        using 3 by (auto simp: f_def)
      finally show ?thesis .
    qed
    thus ?case
      by (auto simp: multiset_eq_iff)
  next
    case 4
    thus ?case
      by (auto simp: fun_eq_iff f_def count_g)
  qed
  hence "card {B. B ⊆# A} = card (Π⇩E x∈set_mset A. {0..count A x})"
    using bij_betw_same_card by blast
  thus ?thesis
    by (simp add: card_PiE set_Pow_mset)
qed

lemma empty_in_Pow_mset[iff]: ‹{#} ∈# Pow_mset B›
  by (induction B) auto

lemma full_in_Pow_mset[iff]: ‹B ∈# Pow_mset B›
  by (induction B) auto

lemma Pow_mset_nempty[iff]: ‹Pow_mset B ≠ {#}›
  using full_in_Pow_mset[of B] by force

lemma Pow_mset_single_empty[iff]: ‹Pow_mset B = {#{#}#} ⟷ B = {#}›
  using full_in_Pow_mset[of B] by fastforce

lemma Pow_mset_mono: ‹A ⊆# B ⟹ Pow_mset A ⊆# Pow_mset B›
  apply (induction A arbitrary: B)
  subgoal by auto
  subgoal premises p for x A B
    using p(1)[of ‹remove1_mset x B›] p(2)
    by (cases ‹x∈#B›)
     (auto dest!: multi_member_split
      simp add: image_mset_subseteq_mono subset_mset.add_mono)
  done


subsubsection ‹Variants around head and last›

definition option_hd :: ‹'a list ⇒ 'a option› where
  ‹option_hd xs = (if xs = [] then None else Some (hd xs))›

lemma option_hd_None_iff[iff]: ‹option_hd zs = None ⟷ zs = []›  ‹None = option_hd zs ⟷ zs = []›
  by (auto simp: option_hd_def)

lemma option_hd_Some_iff[iff]: ‹option_hd zs = Some y ⟷ (zs ≠ [] ∧ y = hd zs)›
  ‹Some y = option_hd zs ⟷ (zs ≠ [] ∧ y = hd zs)›
  by (auto simp: option_hd_def)

lemma option_hd_Some_hd[simp]: ‹zs ≠ [] ⟹ option_hd zs = Some (hd zs)›
  by (auto simp: option_hd_def)

lemma option_hd_Nil[simp]: ‹option_hd [] = None›
  by (auto simp: option_hd_def)

definition option_last where
  ‹option_last l = (if l = [] then None else Some (last l))›

lemma
  option_last_None_iff[iff]: ‹option_last l = None ⟷ l = []› ‹None = option_last l ⟷ l = []› and
  option_last_Some_iff[iff]:
    ‹option_last l = Some a ⟷ l ≠ [] ∧ a = last l›
    ‹Some a = option_last l ⟷ l ≠ [] ∧ a = last l›
  by (auto simp: option_last_def)

lemma option_last_Some[simp]: ‹l ≠ [] ⟹ option_last l = Some (last l)›
  by (auto simp: option_last_def)

lemma option_last_Nil[simp]: ‹option_last [] = None›
  by (auto simp: option_last_def)

lemma option_last_remove1_not_last:
  ‹x ≠ last xs ⟹ option_last xs = option_last (remove1 x xs)›
  by (cases xs rule: rev_cases)
    (auto simp: option_last_def remove1_Nil_iff remove1_append)

lemma option_hd_rev: ‹option_hd (rev xs) = option_last xs›
  by (cases xs rule: rev_cases) auto

lemma map_option_option_last:
  ‹map_option f (option_last xs) = option_last (map f xs)›
  by (cases xs rule: rev_cases) auto


end