Theory List_More

(* Author: Dmitry Traytel *)

theory List_More
imports Main "List-Index.List_Index" "HOL-Library.Multiset"
begin

subsection ‹Library Functions›

abbreviation "bool_product_lists n ≡ product_lists (replicate n [True, False])"

lemma in_set_bool_product_lists[simp]:
  "bs ∈ set (bool_product_lists n) ⟷ length bs = n"
proof (induct n arbitrary: bs)
  case (Suc n) thus ?case by (cases bs) auto
qed simp

text ‹More on sort and remdups›

lemma insort_min[simp]: "∀y ∈ set xs. x < y ⟹ insort x xs = x # xs"
  by (induct xs) auto

lemma insort_max[simp]: "∀y ∈ set xs. x > y ⟹ insort x xs = xs @ [x]"
  by (induct xs) auto

lemma insort_snoc[simp]: "∀z ∈ set xs. y > z ⟹
  insort x (xs @ [y]) = (if x < y then insort x xs @ [y] else xs @ [y, x])"
  by (induct xs) auto

declare set_insort_key[simp]

lemma insort_remdups[simp]: "⟦sorted xs; a ∉ set xs⟧ ⟹ insort a (remdups xs) = remdups (insort a xs)"
proof (induct xs)
  case (Cons x xs) thus ?case by (cases xs) (auto)
qed simp

lemma remdups_insort[simp]: "a ∈ set xs ⟹ remdups (insort a xs) = remdups xs"
  by (induct xs) auto

lemma sort_remdups[simp]: "sort (remdups xs) = remdups (sort xs)"
  by (induct xs) auto

lemma sort_map_insort[simp]: "sorted xs ⟹ sort (map f (insort a xs)) = insort (f a) (sort (map f xs))"
  by (induct xs) (auto simp: insort_left_comm)

lemma sort_map_sort[simp]: "sort (map f (sort xs)) = sort (map f xs)"
  by (induct xs) auto

lemma remdups_append: "remdups (xs @ ys) = remdups (filter (λx. x ∉ set ys) xs) @ remdups ys"
  by (induct xs) auto

lemma remdups_concat_map_remdups:
  "remdups (concat (map f (remdups xs))) = remdups (concat (map f xs))"
  by (induct xs) (auto simp: remdups_append filter_empty_conv)

(*remdups'*)

primrec remdups' where
  "remdups' f [] = []"
| "remdups' f (x # xs) =
    (case List.find (λy. f x = f y) xs of None ⇒ x # remdups' f xs | _ ⇒ remdups' f xs)"

lemma map_remdups'[simp]: "map f (remdups' f xs) = remdups (map f xs)"
  by (induct xs) (auto split: option.splits simp add: find_Some_iff find_None_iff)

lemma remdups'_map[simp]: "remdups' f (map g xs) = map g (remdups' (f o g) xs)"
  by (induct xs) (auto split: option.splits simp add: find_None_iff,
                auto simp: find_Some_iff elim: imageI[OF nth_mem])

lemma map_apfst_remdups':
  "map (f o fst) (remdups' snd xs) = map fst (remdups' snd (map (apfst f) xs))"
  by (auto simp: comp_def)

lemma set_remdups'[simp]: "f ` set (remdups' f xs) = f ` set xs"
  by (induct xs) (auto split: option.splits simp add: find_Some_iff)

lemma subset_remdups': "set (remdups' f xs) ⊆ set xs"
  by (induct xs) (auto split: option.splits)

lemma find_append[simp]:
  "List.find P (xs @ ys) = None = (List.find P xs = None ∧ List.find P ys = None)"
  by (induct xs) auto

lemma subset_remdups'_append: "set (remdups' f (xs @ ys)) ⊆ set (remdups' f xs) ∪ set (remdups' f ys)"
  by (induct xs arbitrary: ys) (auto split: option.splits)

lemmas mp_remdups' = subsetD[OF subset_remdups']
lemmas mp_remdups'_append = subsetD[OF subset_remdups'_append]

lemma inj_on_set_remdups'[simp]: "inj_on f (set (remdups' f xs))"
  by (induct xs) (auto split: option.splits simp add: find_None_iff dest!: mp_remdups')

lemma distinct_remdups'[simp]: "distinct (map f (remdups' f xs))"
  by (induct xs) (auto split: option.splits simp: find_None_iff)

lemma distinct_remdups'_strong: "(∀x∈set xs. ∀y∈set xs. g x = g y ⟶ f x = f y) ⟹
  distinct (map g (remdups' f xs))"
proof (induct xs)
  case (Cons x xs) thus ?case
    by (auto split: option.splits) (fastforce simp: find_None_iff dest!: mp_remdups')
qed simp

lemma set_remdups'_strong:
  "f ` set (remdups' g xs) = f ` set xs" if "∀x∈set xs. ∀y∈set xs. g x = g y ⟶ f x = f y"
using that proof (induction xs)
  case Nil
  then show ?case
    by simp
next
  case (Cons x xs)
  then have "∀x∈set xs. ∀y∈set xs. g x = g y ⟶ f x = f y"
    by (auto simp only: set_simps)
  then have "f ` set (remdups' g xs) = f ` set xs"
    by (rule Cons.IH)
  then show ?case
    by (auto simp add: find_Some_iff split: option.splits)
      (metis Cons.prems image_eqI list.set_intros(1) list.set_intros(2) nth_mem)
qed

(*multisets only needed below*)
lemma multiset_concat_gen: "M + mset (concat xs) = fold (λx M. M + mset x) xs M"
  by (induct xs arbitrary: M) (auto, metis union_assoc)

corollary multiset_concat: "mset (concat xs) = fold (λx M. M + mset x) xs {#}"
  using multiset_concat_gen[of "{#}" xs] by simp

lemma fold_mset_insort[simp]: "fold (λx M. M + mset (f x)) (insort x xs) M =
  fold (λx M. M + mset (f x)) xs (mset (f x) + M)"
  by (induct xs arbitrary: M) (auto simp: ac_simps)

lemma fold_mset_sort[simp]:
  "fold (λx M. M + mset (f x)) (sort xs) M = fold (λx M. M + mset (f x)) xs M"
  by (induct xs arbitrary: M) (auto simp: ac_simps)

lemma multiset_concat_map_sort[simp]:
  "mset (concat (map f (sort xs))) = mset (concat (map f xs))"
  by (auto simp: multiset_concat fold_map o_def)

lemma sort_concat_map_sort[simp]: "sort (concat (map f (sort xs))) = sort (concat (map f xs))"
  by (auto intro: properties_for_sort)

end