Theory List_Util

theory List_Util
  imports Main
begin

section ‹General Lists›

lemma list_cases_3:
  "T = [] ∨ (∃x. T = [x]) ∨ (∃a b xs. T = a # b # xs)"
proof (cases T)
  case Nil
  then show ?thesis by simp
next
  case (Cons a list)
  then show ?thesis
  proof (cases list)
    case Nil
    with ‹T = a # list›
    show ?thesis
      by simp
  next
    case (Cons a' list')
    with ‹T = a # list›
    show ?thesis
      by simp
  qed
qed

lemma length_cons_cons:
  "T = a # b # xs ⟹ ∃n. length T = Suc (Suc n)"
  by simp

lemma length_Suc_Suc:
  "length T = Suc (Suc n) ⟹ ∃a b xs. T = a # b # xs"
  by (metis length_Suc_conv)

lemma length_Suc_0:
  "length xs = Suc 0 ⟹ ∃x. xs = [x]"
  by (simp add: length_Suc_conv)

lemma map_eq_replicate:
  "∀x ∈ set xs. f x = k ⟹ map f xs = replicate (length xs) k"
  by (metis map_eq_conv map_replicate_const)

lemma map_upt_eq_replicate:
  "∀x ∈ set [i..<j]. f x = k ⟹ map f [i..<j] = replicate (j - i) k"
  by (metis length_upt map_eq_replicate)

lemma in_set_list_update:
  "⟦x ∈ set xs; xs ! k ≠ x⟧ ⟹ x ∈ set (xs[k := y])"
  by (metis in_set_conv_nth length_list_update nth_list_update_neq)

lemma Max_greD:
  "i < length s ⟹ Max (set s) ≥ s ! i"
  by clarsimp


lemma list_neq_rc1:
  "(∃z zs. xs = ys @ z # zs) ⟹ xs ≠ ys"
  by fastforce

lemma list_neq_rc2:
  "(∃z zs. ys = xs @ z # zs) ⟹ xs ≠ ys"
  by fastforce

lemma list_neq_rc3:
  "(∃x y as bs cs. xs = as @ x # bs ∧ ys = as @ y # cs ∧ x ≠ y) ⟹ xs ≠ ys"
  by fastforce

lemma list_neq_rc:
  "(∃z zs. xs = ys @ z # zs) ∨
   (∃z zs. ys = xs @ z # zs) ∨
   (∃x y as bs cs. xs = as @ x # bs ∧ ys = as @ y # cs ∧ x ≠ y) ⟹
    xs ≠ ys"
  by (elim disjE conjE list_neq_rc1 list_neq_rc2 list_neq_rc3)

lemma list_neq_fc:
  "xs ≠ ys ⟹
   (∃z zs. xs = ys @ z # zs) ∨
   (∃z zs. ys = xs @ z # zs) ∨
   (∃x y as bs cs. xs = as @ x # bs ∧ ys = as @ y # cs ∧ x ≠ y)"
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case
    by (metis append_Nil list.exhaust)
next
  case (Cons a xs ys)
  note IH = this
  then show ?case
  proof (cases ys)
    case Nil
    then show ?thesis
      by simp
  next
    case (Cons b ys')
    assume "ys = b # ys'"
    show ?thesis
    proof (cases "a = b")
      assume "a ≠ b"
      with ‹ys = b # ys'› 
      show ?thesis
        by blast
    next
      assume "a = b"
      with IH(2) ‹ys = b # ys'›
      have "xs ≠ ys'"
        by simp
      with IH(1)[of ys']
      show ?thesis
        by (metis Cons_eq_appendI ‹a = b› local.Cons)
    qed
  qed
qed

lemma list_neq_cases:
  "xs ≠ ys ⟷
   (∃z zs. xs = ys @ z # zs) ∨
   (∃z zs. ys = xs @ z # zs) ∨
   (∃x y as bs cs. xs = as @ x # bs ∧ ys = as @ y # cs ∧ x ≠ y)"
  using list_neq_fc list_neq_rc by blast

section ‹Find›

lemma findSomeD:
  "find P xs = Some x ⟹ P x ∧ x ∈ set xs"
  by (induct xs) (auto split: if_split_asm)

lemma findNoneD:
  "find P xs = None ⟹ ∀x ∈ set xs. ¬P x"
  by (induct xs) (auto split: if_split_asm)

section ‹Filter›

lemma filter_update_nth_success:
  "⟦P v; i < length xs⟧ ⟹
    filter P (xs[i := v]) = (filter P (take i xs)) @ [v] @ (filter P (drop (Suc i) xs))"
  by (simp add: upd_conv_take_nth_drop)

lemma filter_update_nth_fail:
  "⟦¬P v; i < length xs⟧ ⟹
    filter P (xs[i := v]) = (filter P (take i xs)) @ (filter P (drop (Suc i) xs))"
  by (simp add: upd_conv_take_nth_drop)

lemma filter_take_nth_drop_success:
  "⟦i < length xs; P (xs ! i)⟧ ⟹
    filter P xs = (filter P (take i xs)) @ [xs ! i] @ (filter P (drop (Suc i) xs))"
  by (metis filter_update_nth_success list_update_id)

lemma filter_take_nth_drop_fail:
  "⟦i < length xs; ¬P (xs ! i)⟧ ⟹
    filter P xs = (filter P (take i xs)) @ (filter P (drop (Suc i) xs))"
  by (metis filter_update_nth_fail list_update_id)

lemma filter_nth_1:
  "⟦i < length xs; P (xs ! i)⟧ ⟹
   ∃i'. i' < length (filter P xs) ∧ (filter P xs) ! i' = xs ! i"
proof (induct xs arbitrary: i)
  case Nil
  then show ?case
    by simp
next
  case (Cons a xs i)
  note IH = this
  show ?case
  proof (cases i)
    case 0
    with IH(3)
    show ?thesis
      by fastforce
  next
    case (Suc n)
    with IH(1)[of n] IH(2,3)
    have "∃i'<length (filter P xs). filter P xs ! i' = xs ! n"
      by fastforce
    then show ?thesis
      using Suc by auto
  qed  
qed

lemma filter_nth_2:
  "⟦i < length (filter P xs)⟧ ⟹
   ∃i'. i' < length xs ∧ (filter P xs) ! i = xs ! i'"
proof (induct xs arbitrary: i)
  case Nil
  then show ?case
    by simp
next
  case (Cons a xs i)
  note IH = this
  then show ?case
  proof (cases i)
    case 0
    then show ?thesis
      using Cons.hyps Cons.prems by force
  next
    case (Suc n)
    with IH(1)[of n] IH(2)
    have "∃i'<length xs. filter P xs ! n = xs ! i'"
      by (metis filter.simps(2) length_Cons not_less_eq not_less_iff_gr_or_eq)
    then show ?thesis
      by (metis Cons.hyps Cons.prems Suc filter.simps(2) length_Cons not_less_eq nth_Cons_Suc)
  qed
qed

lemma filter_nth_relative_1:
  "⟦i < length xs; P (xs ! i); j < i; P (xs ! j)⟧ ⟹
   ∃i' j'. i' < length (filter P xs) ∧ j' < i' ∧ (filter P xs) ! i' = xs ! i ∧
    (filter P xs) ! j' = xs ! j"
proof (induct xs arbitrary: i j)
  case Nil
  then show ?case
    by simp
next
  case (Cons a xs i j)
  note IH = this
  show ?case
  proof (cases i)
    case 0
    then show ?thesis
      using IH(4) by blast
  next
    case (Suc n)
    assume "i = Suc n"
    show ?thesis
    proof (cases j)
      case 0
      with filter_nth_1[of n xs P] IH(2,3) ‹i = Suc n› IH(4-)
      show ?thesis
        by (metis filter.simps(2) length_Cons not_less_eq nth_Cons_0 nth_Cons_Suc zero_less_Suc)
    next
      case (Suc m)
      with IH(1)[of n m] IH(2-) ‹i = Suc n›
      show ?thesis 
        by fastforce
    qed
  qed
qed

lemma filter_nth_relative_neq_1:
  assumes "i < length xs" "P (xs ! i)" "j < length xs" "P (xs ! j)" "i ≠ j"
  shows "∃i' j'. i' < length (filter P xs) ∧ j' < length (filter P xs) ∧ (filter P xs) ! i' = xs ! i ∧
                 (filter P xs) ! j' = xs ! j ∧ i' ≠ j'"
proof (cases "i < j")
  assume "i < j"
  with filter_nth_relative_1[where P = P, OF assms(3,4) _ assms(2)]
  show ?thesis
    by (metis (no_types, lifting) nat_neq_iff order_less_trans)
next
  assume "¬ i < j"
  with assms(5)
  have "j < i"
    by auto
  with filter_nth_relative_1[where P = P, OF assms(1,2) _ assms(4)]
  show ?thesis
    using order_less_trans by blast
qed

lemma filter_nth_relative_2:
  "⟦i < length (filter P xs); j < i⟧ ⟹
   ∃i' j'. i' < length xs ∧ j' < i' ∧ (filter P xs) ! i = xs ! i' ∧ (filter P xs) ! j = xs ! j'"
proof (induct xs arbitrary: i j)
  case Nil
  then show ?case
    by simp
next
  case (Cons a xs i j)
  note IH = this

  let ?goal = "∃i' j'. i' < length (a # xs) ∧ j' < i' ∧ filter P (a # xs) ! i = (a # xs) ! i' ∧
                       filter P (a # xs) ! j = (a # xs) ! j'"
  show ?case
  proof (cases i)
    case 0
    then show ?goal
      using IH(3) by blast
  next
    case (Suc n)
    assume "i = Suc n"
    show ?thesis
    proof (cases j)
      case 0
      assume "j = 0"
      from filter_nth_2[of n P xs] IH(2)
      have "∃i'<length xs. filter P xs ! n = xs ! i'"
        using Suc order_less_trans by fastforce

      show ?goal
      proof (cases "P a")
        assume "P a"
        then show ?goal
          by (metis "0" Suc ‹∃i'<length xs. filter P xs ! n = xs ! i'› filter.simps(2)
                    length_Cons not_less_eq nth_Cons_0 nth_Cons_Suc zero_less_Suc)
      next
        assume "¬ P a"
        then show ?goal
          using Cons.hyps IH(2,3) Suc_less_eq by fastforce
        qed
    next
      case (Suc m)
      with IH(1)[of n m] IH(2-) ‹i = Suc n›
      have "∃i' j'. i' < length xs ∧ j' < i' ∧ filter P xs ! n = xs ! i' ∧
                    filter P xs ! m = xs ! j'"
        by (metis filter.simps(2) length_Cons not_less_eq not_less_iff_gr_or_eq)
      then obtain i' j' where
        A: "i' < length xs" "j' < i'" "filter P xs ! n = xs ! i'" "filter P xs ! m = xs ! j'"
        by blast
      show ?goal
      proof (cases "P a")
        assume "P a"
        then show ?goal
          using A Suc ‹i = Suc n› by force
      next
        assume "¬ P a"
        then show ?goal
          using Cons.hyps IH(2,3) by fastforce
      qed
    qed
  qed
qed

lemma filter_nth_relative_neq_2:
  assumes "i < length (filter P xs)" "j < length (filter P xs)" "i ≠ j"
  shows "∃i' j'. i' < length xs ∧ j' < length xs ∧ xs ! i' = (filter P xs) ! i ∧
                 xs ! j' = (filter P xs) ! j ∧ i' ≠ j'"
proof (cases "i < j")
  assume "i < j"
  with filter_nth_relative_2[OF assms(2), of i]
  show ?thesis
    by (metis dual_order.strict_trans exists_least_iff)
next
  assume "¬ i < j"
  with assms(3)
  have "j < i"
    by auto
  with filter_nth_relative_2[OF assms(1), of j]
  show ?thesis
    by (metis nat_neq_iff order_less_trans)
qed

lemma filter_find:
  "filter P xs ≠ [] ⟹ find P xs = Some ((filter P xs) ! 0)"
  by (induct xs; auto)

lemma filter_nth_update_subset:
  "set (filter P (xs[i := v])) ⊆ {v} ∪ set (filter P xs)"
proof
  fix x
  assume "x ∈ set (filter P (xs[i := v]))"
  with filter_set member_filter
  have "x ∈ set (xs[i := v])" "P x"
    by auto
  hence "∃k < length (xs[i := v]). (xs[i := v]) ! k = x"
    by (simp add: in_set_conv_nth)
  then obtain k where
    "k < length (xs[i := v])"
    "(xs[i := v]) ! k = x"
    by blast
  hence "k < length xs"
    by simp

  from ‹(xs[i := v]) ! k = x› ‹k < length (xs[i := v])›
  have "k = i ⟹ x = v"
    by simp
  moreover
  have "k ≠ i ⟹ x ∈ set (filter P xs)"
    using ‹P x› ‹k < length xs› ‹xs[i := v] ! k = x› by auto
  ultimately
  show "x ∈ {v} ∪ set (filter P xs)"
    by blast
qed

section ‹Upt›

lemma card_upt:
  "card {0..<n} = n"
  by simp

lemma bounded_distinct_subset_upt_length:
  "⟦distinct xs; ∀i<length xs. xs ! i < length xs⟧ ⟹ set xs ⊆ {0..<length xs}"
  by (intro subsetI; clarsimp simp: in_set_conv_nth)

lemma bounded_distinct_eq_upt_length:
  assumes "distinct xs" 
  assumes "∀i < length xs. xs ! i < length xs"
  shows "set xs = {0..<length xs}"
proof (intro card_subset_eq finite_atLeastLessThan
              bounded_distinct_subset_upt_length[OF assms] )
  from distinct_card[OF assms(1)] card_upt[of "length xs"]
  show "card (set xs) = card {0..<length xs}"
    by simp
qed

lemma set_map_nth_subset:
  assumes "n ≤ length xs"
  shows "set (map (nth xs) [0..<n]) ⊆ set xs"
  using assms by clarsimp

lemma set_map_nth_eq:
  "set (map (nth xs) [0..<length xs]) = set xs"
  by (intro equalityI set_map_nth_subset subsetI; simp add: map_nth)

lemma distinct_map_nth:
  assumes "distinct xs"
  assumes "n ≤ length xs"
  shows "distinct (map (nth xs) [0..<n])"
  using assms by (simp add: distinct_conv_nth)
end