Theory More_List

(* Author: Simon Wimmer *)
theory More_List
  imports
    Main
    Instantiate_Existentials
begin

section ‹First and Last Elements of Lists›

lemma (in -) hd_butlast_last_id:
  "hd xs # tl (butlast xs) @ [last xs] = xs" if "length xs > 1"
  using that by (cases xs) auto

section ‹@{term list_all}›

lemma (in -) list_all_map:
  assumes inv: "⋀ x. P x ⟹ ∃ y. f y = x"
    and all: "list_all P as"
  shows "∃ as'. map f as' = as"
  using all
    apply (induction as)
   apply (auto dest!: inv)
  subgoal for as' a
    by (inst_existentials "a # as'") simp
  done

section ‹@{term list_all2}›

lemma list_all2_op_map_iff:
  "list_all2 (λ a b. b = f a) xs ys ⟷ map f xs = ys"
  unfolding list_all2_iff
  proof (induction xs arbitrary: ys)
    case Nil
    then show ?case by auto
  next
    case (Cons a xs ys)
    then show ?case by (cases ys) auto
  qed

lemma list_all2_last:
  "R (last xs) (last ys)" if "list_all2 R xs ys" "xs ≠ []"
  using that
  unfolding list_all2_iff
  proof (induction xs arbitrary: ys)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs ys)
    then show ?case by (cases ys) auto
  qed

lemma list_all2_set1:
  "∀x∈set xs. ∃xa∈set as. P x xa" if "list_all2 P xs as"
  using that
proof (induction xs arbitrary: as)
  case Nil
  then show ?case by auto
next
  case (Cons a xs as)
  then show ?case by (cases as) auto
qed

lemma list_all2_swap:
  "list_all2 P xs ys ⟷ list_all2 (λ x y. P y x) ys xs"
  unfolding list_all2_iff by (fastforce simp: in_set_zip)+

lemma list_all2_set2:
  "∀x∈set as. ∃xa∈set xs. P xa x" if "list_all2 P xs as"
  using that by - (rule list_all2_set1, subst (asm) list_all2_swap)

section ‹Distinct lists›

(* XXX Duplication with Floyd_Warshall.thy *)
lemma distinct_length_le:"finite s ⟹ set xs ⊆ s ⟹ distinct xs ⟹ length xs ≤ card s"
  by (metis card_mono distinct_card)

section ‹@{term filter}›

lemma filter_eq_appendD:
  "∃ xs' ys'. filter P xs' = xs ∧ filter P ys' = ys ∧ as = xs' @ ys'" if "filter P as = xs @ ys"
  using that
proof (induction xs arbitrary: as)
  case Nil
  then show ?case
    by (inst_existentials "[] :: 'a list" as) auto
next
  case (Cons a xs)
  from filter_eq_ConsD[OF Cons.prems[simplified]] obtain us vs where
    "as = us @ a # vs" "∀u∈set us. ¬ P u" "P a" "filter P vs = xs @ ys"
    by auto
  moreover from Cons.IH[OF ‹_ = xs @ ys›] obtain xs' ys where
    "filter P xs' = xs" "vs = xs' @ ys"
    by auto
  ultimately show ?case
    by (inst_existentials "us @ [a] @ xs'" ys) auto
qed

lemma list_all2_elem_filter:
  assumes "list_all2 P xs us" "x ∈ set xs"
  shows "length (filter (P x) us) ≥ 1"
  using assms by (induction xs arbitrary: us) (auto simp: list_all2_Cons1)

lemma list_all2_replicate_elem_filter:
  assumes "list_all2 P (concat (replicate n xs)) ys" "x ∈ set xs"
  shows "length (filter (P x) ys) ≥ n"
  using assms
  by (induction n arbitrary: ys; fastforce dest: list_all2_elem_filter simp: list_all2_append1)

section ‹Sublists›

lemma nths_split:
  "nths xs (A ∪ B) = nths xs A @ nths xs B" if "∀ i ∈ A. ∀ j ∈ B. i < j"
  using that
  proof (induction xs arbitrary: A B)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs)
    let ?A = "{j. Suc j ∈ A}" and ?B = "{j. Suc j ∈ B}"
    from Cons.prems have *: "∀i∈?A. ∀a∈?B. i < a"
      by auto
    have [simp]: "{j. Suc j ∈ A ∨ Suc j ∈ B} = ?A ∪ ?B"
      by auto
    show ?case
      unfolding nths_Cons
    proof (clarsimp, safe, goal_cases)
      case 2
      with Cons.prems have "A = {}"
        by auto
      with Cons.IH[OF *] show ?case by auto
    qed (use Cons.prems Cons.IH[OF *] in auto)
  qed

lemma nths_nth:
  "nths xs {i} = [xs ! i]" if "i < length xs"
  using that
  proof (induction xs arbitrary: i)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs)
    then show ?case
      by (cases i) (auto simp: nths_Cons)
  qed

lemma nths_shift:
  "nths (xs @ ys) S = nths ys {x - length xs | x. x ∈ S}" if
  "∀ i ∈ S. length xs ≤ i"
  using that
proof (induction xs arbitrary: S)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  have [simp]: "{x - length xs |x. Suc x ∈ S} = {x - Suc (length xs) |x. x ∈ S}" if "0 ∉ S"
    using that apply safe
     apply force
    subgoal for x x'
      by (cases x') auto
    done
  from Cons.prems show ?case
    by (simp, subst nths_Cons, subst Cons.IH; auto)
qed

lemma nths_eq_ConsD:
  assumes "nths xs I = x # as"
  shows
    "∃ ys zs.
      xs = ys @ x # zs ∧ length ys ∈ I ∧ (∀ i ∈ I. i ≥ length ys)
      ∧ nths zs ({i - length ys - 1 | i. i ∈ I ∧ i > length ys}) = as"
  using assms
proof (induction xs arbitrary: I x as)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  from Cons.prems show ?case
    unfolding nths_Cons
    apply (auto split: if_split_asm)
    subgoal
      by (inst_existentials "[] :: 'a list" xs; force intro: arg_cong2[of xs xs _ _ nths])
    subgoal
      apply (drule Cons.IH)
      apply safe
      subgoal for ys zs
        apply (inst_existentials "a # ys" zs)
           apply simp+
         apply standard
        subgoal for i
          by (cases i; auto)
        apply (rule arg_cong2[of zs zs _ _ nths])
         apply simp
        apply safe
        subgoal for _ i
          by (cases i; auto)
        by force
      done
    done
qed

lemma nths_out_of_bounds:
  "nths xs I = []" if "∀i ∈ I. i ≥ length xs"
  (* Found by sledgehammer, then modified *)
proof -
  have
    "∀N as.
      (∃n. n ∈ N ∧ ¬ length (as::'a list) ≤ n)
      ∨ (∀asa. nths (as @ asa) N = nths asa {n - length as |n. n ∈ N})"
    using nths_shift by blast
  then have
    "⋀as. nths as {n - length xs |n. n ∈ I} = nths (xs @ as) I
      ∨ nths (xs @ []) I = []"
    using that by fastforce
  then have "nths (xs @ []) I = []"
    by (metis (no_types) nths_nil)
  then show ?thesis
    by simp
qed

lemma nths_eq_appendD:
  assumes "nths xs I = as @ bs"
  shows
    "∃ ys zs.
        xs = ys @ zs ∧ nths ys I = as
        ∧ nths zs {i - length ys | i. i ∈ I ∧ i ≥ length ys} = bs"
  using assms
proof (induction as arbitrary: xs I)
  case Nil
  then show ?case
    by (inst_existentials "[] :: 'a list" "nths bs") auto
next
  case (Cons a ys xs)
  from nths_eq_ConsD[of xs I a "ys @ bs"] Cons.prems
  obtain ys' zs' where
      "xs = ys' @ a # zs'"
      "length ys' ∈ I"
      "∀i ∈ I. i ≥ length ys'"
      "nths zs' {i - length ys' - 1 |i. i ∈ I ∧ i > length ys'} = ys @ bs"
    by auto
  moreover from Cons.IH[OF ‹nths zs' _ = _›] obtain ys'' zs'' where
    "zs' = ys'' @ zs''"
    "ys = nths ys'' {i - length ys' - 1 |i. i ∈ I ∧ length ys' < i}"
    "bs = nths zs'' {i - length ys'' |i. i ∈ {i - length ys' - 1 |i. i ∈ I ∧ length ys' < i} ∧ length ys'' ≤ i}"
    by auto
  ultimately show ?case
    apply (inst_existentials "ys' @ a # ys''" zs'')
      apply (simp; fail)
    subgoal
      by (simp add: nths_out_of_bounds nths_append nths_Cons)
        (rule arg_cong2[of ys'' ys'' _ _ nths]; force)
    subgoal
      by safe (rule arg_cong2[of zs'' zs'' _ _ nths]; force) (* Slow *)
    done
qed

lemma filter_nths_length:
  "length (filter P (nths xs I)) ≤ length (filter P xs)"
proof (induction xs arbitrary: I)
  case Nil
  then show ?case
    by simp
next
  case Cons
  then show ?case
  (* Found by sledgehammer *)
  proof -
    fix a :: 'a and xsa :: "'a list" and Ia :: "nat set"
    assume a1: "⋀I. length (filter P (nths xsa I)) ≤ length (filter P xsa)"
    have f2:
      "∀b bs N. if 0 ∈ N then nths ((b::'a) # bs) N =
        [b] @ nths bs {n. Suc n ∈ N} else nths (b # bs) N = [] @ nths bs {n. Suc n ∈ N}"
      by (simp add: nths_Cons)
    have f3:
      "nths (a # xsa) Ia = [] @ nths xsa {n. Suc n ∈ Ia}
        ⟶ length (filter P (nths (a # xsa) Ia)) ≤ length (filter P xsa)"
      using a1 by (metis append_Nil)
    have f4: "length (filter P (nths xsa {n. Suc n ∈ Ia})) + 0 ≤ length (filter P xsa) + 0"
      using a1 by simp
    have f5:
      "Suc (length (filter P (nths xsa {n. Suc n ∈ Ia})) + 0)
      = length (a # filter P (nths xsa {n. Suc n ∈ Ia}))"
      by force
    have f6: "Suc (length (filter P xsa) + 0) = length (a # filter P xsa)"
      by simp
    { assume "¬ length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
      { assume "nths (a # xsa) Ia ≠ [a] @ nths xsa {n. Suc n ∈ Ia}"
        moreover
        { assume
            "nths (a # xsa) Ia = [] @ nths xsa {n. Suc n ∈ Ia}
            ∧ length (filter P (a # xsa)) ≤ length (filter P xsa)"
          then have "length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
            using a1 by (metis (no_types) append_Nil filter.simps(2) impossible_Cons) }
        ultimately have "length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
          using f3 f2 by (meson dual_order.trans le_cases) }
      then have "length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
        using f6 f5 f4 a1 by (metis Suc_le_mono append_Cons append_Nil filter.simps(2)) }
    then show "length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
      by meson
  qed
qed

end (* Theory *)